Automated Theorem Proving

• book 3
• theorem proving 1
• logic 2

• 1 introduction
• 2 Natural Deduction
  • 2.1 Intuitionistic Natural Deduction
    • local soundness, completeness, reduction, expansion
    • quantification
    • rules of intuitionistic natural deduction
  • 2.2 Classical Logic
  • 2.3 Localizing Hypotheses
  • 2.4 Proof Terms
• 3 Sequent Calculus
  • 3.1 Intercalation

http://www.cs.cmu.edu/~fp/courses/atp/handouts.html http://www.cs.cmu.edu/~fp/courses/atp/handouts/atp.pdf

1 introduction

Automated deduction is concerned with the mechanization of formal reasoning, following the laws of logic. The roots of the field go back to the end of the last century when Frege developed his Begriffsschrift, the first comprehensive effort to develop a formal language suitable as a foundation for mathematics. Alas, Russell discovered a paradox which showed that Frege’s system was inconsistent, …

inconsistent

the truth of every proposition can be derived in it

Gentzen’s formulation of the predicate calculus in a system of natural deduction provides a major milestone for the field.

Gentzen’s seminal work also contains an early consistency proof for a formal logical system. As a technical device he introduced the sequent calculus and showed that it derives the same theorems as natural deduction. The famous Hauptsatz¹ establishes that all proofs in the sequent calculus can be found according to a simple strategy.

Among the backward searching procedures we find tableaux, connection methods, matrix methods and some forms of resolution. Among the forward searching procedures we find classical resolution and the inverse method.

The prominence of resolution among these methods is no accident, since Robinson’s seminal paper represented a major leap forward in the state of the art. It is natural to expect that a combination of forward and backward search could improve the efficiency of theorem proving system. Such a combination, however, has been elusive up to now, due to the largely incompatible basic choices in design and implementation of the two kinds of search procedures.

There is one further dimension to consider: which logic do we reason in? In philosophy, mathematics, and computer science many different logics are of interest. … (to mention just a few). While each logic requires its own considerations, many techniques are shared. This can be attributed in part to the common root of different logics in natural deduction and the sequent calculus. Another reason is that low-level efficiency improvements are relatively independent of higher-level techniques.

intuitionistic logic

intuitionistic propositions correspond to logical specifications and proofs to functional programs

more complex than classical logic and exhibits phenomena obscured by special properties which apply only to classical logic.

there are relatively straightforward interpretations of classical in intuitionistic logic which permits us to study logical interpretations in connection with theorem proving procedures

… to transfer methods to different logics or applications …

2 Natural Deduction

“First I wanted to construct a formalism which comes as close as possible to actual reasoning. Thus arose a “calculus of natural deduction”. — Gerhard Gentzen Untersuchungen über das logische Schließen

(Our fundamental notion) a judgment based on evidence

For example, we might make the judgment “It is raining” based on visual evidence. Or we might make the judgment “‘A implies A’ is true for any proposition A” based on a derivation.

The use of the notion of a judgment as conceptual prior to the notion of proposition has been advocated by Martin-L̈of.

• A hypothetical judgment has the form “J2 under hypothesis J1”
  • Formal evidence for a hypothetical judgment is a hypothetical derivation where we can freely use the hypothesis J1 in the derivation of J2.
• A parametric judgment has the form “J for any a” where a is a parameter which may occur in J.
  • We make this judgment if we are prepared to make the judgment [O/a]J for arbitrary objects O of the right category. Here [O/a]J is our notation for substituting the object O for parameter a in the judgment J.
  • Formal evidence for a parametric judgment J is a parametric derivation with free occurrences of the parameter a.
• Formal evidence for a judgment in form of a derivation

  • the alternative (brief) notation D :: J. A hypothetical judgment is written as, (u is a label which identifies the hypothesis J1)

    -- u
    J1 
    ...
    J2
    

    While these are interesting and in many ways useful approaches to logic specification, neither of them comes particularly close to capturing the practice of mathematical reasoning. This was Gentzen’s point of departure for the design of a system of natural deduction…. the great advantage that one can define all logical connectives without reference to any other connective. This principle of modularity extends to the meta-theoretic study of natural deduction and simplifies considering fragments and extension of logics. … There is another advantage to natural deduction, namely that its proofs are isomorphic to the terms in a λ-calculus via the so-called Curry-Howard isomorphism, which establishes many connections to functional programming.

sequent calculus as a calculus of proof search for natural deduction and explicitly relate the two forms of presentation.

sequent calculus

also introduced by Gentzen in his seminal paper [Gen35]

split the single judgment of truth into two: “A is an assumption” and “A is true”.

need an explicit rule to state that “A is an assumption” is sufficient evidence for “A is a true”. The reverse, if “A is true” then “A may be used as an assumption” is the Cut rule which he proved to be redundant in his Hauptsatz.

2.1 Intuitionistic Natural Deduction

• the (first-order) terms built up from variables x, y, function symbols f, g, and parameters a, b

  t ::= x | a | f(t1,...,tn)
  

  • A constant c is simply a function symbol with arity 0 c().

• the propositions built up from predicate symbols P, Q

  A ::= P(t1,...,tn)| A1∧A2 | A1⊃A2 | A1∨A2 | ¬A | ⊥ | ⊤ | ∀x.A | ∃x.A
  

  • A propositional constant P is simply a predicate symbol with no arguments P()
  • the variable x is bound in propositions of the form ∀x.A and ∃x.A
  • use parentheses to disambiguate and assume that ∧ and ∨ bind more tightly than ⊃
  • [t/x]A for the result of substituting the term t for the variable x in A

• The main judgment of natural deduction — hypothetical judgment

    C true, from hypotheses A1 true, . . . , An true.
  

