The Naturality of Natural Deduction (II): On Atomic Polymorphism and Generalized Propositional Connectives

Studia Logica - In a previous paper (of which this is a prosecution) we investigated the extraction of proof-theoretic properties of natural deduction derivations from their impredicative...     

Constructing Natural Extensions of Propositional Logics

The proofs of some results of abstract algebraic logic, in particular of the transfer principle of Czelakowski, assume the existence of so-called natural extensions of a logic by a set of new variables. Various constructions of natural extensions, claimed to be equivalent, may be found in the literature. In particular, these include a syntactic construction due to Shoesmith and Smiley and a related construction due to ?o? and Suszko. However, it was recently observed by Cintula and Noguera that both of these constructions fail in the sense that they do not necessarily yield a logic. Here we show that whenever the ?o?–Suszko construction yields a logic, so does the Shoesmith–Smiley construction, but not vice versa. We also describe the smallest and the largest conservative extension of a logic by a set of new variables and show that contrary to some previous claims in the literature, a logic of cardinality \({\kappa}\) may have more than one conservative extension of cardinality \({\kappa}\) by a set of new variables. In this connection we then correct a mistake in the formulation of a theorem of Dellunde and Jansana.     

Natural Deduction for Dual-intuitionistic Logic

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.     

Natural Deduction and Curry's Paradox

Curry's paradox, sometimes described as a general version of the better known Russell's paradox, has intrigued logicians for some time. This paper examines the paradox in a natural deduction setting and critically examines some proposed restrictions to the logic by Fitch and Prawitz. We then offer a tentative counterexample to a conjecture by Tennant proposing a criterion for what is to count as a genuine paradox.     

Natural Deduction for Non-Classical Logics

We present a framework for machine implementation of families of non-classical logics with Kripke-style semantics. We decompose a logic into two interacting parts, each a natural deduction system: a base logic of labelled formulae, and a theory of labels characterizing the properties of the Kripke models. By appropriate combinations we capture both partial and complete fragments of large families of non-classical logics such as modal, relevance, and intuitionistic logics. Our approach is modular and supports uniform proofs of soundness, completeness and proof normalization. We have implemented our work in the Isabelle Logical Framework.     

Substructural Logics in Natural Deduction

Extensions of Natural Deduction to Substructural Logics of IntuitionisticLogic are shown: Fragments of Intuitionistic Linear, Relevantand BCK Logic. Rules for implication, conjunction, disjunctionand falsum are defined, where conjunction and disjunction respectcontexts of assumptions. So, conjunction and disjunction areadditive in the terminology of linear logic. Explicit contractionand weakening rules are given. It is shown that conversionsand permutations can be adapted to all these rules, and thatweak normalisation and subformula property holds. The resultsgeneralise to quantification.     

A Double Deduction System for Quantum Logic Based On Natural Deduction

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

Semantic Values for Natural Deduction Derivations

Drawing upon Martin-Löf’s semantic framework for his constructive type theory, semantic values are assigned also to natural-deduction derivations, while observing the crucial distinction between (logical) consequence among propositions and inference among judgements. Derivations in Gentzen’s (1934–5) format with derivable formulae dependent upon open assumptions, stand, it is suggested, for proof-objects (of propositions), whereas derivations in Gentzen’s (1936) sequential format are (blue-prints for) proof-acts.     

Normal Natural Deduction Proofs (in classical logic)

Natural deduction (for short: nd-) calculi have not been used systematically as a basis for automated theorem proving in classical logic. To remove objective obstacles to their use we describe (1) a method that allows to give semantic proofs of normal form theorems for nd-calculi and (2) a framework that allows to search directly for normal nd-proofs. Thus, one can try to answer the question: How do we bridge the gap between claims and assumptions in heuristically motivated ways? This informal question motivates the formulation of intercalation calculi. Ic-calculi are the technical underpinnings for (1) and (2), and our paper focuses on their detailed presentation and meta-mathematical investigation in the case of classical predicate logic. As a central theme emerges the connection between restricted forms of nd-proofs and (strategies for) proof search: normal forms are not obtained by removing local "detours", but rather by constructing proofs that directly reflect proof-strategic considerations. That theme warrants further investigation.

     

Pandora: A Reasoning Toolbox using Natural Deduction Style

Pandora is a tool for supporting the learning of first ordernatural deduction. It includes a help window, an interactivecontext sensitive tutorial known as the "e-tutor" and facilitiesto save, reload and export to LATEX. Every attempt to applya natural deduction rule is met with either success or a helpfulerror message, providing the student with instant feedback.Detailed electronic logs of student usage are recorded for evaluationpurposes. This paper describes the basic functionality, thee-tutor, our experiences of using the tool in teaching and ourfuture plans.     

Establishing Connections between Aristotle's Natural Deduction and First-Order Logic

This article studies the mathematical properties of two systems that model Aristotle's original syllogistic and the relationship obtaining between them. These systems are Corcoran's natural deduction syllogistic and ?ukasiewicz's axiomatization of the syllogistic. We show that by translating the former into a first-order theory, which we call T _RD, we can establish a precise relationship between the two systems. We prove within the framework of first-order logic a number of logical properties about T _RD that bear upon the same properties of the natural deduction counterpart – that is, Corcoran's system. Moreover, the first-order logic framework that we work with allows us to understand how complicated the semantics of the syllogistic is in providing us with examples of bizarre, unexpected interpretations of the syllogistic rules. Finally, we provide a first attempt at finding the structure of that semantics, reducing the search to the characterization of the class of models of T _RD.     

Natural Deduction Calculi and Sequent Calculi for Counterfactual Logics

In this paper we present labelled sequent calculi and labelled natural deduction calculi for the counterfactual logics CK + {ID, MP}. As for the sequent calculi we prove, in a semantic manner, that the cut-rule is admissible. As for the natural deduction calculi we prove, in a purely syntactic way, the normalization theorem. Finally, we demonstrate that both calculi are sound and complete with respect to Nute semantics [12] and that the natural deduction calculi can be effectively transformed into the sequent calculi.