. This paper continues a systematic approach to build natural deduction calculi and corresponding proof procedures for non-classical logics. Our attention is now paid to the framework of paraconsistent logics. These logics are used, in particular, for reasoning about systems where paradoxes do not lead to the `deductive explosion', i.e., where formulae of the type `A follows from false', for any A, are not valid. We formulate the natural deduction system for the logic PCont, explain its (...) main concepts, define a proof searching technique and illustrate it by examples. The presentation is accompanied by demonstrating the correctness of these developments. (shrink)

Varieties of natural deduction systems are introduced for Wansing’s paraconsistent non-commutative substructural logic, called a constructive sequential propositional logic (COSPL), and its fragments. Normalization, strong normalization and Church-Rosser theorems are proved for these systems. These results include some new results on full Lambek logic (FL) and its fragments, because FL is a fragment of COSPL.

Firstly, a natural deduction system in standard style is introduced for Nelson's para-consistent logic N4, and a normalization theorem is shown for this system. Secondly, a natural deduction system in sequent calculus style is introduced for N4, and a normalization theorem is shown for this system. Thirdly, a comparison between various natural deduction systems for N4 is given. Fourthly, a strong normalization theorem is shown for a natural deduction system for a (...) sublogic of N4. Fifthly, a strong normalization theorem is proved for a typed λ-calculus for a neighbor of N4. Finally, it is remarked that the natural deduction frameworks presented can also be adapted for Wansing's basic connexive logic C. (shrink)

This presentation of Aristotle's natural deduction system supplements earlier presentations and gives more historical evidence. Some fine-tunings resulted from conversations with Timothy Smiley, Charles Kahn, Josiah Gould, John Kearns,John Glanvillle, and William Parry.The criticism of Aristotle's theory of propositions found at the end of this 1974 presentation was retracted in Corcoran's 2009 HPL article "Aristotle's demonstrative logic".

We introduce a natural deduction system for the until-free subsystem of the branching time logic Although we work with labelled formulas, our system differs conceptually from the usual labelled deduction systems because we have no relational formulas. Moreover, no deduction rule embodies semantic features such as properties of accessibility relation or similar algebraic properties. We provide a suitable semantics for our system and prove that it is sound and weakly complete with respect to such semantics.

This paper is concerned with a natural deduction system for First Degree Entailment (FDE). First, we exhibit a brief history of FDE and of combined systems whose underlying idea is used in developing the natural deduction system. Then, after presenting the language and a semantics of FDE, we develop a natural deduction system for FDE. We then prove soundness and completeness of the system with respect to the semantics. The system neatly represents (...) the four-valued semantics for FDE. (shrink)

The aim of the paper is to present two natural deduction systems for Intuitionistic Sentential Calculus with Identity ( ISCI ); a syntactically motivated \(\mathsf {ND}^1_{\mathsf {ISCI}}\) and a semantically motivated \(\mathsf {ND}^2_{\mathsf {ISCI}}\). The formulation of \(\mathsf {ND}^1_{\mathsf {ISCI}}\) is based on the axiomatic formulation of ISCI. Its rules cannot be straightforwardly classified as introduction or elimination rules; ISCI -specific rules are based on axioms characterizing the identity connective. The system does not enjoy the standard subformula property, (...) but due to the normalization procedure non-subformulas can label only leaves of proofs. In \(\mathsf {ND}^2_{\mathsf {ISCI}}\), we propose only two general identity-related rules, in reference to the treatment of the identity connective in First-Order Logic. (shrink)

The sentential calculus SC of Kalish and Montague is extended to modal sentences. Rules of inference and a derivation procedure are added. The resultant natural deduction system SMC is like a system for S4 due to Fitch, but SMC is for S5 and the restriction on necessity derivation concerns.terminations of such derivations whereas the restriction on strict subordinate proof in Fitch's system concerns the line-by-line development of such proofs. An axiomatic system AxMC for S5 founded (...) on SC is presented and it is shown that SMC and AxMC are equivalent : what ever is derivable in one system is derivable in the other. (shrink)

