An Adaptive Logic Based on Jaśkowskiˈs Approach to Paraconsistency

In this paper, I present the modal adaptive logic AJ ^r (based on S5) as well as the discussive logic D ^r ₂ that is defined from it. D ^r ₂ is a (non-monotonic) alternative for Jaśkowski’s paraconsistent system D ₂ . Like D ₂ , D ^r ₂ validates all single-premise rules of Classical Logic. However, for formulas that behave consistently, D ^r ₂ moreover validates all multiple-premise rules of Classical Logic. Importantly, and unlike in the case of D ₂ , this does not require the introduction of discussive connectives. It is argued that this has clear advantages with respect to one of the main application contexts of discussive logics, namely the interpretation of discussions.*Research for this paper was indirectly supported by the Flemish Minister responsible for Science and Technology (contract BIL1/8). The author is indebted to Leon Horsten, Jo?o Marcos, Jerzy Perzanowski, Liza Verhoeven, and especially to the referee and to Diderik Batens for comments and suggestions.     

Proof theory and mathematical meaning of paraconsistent C-systems

A proof-theoretic analysis and new arithmetical semantics are proposed for some paraconsistent C-systems, which are a relevant sub-class of Logics of Formal Inconsistency (LFIs) introduced by W.A. Carnielli et al. (2002, 2005) [8] and [9]. The sequent versions BC, CI, CIL of the systems bC, Ci, Cil presented in Carnielli et al. (2002, 2005) [8] and [9] are introduced and examined. BC, CI, CIL admit the cut-elimination property and, in general, a weakened sub-formula property. Moreover, a formal notion of constructive paraconsistent system is given, and the constructivity of CI is proven. Further possible developments of proof theory and provability logic of CI-based arithmetical systems are sketched, and a possible weakened Hilbert?s program is discussed. As to the semantical aspects, arithmetical semantics interprets C-system formulas into Provability Logic sentences of classical Arithmetic PA (Artemov and Beklemishev (2004) [2], Japaridze and de Jongh (1998) [19], Gentilini (1999) [15], Smorynski (1991) [22]): thus, it links the notion of truth to the notion of provability inside a classical environment. It makes true infinitely many contradictions B∧¬B and falsifies many arbitrarily complex instances of non-contradiction principle ¬(A∧¬A). Moreover, arithmetical models falsify both classical logic LK and intuitionistic logic LJ, so that a kind of metalogical completeness property of LFI-paraconsistent logic w.r.t. arithmetical semantics is proven. As a work in progress, the possibility to interpret CI-based paraconsistent Arithmetic PACI into Provability Logic of classical Arithmetic PA is discussed, showing the role that PACIarithmetical models could have in establishing new meta-mathematical properties, e.g. in breaking classical equivalences between consistency statements and reflection principles.     

The Method of Socratic Proofs for Modal Propositional Logics: K5, S4.2, S4.3, S4F,S4R,S4M and G

The aim of this paper is to present the method of Socratic proofs for seven modal propositional logics: K5, S4.2, S4.3, S4M, S4F, S4R and G. This work is an extension of [10] where the method was presented for the most common modal propositional logics: K, D, T, KB, K4, S4 and S5. Presented by Jacek Malinowski     

Constructive Logic with Strong Negation is a Substructural Logic. I

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     

Varieties of Three-Valued Heyting Algebras with a Quantifier

This paper is devoted to the study of some subvarieties of the variety Qof Q-Heyting algebras, that is, Heyting algebras with a quantifier. In particular, a deeper investigation is carried out in the variety Q ₃ of three-valued Q-Heyting algebras to show that the structure of the lattice of subvarieties of Qis far more complicated that the lattice of subvarieties of Heyting algebras. We determine the simple and subdirectly irreducible algebras in Q ₃ and we construct the lattice of subvarieties (Q ₃ ) of the variety Q ₃ .     

A Rule-Extension of the Non-Associative Lambek Calculus

An extension L ⁺ of the non-associative Lambek calculus Lis defined. In L ⁺ the restriction to formula-conclusion sequents is given up, and additional left introduction rules for the directional implications are introduced. The system L ⁺ is sound and complete with respect to a modification of the ternary frame semantics for L.     

A 2-categorial Generalization of the Concept of Institution

