A graphic means of representing deductive proofs in a sentential system of symbolic logic is presented. Proof construction is characterized as a domain of the cognitive theory of problem solving, and three different interface designs for supporting the working backwards method of proof construction are demonstrated. Following a description of the rule set and the working backwards method, an analysis is given of student performance data that has guided interface development during the past two years. One (...) interface design is shown to be superior to the others in respect to working backwards. Finally, some general conclusions are drawn concerning the relevance of instructional programs for empirically documenting student difficulties and for improving interface designs. (shrink)

Charles Peirce’s alpha system \ is reformulated into a deep inference system where the rules are given in terms of deep graphical structures and each rule has its symmetrical rule in the system. The proof analysis of \ is given in terms of two embedding theorems: the system \ and Brünnler’s deep inference system for classical propositional logic can be embedded into each other; and the system \ and Gentzen sequent calculus \ can (...) be embedded into each other. (shrink)

This paper presents a proof of concept for a graphical models approach to assessing the moral coherence and moral robustness of systems of social interactions. “Moral coherence” refers to the degree to which the rights and duties of agents within a system are effectively respected when agents in the system comply with the rights and duties that are recognized as in force for the relevant context of interaction. “Moral robustness” refers to the degree to which a (...) class='Hi'>system of social interaction is configured to ensure that the interests of agents are effectively respected even in the face of noncompliance. Using the case of conscientious objection of pharmacists to filling prescriptions for emergency contraception as an example, we illustrate how a graphical models approach can help stakeholders identify structural weaknesses in systems of social interaction and evaluate the relative merits of alternate organizational structures. By illustrating the merits of a graphical models approach we hope to spur further developments in this area. (shrink)

The issue of what constitutes a valid logical inference is a difficult question. At a minimum, we believe a permissible step in a proof must provide the reader with rational grounds to believe that the new step is a logically necessary consequence of previous assertions. However, this begs the question of what constitutes these rational grounds. Formalist accounts typically describe valid rules of inferences as those that can be found by applying one of the explicit rules of inference in (...) the formal system in which the proof is couched. However, philosophers of mathematics find such a description unhelpful because many inferences in the proofs that mathematicians actually produce cannot be expressed in a formal language, at least not without seriously distorting the semantic content of the inference (e.g., Larvor, 2012). In this chapter, we investigate mathematicians’ perceptions of a particular kind of inference in a particular setting. Specifically, we shed light on what types of graphical inferences mathematicians find permissible in a real analysis proof. Following Larvor (in press), we examine mathematicians’ reactions to metrical graphical inferences (i.e., inferences whose validity depends on the accuracy of the graph that was drawn and whose validity can be changed by minor deformations) and nonmetrical graphical inferences (i.e., inferences whose validity does not depend on a the accuracy of the graph and whose validity is not vulnerable to local deformations). The goal of this chapter is threefold. First, we demonstrate that most mathematicians reject metrical graphical inferences as impermissible in a real analysis proof. Second, we show that many mathematicians regard nonmetrical graphical inferences as permissible in a real analysis proofs. Third, we illustrate how mathematicians collectively disagree on the permissibility of nonmetrical inferences. (shrink)

ABSTRACT Real-time graphical interval logic is a modal logic for reasoning about time in which the basic modality is the interval. The logic differs from other logics in that it has a natural intuitive graphical representation that resembles the timing diagrams drawn by system designers. We have developed an automted deduction system for the logic, which includes a theorem prover and a user interface. The theorem prover checks the validity of proofs in the logic and produces counterexamples to (...) invalid proofs. The user interface includes a graphical editor that enables the user to create graphical formulas on a workstation display, and a database and proof manager that tracks proof dependencies and allows graphical formulas to be stored and retrieved. In this paper we describe the logic, the automated deduction system, and an application to robotics. (shrink)