In this paper two different natural deduction systems forhybrid logic are compared and contrasted.One of the systems was originally given by the author of the presentpaper whereasthe other system under consideration is a modifiedversion of a natural deductionsystem given by Jerry Seligman.We give translations in both directions between the systems,and moreover, we devise a set of reduction rules forthe latter system bytranslation of already known reduction rules for the former system.

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.

In this paper we study natural deduction for the intuitionistic and classical (normal) modal logics obtained from the combinations of the axioms T, B, 4 and 5. In this context we introduce a new multi-contextual structure, called T-sequent, that allows to design simple labelfree natural deduction systems for these logics. After proving that they are sound and complete we show that they satisfy the normalization property and consequently the subformula property in the intuitionistic case.

The paper is devoted to the concise description of some Natural Deduction System (ND for short) for Linear Temporal Logic. The system's distinctive feature is that it is labelled and analytical. Labels convey necessary semantic information connected with the rules for temporal functors while the analytical character of the rules lets the system work as a decision procedure. It makes it more similar to Labelled Tableau Systems than to standard Natural Deduction. In fact, our solution (...) of linearity representation is rather independent of the underlying proof method, provided that some form of (analytic) cut is admissible. We will also discuss some generalisations of the system and compare it with other formalizations of linearity. (shrink)

In this paper, we investigate the possibility of translating a fragment of natural deduction system (NDS) for natural language semantics into modern type theory (MTT), originally suggested by Luo (2014). Our main goal will be to examine and translate the basic rules of NDS (namely, meta-rules, structural rules, identity rules, noun rules and rules for intersective and subsective adjectives) to MTT. Additionally, we will also consider some of their general features.

For each truth-functionally complete set of connectives, we construct a sound and complete natural deduction system containing no axioms and the smallest possible number of inference rules, namely one.

The paper contains an exposition of standard ND-formalizations for modal logics. For the sake of simplicity, it is limited to propositional monomodal logics because focus is on methods not on logics. Some of the discussed approaches, however, may be easily extended to first order modal logics of different sorts or to multimodal logics . Natural Deduction is understood in the strict sense, explained below; neither Gentzen Sequent Calculus, nor Tableau Systems belong to that group. Moreover, some ND-systems with generalized (...) apparatus, like [2] or [3] are also omitted in this survey. There are four basic approaches to modality via NDformalization, which are compared and evaluated with respect to their generality: modalization of assumptions, modalization of reiteration rule, modalization of rules, application of modal assumptions. We focus on practical matters, especially on the applicability of discussed approaches, the only exception is the discussion of independent rules for necessity and possibility in the last section. (shrink)

In 1934 Stanisław Jaśkowski published his groundbreaking work on natural deduction. At the same year Gerhard Gentzen also published a work on the same topic. We aim at presenting of Jaśkowski’s system and provide a comparison with Gentzen’s approach. We also try to outline the influence of Jaśkowski’s approach on the later development of natural deduction systems.

It is often said that in a purely formal perspective, intuitionistic logic has no obvious advantage to deal with the liar-type paradoxes. In this paper, we will argue that the standard intuitionistic natural deduction systems are vulnerable to the liar-type paradoxes in the sense that the acceptance of the liar-type sentences results in inference to absurdity (⊥). The result shows that the restriction of the Double Negation Elimination (DNE) fails to block the inference to ⊥. It is, however, not (...) the problem of the intuitionistic approaches to the liar-type paradoxes but the lack of expressive power of the standard intuitionistic natural deduction system. We introduce a meta-level negation for a given system and a meta-level absurdity, ⋏, to the intuitionistic system. We shall show that in the system, the inference to ⊥ is not given without the assumption that the system is complete. Moreover, we consider the Double Meta-Level Negation Elimination rules (DMNE) which implicitly assume the completeness of the system. Then, the restriction of DMNE can rule out the inference to ⊥. (shrink)