After defining, for each many-sorted signature Σ = (S, Σ), the category Ter(Σ), of generalized terms for Σ (which is the dual of the Kleisli category for \mathbb T_S{\mathbb {T}_{\bf \Sigma}}, the monad in Set ^S determined by the adjunction T_S \dashv G_S{{\bf T}_{\bf \Sigma} \dashv {\rm G}_{\bf \Sigma}} from Set ^S to Alg(Σ), the category of Σ-algebras), we assign, to a signature morphism d from Σ to Λ, the functor d_à{{\bf d}_\diamond} from Ter(Σ) to Ter(Λ). Once defined the mappings that assign, respectively, to a many-sorted signature the corresponding category of generalized terms and to a signature morphism the functor between the associated categories of generalized terms, we state that both mappings are actually the components of a pseudo-functor Ter from Sig to the 2-category Cat. Next we prove that there is a functor Tr^Σ, of realization of generalized terms as term operations, from Alg(Σ) × Ter(Σ) to Set, that simultaneously formalizes the procedure of realization of generalized terms and its naturalness (by taking into account the variation of the algebras through the homomorphisms between them). We remark that from this fact we will get the invariance of the relation of satisfaction under signature change. Moreover, we prove that, for each signature morphism d from Σ to Λ, there exists a natural isomorphism θ ^d from the functor Tr^L °(Id ×d_à){{{\rm Tr}^{\bf {\bf \Lambda}} \circ ({\rm Id} \times {\bf d}_\diamond)}} to the functor Tr^S °(d^* ×Id){{\rm Tr}^{\bf \Sigma} \circ ({\bf d}^* \times {\rm Id})}, both from the category Alg(Λ) × Ter(Σ) to the category Set, where d* is the value at d of the arrow mapping of a contravariant functor Alg from Sig to Cat, that shows the invariant character of the procedure of realization of generalized terms under signature change. Finally, we construct the many-sorted term institution by combining adequately the above components (and, in a derived way, the many-sorted specification institution), but for a strict generalization of the standard notion of institution.     

Alternative semantics for quantified first degree relevant logic

A system FDQ of first degree entailment with quantification, extending classical quantification logic Q by an entailment connective, is axiomatised, and the choice of axioms defended and also, from another viewpoint, criticised. The system proves to be the equivalent to the first degree part of the quantified entailmental system EQ studied by Anderson and Belnap; accordingly the semantics furnished are alternative to those provided for the first degree of EQ by Belnap. A worlds semantics for FDQ is presented, and the soundness and completeness of FDQ proved, the main work of the paper going into the proof of completeness. The adequacy result is applied to yield, as well as the usual corollaries, weak relevance of FDQ and the fact that FDQ is the common first degree of a wide variety of (constant domain) quantified relevant logics. Finally much unfinished business at the first degree is discussed.     

On the Existence of Continua of Logics Between Some Intermediate Predicate Logics

A method for constructing continua of logics squeezed between some intermediate predicate logics, developed by Suzuki [8], is modified and applied to intervals of the form [L, L+ ¬¬S], where Lis a predicate logic, Sis a closed predicate formula. This solves one of the problems from Suzuki's paper.     

A weak intuitionistic propositional logic with purely constructive implication

We introduce subsystems WLJ and SI of the intuitionistic propositional logic LJ, by weakening the intuitionistic implication. These systems are justifiable by purely constructive semantics. Then the intuitionistic implication with full strength is definable in the second order versions of these systems. We give a relationship between SI and a weak modal system WM. In Appendix the Kripke-type model theory for WM is given.This work was partially supported by NSF Grant DCR85-13417     

Undecidability and intuitionistic incompleteness

Let S be a deductive system such that S-derivability (s) is arithmetic and sound with respect to structures of class K. From simple conditions on K and s, it follows constructively that the K-completeness of s implies MP(S), a form of Markov's Principle. If s is undecidable then MP(S) is independent of first-order Heyting arithmetic. Also, if s is undecidable and the S proof relation is decidable, then MP(S) is independent of second-order Heyting arithmetic, HAS. Lastly, when s is many-one complete, MP(S) implies the usual Markov's Principle MP.An immediate corollary is that the Tarski, Beth and Kripke weak completeness theorems for the negative fragment of intuitionistic predicate logic are unobtainable in HAS. Second, each of these: weak completeness for classical predicate logic, weak completeness for the negative fragment of intuitionistic predicate logic and strong completeness for sentential logic implics MP. Beth and Kripke completeness for intuitionistic predicate or sentential logic also entail MP.These results give extensions of the theorem of Gödel and Kreisel (in [4]) that completeness for pure intuitionistic predicate logic requires MP. The assumptions of Gödel and Kreisel's original proof included the Axiom of Dependent Choice and Herbrand's Theorem, no use of which is explicit in the present article.     

An Incomplete Relevant Modal Logic

The relevant modal logic G is a simple extension of the logic RT, the relevant counterpart of the familiar classically based system T. Using the Routley–Meyer semantics for relevant modal logics, this paper proves three main results regarding G: (i) G is semantically complete, but only with a non-standard interpretation of necessity. From this, however, other nice properties follow. (ii) With a standard interpretation of necessity, G is semantically incomplete; there is no class of frames that characterizes G. (iii) The class of frames for G characterizes the classically based logic T.     