PARC is an "appended numeral" system of natural deduction that I learned as an undergraduate and have taught for many years. Despite its considerable pedagogical strengths, PARC appears to have never been published. The system features explicit "tracking" of premises and assumptions throughout a derivation, the collapsing of indirect proofs into conditional proofs, and a very simple set of quantificational rules without the long list of exceptions that bedevil students learning existential instantiation and universal generalization. The system (...) can be used with any Copi-style set of inference rules, so it is quite adaptable to many mainstream symbolic logic textbooks. Consequently, PARC may be especially attractive to logic teachers who find Jaskowski/Gentzen-style introduction/elimination rules to be far less "natural" than Copi-style rules. The PARC system is also keyboard-friendly in comparison to the widely adopted Jaskowski-style graphical subproof system of natural deduction, viz., Fitch diagrams and Copi "bent arrow" diagrams. (shrink)

Proof-theory has traditionally been developed based on linguistic (symbolic) representations of logical proofs. Recently, however, logical reasoning based on diagrammatic or graphical representations has been investigated by logicians. Euler diagrams were introduced in the eighteenth century. But it is quite recent (more precisely, in the 1990s) that logicians started to study them from a formal logical viewpoint. We propose a novel approach to the formalization of Euler diagrammatic reasoning, in which diagrams are defined not in terms of regions as (...) in the standard approach, but in terms of topological relations between diagrammatic objects. We formalize the unification rule, which plays a central role in Euler diagrammatic reasoning, in a style of natural deduction. We prove the soundness and completeness theorems with respect to a formal set-theoretical semantics. We also investigate structure of diagrammatic proofs and prove a normal form theorem. (shrink)

The geometric system of deduction called N-Graphs was introduced by de Oliveira in 2001. The proofs in this system are represented by means of digraphs and, while its derivations are mostly based on Gentzen's sequent calculus, the system gets its inspiration from geometrically based systems, such as the Kneales' tables of development, Statman's proofs-as-graphs, Buss' logical flow graphs, and Girard's proof-nets. Given that all these geometric systems appeal to the classical symmetry between premises and conclusions, providing (...) an intuitionistic version of any of these is an interesting exercise in extending the range of applicability of the geometric system in question. In this article we produce an intuitionistic version of N-Graphs, based on Maehara's LJ' system, as described by Takeuti. Recall that LJ' has multiple conclusions in all but the essential intuitionistic rules, e.g., implication right and negation right. We show soundness and completeness of our intuitionistic N-Graphs with respect to LJ'. We also discuss how we expect to extend this work to a version of N-Graphs corresponding to the intuitionistic logic system FIL (Full Intuitionistic Logic) of de Paiva and Pereira and sketch future developments. (shrink)

