A note on cut-elimination for classical propositional logic

First Order ◽

Sequent System ◽

Logical Rules ◽

Specific Formulation ◽

Automatic Theorem

AbstractIn Schwichtenberg (Studies in logic and the foundations of mathematics, vol 90, Elsevier, pp 867–895, 1977), Schwichtenberg fine-tuned Tait’s technique (Tait in The syntax and semantics of infinitary languages, Springer, pp 204–236, 1968) so as to provide a simplified version of Gentzen’s original cut-elimination procedure for first-order classical logic (Gallier in Logic for computer science: foundations of automatic theorem proving, Courier Dover Publications, London, 2015). In this note we show that, limited to the case of classical propositional logic, the Tait–Schwichtenberg algorithm allows for a further simplification. The procedure offered here is implemented on Kleene’s sequent system G4 (Kleene in Mathematical logic, Wiley, New York, 1967; Smullyan in First-order logic, Courier corporation, London, 1995). The specific formulation of the logical rules for G4 allows us to provide bounds on the height of cut-free proofs just in terms of the logical complexity of their end-sequent.

A proof-theoretic treatment of λ-reduction with cut-elimination: λ-calculus as a logic programming language

10.2178/jsl/1305810770 ◽

2011 ◽

Vol 76 (2) ◽

pp. 673-699 ◽

Cited By ~ 4

Author(s):

Michael Gabbay

Keyword(s):

Logic Programming ◽

Programming Language ◽

Functional Programming ◽

Order Logic ◽

First Order Logic ◽

Cut Elimination ◽

Logic Programming Language ◽

First Order ◽

Functional Programming Language ◽

Sequent System

AbstractWe build on an existing a term-sequent logic for the λ-calculus. We formulate a general sequent system that fully integrates αβη-reductions between untyped λ-terms into first order logic.We prove a cut-elimination result and then offer an application of cut-elimination by giving a notion of uniform proof for λ-terms. We suggest how this allows us to view the calculus of untyped αβ-reductions as a logic programming language (as well as a functional programming language, as it is traditionally seen).

What is an inference rule?

10.2307/2275447 ◽

1992 ◽

Vol 57 (3) ◽

pp. 1018-1045 ◽

Cited By ~ 18

Author(s):

Ronald Fagin ◽

Joseph Y. Halpern ◽

Moshe Y. Vardi

Keyword(s):

Propositional Logic ◽

General Framework ◽

Inference Rule ◽

Order Logic ◽

Semantic Framework ◽

First Order ◽

Extremal Points ◽

The Relationship ◽

General Semantic

AbstractWhat is an inference rule? This question does not have a unique answer. One usually finds two distinct standard answers in the literature; validity inference (σ ⊦vφ for every substitution τ, the validity of τ[σ] entails the validity of τ[φ]), and truth inference (σ⊦l φ if for every substitution τ, the truth of τ[σ] entails the truth of τ[φ]). In this paper we introduce a general semantic framework that allows us to investigate the notion of inference more carefully. Validity inference and truth inference are in some sense the extremal points in our framework. We investigate the relationship between various types of inference in our general framework, and consider the complexity of deciding if an inference rule is sound, in the context of a number of logics of interest: classical propositional logic, a nonstandard propositional logic, various propositional modal logics, and first-order logic.

SUBFORMULA AND SEPARATION PROPERTIES IN NATURAL DEDUCTION VIA SMALL KRIPKE MODELS

The Review of Symbolic Logic ◽

10.1017/s175502030999030x ◽

2010 ◽

Vol 3 (2) ◽

pp. 175-227 ◽

Cited By ~ 3

Author(s):

PETER MILNE

Keyword(s):

Propositional Logic ◽

Natural Deduction ◽

Order Logic ◽

First Order Logic ◽

Kripke Models ◽

Careful Attention ◽

First Order ◽

Invalid Inference ◽

Subformula Property

Various natural deduction formulations of classical, minimal, intuitionist, and intermediate propositional and first-order logics are presented and investigated with respect to satisfaction of the separation and subformula properties. The technique employed is, for the most part, semantic, based on general versions of the Lindenbaum and Lindenbaum–Henkin constructions. Careful attention is paid (i) to which properties of theories result in the presence of which rules of inference, and (ii) to restrictions on the sets of formulas to which the rules may be employed, restrictions determined by the formulas occurring as premises and conclusion of the invalid inference for which a counterexample is to be constructed. We obtain an elegant formulation of classical propositional logic with the subformula property and a singularly inelegant formulation of classical first-order logic with the subformula property, the latter, unfortunately, not a product of the strategy otherwise used throughout the article. Along the way, we arrive at an optimal strengthening of the subformula results for classical first-order logic obtained as consequences of normalization theorems by Dag Prawitz and Gunnar Stålmarck.