Constructive Logic with Strong Negation is a Substructural Logic. II

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 . The main result of Part I of this series [41] shows 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. In this paper, the term equivalence result of Part I [41] is lifted to the setting of deductive systems to establish the definitional equivalence of the logics N and NFL _ew . It follows from the definitional equivalence of these systems that constructive logic with strong negation is a substructural logic. Presented by Heinrich Wansing     

The Incompleteness of RGL

RGLis a version of the modal logic GLbased on the relevant logic R. It is shown that the class of RKframes that verify all theorems of RGLalso verify a scheme that we call (!). If RGLhas (!) as a theorem, however, it is not a relevant logic. I go on to show that not all instances of (!) are theorems of RGL, hence this logic is not complete over any class of RKframes.     

Axiomatization and completeness of uncountably valued approximation logic

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     

Light Affine Set Theory: A Naive Set Theory of Polynomial Time

In [7], a naive set theory is introduced based on a polynomial time logical system, Light Linear Logic (LLL). Although it is reasonably claimed that the set theory inherits the intrinsically polytime character from the underlying logic LLL, the discussion there is largely informal, and a formal justification of the claim is not provided sufficiently. Moreover, the syntax is quite complicated in that it is based on a non-traditional hybrid sequent calculus which is required for formulating LLL.In this paper, we consider a naive set theory based on Intuitionistic Light Affine Logic (ILAL), a simplification of LLL introduced by [1], and call it Light Affine Set Theory (LAST). The simplicity of LAST allows us to rigorously verify its polytime character. In particular, we prove that a function over {0, 1}* is computable in polynomial time if and only if it is provably total in LAST.     

Algebraic logic for classical conjunction and disjunction

In this paper we study the relations between the fragment L of classical logic having just conjunction and disjunction and the variety D of distributive lattices, within the context of Algebraic Logic. We prove that these relations cannot be fully expressed either with the tools of Blok and Pigozzi's theory of algebraizable logics or with the use of reduced matrices for L. However, these relations can be naturally formulated when we introduce a new notion of model of a sequent calculus. When applied to a certain natural calculus for L, the resulting models are equivalent to a class of abstract logics (in the sense of Brown and Suszko) which we call distributive. Among other results, we prove that D is exactly the class of the algebraic reducts of the reduced models of L, that there is an embedding of the theories of L into the theories of the equational consequence (in the sense of Blok and Pigozzi) relative to D, and that for any algebra A of type (2,2) there is an isomorphism between the D-congruences of A and the models of L over A. In the second part of this paper (which will be published separately) we will also apply some results to give proofs with a logical flavour for several new or well-known lattice-theoretical properties.Dedicated to our master, Francesc d'A. Sales, on his 75th birthday     

Gleason's Theorem Has a Constructive Proof

Gleason's theorem for R ³ says that if f is a nonnegative function on the unit sphere with the property that f(x) + f(y) + f(z) is a fixed constant for each triple x,y,z of mutually orthogonal unit vectors, then f is a quadratic form. We examine the issues raised by discussions in this journal regarding the possibility of a constructive proof of Gleason"s theorem in light of the recent publication of such a proof.     

The existence of matrices strongly adequate for E,R and their fragments

A logic is a pair (P,Q) where P is a set of formulas of a fixed propositional language and Q is a set of rules. A formula is deducible from X in the logic (P, Q) if it is deducible from XP via Q. A matrix is strongly adequate to (P, Q) if for any , X, is deducible from X iff for every valuation in , is designated whenever all the formulas in X are. It is proved in the present paper that if Q = {modus ponens, adjunction } and P {E, R, E ⁺, R ⁺, E ^I, R ^I } then there exists a matrix strongly adequate to (P, Q).     

On the Closure Properties of the Class of Full G-models of a Deductive System

In this paper we consider the structure of the class FGModS of full generalized models of a deductive system S from a universal-algebraic point of view, and the structure of the set of all the full generalized models of S on a fixed algebra A from the lattice-theoretical point of view; this set is represented by the lattice FACS_s A of all algebraic closed-set systems C on A such that (A, C) ε FGModS. We relate some properties of these structures with tipically logical properties of the sentential logic S. The main algebraic properties we consider are the closure of FGModS under substructures and under reduced products, and the property that for any A the lattice FACS_s A is a complete sublattice of the lattice of all algebraic closed-set systems over A. The logical properties are the existence of a fully adequate Gentzen system for S, the Local Deduction Theorem and the Deduction Theorem for S. Some of the results are established for arbitrary deductive systems, while some are found to hold only for deductive systems in more restricted classes like the protoalgebraic or the weakly algebraizable ones. The paper ends with a section on examples and counterexamples. Dedicated to the memory of Willem Johannes Blok