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     

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.     

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 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.     

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.     

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     

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.     

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.     

Generic generalized Rosser fixed points

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.     

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.     

Truth,Predication and a Family of Contingent Paradoxes

In truth theory one aims at general formal laws governing the attribution of truth to statements. Gupta’s and Belnap’s revision-theoretic approach provides various well-motivated theories of truth, in particular T* and T#, which tame the Liar and related paradoxes without a Tarskian hierarchy of languages. In property theory, one similarly aims at general formal laws governing the predication of properties. To avoid Russell’s paradox in this area a recourse to type theory is still popular, as testified by recent work in formal metaphysics by Williamson and Hale. There is a contingent Liar that has been taken to be a problem for type theory. But this is because this Liar has been presented without an explicit recourse to a truth predicate. Thus, type theory could avoid this paradox by incorporating such a predicate and accepting an appropriate theory of truth. There is however a contingent paradox of predication that more clearly undermines the viability of type theory. It is then suggested that a type-free property theory is a better option. One can pursue it, by generalizing the revision-theoretic approach to predication, as it has been done by Orilia with his system P*, based on T*. Although Gupta and Belnap do not explicitly declare a preference for T# over T*, they show that the latter has some advantages, such as the recovery of intuitively acceptable principles concerning truth and a better reconstruction of informal arguments involving this notion. A type-free system based on T# rather than T* extends these advantages to predication and thus fares better than P* in the intended applications of property theory.

     

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.     

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     

A Cut-Free Sequent System for the Smallest Interpretability Logic

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.     

On the Representation of N4-Lattices

N4-lattices provide algebraic semantics for the logic N4, the paraconsistent variant of Nelson's logic with strong negation. We obtain the representation of N4-lattices showing that the structure of an arbitrary N4-lattice is completely determined by a suitable implicative lattice with distinguished filter and ideal. We introduce also special filters on N4-lattices and prove that special filters are exactly kernels of homomorphisms. Criteria of embeddability and to be a homomorphic image are obtained for N4-lattices in terms of the above mentioned representation. Finally, subdirectly irreducible N4-lattices are described.     

A Negationless Interpretation of Intuitionistic Theories. I

The present work contains an axiomatic treatment of some parts of the restricted version of intuitionistic mathematics advocated by G. F. C. Griss, also known as negationless intuitionistic mathematics. Formal systems NPC, NA, and FIM ^N for negationless predicate logic, arithmetic, and analysis are proposed. Our Theorem 4 in Section 2 asserts the translatability of Heyting's arithmetic HAinto NA. The result can in fact be extended to a large class of intuitionistic theories based on HAand their negationless counterparts. For instance, in Section 3 this is shown for Kleene's system of intuitionistic analysis FIMand our FIM ^N . This revised version was published online in June 2006 with corrections to the Cover Date.     

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.     

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     

Affective flexibility and generalized anxiety disorder: valence-specific shifting difficulties

ABSTRACT

Background: Growing evidence suggests that generalized anxiety disorder (GAD) is associated with poor affective flexibility, defined as the ability to switch between emotional aspects and non-emotional aspects of a situation. However, it is unclear whether affective inflexibility is valence-specific in GAD.

Methods: Participants with GAD (n?=?21) and non-clinical control participants (n?=?28) were tested on an Affective Switching Task during which participants were asked to categorize pictures either by the valence or by the number of humans present in the pictures.

Results: Individuals with GAD, but not healthy controls, exhibited greater difficulty shifting from emotional aspects of negative material compared to emotional aspects of positive material and shifting to the emotional aspects of positive material compared to emotional aspects of negative material.

Conclusions: These findings suggest that GAD is associated with valence-specific affective flexibility biases. The relevance of the findings and directions for future research are discussed.     

Minimally Abnormal Models In Some Adaptive Logics

In an adaptive logic APL, based on a (monotonic) non-standardlogic PL the consequences of can be defined in terms ofa selection of the PL-models of . An important property ofthe adaptive logics ACLuN1, ACLuN2, ACLuNs1, andACLuNs2 logics is proved: whenever a model is not selected, this isjustified in terms of a selected model (Strong Reassurance). Theproperty fails for Priest's LP ^m because its way of measuring thedegree of abnormality of a model is incoherent – correcting thisdelivers the property.