This paper considers logics which are formally dual to intuitionistic logic in order to investigate a co-constructive logic for proofs and refutations. This is philosophically motivated by a set of problems regarding the nature of constructive truth, and its relation to falsity. It is well known both that intuitionism can not deal constructively with negative information, and that defining falsity by means of intuitionistic negation leads, under widely-held assumptions, to a justification of bivalence. For example, we (...) do not want to equate falsity with the non-existence of a proof since this would render a statement such as “pi is transcendental” false prior to 1882. In addition, the intuitionist account of negation as shorthand for the derivation of absurdity is inadequate, particularly outside of purely mathematical contexts. To deal with these issues, I investigate the dual of intuitionistic logic, co-intuitionistic logic, as a logic of refutation, alongside intuitionistic logic of proofs. Direct proof and refutation are dual to each other, and are constructive, whilst there also exist syntactic, weak, negations within both logics. In this respect, the logic of refutation is weakly paraconsistent in the sense that it allows for statements for which, neither they, nor their negation, are refuted. I provide a proof theory for the co-constructive logic, a formal dualizing map between the logics, and a Kripke-style semantics. This is given an intuitive philosophical rendering in a re-interpretation of Kolmogorov’s logic of problems. (shrink)

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. (shrink)

It is widely accepted that there is a clear sense in which the first-order paraconsistent constructive logic with strong negation of Almukdad and Nelson, QN4, is more constructive than intuitionistic first-order logic, QInt. While QInt and QN4 both possess the disjunction property and the existence property as characteristics of constructiveness (or constructivity), QInt lacks certain features of constructiveness enjoyed by QN4, namely the constructible falsity property and the dual of the existence property. This paper deals with (...) the constructiveness of the contra-classical, connexive, paraconsistent, and contradictory non-trivial first-order logic QC, which is a connexive variant of QN4. It is shown that there is a sense in which QC is even more constructive than QN4. The argument focuses on a problem that is mirror-inverted to Raymond Smullyan’s drinker paradox, namely the invalidity of what will be called the drinker truism and its dual in QN4 (and QInt), and on a version of the Brouwer-Heyting-Kolmogorov interpretation of the logical operations that treats proofs and disproofs on a par. The validity of the drinker truism and its dual together with the greater constructiveness of QC in comparison to QN4 may serve as further motivation for the study of connexive logics and suggests that constructive logic is connexive and contradictory (the latter understood as being negation inconsistent). (shrink)

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 and the equivalent variety semantics of NFL ew 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. (shrink)

We study the connection between factors of the Medvedev lattice and constructive logic. The algebraic properties of these factors determine logics lying in between intuitionistic propositional logic and the logic of the weak law of the excluded middle (also known as De Morgan, or Jankov, logic). We discuss the relation between the weak law of the excluded middle and the algebraic notion of join-reducibility. Finally we discuss autoreducible degrees.

Shapiro and Taschek have argued that simply using intuitionistic logic and its Heyting semantics, one can show that there are no gaps in warranted assertability. That is, given that a discourse is faithfully modeled using Heyting's semantics for the logical constants, then if a statement _S is not warrantedly assertable, its negation (superscript box) _S is. Tennant has argued for this conclusion on similar grounds. I show that these arguments fail, albeit in illuminating ways. An appeal to constructive (...) logic does not commit one to this strong epistemological thesis, but appeals to semantics of intuitionistic logic none the less do give us certain conclusions about the connections between warranted assertability and truth. (edited). (shrink)

In this paper, consistency is understood as the absence of the negation of a theorem, and not, in general, as the absence of any contradiction. We define the basic constructive logic BKc1 adequate to this sense of consistency in the ternary relational semantics without a set of designated points. Then we show how to define a series of logics extending BKc1 within the spectrum delimited by contractionless minimal intuitionistic logic. All logics defined in the paper are paraconsistent (...) logics. (shrink)

This paper considers a topos-theoretic structure for the interpretation of co-constructive logic for proofs and refutations following Trafford :22–40, 2015). It is notoriously tricky to define a proof-theoretic semantics for logics that adequately represent constructivity over proofs and refutations. By developing abstractions of elementary topoi, we consider an elementary topos as structure for proofs, and complement topos as structure for refutation. In doing so, it is possible to consider a dialogue structure between these topoi, and also control their (...) relation such that classical logic is simulated where proofs and refutations are conclusive. (shrink)