The logic $G3^{<}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$ was introduced in Robles and Mendéz as a paraconsistent logic which is based on Gödel’s 3-valued matrix, except that Kleene–Łukasiewicz’s negation is added to the language and is used as the main negation connective. We show that $G3^{<}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$ is exactly the intersection of $G3^{\{1\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$ and $G3^{\{1,0.5\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$, the two truth-preserving 3-valued logics which are based on the same truth tables. We then construct a Hilbert-type system which has for $\to $ as its sole rule of inference, and (...) is strongly sound and complete for $G3^{<}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$. Then we show how, by adding one axiom or one new rule of inference, we get strongly sound and complete systems for $G3^{\{1\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$ and $G3^{\{1,0.5\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$. Finally, we provide quasi-canonical Gentzen-type systems which are sound and complete for those logics and show that they are all analytic, by proving the cut-elimination theorem for them. (shrink)

This paper studies proof systems for the logics of super-strict implication ST2–ST5, which correspond to C.I. Lewis’ systems S2–S5 freed of paradoxes of strict implication. First, Hilbert-style axiomatic systems are introduced and shown to be sound and complete by simulating STn in Sn and backsimulating Sn in STn, respectively(for n=2,...,5). Next, G3-style labelled sequent calculi are investigated. It is shown that these calculi have the good structural properties that are distinctive of G3-style calculi, that they are sound and complete, (...) and it is shown that the proof search for G3. ST2 is terminating and therefore the logic is decidable. (shrink)

The main goal of the paper is to suggest some analytic proof systems for LC and its finite-valued counterparts which are suitable for proof-search. This goal is achieved through following the general Rasiowa-Sikorski methodology for constructing analytic proof systems for semantically-defined logics. All the systems presented here are terminating, contraction-free, and based on invertible rules, which have a local character and at most two premises.

We present sound and complete sequent calculi for the modal mu-calculus with converse modalities, aka two-way modal mu-calculus. Notably, we introduce a cyclic proof system wherein proofs can be represented as finite trees with back-edges, i.e., finite graphs. The sequent calculi incorporate ordinal annotations and structural rules for managing them. Soundness is proved with relative ease as is the case for the modal mu-calculus with explicit ordinals. The main ingredients in the proof of completeness are isolating a (...) class of non-wellfounded proofs with sequents of bounded size, called slim proofs, and a counter-model construction that shows slimness suffices to capture all validities. Slim proofs are further transformed into cyclic proofs by means of re-assigning ordinal annotations. (shrink)

Contact relations have been studied in the context of qualitative geometry and physics since the early 1920s, and have recently received attention in qualitative spatial reasoning. In this paper, we present a sound and complete proof system in the style of Rasiowa and Sikorski (1963) for relation algebras generated by a contact relation.

This paper studies proof systems for the logics of super-strict implication \(\textsf{ST2}\) – \(\textsf{ST5}\), which correspond to C.I. Lewis’ systems \(\textsf{S2}\) – \(\textsf{S5}\) freed of paradoxes of strict implication. First, Hilbert-style axiomatic systems are introduced and shown to be sound and complete by simulating \(\textsf{STn}\) in \(\textsf{Sn}\) and backsimulating \(\textsf{Sn}\) in \(\textsf{STn}\), respectively (for \({\textsf{n}} =2, \ldots, 5\) ). Next, \(\textsf{G3}\) -style labelled sequent calculi are investigated. It is shown that these calculi have the good structural properties that are (...) distinctive of \(\textsf{G3}\) -style calculi, that they are sound and complete, and it is shown that the proof search for \(\mathsf {G3.ST2}\) is terminating and therefore the logic is decidable. (shrink)

We consider the problem about the length of proofs of the sentences $\operatorname{Con}_S(\underline{n})$ saying that there is no proof of contradiction in S whose length is ≤ n. We show the relation of this problem to some problems about propositional proof systems.

We present novel proof systems for various FDE-based modal logics. Among the systems considered are a number of Belnapian modal logics introduced in Odintsov & Wansing and Odintsov & Wansing, as well as the modal logic KN4 with strong implication introduced in Goble. In particular, we provide a Hilbert-style axiom system for the logic $BK^{\square - } $ and characterize the logic BK as an axiomatic extension of the system $BK^{FS} $. For KN4 we provide both an (...) FDE-style axiom system and a decidable sequent calculus for which a contraction elimination and a cut elimination result are shown. (shrink)

A method is presented for constructing natural deduction-style systems for propositional relevant logics. The method consists in first translating formulas of relevant logics into ternary relations, and then defining deduction rules for a corresponding logic of ternary relations. Proof systems of that form are given for various relevant logics. A class of algebras of ternary relations is introduced that provides a relation-algebraic semantics for relevant logics.

In the paper we examine the use of non-classical truth values for dealing with computation errors in program specification and validation. In that context, 3-valued McCarthy logic is suitable for handling lazy sequential computation, while 3-valued Kleene logic can be used for reasoning about parallel computation. If we want to be able to deal with both strategies without distinguishing between them, we combine Kleene and McCarthy logics into a logic based on a non-deterministic, 3-valued matrix, incorporating both options as a (...) non-deterministic choice. If the two strategies are to be distinguished, Kleene and McCarthy logics are combined into a logic based on a 4-valued deterministic matrix featuring two kinds of computation errors which correspond to the two computation strategies described above. For the resulting logics, we provide sound and complete calculi of ordinary, two-valued sequents. (shrink)

The paper describes and proves completeness theorems for a series of proof systems formalizing common sense reasoning about uncertain knowledge in the case where this consists of sets of linear constraints on a probability function.

Planning with incomplete knowledge becomes a very active research area since late 1990s. Many logical formalisms introduce sensing actions and conditional plans to address the problem. The action language $\mathcal{A}_{K}$ invented by Son and Baral is a well-known framework for this purpose. In this paper, we propose so-called cautious and weakly cautious semantics for $\mathcal{A}_{K}$ , in order to allow an agent to generate and execute reliable plans in safety-critical environments. Intuitively speaking, cautious and weakly cautious semantics enable the agent (...) to know exactly what happens after the execution of an action. Computational complexity analysis shows that cautious semantics reduces the reasoning complexity of $\mathcal{A}_{K}$ , it is also worth to point out that many useful domains could still be expressed with this setting. Another important contribution of our work is the development of Hoare style proof systems. These proof systems are served as inference mechanisms for the verification of conditional plans, and proved to be sound and complete. In addition, they could also be used for plan generation, in the sense that constructing a derivation is indeed a procedure to finding a plan. We point out that the proof systems posses a nice property for off-line planning, that is, the agent could generate and store short proofs in her spare time, and perform quick plan query by easily constructing a long proof from the stored shorter ones (under the assumption that sufficient proofs are stored). (shrink)

We present relational proof systems for the four groups of theories of spatial reasoning: contact relation algebras, Boolean algebras with a contact relation, lattice-based spatial theories, spatial theories based on a proximity relation.

We present a series of proof systems for exact entailment (i.e. relevant truthmaker preservation from premises to conclusion) and prove soundness and completeness. Using the proof systems, we observe that exact entailment is not only hyperintensional in the sense of Cresswell but also in the sense recently proposed by Odintsov and Wansing.

A fast consistency prover is a consistent polytime axiomatized theory that has short proofs of the finite consistency statements of any other polytime axiomatized theory. Krajíček and Pudlák have proved that the existence of an optimal propositional proof system is equivalent to the existence of a fast consistency prover. It is an easy observation that NP = coNP implies the existence of a fast consistency prover. The reverse implication is an open question. In this paper we define the (...) notion of an unlikely fast consistency prover and prove that its existence is equivalent to NP = coNP. Next it is proved that fast consistency provers do not exist if one considers RE axiomatized theories rather than theories with an axiom set that is recognizable in polynomial time. (shrink)

The paper describes and proves completeness theorems for a series of proof systems formalizing common sense reasoning about uncertain knowledge in the case where this consists of sets of linear constraints on a probability function.

In this paper we provide a proof theoretical investigation of logical argumentation, where arguments are represented by sequents, conflicts between arguments are represented by sequent elimination rules, and deductions are made by dynamic proof systems extending standard sequent calculi. The idea is to imitate argumentative movements in which certain claims are introduced or withdrawn in the presence of counter-claims. This is done by a dynamic evaluation of sequences of sequents, in which the latter are considered ‘derived’ or ‘not (...) derived’ according to the content of the sequence. We show that decisive conclusions of such a process correspond to well-accepted consequences of the underlying argumentation framework. The outcome is therefore a general and modular proof-theoretical approach for paraconsistent and non-monotonic reasoning with argumentation systems. (shrink)

A Frege proof systemFis any standard system of prepositional calculus, e.g., a Hilbert style system based on finitely many axiom schemes and inference rules. An Extended Frege systemEFis obtained fromFas follows. AnEF-sequence is a sequence of formulas ψ1, …, ψκsuch that eachψiis either an axiom ofF, inferred from previous ψuand ψv by modus ponens or of the formq↔ φ, whereqis an atom occurring neither in φ nor in any of ψ1,…,ψi−1. Suchq↔ φ, is called an extension axiom (...) andqa new extension atom. AnEF-proof is anyEF-sequence whose last formula does not contain any extension atom. In [12], S. A. Cook and R. Reckhow proved that the pigeonhole principlePHPhas a simple polynomial sizeEF-proof and conjectured thatPHPdoes not admit polynomial sizeF-proof. In [5], S. R. Buss refuted this conjecture by furnishing polynomial sizeF-proof forPHP. Since then the important separation problem of polynomial sizeFand polynomial sizeEFhas not shown any progress.In [11], S. A. Cook introduced the systemPV, a free variable equational logic whose provable functional equalities are ‘polynomial time verifiable’ and showed that the metamathematics ofFandEFcan be developed inPVand the soundness ofEFproved inPV. In [3], S. R. Buss introduced the first order systemand showed thatis essentially a conservative extension ofPV. There he also introduced a second order system. (shrink)

A Frege proof systemFis any standard system of prepositional calculus, e.g., a Hilbert style system based on finitely many axiom schemes and inference rules. An Extended Frege systemEFis obtained fromFas follows. AnEF-sequence is a sequence of formulas ψ1, …, ψκsuch that eachψiis either an axiom ofF, inferred from previous ψuand ψv by modus ponens or of the formq↔ φ, whereqis an atom occurring neither in φ nor in any of ψ1,…,ψi−1. Suchq↔ φ, is called an extension axiom (...) andqa new extension atom. AnEF-proof is anyEF-sequence whose last formula does not contain any extension atom. In [12], S. A. Cook and R. Reckhow proved that the pigeonhole principlePHPhas a simple polynomial sizeEF-proof and conjectured thatPHPdoes not admit polynomial sizeF-proof. In [5], S. R. Buss refuted this conjecture by furnishing polynomial sizeF-proof forPHP. Since then the important separation problem of polynomial sizeFand polynomial sizeEFhas not shown any progress.In [11], S. A. Cook introduced the systemPV, a free variable equational logic whose provable functional equalities are ‘polynomial time verifiable’ and showed that the metamathematics ofFandEFcan be developed inPVand the soundness ofEFproved inPV. In [3], S. R. Buss introduced the first order systemand showed thatis essentially a conservative extension ofPV. There he also introduced a second order system. (shrink)

New propositional and first-order paraconsistent logics (called L ω and FL ω , respectively) are introduced as Gentzen-type sequent calculi with classical and paraconsistent negations. The embedding theorems of L ω and FL ω into propositional (first-order, respectively) classical logic are shown, and the completeness theorems with respect to simple semantics for L ω and FL ω are proved. The cut-elimination theorems for L ω and FL ω are shown using both syntactical ways via the embedding theorems and semantical ways (...) via the completeness theorems. (shrink)

In the period 1893–1897 Charles Dodgson, writing as Lewis Carroll, published two books and two articles on logic topics. Manuscript material first published in 1977 together with letters and diary entries provide evidence that he was working toward a visual proof system for complex syllogistic propositional logic based on a mechanical tree method that he devised.

Gentzen’s sequent calculi LK and LJ are landmark proof systems. They identify the structural rules of weakening and contraction as notable inference rules, and they allow for an elegant statement and proof of both cut elimination and consistency for classical and intuitionistic logics. Among the undesirable features of those sequent calculi is that their inferences rules are low-level and frequently permute over each other. As a result, large-scale structures within sequent calculus proofs are hard to identify. In this (...) paper, we present a different approach to designing a sequent calculus for classical logic. Starting with Gentzen’s LK proof system, we examine the proof search meaning of his inference rules and classify those rules as involving either don’t care nondeterminism or don’t know nondeterminism. Based on that classification, we design the focused proof system LKF in which inference rules belong to one of two phases of proof construction depending on which flavor of nondeterminism they involve. We then prove that the cut rule and the general form of the initial rule are admissible in LKF. Finally, by showing that the inference rules for LK are all admissible in LKF, we can give a relative completeness proof for LKF provability with respect to LK provability. We shall also apply these properties of the LKF proof system to establish other meta-theoretic properties of classical logic, including Herbrand’s theorem. (shrink)

The core language can be extended by defining additional logical constants. E.g., we can add ‘→’ (implication), ‘∨’ (disjunction), and ‘∀x’ (universal quantifiers). The choice of logical primitives is not as optional in DPL as it is in standard predicate logic.

We use the theory of domains with totality to construct some logics generalizing ω-logic and β-logic and we prove a completenes theorem for these logics. The key application is E-logic, the logic related to the functional 3E. We prove a compactness theorem for sets of sentences semicomputable in 3E.

An operation on inferential rules, called H-operation, is used to minimize the axiom basis for classical logic.

We present a complete and cut-free proof-system for a fragment of MTL, where modal operators are only labelled by bounded intervals with rational endpoints.

The non-Fregean logic SCI is obtained from the classical sentential calculus by adding a new identity connective = and axioms which say ?a = ß' means ?a is identical to ß'. We present complete and sound proof system for SCI in the style of Rasiowa-Sikorski. It provides a natural deduction-style method of reasoning for the non-Fregean sentential logic SCI.

An operation on inferential rules, called H-operation, is used to minimize the axiom basis for classical logic.

We introduce new proof systems G[β] and G ext[β], which are equivalent to the standard equational calculi of λβ- and λβη- conversion, and which may be qualified as ‘analytic’ because it is possible to establish, by purely proof-theoretical methods, that in both of them the transitivity rule admits effective elimination. This key feature, besides its intrinsic conceptual significance, turns out to provide a common logical background to new and comparatively simple demonstrations—rooted in nice proof-theoretical properties of transitivity-free (...) derivations—of a number of well-known and central results concerning β- and βη-reduction. The latter include the Church–Rosser theorem for both reductions, the Standardization theorem for β- reduction, as well as the Normalization (Leftmost reduction) theorem and the Postponement of η-reduction theorem for βη-reduction. (shrink)

Gentzen's systems of natural deduction and sequent calculus were byproducts in his program of proving the consistency of arithmetic and analysis. It is suggested that the central component in his results on logical calculi was the use of a tree form for derivations. It allows the composition of derivations and the permutation of the order of application of rules, with a full control over the structure of derivations as a result. Recently found documents shed new light on the discovery of (...) these calculi. In particular, Gentzen set up five different forms of natural calculi and gave a detailed proof of normalization for intuitionistic natural deduction. An early handwritten manuscript of his thesis shows that a direct translation from natural deduction to the axiomatic logic of Hilbert and Ackermann was, in addition to the influence of Paul Hertz, the second component in the discovery of sequent calculus. A system intermediate between the sequent calculus LI and axiomatic logic, denoted LIG in unpublished sources, is implicit in Gentzen's published thesis of 1934—35. The calculus has half rules, half “groundsequents,” and does not allow full cut elimination. Nevertheless, a translation from LI to LIG in the published thesis gives a subformula property for a complete class of derivations in LIG. After the thesis, Gentzen continued to work on variants of sequent calculi for ten more years, in the hope to find a consistency proof for arithmetic within an intuitionistic calculus. (shrink)

This paper is about non-labelled proof-systems for hybrid logic, that is, proofsystems where arbitrary formulas can occur, not just satisfaction statements. We give an overview of such proof-systems, focusing on analytic systems: Natural deduction systems, Gentzen sequent systems and tableau systems. We point out major results and we discuss a couple of striking facts, in particular that nonlabelled hybrid-logical natural deduction systems are analytic, but this is not proved in the usual way via step-by-step normalization of derivations.

We link two concepts from the literature, namely hard sequences for the satisfiability problem sat and so‐called pseudo proof systems proposed for study by Krajíček. Pseudo proof systems are elements of a particular nonstandard model constructed by forcing with random variables. We show that the existence of mad pseudo proof systems is equivalent to the existence of a randomized polynomial time procedure with a highly restrictive use of randomness which produces satisfiable formulas whose satisfying assignments are probably (...) hard to find. (shrink)

Rather than being random deviation, student errors can be a source of insight into the nature of student difficulties. This paper reports on (and offers pedagogical advice concerning) many common student errors in the construction of proofs, in the application of inference and replacement rules, and in the choice of proof strategies. In addition, a detailed description of the bottom-up strategy for “working backwards” is supplied, along with a discussion of the main difficulties students face when trying to solve (...) proofs in this fashion. Ultimately, it is argued that students can employ both top-down and bottom-up proofs strategies by making use of a graphic proof representation. (shrink)

The main goal of this paper is to provide an abstract framework for constructing proof systems for various many-valued logics. Using the framework it is possible to generate strongly complete proof systems with respect to any finitely valued deterministic and non-deterministic logic. I provide a couple of examples of proof systems for well-known many-valued logics and prove the completeness of proof systems generated by the framework.