• certain structural properties of derivations are tacitly assumed, independently of any logical inferences.

  • Hypothesis If we have a hypothesis A true than we can conclude A true.
  • Weakening Hypotheses need not be used.
  • Duplication Hypotheses can be used more than once.
  • Exchange The order in which hypotheses are introduced is irrelevant.

local soundness, completeness, reduction, expansion

local soundness property

if we introduce a connective and then immediately eliminate it, we should be able to erase this detour and find a more direct derivation of the conclusion without using the connective

local completeness property

eliminate a connective in a way which retains sufficient information to reconstitute it by an introduction rule

… local reduction and expansion judgments …

… orthogonality of the connectives

One of the important principles of natural deduction is that each connective should be defined only in terms of inference rules without reference to other logical connectives or quantifiers.

… reduction between derivations …

Truth

There is only an introduction rule for ⊤

Since we put no information into the proof of ⊤, we know nothing new if we have an assumption ⊤ and therefore we have no elimination rule and no local reduction.

⊤ as a 0-ary conjunction

Falsehood

Since we should not be able to derive falsehood, there is no introduction rule for ⊥.

⊥ as a 0-ary disjunction

quantification

Universal Quantification

in a general treatment of predicate logic we would like to prove statements which are true for all domains of quantification. Thus we can only say that ∀x.A should be provable if [a/x]A is provable for a new parameter a (free variable) about which we can make no assumption

Existential Quantification.

conclude that ∃x. A is true when there is a term t such that [t/x]A is true

rules of intuitionistic natural deduction

2.2 Classical Logic

There are three commonly used ways one can construct a system of classical natural deduction by adding one additional rule of inference. ⊥C is called Proof by Contradiction or Rule of Indirect Proof, ¬¬C is the Double Negation Rule, and XM is referred to as Excluded Middle.

2.3 Localizing Hypotheses

• In natural deduction, correct use of hypotheses and parameters is a global property of a derivation.

• a formulation of natural deduction for intuitionistic logic with localized hypotheses, but not parameters. For this need a notation for hypotheses which we call a context.

  • “·” represents the empty context, and Γ,u:A adds hypothesis A true labeled u to Γ.

      Contexts Γ ::= · | Γ, u:A
      Γ,· = Γ
      Γ, (Γ′, u:A) = (Γ, Γ′), u:A
    

Theorem 2.1 (Structural Properties of Hypotheses)

The following properties hold for intuitionistic natural deduction.

• (Exchange) If Γ1, u1:A, Γ2, u2:B, Γ3 ⊢ C then Γ1, u2:B, Γ2, u1:A, Γ3 ⊢ C.
• (Weakening) If Γ1, Γ2 ⊢ C then Γ1, u:A, Γ2 ⊢ C.
• (Contraction) If Γ1, u1:A, Γ2, u2:A, Γ3 ⊢ C then Γ1, u:A, Γ2, Γ3 ⊢ C.
• (Substitution) If Γ1,u:A,Γ2 ⊢ C and Γ1 ⊢ A then Γ1,Γ2 ⊢ C.

use the principle of structural induction over derivations: prove a property for all derivations by showing that, whenever it holds for the premisses of an inference, it holds for the conclusion. show the property outright when the rule under consideration has no premises (such rules are the base cases for the induction).

It is also possible to localize the derivations themselves, using proof terms. These proof terms form a λ-calculus closely related to functional programming. When parameters, hypotheses, and proof terms are all localized our main judgment becomes decidable. In the terminology of Martin-L̈of [ML94], the main judgment is then analytic rather than synthetic. We no longer need to go outside the judgment itself in order to collect evidence for it: An analytic judgment encapsulates its own evidence.

2.4 Proof Terms

⊢ A

The basic judgment of natural deduction: the derivability of a formula A.

• strong correspondence between (intuitionistic) derivations and λ-terms
• formulas A act as types classifying λ-terms

isomorphism (in the propositional case)

formulas are isomorphic to types and derivations are isomorphic to simply-typed λ-terms. called the propositions-as-types and proofs-as-programs paradigms.

Γ ⊢ M : A

express the judgment M is a proof term for A under hypotheses Γ

⟨M,N⟩ can be seen as a representation of the proof of A∧B by ∧-introduction

Conjunction

proof term for a conjunction is simply the pair of proofs of the premisses

Implication

The proof of an implication A ⊃ B will be represented by a function which maps proofs of A to proofs of B. The introduction rule explicitly forms such a function by λ-abstraction and the elimination rule applies the function to an argument.

Disjunction

the proof term for disjunction introduction is the proof of the premiss together with an indication whether it was inferred by introduction on the left or on the right.

The elimination rule corresponds to a case construction.

We can now see that the formulas act as types for proof terms. Shifting to the usual presentation of the typed λ-calculus we use τ and σ as symbols for types, and τ × σ for the product type, τ → σ for the function type, τ + σ for the disjoint sum type, 1 for the unit type and 0 for the empty or void type. Base types b remain unspecified, just as the basic propositions of the propositional calculus remain unspecified.

          Types τ::= b | τ1×τ2 | τ1→τ2 | τ1+τ2 | 1 | 0
 Propositions A::= p | A1∧A2 | A1⊃A2 | A1∨A2 | ⊤ | ⊥

now summarize and restate the rules above, using the notation of types instead of propositions (omitting only the case for negation). Γ now declare variables with their types:

3 Sequent Calculus

sequent calculus as a formal system for proof search in natural deduction

3.1 Intercalation

A simple strategy in the search for a natural deduction is to use introduction rules reasoning bottom-up (from the proposed theorem towards the hypotheses) and the elimination rules top-down (from the assumptions towards the proposed theorem). When they meet in the middle we have found a normal deduction.