The metatheory of the classical propositional calculus is not axiomatizable

10.2307/2274233 ◽

1985 ◽

Vol 50 (2) ◽

pp. 451-457 ◽

Cited By ~ 7

Author(s):

Ian Mason

Keyword(s):

Propositional Logic ◽

Propositional Calculus ◽

Interpolation Property ◽

Interpolation Theorem ◽

Order Logic ◽

First Order Logic ◽

Elementary Property ◽

Open Problems ◽

First Order

In this paper we investigate the first order metatheory of the classical propositional logic. In the first section we prove that the first order metatheory of the classical propositional logic is undecidable. Thus as a mathematical object even the simplest of logics is, from a logical standpoint, quite complex. In fact it is of the same complexity as true first order number theory.This result answers negatively a question of J. F. A. K. van Benthem (see [van Benthem and Doets 1983]) as to whether the interpolation theorem in some sense completes the metatheory of the calculus. Let us begin by motivating the question that we answer. In [van Benthem and Doets 1983] it is claimed that a folklore prejudice has it that interpolation was the final elementary property of first order logic to be discovered. Even though other properties of the propositional calculus have been discovered since Craig's orginal paper [Craig 1957] (see for example [Reznikoff 1965]) there is a lot of evidence for the fundamental nature of the property. In abstract model theory for example one finds that very few logics have the interpolation property. There are two well-known open problems in this area. These are1. Is there a logic satisfying the full compactness theorem as well as the interpolation theorem that is not equivalent to first order logic even for finite models?2. Is there a logic stronger than L(Q), the logic with the quantifierthere exist uncountably many, that is countably compact and has the interpolation property?

Extensions in graph normal form

Logic Journal of IGPL ◽

10.1093/jigpal/jzaa054 ◽

2020 ◽

Author(s):

Michał Walicki

Keyword(s):

Normal Form ◽

Fixed Points ◽

Propositional Logic ◽

Order Logic ◽

First Order Logic ◽

First Order ◽

Special Cases

Abstract Graph normal form, introduced earlier for propositional logic, is shown to be a normal form also for first-order logic. It allows to view syntax of theories as digraphs, while their semantics as kernels of these digraphs. Graphs are particularly well suited for studying circularity, and we provide some general means for verifying that circular or apparently circular extensions are conservative. Traditional syntactic means of ensuring conservativity, like definitional extensions or positive occurrences guaranteeing exsitence of fixed points, emerge as special cases.

Making Automatic Theorem Provers more Versatile

10.29007/n6j7 ◽

2018 ◽

Author(s):

Simon Cruanes

Keyword(s):

Higher Order ◽

Order Logic ◽

Higher Order Logic ◽

Research Directions ◽

First Order ◽

Theorem Provers ◽

Smt Solvers ◽

Automatic Theorem Provers ◽

Automatic Theorem

We argue that automatic theorem provers should become more versatile and should be able to tackle problems expressed in richer input formats. Salient research directions include (i) developing tight combinations of SMT solvers and first-order provers; (ii) adding better handling of theories in first-order provers; (iii) adding support for inductive proving; (iv) adding support for user-defined theories and functions; and (v) bringing to the provers some basic abilities to deal with logics beyond first-order, such as higher-order logic.

Lifting propositional proof compression algorithms to first-order logic

Journal of Logic and Computation ◽

10.1093/logcom/exaa065 ◽

2020 ◽

Author(s):

Jan Gorzny ◽

Ezequiel Postan ◽

Bruno Woltzenlogel Paleo

Keyword(s):

Propositional Logic ◽

Empirical Evaluation ◽

Order Logic ◽

Automated Deduction ◽

First Order Logic ◽

Compression Algorithms ◽

International Conference ◽

First Order ◽

Theorem Provers ◽

Resolution Proofs