In the present paper I wish to regard constructivelogic as a self-contained system for the treatment ofepistemological issues; the explanations of theconstructivist logical notions are cast in anepistemological mold already from the outset. Thediscussion offered here intends to make explicit thisimplicit epistemic character of constructivism.Particular attention will be given to the intendedinterpretation laid down by Heyting. This interpretation, especially as refined in the type-theoretical work of Per Martin-Löf, puts thesystem on par with the early efforts of Frege andWhitehead-Russell. This quite (...) recent work, however,has proved valuable not only in the philosophy andfoundations of mathematics, but has also foundpractical application in computer science, where thelanguage of constructivism serves as an implementableprogramming language, and within the philosophy oflanguage.\footnote{Nordstr\"{o}m et al. give an overview of the work in computerscience, whereas Ranta provides an impressiveconstructivist alternative to Montague Grammar usingthe richer type structure of Martin-L\"{o}f in placeof the simple classical type theory of Church.} Mypresentation will be carried out through a contrastwith standard metamathematical work.\footnote{Troelstra and van Dalen give an encyclopedictreatment of the metamathematics of constructivism.}In the course of the development I have occasion tooffer some novel considerations on thenature of proof and inference. (shrink)

In this paper, consistency is understood in the standard way, i.e. as the absence of a contradiction. The basic constructive logic BKc4, which is adequate to this sense of consistency in the ternary relational semantics without a set of designated points, is defined. Then, it is shown how to define a series of logics by extending BKc4 up to minimal intuitionistic logic. All logics defined in this paper are paraconsistent logics.

A proof is given that the set of maximal intermediate propositional logics with the disjunction property and the set of maximal intermediate predicate logics with the disjunction property and the explicit definability property have the power of continuum. To prove our results, we introduce various notions which might be interesting by themselves. In particular, we illustrate a method to generate wide sets of pairwise "constructively incompatible constructive logics". We use a notion of "semiconstructive" logic and define wide sets (...) of "constructive" logics by representing the "constructive" logics as "limits" of decreasing sequences of "semiconstructive" logics. Also, we introduce some generalizations of the usual filtration techniques for propositional logics. For instance, "filtrations over rank formulas" are used to show that any two different logics belonging to a suitable uncountable set of "constructive" logics are "constructively incompatible". (shrink)

In this paper, consistency is understood as absolute consistency (i.e. non-triviality). The basic constructive logic BKc6, which is adequate to this sense of consistency in the ternary relational semantics without a set of designated points, is defined. Then, it is shown how to define a series of logics by extending BKc6 up to contractionless intuitionistic logic. All logics defined in this paper are paraconsistent logics.

The aim of the paper is to show that topoi are useful in the categorial analysis of the constructive logic with strong negation. In any topos ϵ we can distinguish an object Λ and its truth-arrows such that sets ϵ have a Nelson algebra structure. The object Λ is defined by the categorial counterpart of the algebraic FIDEL-VAKARELOV construction. Then it is possible to define the universal quantifier morphism which permits us to make the first order predicate calculus. (...) The completeness theorem is proved using the Kripke-type semantic defined by THOMASON. (shrink)

The logic BKc1 is the basic constructive logic for weak consistency in the ternary relational semantics without a set of designated points. In this paper, a number of extensions of B Kc1 defined with a propositional falsity constant are defined. It is also proved that weak consistency is not equivalent to negation-consistency or absolute consistency in any logic included in positive contractionless intermediate logic LC plus the constructive negation of BKc1 and the contraposition axioms.

We study axiomatic extensions of the propositional constructive logic with strong negation having the disjunction property in terms of corresponding to them varieties of Nelson algebras. Any such varietyV is characterized by the property: (PQWC) ifA,B V, thenA×B is a homomorphic image of some well-connected algebra ofV.We prove:• each varietyV of Nelson algebras with PQWC lies in the fibre –1(W) for some varietyW of Heyting algebras having PQWC, • for any varietyW of Heyting algebras with PQWC the least (...) and the greatest varieties in –1(W) have PQWC, • there exist varietiesW of Heyting algebras having PQWC such that –1(W) contains infinitely many varieties (of Nelson algebras) with PQWC. (shrink)

to constructive systems is significant for contemporary metaphysics. However, many are surprised by these results, having learned that the Axiom of Choice (AC) is constructively valid. Indeed, even among specialists there were, until recently, reasons for puzzlement-rival versions of Intuitionistic Type Theory, one where (AC) is valid, another where it implies classical logic. This paper accessibly explains the situation, puts the issues in a broader setting by considering other choice principles, and draws philosophical morals for the understanding of (...) quantification, choice principles, and the prospects for constructivism. (shrink)

The logic BKc6 is the basic constructive logic in the ternary relational semantics adequate to consistency understood as absolute consistency, i.e., non-triviality. Negation is introduced in BKc6 with a negation connective. The aim of this paper is to define the logic BKc6F. In this logic negation is introduced via a propositional falsity constant. We prove that BKc6 and BKc6F are definitionally equivalent. Then, we show how to extend BKc6F within the spectrum of logics delimited by (...) contractionless intuitionistic logic. All logics defined in the paper are paraconsistent logics. (shrink)

The logic BKc1 is the basic constructive logic in the ternary relational semantics adequate to consistency understood as the absence of the negation of any theorem. Negation is introduced in BKc1 with a negation connective. The aim of this paper is to define the logic BKc1F. In this logic negation is introduced via a propositional falsity constant. We prove that BKc1 and BKc1F are definitionally equivalent.

We extend to the predicate frame a previous characterization of the maximal intermediate propositional constructive logics. This provides a technique to get maximal intermediate predicate constructive logics starting from suitable sets of classically valid predicate formulae we call maximal nonstandard predicate constructive logics. As an example of this technique, we exhibit two maximal intermediate predicate constructive logics, yet leaving open the problem of stating whether the two logics are distinct. Further properties of these logics will be (...) also investigated. (shrink)

This thesis introduces the "method of structural refinement", which serves as a means of transforming the relational semantics of a modal and/or constructive logic into an 'economical' proof system by connecting two proof-theoretic paradigms: labelled and nested sequent calculi. The formalism of labelled sequents has been successful in that cut-free calculi in possession of desirable proof-theoretic properties can be automatically generated for large classes of logics. Despite these qualities, labelled systems make use of a complicated syntax that explicitly (...) incorporates the semantics of the associated logic, and such systems typically violate the subformula property to a high degree. By contrast, nested sequent calculi employ a simpler syntax and adhere to a strict reading of the subformula property, making such systems useful in the design of automated reasoning algorithms. However, the downside of the nested sequent paradigm is that a general theory concerning the automated construction of such calculi (as in the labelled setting) is essentially absent, meaning that the construction of nested systems and the confirmation of their properties is usually done on a case-by-case basis. The refinement method connects both paradigms in a fruitful way, by transforming labelled systems into nested (or, refined labelled) systems with the properties of the former preserved throughout the transformation process. To demonstrate the method of refinement and some of its applications, we consider grammar logics, first-order intuitionistic logics, and deontic STIT logics. The introduced refined labelled calculi will be used to provide the first proof-search algorithms for deontic STIT logics. Furthermore, we employ our refined labelled calculi for grammar logics to show that every logic in the class possesses the effective Lyndon interpolation property. (shrink)

Ishihara's problem of decidable variables asks which class of decidable propositional variables is sufficient to warrant classical theorems in intuitionistic logic. We present several refinements to the class proposed by Ishii for this problem, which also allows the class to cover Glivenko's logic. We also treat the extension of the problem to minimal logic, suggesting a couple of new classes.

We propose contractionless constructive logic which is obtained from Nelson's constructive logic by deleting contractions. We discuss the consistency of a naive set theory based on the proposed logic in relation to Curry's paradox. The philosophical significance of contractionless constructive logic is also argued in comparison with Fitch's and Prawitz's systems.

In a standard sense, consistency and paraconsistency are understood as the absence of any contradiction and as the absence of the ECQ (‘E contradictione quodlibet’) rule, respectively. The concepts of weak consistency (in two different senses) as well as that of F -consistency have been defined by the authors. The aim of this paper is (a) to define alternative (to the standard one) concepts of paraconsistency in respect of the aforementioned notions of weak consistency and F -consistency; (b) to define (...) the concept of strong paraconsistency; (c) to build up a series of strongly paraconsistent logics; (d) to define the basic constructive logic adequate to a rather weak sense of consistency. All logics treated in this paper are strongly paraconsistent. All of them are sound and complete in respect a modification of Routley and Meyer’s ternary relational semantics for relevant logics (no logic in this paper is relevant). (shrink)

Certain extensions of Nelson's constructive logic N with strong negation have recently become important in arti.cial intelligence and nonmonotonic reasoning, since they yield a logical foundation for answer set programming (ASP). In this paper we look at some extensions of Nelson's .rst-order logic as a basis for de.ning nonmonotonic inference relations that underlie the answer set programming semantics. The extensions we consider are those based on 2-element, here-and-there Kripke frames. In particular, we prove completeness for .rst-order here-and-there (...) logics, and their minimal strong negation extensions, for both constant and varying domains. We choose the constant domain version, which we denote by QNc5, as a basis for de.ning a .rst-order nonmonotonic extension called equilibrium logic. We establish several metatheoretic properties of QNc5, including Skolem forms and Herbrand theorems and Interpolation, and show that the .rst-oder version of equilibrium logic can be used as a foundation for answer set inference. (shrink)

This paper examines the relationships between the many-valued logics G~ and Gn~ of Esteva, Godo, Hajek, and Navara, i.e., Godel logic G enriched with Łukasiewicz negation, and neighbors of intuitionistic logic. The popular fragments of Rauszer's Heyting-Brouwer logic HB admit many-valued extensions similar to G which may likewise be enriched with Łukasiewicz negation; the fuzzy extensions of these logics, including HB, are equivalent to G ~, as are their n-valued extensions equivalent to Gn~ for any n ≥ (...) 2. These enriched systems extend Wansing's logic I4C4, showing that Łukasiewicz negation is a species of Nelson's negation of constructible falsity and yielding a Kripke-style semantics for G~ and Gn~ to complement the many-valued semantics. (shrink)

Our conception of logical space is the set of distinctions we use to navigate the world. Agustn Rayo argues that this is shaped by acceptance or rejection of 'just is'-statements: e.g. 'to be composed of water just is to be composed of H2O'. He offers a novel conception of metaphysical possibility, and a new trivialist philosophy of mathematics.

We use formal semantic analysis based on new constructions to study abstract realizability, introduced by Läuchli in 1970, and expose its algebraic content. We claim realizability so conceived generates semantics-based intuitive confidence that the Heyting Calculus is an appropriate system of deduction for constructive reasoning.Well-known semantic formalisms have been defined by Kripke and Beth, but these have no formal concepts corresponding to constructions, and shed little intuitive light on the meanings of formulae. In particular, the completeness proofs for these (...) semantics do not generate confidence in the sufficiency of the Heyting Calculus, since we have no reason to believe that every intuitively constructive truth is valid in the formal semantics.Läuchli has proved completeness for a realizability semantics with formal concepts analogous to constructions. We argue in some detail that, in spite of a certain inherent inexactness of the analogy, every intuitively constructive truth is valid in Läuchli semantics, and therefore the Heyting Calculus is powerful enough to prove all constructive truths. Our argument is based on the postulate that a uniformly constructible object must be communicable in spite of imprecision in our language, and that the permutations in Läuchli's semantics represent conceivable imprecision in a language, while allowing a certain amount of freedom in choosing the particular structure of the language.We give a detailed generalization of Läuchli's proof of completeness for the propositional part of the Heyting Calculus, in order to make explicit constructive and algebraic content.In our treatment, we establish several new results about Läuchli models. We show how to extend the sconing and gluing constructions familiar from Kripke and Frame semantics and Topos theory, to Läuchli models, and use them to give an algebraic approach to countermodel construction. In particular, the Läuchli arguments are given without the restriction to the integers, Z, as a group of permutations, which makes much of the coding scheme used in Läuchli's original paper transparent.We also make use of a new propositions-as-types syntax for the Heyting calculus, with limited nondeterminism, in which validity of formulae can be decided without loop-detection. (shrink)

We present a geometric construction that yields completeness results for modal logics including K4, KD4, GL and GL n with respect to certain subspaces of the rational numbers. These completeness results are extended to the bimodal case with the universal modality.

In this paper, we show that the predicate logics of consistent extensions of Heyting's Arithmetic plus Church's Thesis with uniqueness condition are complete $\Pi _{2}^{0}$. Similarly, we show that the predicate logic of HA*, i.e. Heyting's Arithmetic plus the Completeness Principle (for HA*) is complete $\Pi _{2}^{0}$. These results extend the known results due to Valery Plisko. To prove the results we adapt Plisko's method to use Tennenbaum's Theorem to prove 'categoricity of interpretations' under certain assumptions.

Review of "The Construction of Logical Space", by Augustin Rayo. Oxford: OxfordUniversity Press, 2013. Pp. xix+220. H/b$35.00.

In Poggiolesi we have introduced a rigorous definition of the notion of complete and immediate formal grounding; in the present paper our aim is to construct a logic for the notion of complete and immediate formal grounding based on that definition. Our logic will have the form of a calculus of natural deduction, will be proved to be sound and complete and will allow us to have fine-grained grounding principles.

A construction principle for natural deduction systems for arbitrary, finitely-many-valued first order logics is exhibited. These systems are systematically obtained from sequent calculi, which in turn can be automatically extracted from the truth tables of the logics under consideration. Soundness and cut-free completeness of these sequent calculi translate into soundness, completeness, and normal-form theorems for natural deduction systems.

We show that numerous distinctive concepts of constructive mathematics arise automatically from an “antithesis” translation of affine logic into intuitionistic logic via a Chu/Dialectica construction. This includes apartness relations, complemented subsets, anti-subgroups and anti-ideals, strict and non-strict order pairs, cut-valued metrics, and apartness spaces. We also explain the constructive bifurcation of some classical concepts using the choice between multiplicative and additive affine connectives. Affine logic and the antithesis construction thus systematically “constructivize” classical definitions, handling the (...) resulting bookkeeping automatically. (shrink)