This book provides a detailed exposition of one of the most practical and popular methods of proving theorems in logic, called Natural Deduction. It is presented both historically and systematically. Also some combinations with other known proof methods are explored. The initial part of the book deals with Classical Logic, whereas the rest is concerned with systems for several forms of Modal Logics, one of the most important branches of modern logic, which has wide applicability.

The relation between logic and thought has long been controversial, but has recently influenced theorizing about the nature of mental processes in cognitive science. One prominent tradition argues that to explain the systematicity of thought we must posit syntactically structured representations inside the cognitive system which can be operated upon by structure sensitive rules similar to those employed in systems of natural deduction. I have argued elsewhere that the systematicity of human thought might better be explained as resulting (...) from the fact that we have learned natural languages which are themselves syntactically structured. According to this view, symbols of natural language are external to the cognitive processing system and what the cognitive system must learn to do is produce and comprehend such symbols. In this paper I pursue that idea by arguing that ability in natural deduction itself may rely on pattern recognition abilities that enable us to operate on external symbols rather than encodings of rules that might be applied to internal representations. To support this suggestion, I present a series of experiments with connectionist networks that have been trained to construct simple natural deductions in sentential logic. These networks not only succeed in reconstructing the derivations on which they have been trained, but in constructing new derivations that are only similar to the ones on which they have been trained. (shrink)

Anderson and Belnap presented indexed Fitch-style natural deduction systems for the relevant logics R, E, and T. This work was extended by Brady to cover a range of relevant logics. In this paper I present indexed tree natural deduction systems for the Anderson–Belnap–Brady systems and show how to translate proofs in one format into proofs in the other, which establishes the adequacy of the tree systems.

The author presents a deduction system for Quantum Logic. This system is a combination of a natural deduction system and rules based on the relation of compatibility. This relation is the logical correspondant of the commutativity of observables in Quantum Mechanics or perpendicularity in Hilbert spaces. Contrary to the system proposed by Gibbins and Cutland, the natural deduction part of the system is pure: no algebraic artefact is added. The rules of the (...) class='Hi'>system are the rules of Classical Natural Deduction in which is added a control of contexts using the compatibility relation. The author uses his system to prove the following theorem: if propositions of a quantum logical propositional calculus system are mutually compatible, they form a classical subsystem. (shrink)

The main result of this paper is a normalizing system of natural deduction for the full language of intuitionistic linear logic. No explicit weakening or contraction rules for -formulas are needed. By the systematic use of general elimination rules a correspondence between normal derivations and cut-free derivations in sequent calculus is obtained. Normalization and the subformula property for normal derivations follow through translation to sequent calculus and cut-elimination.

In 2015 Dag Prawitz proposed a natural deduction ecumenical system, where classical logic and intuitionistic logic are codified in the same system. In his ecumenical system, Prawitz recovers the harmony of rules, but the rules for the classical operators do not satisfy separability. In fact, the classical rules are not pure, in the sense that negation is used in the definition of the introduction and elimination rules for the classical operators. In this work we propose an (...) ecumenical system adapting, to the natural deduction framework, Girard’s mechanism of stoup. This allows for the definition of a pure harmonic natural deduction system for the propositional fragment of Prawitz’s ecumenical logic. We conclude by presenting an extension proposal to the first-order setting and a different approach to purity based on some ideas proposed by Julien Murzi. (shrink)

We present a natural deduction system for dual-intuitionistic logic. Its distinctive feature is that it is a single-premise multiple-conclusions system. Its relationships with the natural deduction systems for intuitionistic and classical logic are discussed.

Methods available for the axiomatization of arbitrary finite-valued logics can be applied to obtain sound and complete intelim rules for all truth-functional connectives of classical logic including the Sheffer stroke and Peirce’s arrow. The restriction to a single conclusion in standard systems of natural deduction requires the introduction of additional rules to make the resulting systems complete; these rules are nevertheless still simple and correspond straightforwardly to the classical absurdity rule. Omitting these rules results in systems for intuitionistic versions (...) of the connectives in question. (shrink)