Abstract Proofs are a key feature of modern propositional and first-order theorem provers. Proofs generated by such tools serve as explanations for unsatisfiability of statements. However, these explanations are complicated by proofs which are not necessarily as concise as possible. There are a wide variety of compression techniques for propositional resolution proofs but fewer compression techniques for first-order resolution proofs generated by automated theorem provers. This paper describes an approach to compressing first-order logic proofs based on lifting proof compression ideas used in propositional logic to first-order logic. The first approach lifted from propositional logic delays resolution with unit clauses, which are clauses that have a single literal. The second approach is partial regularization, which removes an inference $\eta $ when it is redundant in the sense that its pivot literal already occurs as the pivot of another inference in every path from $\eta $ to the root of the proof. This paper describes the generalization of the algorithms LowerUnits and RecyclePivotsWithIntersection (Fontaine et al.. Compression of propositional resolution proofs via partial regularization. In Automated Deduction—CADE-23—23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31–August 5, 2011, p. 237--251. Springer, 2011) from propositional logic to first-order logic. The generalized algorithms compresses resolution proofs containing resolution and factoring inferences with unification. An empirical evaluation of these approaches is included.

Jon Barwise and John Etchemendy, The language of first-order logic, including the IBM-compatible Windows version of Tarski's world 4.0. Third edition of LVIII 362. CSLI lecture notes.no. 34. Center for the Study of Language and Information, Stanford 1992. also distributed by Cambridge University Press, New York, xiv + 319 pp. + disk.

10.2307/2586517 ◽

1999 ◽

Vol 64 (2) ◽

pp. 916-918

Author(s):

Don Fallis

Keyword(s):

New York ◽

Order Logic ◽

First Order Logic ◽

Cambridge University ◽

First Order

A First Course in Logic

10.1093/oso/9780198529804.001.0001 ◽

2004 ◽

Cited By ~ 3

Author(s):

Shawn Hedman

Keyword(s):

Propositional Logic ◽

Proof Theory ◽

Order Logic ◽

First Order Logic ◽

University Of Maryland ◽

First Order ◽

Science Philosophy ◽

The University ◽

Second Order Logic ◽

Theory And Model

The ability to reason and think in a logical manner forms the basis of learning for most mathematics, computer science, philosophy and logic students. Based on the author's teaching notes at the University of Maryland and aimed at a broad audience, this text covers the fundamental topics in classical logic in an extremely clear, thorough and accurate style that is accessible to all the above. Covering propositional logic, first-order logic, and second-order logic, as well as proof theory, computability theory, and model theory, the text also contains numerous carefully graded exercises and is ideal for a first or refresher course.

Proof theory

A First Course in Logic ◽

10.1093/oso/9780198529804.003.0007 ◽

2004 ◽

Author(s):

Shawn Hedman

Keyword(s):

Propositional Logic ◽

Completeness Theorem ◽

Formal Proof ◽

Order Logic ◽

Truth Table ◽

First Order Logic ◽

Formal Proofs ◽

Systematic Method ◽

First Order

As with any logic, the semantics of first-order logic yield rules for deducing the truth of one sentence from that of another. In this chapter, we develop both formal proofs and resolution for first-order logic. As in propositional logic, each of these provides a systematic method for proving that one sentence is a consequence of another. Recall the Consequence problem for propositional logic. Given formulas F and G, the problemis to decide whether or not G is a consequence of F. From Chapter 1, we have three approaches to this problem: • We could compute the truth table for the formula F → G. If the truth values are all 1s then we conclude that F → G is a tautology and G is a consequence of F. Otherwise, G is not a consequence of F. • Using Tables 1.5 and 1.6, we could try to formally derive G from {F}. By the Completeness Theorem for propositional logic, G is a consequence of F if and only if {F} ├ G. • We could use resolution. By Theorem1.76, G is a consequence of F if and only if ∅ ∈ Res(H) where H is a formula in CNF equivalent to (F ∧￢G). Using these methods not only can we determine whether one formula is a consequence of another, but also we can determine whether a given formula is a tautology or a contradiction. A formula F is a tautology if and only if F is a consequence of (A∨￢A) if and only if ￢F is a contradiction. In this chapter, we consider the analogous problems for first-order logic. Given formulas φ and ψ, how can we determine whether ψ is a consequence of φ? Equivalently, how can we determine whether a given formula is a tautology or a contradiction? We present three methods for answering these questions. • In Section 3.1, we define a notion of formal proof for first-order logic by extending Table 1.5. • In Section 3.3, we “reduce” formulas of first-order logic to sets of formulas of propositional logic where we use resolution as defined in Chapter 1.