共查询到20条相似文献,搜索用时 15 毫秒
1.
The goal of this two-part series of papers is to show that constructive logic with strong negation N is definitionally equivalent to a certain axiomatic extension NFL
ew
of the substructural logic FL
ew
. In this paper, it is shown that the equivalent variety semantics of N (namely, the variety of Nelson algebras) and the equivalent variety semantics of NFL
ew
(namely, a certain variety of FL
ew
-algebras) are term equivalent. This answers a longstanding question of Nelson [30]. Extensive use is made of the automated
theorem-prover Prover9 in order to establish the result.
The main result of this paper is exploited in Part II of this series [40] to show that the deductive systems N and NFL
ew
are definitionally equivalent, and hence that constructive logic with strong negation is a substructural logic over FL
ew
.
Presented by Heinrich Wansing 相似文献
2.
The idea of interpretability logics arose in Visser [Vis90]. He introduced the logics as extensions of the provability logic GLwith a binary modality . The arithmetic realization of A B in a theory T will be that T plus the realization of B is interpretable in T plus the realization of A (T + A interprets T + B). More precisely, there exists a function f (the relative interpretation) on the formulas of the language of T such that T + B C implies T + A f(C).The interpretability logics were considered in several papers. An arithmetic completeness of the interpretability logic ILM, obtained by adding Montagna's axiom to the smallest interpretability logic IL, was proved in Berarducci [Ber90] and Shavrukov [Sha88] (see also Hájek and Montagna [HM90] and Hájek and Montagna [HM92]). [Vis90] proved that the interpretability logic ILP, an extension of IL, is also complete for another arithmetic interpretation. The completeness with respect to Kripke semantics due to Veltman was, for IL, ILMand ILP, proved in de Jongh and Veltman [JV90]. The fixed point theorem of GLcan be extended to ILand hence ILMand ILP(cf. de Jongh and Visser [JV91]). The unary pendant "T interprets T + A" is much less expressive and was studied in de Rijke [Rij92]. For an overview of interpretability logic, see Visser [Vis97], and Japaridze and de Jongh [JJ98].In this paper, we give a cut-free sequent system for IL. To begin with, we give a cut-free system for the sublogic IL4of IL, whose -free fragment is the modal logic K4. A cut-elimination theorem for ILis proved using the system for IK4and a property of Löb's axiom. 相似文献
3.
《The Journal of social psychology》2012,152(1):141-143
Abstract [Hunt, J. McV. (Ed.). Personality and the Behavior Disorders. New York: Ronald Press, 1944. Pp. 1242 (2 vols.)]. Reviewed by C. H. Patterson 相似文献
4.
Let S denote the variety of Sugihara algebras. We prove that the lattice (K) of subquasivarieties of a given quasivariety K
S is finite if and only if K is generated by a finite set of finite algebras. This settles a conjecture by Tokarz [6]. We also show that the lattice (S) is not modular. 相似文献
5.
Wojciech Buszkowski 《Studia Logica》1996,57(2-3):303-323
We prove the finite model property (fmp) for BCI and BCI with additive conjunction, which answers some open questions in Meyer and Ono [11]. We also obtain similar results for some restricted versions of these systems in the style of the Lambek calculus [10, 3]. The key tool is the method of barriers which was earlier introduced by the author to prove fmp for the product-free Lambek calculus [2] and the commutative product-free Lambek calculus [4].Presented by H. Ono 相似文献
6.
To the standard propositional modal system of provability logic constants are added to account for the arithmetical fixed points introduced by Bernardi-Montagna in [5]. With that interpretation in mind, a system LR of modal propositional logic is axiomatized, a modal completeness theorem is established for LR and, after that, a uniform arithmetical (Solovay-type) completeness theorem with respect to PA is obtained for LR.
This paper supersedes: Franco Montagna, Extremely undecidable sentences and generic generalized Rosser's fixed points, Rapporto Matematico, No. 95, Siena, 1983. 相似文献
7.
C. J. van Alten 《Studia Logica》2006,83(1-3):425-445
A biresiduation algebra is a 〈/,\,1〉-subreduct of an integral residuated lattice. These algebras arise as algebraic models of the implicational fragment
of the Full Lambek Calculus with weakening. We axiomatize the quasi-variety B of biresiduation algebras using a construction for integral residuated lattices. We define a filter of a biresiduation algebra
and show that the lattice of filters is isomorphic to the lattice of B-congruences and that these lattices are distributive. We give a finite basis of terms for generating filters and use this
to characterize the subvarieties of B with EDPC and also the discriminator varieties. A variety generated by a finite biresiduation algebra is shown to be a subvariety
of B. The lattice of subvarieties of B is investigated; we show that there are precisely three finitely generated covers of the atom.
Mathematics Subject Classification (2000): 03G25, 06F35, 06B10, 06B20
Dedicated to the memory of Willem Johannes Blok 相似文献
8.
Hirokazu Nishimura 《Studia Logica》1981,40(2):89-98
The aims of this paper are: (1) to present tense-logical versions of such classical notions as saturated and special models; (2) to establish several fundamental existence theorems about these notions; (3) to apply these powerful techniques to tense complexity.In this paper we are concerned exclusively with quantifiedK
1 (for linear time) with constant domain. Our present research owes much to Bowen [2], Fine [5] and Gabbay [6]. 相似文献
9.
We show that the modal μ-calculus over GL collapses to the modal fragment by showing that the fixpoint formula is reached after two iterations and answer to a question
posed by van Benthem in [4]. Further, we introduce the modal μ
~-calculus by allowing fixpoint constructors for any formula where the fixpoint variable appears guarded but not necessarily
positive and show that this calculus over GL collapses to the modal fragment, too. The latter result allows us a new proof of the de Jongh, Sambin Theorem and provides
a simple algorithm to construct the fixpoint formula.
Presented by Melvin Fitting 相似文献
10.
The aim of this paper is to define a λ-calculus typed in aMixed (commutative and non-commutative) Intuitionistic Linear Logic.
The terms of such a calculus are the labelling of proofs of a linear intuitionistic mixed natural deduction NILL, which is based on the non-commutative linear multiplicative sequent calculus MNL [RuetAbrusci 99]. This linear λ-calculus involves three linear arrows: two directional arrows and a nondirectional one (the
usual linear arrow). Moreover, the -terms are provided with seriesparallel orders on free variables.
We prove a normalization theorem which explicitly gives the behaviour of the order during the normalization procedure.
Special Issue Categorial Grammars and Pregroups Edited by Wojciech Buszkowski and Anne Preller 相似文献
11.
Plain Semi-Post algebras as a poset-based generalization of post algebras and their representability
Semi-Post algebras of any type T being a poset have been introduced and investigated in [CR87a], [CR87b]. Plain Semi-Post algebras are in this paper singled out among semi-Post algebras because of their simplicity, greatest similarity with Post algebras as well as their importance in logics for approximation reasoning ([Ra87a], [Ra87b], [RaEp87]). They are pseudo-Boolean algebras generated in a sense by corresponding Boolean algebras and a poset T. Every element has a unique descending representation by means of elements in a corresponding Boolean algebra and primitive Post constants which form a poset T. An axiomatization and another characterization, subalgebras, homomorphisms, congruences determined by special filters and a representability theory of these algebras, connected with that for Boolean algebras, are the subject of this paper.To the memory of Jerzy SupeckiResearch reported here has been supported by Polish Government Grant CPBP 01.01 相似文献
12.
We generalize the incompleteness proof of the modal predicate logic Q-S4+ p p + BF described in Hughes-Cresswell [6]. As a corollary, we show that, for every subframe logic Lcontaining S4, Kripke completeness of Q-L+ BF implies the finite embedding property of L. 相似文献
13.
The least element 0 of a finite meet semi-distributive lattice is a meet of meet-prime elements. We investigate conditions
under which the least element of an algebraic, meet semi-distributive lattice is a (complete) meet of meet-prime elements.
For example, this is true if the lattice has only countably many compact elements, or if |L| < 2ℵ0, or if L is in the variety generated by a finite meet semi-distributive lattice. We give an example of an algebraic, meet semi-distributive
lattice that has no meet-prime element or join-prime element. This lattice L has |L| = |LC| = 2ℵ0 where Lc is the set of compact elements of L.
Dedicated to the memory of Willem Johannes Blok
AMS subject classification: 06B05
While working on this paper, the first author was supported by the INTAS grant no. 03-51-4110, the second author was partially
supported by the Hungarian National Foundation for Scientific Research (OTKA) grant no. T37877, and the third author was supported
by the US National Science Foundation grant no. DMS0245622. 相似文献
14.
George Weaver 《逻辑史和逻辑哲学》2017,38(1):48-56
König, D. [1926. ‘Sur les correspondances multivoques des ensembles’, Fundamenta Mathematica, 8, 114–34] includes a result subsequently called König's Infinity Lemma. Konig, D. [1927. ‘Über eine Schlussweise aus dem Endlichen ins Unendliche’, Acta Litterarum ac Scientiarum, Szeged, 3, 121–30] includes a graph theoretic formulation: an infinite, locally finite and connected (undirected) graph includes an infinite path. Contemporary applications of the infinity lemma in logic frequently refer to a consequence of the infinity lemma: an infinite, locally finite (undirected) tree with a root has a infinite branch. This tree lemma can be traced to [Beth, E. W. 1955. ‘Semantic entailment and formal derivability’, Mededelingen der Kon. Ned. Akad. v. Wet., new series 18, 13, 309–42]. It is argued that Beth independently discovered the tree lemma in the early 1950s and that it was later recognized among logicians that Beth's result was a consequence of the infinity lemma. The equivalence of these lemmas is an easy consequence of a well known result in graph theory: every connected, locally finite graph has among its partial subgraphs a spanning tree. 相似文献
15.
A Proof of Standard Completeness for Esteva and Godo's Logic MTL 总被引:7,自引:0,他引:7
In the present paper we show that any at most countable linearly-ordered commutative residuated lattice can be embedded into a commutative residuated lattice on the real unit interval [0, 1]. We use this result to show that Esteva and Godo's logic MTL is complete with respect to interpretations into commutative residuated lattices on [0, 1]. This solves an open problem raised in. 相似文献
16.
This article introduces the three-valuedweakly-intuitionistic logicI
1 as a counterpart of theparaconsistent calculusP
1 studied in [11].I
1 is shown to be complete with respect to certainthree-valued matrices. We also show that in the sense that any proper extension ofI
1 collapses to classical logic.The second part shows thatI
1 is algebraizable in the sense of Block and Pigozzi (cf. [2]) in a way very similar to the algebraization ofP
1 given in [8].In the last part of the paper we suggest the definition of certain hierarchies of finite-valued propositional paraconsistent and weakly-intuitionistic calculi, and comment on their intrinsic interest. 相似文献
17.
We present some equivalent conditions for a quasivariety of structures to be generated by a single structure. The first such condition, called the embedding property was found by A.I. Mal′tsev in [6]. It says that if are nontrivial, then there exists such that A and B are embeddable into C. One of our equivalent conditions states that the set of quasi-identities valid in is closed under a certain Gentzen type rule which is due to J. Łoś and R. Suszko [5].
Presented by Jacek Malinowski 相似文献
18.
Andreja Prijatelj 《Studia Logica》1996,57(2-3):437-456
In this paper, we consider multiplicative-additive fragments of affine propositional classical linear logic extended with n-contraction. To be specific, n-contraction (n 2) is a version of the contraction rule where (n+ 1) occurrences of a formula may be contracted to n occurrences. We show that expansions of the linear models for (n + 1)- valued ukasiewicz logic are models for the multiplicative-additive classical linear logic, its affine version and their extensions with n-contraction. We prove the finite axiomatizability for the classes of finite models, as well as for the class of infinite linear models based on the set of rational numbers in the interval [0, 1]. The axiomatizations obtained in a Gentzen-style formulation are equivalent to finite and infinite-valued ukasiewicz logics.Presented by Jan Zygmunt 相似文献
19.
Burghard Herrmann 《Studia Logica》1996,57(2-3):419-436
The notion of an algebraizable logic in the sense of Blok and Pigozzi [3] is generalized to that of a possibly infinitely algebraizable, for short, p.i.-algebraizable logic by admitting infinite sets of equivalence formulas and defining equations. An example of the new class is given. Many ideas of this paper have been present in [3] and [4]. By a consequent matrix semantics approach the theory of algebraizable and p.i.-algebraizable logics is developed in a different way. It is related to the theory of equivalential logics in the sense of Prucnal and Wroski [18], and it is extended to nonfinitary logics. The main result states that a logic is algebraizable (p.i.-algebraizable) iff it is finitely equivalential (equivalential) and the truth predicate in the reduced matrix models is equationally definable.Most of the results of the present and a forthcoming paper originally appeared in [13].Presented by Wolfgang Rautenberg 相似文献
20.
Helena Rasiowa 《Studia Logica》1994,53(1):137-160
A first order uncountably valued logicL
Q(0,1) for management of uncertainty is considered. It is obtained from approximation logicsL
T
of any poset type (T, ) (see Rasiowa [17], [18], [19]) by assuming (T, )=(Q(0, 1), ) — whereQ(0, 1) is the set of all rational numbersq such that 0<q<1 and is the arithmetic ordering — by eliminating modal connectives and adopting a semantics based onLT-fuzzy sets (see Rasiowa and Cat Ho [20], [21]). LogicL
Q(0,1) can be treated as an important case ofLT-fuzzy logics (introduced in Rasiowa and Cat Ho [21]) for (T, )=(Q(0, 1), ), i.e. asLQ(0, 1)-fuzzy logic announced in [21] but first examined in this paper.L
Q(0,1) deals with vague concepts represented by predicate formulas and applies approximate truth-values being certain subsets ofQ(0, 1). The set of all approximate truth-values consists of the empty set ø and all non-empty subsetss ofQ(0, 1) such that ifqs andqq, thenqs. The setLQ(0, 1) of all approximate truth-values is uncountable and covers up to monomorphism the closed interval [0, 1] of the real line.LQ(0, 1) is a complete set lattice and therefore a pseudo-Boolean (Heyting) algebra. Equipped with some additional operations it is a basic plain semi-Post algebra of typeQ(0, 1) (see Rasiowa and Cat Ho [20]) and is taken as a truth-table forL
Q(0,1) logic.L
Q(0,1) can be considered as a modification of Zadeh's fuzzy logic (see Bellman and Zadeh [2] and Zadeh and Kacprzyk, eds. [29]). The aim of this paper is an axiomatization of logicL
Q(0,1) and proofs of the completeness theorem and of the theorem on the existence ofLQ(0, 1)-models (i.e. models under the semantics introduced) for consistent theories based on any denumerable set of specific axioms. Proofs apply the theory of plain semi-Post algebras investigated in Cat Ho and Rasiowa [4].Presented byCecylia Rauszer 相似文献