Here is a deft and new introduction to Gentzen proof techniques in axiom systems and to the analysis of formal axiom systems; in short, axiomatics inside and out. Treating of deduction in propositional and predicate logic, metatheoretical problems about both set theory and its paradoxes, the book is flexibly structured for selective use as a text. Yet the discussion is unified and motivated by the concept of the axiomatic system--the history of its use and analysis, and its present practical (...) and theoretical status. Well-chosen illustrations convey an historical overview of Euclid, non-Euclidean geometers, Peano, Boole, Hilbert and Gödel.--P. D. J. (shrink)

This is a companion paper to Braüner where a natural deduction system for propositional hybrid logic is given. In the present paper we generalize the system to the first-order case. Our natural deduction system for first-order hybrid logic can be extended with additional inference rules corresponding to conditions on the accessibility relations and the quantifier domains expressed by so-called geometric theories. We prove soundness and completeness and we prove a normalisation theorem. Moreover, we give an (...) axiom system first-order hybrid logic. (shrink)

A first-order language with a defined identity predicate is proposed whose apparatus for atomic predication is sensitive to grammatical categories of natural language. Subatomic natural deduction systems are defined for this naturalistic first-order language. These systems contain subatomic systems which govern the inferential relations which obtain between naturalistic atomic sentences and between their possibly composite components. As a main result it is shown that normal derivations in the defined systems enjoy the subexpression property which subsumes the subformula property (...) with respect to atomic and identity formulae as a special case. The systems admit a proof-theoretic semantics which does not only apply to logically compound but also to atomic and identity formulae—as well as to their components. The potential of the defined systems for a meticulous first-order analysis of natural inferences whose validity crucially depends on expressions of some of the aforementioned categories is demonstrated. (shrink)

We present a sound and complete Fitch-style natural deduction system for an S5 modal logic containing an actuality operator, a diagonal necessity operator, and a diagonal possibility operator. The logic is two-dimensional, where we evaluate sentences with respect to both an actual world (first dimension) and a world of evaluation (second dimension). The diagonal necessity operator behaves as a quantifier over every point on the diagonal between actual worlds and worlds of evaluation, while the diagonal possibility quantifies over (...) some point on the diagonal. Thus, they are just like the epistemic operators for apriority and its dual. We take this extension of Fitch’s familiar derivation system to be a very natural one, since the new rules and labeled lines hereby introduced preserve the structure of Fitch’s own rules for the modal case. (shrink)

Harold Hodes in [1] introduces an extension of first-order modal logic featuring a backtracking operator, and provides a possible worlds semantics, according to which the operator is a kind of device for ‘world travel’; he does not provide a proof theory. In this paper, I provide a natural deduction system for modal logic featuring this operator, and argue that the system can be motivated in terms of a reading of the backtracking operator whereby it serves to indicate (...) modal scope. I prove soundness and completeness theorems with respect to Hodes’ semantics, as well as semantics with fewer restrictions on the accessibility relation. (shrink)

Extant semantic theories for languages containing vague expressions violate intuition by delivering the same verdict on two principles of classical propositional logic: the law of noncontradiction and the law of excluded middle. Supervaluational treatments render both valid; many-Valued treatments, Neither. The core of this paper presents a natural deduction system, Sound and complete with respect to a 'mixed' semantics which validates the law of noncontradiction but not the law of excluded middle.

We can formalize judgments as logical formulas. Judgment aggregation deals with judgments of several agents, which need to be aggregated to a collective judgment. There are several logical formalizations of judgment aggregation. This paper focuses on a modal formalization which nicely expresses classical properties of judgment aggregation rules and famous results of social choice theory, like Arrow’s impossibility theorem. A natural deduction system for modal logic of judgment aggregation is presented in this paper. The system is sound (...) and complete. As an example of derivation, a formal proof of Arrow’s impossibility theorem is given. (shrink)

In this paper, we present sound and complete natural deduction systems for Fitting’s four-valued generalizations of Kleene’s three-valued regular logics.