Chapter 2:
Proof Rules for Predicate Logic

Proof and beauty
Mar 31st 2005
From The Economist print edition

Just what does it mean to prove something?

UOD erat demonstrandum. These three words of Latin, meaning, “which was to be shown”, traditionally mark the end of a mathematical proof. And, for centuries, a proof was exactly that: showing something by breaking it down into readily agreed-upon steps. Proving something was a matter of convincing one's peers that it has indeed been shown—no more, and no less. The rhetorical flourish of a Latin epigram also has served to indicate that the notion of proof is well understood, and commonly agreed. But that notion is now in flux. The use of computers to prove mathematical theorems is forcing mathematicians to re-examine the foundations of their discipline. 

Through much of the 20th century, questions of mathematical rigour were passed off to logicians and philosophers—working mathematicians have been, for the most part, content to work with an intuitive definition of proof. 

This notion works when each step of a proof is transparent, and can be examined by all. Proof is then just a process of reducing one big, non-obvious step, to a bunch of small, obvious ones. However, if a computer is used to make this reduction, then the number of small, obvious steps can be in the hundreds of thousands—impractical even for the most diligent mathematician to check by hand. Critics of computer-aided proof claim that this impracticability means that such proofs are inherently flawed. However, its defenders point out that some theorems that many mathematicians consider to have been proved in the classical manner also have proofs which are so long as to be uncheckable. 

The most famous case of this is something called the classification of finite simple groups. These are abstract objects with certain mathematical properties; the claim is that, over a 30-year span in a series of papers totalling some 15,000 pages, all possible such objects were enumerated. Though the mathematical consensus is that the classification (nicknamed the “enormous theorem”) is complete, there are sceptics who point out that the dispersed proof is essentially unverifiable. 

What, then, does constitute a proof in the modern age? Two recent examples of how computers have been used to prove important mathematical results illustrate how the field is changing.

A colouring problem

The first is the “four colour theorem”, which is perhaps the mathematical theorem most likely to bedevil a toddler. It states that any planar map (that is to say, a flat one) can be coloured with at most four colours in a way that no two regions with the same colour share a border. It was first proposed in 1852 but, despite efforts by a century's worth of mathematicians, went unproven until 1976, when Kenneth Appel and Wolfgang Haken, then of the University of Illinois, announced that they had proved the result. However, Dr Appel and Dr Haken used a computer to help them prove the result by examining about 10,000 cases. (Their proof also relied on a lot of old-fashioned gruntwork.)

A new proof, in a paper just written by Georges Gonthier, of Microsoft Research, in Cambridge, England, also uses a computer. Dr Gonthier used similar techniques to those of Dr Appel and Dr Haken in his proof. However, rather than have part of the proof done by hand, and part by computer, he has automated the entire proof, and done so in such a manner that it is a formal proof. 

Formal proof is a notion developed in the early part of the 20th century by logicians such as Bertrand Russell and Gottlob Frege, along with mathematicians such as David Hilbert (who can fairly be described as the father of modern mathematics) and Nicolas Bourbaki, the pseudonym of a group of French mathematicians who sought to place all of mathematics on a rigorous footing. This effort was subtle, but its upshot can be described simply. It is to replace, in proofs, standard mathematical reasoning which, in essence, relies on hand-waving arguments (it should be obvious to everyone that B follows from A) with formal logic. 

The benefit of formal logic is that it is pure syntax. At no point does proceeding from one step to the next require understanding, let alone mathematical intuition. It is merely a matter of applying an agreed-upon set of rules (for instance, that any thing is equal to itself, or that if something is true for all members of a set of objects, it is true for any one specific object) to a set of agreed-upon structures, such as sets of objects. Formal proofs, however, never gained a foothold in the mainstream mathematical community because they are tedious—they take many steps to prove something in cases in which a mathematician might just take one. To those who would use a computer, however, they have two virtues. 

The first is that computers, with their tolerance for tedium, are particularly suited to writing the steps of a formal proof down. The second is that, by writing those steps down in what is called a “proof witness” instead of just announcing that a program had arrived at a true result, outsiders might gain greater confidence in a result derived from a computer. 

As Dr Gonthier, and other supporters of the use of computers, point out, there is no reason to think that humans are less fallible than computers when doing long computations or proofs. Indeed, the opposite might be true.

The idea behind both proofs of the four colour theorem is to suppose that the theorem is violated—to assume, in other words, that there is some sort of map that requires five colours to fill in. The next step is to find the mathematically simplest versions of such maps. (What is meant by simplicity in this case is actually quite involved.) Dr Gonthier then showed that all these maps can, in fact, be re-coloured with only four colours, establishing the theorem by contradiction. The catch is that there are many such regions, which must be examined on a case-by-case basis; part of the mathematical difficulty lies in proving that the cases considered suffice to cover all possible maps, and part stems from proving that each individual case is indeed colourable with just four colours. 

Dr Gonthier says he is going to submit his paper to a scientific journal in the next few weeks. But he would do well not to get his hopes up about getting his paper published anytime soon. A 1998 paper which proved another long-standing conjecture using a computer, by Thomas Hales, of the University of Pittsburgh, has only recently been accepted by the Annals of Mathematics, perhaps the field's most prestigious journal, and is scheduled to be published later this year.

The music of the spheres

Dr Hales proved Kepler's conjecture, which is that the most efficient way to pack spheres in a box is the way grocers usually pack oranges—in a so-called “face-centred cubic lattice”—the arrangement whereby each layer of oranges is shifted so that an orange touches four oranges in the layer below. Kepler posited the conjecture in 1611, and it had long resisted efforts at proof. Indeed, Hilbert made it one of his list of the 23 most difficult and fundamental questions in mathematics, in 1900. Dr Hales proved the conjecture by using a trick different in nature to Dr Gonthier's.

Rather than argue by contradiction, he reduced what was a problem about an infinite number of things (the Kepler conjecture considers an infinite number of spheres in an infinitely large space) to a statement about a finite, but very large, number of mathematical objects. He then used the computer to prove bounds about these objects, some of which, he says, can be thought of as sculptures made of cables and struts. Loosely speaking, he reduced the Kepler conjecture to a problem of considering whether, given a set of cables, which have no minimum length, but can only be stretched to a certain extent, and struts, which have a limit on how much they can be compressed, one can build a sculpture of a certain type. Dr Hales used a computer, as there were roughly 100,000 such structures that had to be considered in order to prove the Kepler conjecture.

Although the Annals will publish Dr Hales's paper, Peter Sarnak, an editor of the Annals, whose own work does not involve the use of computers, says that the paper will be accompanied by an unusual disclaimer, stating that the computer programs accompanying the paper have not undergone peer review. There is a simple reason for that, Dr Sarnak says—it is impossible to find peers who are willing to review the computer code. However, there is a flip-side to the disclaimer as well—Dr Sarnak says that the editors of the Annals expect to receive, and publish, more papers of this type—for things, he believes, will change over the next 20-50 years. Dr Sarnak points out that maths may become “a bit like experimental physics” where certain results are taken on trust, and independent duplication of experiments replaces examination of a colleague's paper.

Some of the movement towards that direction may be forestalled by efforts of Dr Gonthier's type to use computers to provide formal proofs and proof witnesses. It is possible that mathematicians will trust computer-based results more if they are backed up by transparent logical steps, rather than the arcane workings of computer code, which could more easily contain bugs that go undetected. Indeed, it is for this exact reason that Dr Hales is currently leading a collaborative project to provide a formal proof of the Kepler conjecture. In perhaps a more prosaic example of mathematics embracing technology, he is co-ordinating that effort using a blog called Flyspeck (the word, Dr Hales explains, means to examine closely).

Why should the non-mathematician care about things of this nature? The foremost reason is that mathematics is beautiful, even if it is, sadly, more inaccessible than other forms of art. The second is that it is useful, and that its utility depends in part on its certainty, and that that certainty cannot come without a notion of proof. Dr Gonthier, for instance, and his sponsors at Microsoft, hope that the techniques he and his colleagues have developed to formally prove mathematical theorems can be used to “prove” that a computer program is free of bugs—and that would certainly be a useful proposition in today's software society if it does, indeed, turn out to be true.

Copyright (c) 2005 The Economist Newspaper and The Economist Group. All rights reserved.

Taken from “The Economist” newspaper's online version at http://www.economist.com/science/PrinterFriendly.cfm?Story_ID=3809661.

Introduction

Proof Situations and Proofs

We do not give a formal definition of “proof”, it should be understood that a proof should not only tell whether or not the goal follows from the assumptions but it should also convince the reader (listener) by giving arguments why the goal is true whenever the assumptions hold. (“Truth” of a formula here refers to the semantics of expressions introduced in Chapter 1.)
Example of a proof situation in which the answer “proved” is trivially known:  Any proof situation in which the goal formula can be obtained from one of the formulae in the knowledge base by substitution, i.e. the goal formula is an instance of a formula in the knowledge base. The easiest case is when the goal is equal to one of the formulae in the knowledge base.
Here, we do not discuss in which sense the reasoning steps in a proof must be algorithmic. However, in each of the reasoning steps which we introduce and train below, it should be clear that they can be “checked” by computers. (The Theorema system is a system that does not only allow to check reasoning steps algorithmically but also to produce such steps algorithmically to a certain extent.)

Conventions on Free Variables

Intuitive Notion: The “Distance” between the Goal and the Knowledge Base

A proof is finished, when the goal is contained in the knowledge base, i.e. the distance between goal and knowledge base is zero, or the goal is an instance of a formula in the knowledge base, i.e. the goal is very close to a formula in the knowledge base, i.e. the distance between goal and knowledge base is “small”. At the beginning of a proof, the goal is neither contained in the knowledge base nor is the goal already very close to a formula in the knowledge base, i.e. there is a “big” distance between goal and knowledge base—otherwise the proof is trivial! The aim of each individual proof step should therefore be to reduce the distance between goal and knowledge base.
Now think of each formula as a point in the plane and the knowledge base as the area containing all formulae it is composed of. Each reasoning step modifies the goal or the knowledge base.

Notation in Reasoning Rules

(Underscript[∀ , ξ, η, …])F

(Underscript[∀ , ξ, η, …])F

The Role of Propositional Logic in Predicate Logic Proving

Elementary Parts of Formulae

x ∈ 
        A => (x ∈ A ∨ 
            x ∈ B)  .

x ∈ A

x ∈ B  .

\(𝒜 => \(\((𝒜 ∨ ℬ)\)\(\ \ \)\(.\)\)\)

\(\((A ⋂ 
            B = ∅)\) ⇔ \(¬ ∃ \+x\((x ∈ A ∧ x ∈ B)\)\)\)

A ⋂ B = ∅

(Underscript[∃ , x])(x ∈ A ∧ 
          x ∈ B)

\(𝒜 ⇔ \(¬ ℬ\)\)

Truth Tables

Propositional Consequences, Propositional Tautologies, Propositional Equivalences

A formula U is a propositional tautology iff U is (always) true iff U obtains the truth value “true” for all assignments of truth values to the elementary parts of U.
Formulae U and V are propositionally equivalent iff U is a propositional consequence of V and V is a propositional consequence of U. 
It is clear that formulae U and V are propositionally equivalent iff, for any assignment of truth values to the elementary parts of U and V, they obtain identical truth values. 
Also, U and V are propositionally equivalent iff U ⇔ V is a propositional tautology.

(x ∈ A ∧ 
          x ∈ C) ∨ (x ∈ B ∧ 
          x ∈ C)

x ∈ A ∨ x ∈ B

x ∈ C   .

({{x ∈ A, x ∈ B, x ∈ 
            C, x ∈ A ∨ 
            x ∈ B

          , (x ∈ A ∧ 
                x ∈ C) ∨ (x ∈ B ∧ 
                x ∈ C)}, {true, true, true, true, true}, {true, true, □, true, □}, {true, □, true, true, true}, {true, □, □, true, □}, {□, true, true, true, true}, {□, true, □, true, □}, {□, □, true, □, □}, {□, □, □, □, □}})

(x ∈ A ∧ 
          x ∈ C) ∨ (x ∈ B ∧ 
          x ∈ C)

((x ∈ A ∨ x ∈ B) ∧ 
          x ∈ 
            C) ⇔ ((x ∈ A ∧ 
              x ∈ C) ∨ (x ∈ B ∧ 
              x ∈ C))

({{x ∈ A, x ∈ B

            }, {true, true}, {true, true}, {true, □}, {true, □}, {□, true}, {□, true}, {□, □}, {□, □}})({{x ∈ C

            }, {true}, {□}, {true}, {□}, {true}, {□}, {true}, {□}})({{(x ∈ A ∨ 
                  x ∈ B) ∧ x ∈ 
                C

              }, {true}, {□}, {true}, {□}, {true}, {□}, {□}, {□}})({{(x ∈ A ∧ 
                  x ∈ C) ∨ (x ∈ B ∧ 
                  x ∈ C)

            }, {true}, {□}, {true}, {□}, {true}, {□}, {□}, {□}})

((x ∈ A ∨ x ∈ B) ∧ 
          x ∈ 
            C) ⇔ ((x ∈ A ∧ 
              x ∈ C) ∨ (x ∈ B ∧ 
              x ∈ C))

((x ∈ A ∨ x ∈ B) ∧ 
        x ∈ C)

((x ∈ A ∧ 
            x ∈ C) ∨ (x ∈ B ∧ 
            x ∈ C))

((x ∈ A ∨ x ∈ B) ∧ 
        x ∈ C)

((x ∈ A ∧ 
            x ∈ C) ∨ (x ∈ B ∧ 
            x ∈ C))

Pure Propositional Logic Proof Parts

(x ∈ A ∧ 
          x ∈ C) ∨ (x ∈ B ∧ 
          x ∈ C)

x ∈ A ∨ x ∈ B

x ∈ C   .

Propositional Proof Rules for Structuring General Proofs in a Natural Way

We will explain this important role of propositional logic within predicate logic in the examples. In fact, most of the proofs that occur in practice, use propositional logic for structuring proofs before one applies (general and special) quantifier rules. Hence, although propositional logic is trivial as a stand–alone proof technique, it is of essential importance as a structuring tool for full predicate logic proofs.
Roughly, the natural deduction rules for connectives contain (at least) one proof rule for each propositional connective occurring as outermost symbol in the goal or in a formula in the knowledge base. In addition to those there are natural deduction rules for the quantifiers `∀' and `∃', again both for the quantifier occurring as outermost symbol in the goal or in a formula in the knowledge base.

Natural Deduction Proof Rules for Propositional Connectives

Rules for Knowledge Base Expansion

Rule (“Propositional Consequence”)

F, 
G, 
…

U

Rule (“Propositional Tautology”)

U

U

Rule (“Case Distinction on Disjunction in Knowledge Base”)

F

G ∨ H

F

G

F

H   .

Rules for Universally Quantified Propositional Formulae

Rule (“Expansion of Universally Quantified Conjunction in Knowledge Base”)

(Underscript[∀ , ξ, η, …])(F ∧ 
          G)

(Underscript[∀ , ξ, η, …])F

(Underscript[∀ , ξ, η, …])G

Rule (“Universally Quantified Implication in Knowledge Base: Modus Ponens”)

(Underscript[∀ , ξ, η, …])F => 
      G

(Subscript[F, ξ, η, … -> s, t, …])

(Subscript[G, ξ, η, … -> s, t, …])

\(∀ \+\(α, β, …\)G\_\(ξ, η, … -> s, t, …\)\)

Rule (“Universally Quantified Implication in Knowledge Base: Modus Ponens Special Case”)

(Underscript[∀ , ξ, η, …])(F ∧ H) => 
      G

(Subscript[F, ξ, η, … -> s, t, …])

(Subscript[H, ξ, η, … -> s, t, …])

(Subscript[G, ξ, η, … -> s, t, …])

\(∀ \+\(α, β, …\)G\_\(ξ, η, … -> s, t, …\)\)

Rule (“Reflexivity of Implication”)

(Underscript[∀ , ξ, η, …])F => 
      F

Rule (“Transitivity of Implication”)

(Underscript[∀ , ξ, η, …])F => 
      G

(Underscript[∀ , ξ, η, …])G => 
      H

(Underscript[∀ , ξ, η, …])F => 
      H

Rule (“Equivalence Rewriting”)

(Underscript[∀ , ξ, η, …])(F ⇔ 
          G)

H

(Subscript[F, ξ, η, … -> s, t, …])

\(H\_\(p ↦ G\_\(ξ, η, … -> s, t, …\)\)\)

(Underscript[∀ , ξ, η, …])(F ⇔ 
          G)

(Underscript[∀ , ξ, η, …])(G ⇔ 
          F)

Rule (“Reflexivity of Equivalence”)

(Underscript[∀ , ξ, η, …])F ⇔ 
        F

Rule (“Symmetry of Equivalence”)

(Underscript[∀ , ξ, η, …])F ⇔ 
        G

(Underscript[∀ , ξ, η, …])G ⇔ 
        F

Rule (“Transitivity of Equivalence”)

(Underscript[∀ , ξ, η, …])F ⇔ 
        G

(Underscript[∀ , ξ, η, …])G ⇔ 
        H

(Underscript[∀ , ξ, η, …])F ⇔ 
        H

Rule (“Split Equivalence into Implication”)

(Underscript[∀ , ξ, η, …])F ⇔ 
        G

(Underscript[∀ , ξ, η, …])F => 
      G

(Underscript[∀ , ξ, η, …])G => 
      F

Rule (“Equality Rewriting in Formulae”)

(Underscript[∀ , ξ, η, …])(u = 
          v)

H

(Subscript[u, ξ, η, … -> s, t, …])

\(H\_\(p ⇥ v\_\(ξ, η, … -> s, t, …\)\)\)

(Underscript[∀ , ξ, η, …])(u = 
          v)

(Underscript[∀ , ξ, η, …])(v = 
          u)

Rule (“Equality Rewriting in Terms”)

(Underscript[∀ , ξ, η, …])(u = 
          v)

(Subscript[u, ξ, η, … -> s, t, …])

\(h = 
      h\_\(p ⇥ v\_\(ξ, η, … -> s, t, …\)\)\)

Rule (“Reflexivity of Equality”)

(Underscript[∀ , ξ, η, …])s = s

Rule (“Symmetry of Equality”)

(Underscript[∀ , ξ, η, …])s = t

(Underscript[∀ , ξ, η, …])t = s

Rule (“Transitivity of Equality”)

(Underscript[∀ , ξ, η, …])r = s

(Underscript[∀ , ξ, η, …])s = t

(Underscript[∀ , ξ, η, …])r = t

Notation for Rewriting Chains

Such symbolic computation reasoning chains are presented in various forms. Here, we introduce one form: The following notation

(Subscript[F, 0])

↧  by (label 1) with x, 
    y, … -> (Subscript[s, 1]), (Subscript[t, 1]), …

(Subscript[F, 1])

↧  by (label 2) with x, 
    y, … -> (Subscript[s, 2]), (Subscript[t, 2]), …

(Subscript[F, 2])

↧  by (label 3) with x, 
    y, … -> (Subscript[s, 3]), (Subscript[t, 3]), …

...

↧  by (label k) with x, 
    y, … -> (Subscript[s, k]), (Subscript[t, k]), …

(Subscript[F, k])

means that

(Subscript[F, 0]) => (Subscript[F, 1])

(Subscript[F, 1]) => (Subscript[F, 2])

...

(Subscript[F, 0])  =>  (Subscript[F, 1]) =>  
        (Subscript[F, 2]) …

(Subscript[F, 0]) => (Subscript[F, 1]) => …

(Subscript[F, 0])

(Subscript[F, 1])

...

Rules for Goal Reduction

Rule (“Proof by Contradiction”)

¬ F

F

G ∧ ¬ G.

G ∧ ¬ G

In principle, the proof technique of proving by contradiction can be applied in just every proof problem: In order to prove a closed formula

F

¬ F

However, is it advisable to attempt, first, a “direct proof” before one attempts an “indirect proof” because, sometimes, direct proofs give more information than indirect proofs. It is also worth mentioning that “real life proving” as a fundamental part of mathematical exploration is typically applied in situations where it is not known whether or not a given formula F is true or false (under a given knowledge base).  Hence, the basic exploration cycle for analyzing the truth of a “conjectured” formula F by proving is as follows:

Rule (“Equivalence Rewriting”)

F

F ⇔ G

G   .

¬ F

¬ (F ∧ 
              G) ⇔ ¬ F ∨ ¬ G

¬ (F ∨ 
              G) ⇔ ¬ F ∧ ¬ G

¬ (Underscript[∀ , x]) 
          F ⇔ (Underscript[∃ , x])¬ F

¬ (Underscript[∃ , x]) 
          F ⇔ (Underscript[∀ , x])¬ F

Rule (“Decomposition of Conjunctions”)

F ∧ G ∧ …

F

G

…

Rule (“Splitting Disjunctions I”)

F ∨ G ∨ …

F

G

…

Rule (“Deduction Rule”)

F => G

G

F   .

Rule (“Contraposition”)

\(\((F => 
          G)\) ⇔ \(\((¬ G => ¬ F)\)\(\ \ \ \)\(.\)\)\)

F => G

¬ F

¬ G   .

Rule (“Contradiction”)

(F => 
          G) ⇔ (¬ F ∨ 
            G)   .

F => G

F

¬ G

Rule (“Splitting Disjunctions II”)

\(\((F ∨ G ∨ 
          H ∨ …)\) ⇔ \((¬ \((G ∨ 
                H ∨ …)\) => 
          F)\) ⇔ \(\((¬ G ∧ ¬ H ∧ … => F)\)\(\ \ \ \)\(.\)\)\)

F ∨ G ∨ H ∨ …

¬ G

¬ H

¬ …

F   .

Rule (“Prove Both Directions”)

F ⇔ G

G

F

F

G   .

Rule (“Prove Multi Equivalence”)

F ⇔ 
      G ⇔ … ⇔ 
      H

F => G

G => …

…

H => F   .

F

G

…

H   .

Rule (“Symbolic Computation Goal Reduction”)

F ⇔ G

G

F   .

G ⇔ H

H ⇔ …

…

… ⇔ 
      F   ,

Rule (“Symbolic Computation Equality Proving”)

s = t

s

t

Rule (“Equality Proving by Simplification”)

s = t

s

\(\(s\&~\)\)

t

\(\(t\&~\)\)

\(\(s\&~\) = \(\(t\&~\)\(\ \ \ \)\(.\)\)\)

Rule (“Goal Reduction using Implications”)

(Subscript[G, ξ, η, … -> s, t, …])

(Underscript[∀ , ξ, η, …])F => 
      G

(Subscript[F, ξ, η, … -> s, t, …])

(Subscript[G, ξ, η, … -> s, t, …])

(Underscript[∃ , ζ]) (Subscript[F, ξ, η, … -> s, 
            t, …])   .

(Underscript[∀ , x, y, z])(x ≤ y ∧ 
            y ≤ z) => 
      x ≤ z    (Trans)

a ≤ b

(Underscript[∃ , y])(a ≤ y ∧ 
            y ≤ b)   .

a ≤ (Subscript[y, 0])   and

(Subscript[y, 0]) ≤ b

a ≤ b

Natural Deduction Rules for Quantified Formulae

Rules for Knowledge Base Expansion

Rule (“Instanciation of Universal Quantifier”)

(Underscript[∀ , ξ, η, …])F

(Subscript[F, ξ, η, … -> s, t, …])

\(∀ \+\(α, β, …\)F\_\(ξ, η, … -> s, t, …\)\)

An instanciation step is usually announced in a proof by saying:

(Underscript[∀ , ξ, η, …])F

(Subscript[F, ξ, η, … -> s, 
        t, …])

Rule (“Skolem Constants”)

(Underscript[∃ , ξ, η, …])F

(Subscript[F, ξ, η, … -> x0, y0, …])

(Underscript[∃ , ξ, η, …])F

(Subscript[F, ξ, η, … -> x0, 
          y0, …])   .

Rule (“Skolem Functions”)

\(∀ \+\(α, β, …\)\(∃ \+\(ξ, η, …\)F\)\)

\(∀ \+\(α, β, …\)F\_\(ξ, η, … -> x0[α, β, …], y0[α, β, …], …\)\)

\(∀ \+\(α, β, …\)\(∃ \+\(ξ, η, …\)F\)\)

\(∀ \+\(α, β, …\)\(\(F\_\(ξ, η, … -> x0[α, β, …], 
            y0[α, β, …], …\)\)\(\ \ \ \)\(.\)\)\)

Rules for Goal Reduction

Rule (“Arbitrary But Fixed”)

(Underscript[∀ , ξ, η, …])F

\(F\_\(ξ, η, … -> ξ\_0, η\_0, …\)\)

\(\(\(F\_\(ξ, η, … -> ξ\_0, η\_0, …\)\)\(\ \ \)\)\)

Assume one succeeds to prove that

\(\(\(F\_\(ξ, η, … -> ξ\_0, η\_0, …\)\)\(\ \ \)\)\)

(Underscript[∀ , ξ, η, …])F

\(\(\(F\_\(ξ, η, … -> ξ\_0, η\_0, …\)\)\(\ \ \)\)\)

It is also important that  symbols `(Subscript[ξ, 0])' etc. are really new, i.e. they do not occur anywhere in the knowledge base and neither in F. If we use symbols `c', `d', etc. for which there is already knowledge available in the knowledge base, the proof of

(Subscript[F, ξ, η, … -> c, 
        c, …])

The proof technique “arbitrary but fixed” is very important in situations where formulae containing free variables are nested and the proof process for the individual quantifiers must be carefully distinguished. Sometimes, however, only the outermost universal quantifier has to be treated by the “arbitrary but fixed”. In such cases, it is unusual to really introduce new constants by the “arbitrary but fixed” technique. Rather, one just uses the variable names `ξ', etc. as new constants and one may say, for example,

Rule (“Find Appropriate Terms”)

(Underscript[∃ , ξ, η, …])F

(Subscript[F, ξ, η, … -> s, t, …])

Case Distinction

({{p[t,{({{(Subscript[t, 1]), ⇐, (Subscript[F, 1])}, {(Subscript[t, 2]), ⇐, (Subscript[F, 2])}, {(Subscript[t, 3]), ⇐, otherwise}})} ], or, 𝒞[H ,{({{(Subscript[G, 1]), ⇐, (Subscript[F, 1])}, {(Subscript[G, 2]), ⇐, (Subscript[F, 2])}, {(Subscript[G, 3]), ⇐, otherwise}})} ]}})

({{{({{p[t, (Subscript[t, 1])], ⇐, (Subscript[F, 1])}, {p[t, (Subscript[t, 2])], ⇐, (Subscript[F, 2])}, {p[t, (Subscript[t, 3])], ⇐, otherwise}})} , or, {({{𝒞[H, (Subscript[G, 1])], ⇐, (Subscript[F, 1])}, {𝒞[H, (Subscript[G, 2])], ⇐, (Subscript[F, 2])}, {𝒞[H, (Subscript[G, 3])], ⇐, otherwise}})} , respectively.}})

{({{(Subscript[G, 1]), ⇐, (Subscript[F, 1])}, {(Subscript[G, 2]), ⇐, (Subscript[F, 2])}, {(Subscript[G, 3]), ⇐, otherwise}})}

\(F\_1 => \(G\_1\ \  ∧ \ ¬ F\_1 ∧ 
          F\_2 => \(G\_2\ \ \  ∧ \ \ \ ¬ F\_1 ∧ ¬ F\_2 => \(\(G\_3\)\(\ \ \ \)\(.\)\)\)\)\)

({{f[x]:={({{(Subscript[t, 1]), ⇐, (Subscript[F, 1])}, {(Subscript[t, 2]), ⇐, (Subscript[F, 2])}, {(Subscript[t, 3]), ⇐, otherwise}})} , or, H :⇔{({{(Subscript[G, 1]), ⇐, (Subscript[F, 1])}, {(Subscript[G, 2]), ⇐, (Subscript[F, 2])}, {(Subscript[G, 3]), ⇐, otherwise}})} }})

({{{({{f[x] := (Subscript[t, 1]), ⇐, (Subscript[F, 1])}, {f[x] := (Subscript[t, 2]), ⇐, (Subscript[F, 2])}, {f[x] := (Subscript[t, 3]), ⇐, otherwise}})} , or, {({{\(H\  : \(\(⇔\)\(G\_1\)\)\), ⇐, (Subscript[F, 1])}, {\(H\  : \(\(⇔\)\(G\_2\)\)\), ⇐, (Subscript[F, 2])}, {\(H\  : \(\(⇔\)\(G\_3\)\)\), ⇐, otherwise}})} }})

Rule (“Expansion of Case Distinction”)

{({{(Subscript[G, 1]), ⇐, (Subscript[F, 1])}, {(Subscript[G, 2]), ⇐, (Subscript[F, 2])}, {(Subscript[G, 3]), ⇐, otherwise}})}

(Subscript[F, 1]) => (Subscript[G, 1])

¬ (Subscript[F, 1]) ∧ (Subscript[F, 2]) => (Subscript[G, 2])

¬ (Subscript[F, 1]) ∧ ¬ (Subscript[F, 2])=>(Subscript[G, 3])

Rule (“Reduction of Case Distinction”)

{({{(Subscript[G, 1]), ⇐, (Subscript[F, 1])}, {(Subscript[G, 2]), ⇐, (Subscript[F, 2])}, {(Subscript[G, 3]), ⇐, otherwise}})}

Prove (Subscript[G, 1]) under the assumption (Subscript[F, 1])

Prove (Subscript[G, 2]) under the assumption ¬ (Subscript[F, 1]) ∧ 
      (Subscript[F, 2])

\(Prove\ G\_3\ under\ the\ assumption\ \(¬ F\_1\) ∧ ¬ F\_2\)

|x|:={({{x, ⇐, x ≥ 0}, {-x, ⇐, otherwise}})}

\(∀ \+\(x, y ∈ ℝ\)|x + 
            y| ≤ |x| + |y|\)

{({{\(x\_0 + 
                  y\_0 ≤ \(\(|x\_0|\)\(+\)\(|y\_0|\)\(\ \)\)\), ⇐, (Subscript[x, 0]) + (Subscript[y, 0]) ≥ 0}, {\(\(-\((x\_0 + 
                      y\_0)\)\) ≤ \(\(|x\_0|\)\(+\)\(|y\_0|\)\(\ \)\)\), ⇐, (Subscript[x, 0]) + (Subscript[y, 0]) < 0}})}

{({{\(x\_0 + 
                  y\_0 ≤ \(\(x\_0\)\(+\)\(|y\_0|\)\(\ \)\)\), ⇐, (Subscript[x, 0]) ≥ 0}, {\(x\_0 + 
                  y\_0 ≤ \(\(-x\_0\)\(+\)\(|y\_0|\)\(\ \)\)\), ⇐, (Subscript[x, 0]) < 0}})}

{({{(Subscript[x, 0]) + (Subscript[y, 0]) ≤ (Subscript[x, 0])+(Subscript[y, 0]) , ⇐, (Subscript[y, 0]) ≥ 0}, {(Subscript[x, 0]) + 
                  (Subscript[y, 0]) ≤ -(Subscript[x, 0])+(-(Subscript[y, 0])) , ⇐, (Subscript[y, 0]) < 0}})}

Theory–Specific Proof Rules and Strategies

Set Theory

Set theory can, however, be introduced in an axiomatic fashion. Roughly speaking, set theory introduces a binary predicate `∈' (membership) and certain axioms that characterize the behaviour of membership. In addition, certain new function and predicate symbols are introduced through explicit definitions in terms of membership. There are several axiomatizations of set theory (Zermelo–Frankel set theory (ZF), von Neuman–Gödel–Bernays set theory (NGB), or type theory of Russell and Whitehead to name a few), which differ in the way how to avoid the well–known paradoxa, but which, on the other hand, do not affect the way how set theory is used in every–day mathematics (at least, the author is not aware of concrete situations in “usual mathematics”, where it would make a difference).
We show the flavour of axiomatic set theory based on axioms of ZF. Most of the axioms deal with the existence of certain sets that are characterized by the way how membership in them can be decided, e.g. there is for each formula P with free variable x and for each set M (where M and S do not occur in P) an axiom of the form

(Underscript[(∃ ! ), S]) (Underscript[∀ , x]) x ∈ 
          S ⇔ (x ∈ M ∧ 
                  P)   .

\(set[M, 
        P] := \(\(∍\)\(\)\(!\)\)\+S\ \(\((∀ \+x x ∈ 
              S ⇔ \((x ∈ M ∧ 
                    P)\))\)\(\ \ \ \)\(.\)\)\)

{x ∈ M | P}

(Underscript[∀ , x]) 
        x ∈ set[M, 
            P]⇔(x ∈ M ∧ 
              P)

(Underscript[∀ , y]) 
        y ∈ {x ∈ M | 
              P} ⇔ (y ∈ M ∧ 
              (Subscript[P, x -> y]))   ,

(Underscript[∀ , x]) 
        x ∈ {x ∈ M | 
              P} ⇔ (x ∈ M ∧ 
              P)   ,

A = 
      B  ⇔  (Underscript[∀ , x]) x ∈ 
            A ⇔ x ∈ B

\(TraditionalForm\`A ⊆ \(B : \(\(⇔\)\(\ \)\(∀ \+x 
                x ∈ A\)\) => 
          x ∈ \(\(B\)\(\ \ \ \)\(.\)\)\)\)

The construction of sets of the form {x | x ∈ M ∧ P} is allowed by the axioms of separation, the construction of sets of different shape must be claimed by axioms. In the sequel, we will introduce certain set constructions or list the rules how to test for membership in various set constructions. All definitions and all membership rules are justified by the underlying axioms of ZF.

∅ := {x | 
          x ≠ x}

A ⋂ 
        B := {x | x ∈ A ∧ x ∈ B}

\(TraditionalForm\`\(⋂A\) := {x | ∀ \+\(y ∈ A\)x ∈ y}\)

A ⋃ 
        B := {x | x ∈ A ∨ x ∈ B}

\(TraditionalForm\`\(⋃A\) := {x | ∃ \+\(y ∈ A\)x ∈ y}\)

𝒫[
        A] := {x | x ⊆ A}

{} := ∅

{a} := {x | x = a}

{a, 
        b} := {a} ⋃ {b} = {x | x = a ∨ x = 
              b}

{(Subscript[a, 1]), …, 
        (Subscript[a, n])} := {(Subscript[a, 1])} ⋃ … ⋃ {(Subscript[a, n])} = {x | 
                x = (Subscript[a, 1]) ∨ … ∨ x = 
                (Subscript[a, n])} = {x | (Underscript[∃ , i = 1, …, n])x = 
              (Subscript[a, i])}

\(TraditionalForm\`{𝔗\_x\( | \+\(x ∈ 
                M\)\)ℭ\_x} := {y | ∃ \+\(x ∈ M\)ℭ\_x ∧ y = 𝔗\_x}\)

\(TraditionalForm\`\(⋂\+\(x ∈ M\)A\_x\ \ \ for\)\ \ \  ⋂ {\(A\_x\)\( | \+\(x ∈ 
                M\)\)}\)

\(TraditionalForm\`\(⋃\+\(x ∈ M\)A\_x\ \ \ for\)\ \ \  ⋃ {\(A\_x\)\( | \+\(x ∈ M\)\)}\)

\(TraditionalForm\`a ∈ \(⋂\+\(x ∈ M\)A\_x\) ⇔ \(∀ \+\(x ∈ M\)a ∈ 
            A\_x\)\)

\(TraditionalForm\`a ∈ \(⋃\+\(x ∈ M\)A\_x\) ⇔ \(∃ \+\(x ∈ M\)a ∈ \(\(A\_x\)\(\ \ \ \)\(.\)\)\)\)

Natural Numbers

Induction Proofs for Universally Quantified Goals over the Natural Numbers

\(TraditionalForm\`\((A\_\(x -> 0\) ∧ ∀ \+\(n ∈ ℕ\)A\_\(x -> n\) => 
          A\_\(x -> n + 1\))\) => ∀ \+\(x ∈ ℕ\)A\_x\)

\(TraditionalForm\`∀ \+\(x ∈ ℕ\)A\_x\)

(Subscript[A, x -> 0])

\(TraditionalForm\`∀ \+\(n ∈ ℕ\)A\_\(x -> n\) => 
      A\_\(x -> n + 1\)\)

(Subscript[A, x -> (Subscript[n, 0])])

(Subscript[A, x -> (Subscript[n, 0]) + 1])

(Subscript[A, x -> 0]) => 
      (Subscript[A, x -> 1])

(Subscript[A, x -> 
          1])   ,

(Subscript[A, x -> 1]) => 
      (Subscript[A, x -> 2])

(Subscript[A, x -> 2])

Here we considered the set of natural numbers to start with 0. However, for some applications it can be convenient to consider 1 the smallest natural number. (Subscript[ℕ, 0]) is in this case commonly written for ℕ ⋃ {0}. The induction axioms are available with respective modification, i.e. the induction base is then

(Subscript[A, x -> 
            1])   .

(Subscript[A, x -> s])

\(TraditionalForm\`\(∀ \+\(x ∈ ℕ\)\)\+\(x ≥ s\)\(\(A\_x\)\(\ \ \ \)\(.\)\)\)

Comment on Presentation of Inference Chains

\(TraditionalForm\`“We\ know\ \ A\_\(x -> 0\) => \(A\_\(x -> 1\) => \(A\_\(x -> 2\) => \(… => 
              A\_\(x -> n\)\)\)\)\ ”\)

“We know  (Subscript[A, x -> 0])(Underscript[=>, (Underscript[↑, (Subscript[A, x -> 0]) => 
                    (Subscript[A, x -> 1])])])(Subscript[A, x -> 1])(Underscript[=>, (Underscript[↑, (Subscript[A, x -> 1]) => 
                      (Subscript[A, x -> 2])])])(Subscript[A, x -> 2])(Underscript[=>, (Underscript[↑, (Subscript[A, x -> 2]) => 
                        (Subscript[A, x -> 3])])])…(Underscript[=>, (Underscript[↑, (Subscript[A, x -> n - 1]) => 
                          (Subscript[A, x -> n])])])(Subscript[A, x -> 
                        n]) ”   ,

“We know  (Subscript[A, x -> 0])(Underscript[=>, (Underscript[↑, (Underscript[by an instance, of ()])])])(Subscript[A, x -> 1])(Underscript[=>, (Underscript[↑, (Underscript[by an instance, of ()])])])(Subscript[A, x -> 2])(Underscript[=>, (Underscript[↑, (Underscript[by an instance, of ()])])])…(Underscript[=>, (Underscript[↑, (Underscript[by an instance, of ()])])])(Subscript[A, x -> n]) ”   ,

Complete Induction

\(TraditionalForm\`\((∀ \+\(n ∈ ℕ\)\((\(∀ \+\(m ∈ ℕ\)\)\+\(m < n\)A\_\(x -> m\))\) => 
          A\_\(x -> n\))\) => ∀ \+\(x ∈ ℕ\)A\_x\)

\(TraditionalForm\`∀ \+\(x ∈ ℕ\)A\_x\)

\(TraditionalForm\`\((\(∀ \+\(m ∈ ℕ\)\)\+\(m < n\_0\)A\_\(x -> m\))\) => 
      A\_\(x -> n\_0\)\)

(Subscript[A, x -> 0])

\(TraditionalForm\`\(∀ \+\(m ∈ ℕ\)\)\+\(m < n\_0\)A\_\(x -> m\)\)

(Subscript[A, x -> 
            (Subscript[n, 0])])   .

Tuples

(Underscript[((Underscript[∀ , x])), is–tuple[x]])(Subscript[A, x])

\(TraditionalForm\`A\_\(x -> ⟨\ ⟩\)\)

\(TraditionalForm\`\(∀ \+τ\)\+\(is–tuple[τ]\)\(∀ \+y A\_\(x -> τ\)\) => \(A\_\(x -> τ⌢y\)\ \ \ \ or\ \ \ \ \(\(∀ \+τ\)\+\(is–tuple[τ]\)\(∀ \+y A\_\(x -> τ\)\)\) => 
        A\_\(x -> y⌣τ\)\)\)

(Subscript[A, x -> (Subscript[τ, 0])])

\(TraditionalForm\`A\_\(x -> τ\_0⌢y\_0\)\ \ \ \ or\ \ \ \ A\_\(x -> y\_0⌣τ\_0\)\)

Similar to natural numbers, there is also a complete induction for tuples. In order to prove

\(TraditionalForm\`\(∀ \+x\)\+\(is–tuple[x] ∧ |x| ≥ L\)A\_x\)

\(TraditionalForm\`\(∀ \+x\)\+\(is–tuple[x] ∧ |x| = L\)A\_x\)

\(TraditionalForm\`∀ \+\(l > L\)\(\(∀ \+x\)\+\(is–tuple[x] ∧ |x| < l\)A\_x\) => \(∀ \+x\)\+\(is–tuple[x] ∧ |x| = l\)A\_x\)

(Subscript[A, x -> (Subscript[τ, 0])])

\(TraditionalForm\`\(∀ \+x\)\+\(is–tuple[x] ∧ |x| < l\_1\)A\_x\)

(Subscript[A, x -> (Subscript[τ, 1])])

Polynomials

Organization

kb = {Point[{-0.8276280552341397`, -0.8327819600432769`}], 
          Point[{0.08405737605422048`, 0.6049077295309309`}], 
          Point[{-0.9287205583655876`, 0.32924112335726874`}], 
          Point[{-0.6561926285293338`, -0.2250175295726643`}], 
          Point[{-0.9454025519755905`, 0.3052011560947061`}], 
          Point[{0.40956983733376884`, -0.8730375437834876`}], 
          Point[{-0.8238082009170353`, -0.9346482158635764`}], 
          Point[{0.7181642563303476`, 0.20961515684236365`}], 
          Point[{0.5481509546235723`, -0.7536794389004724`}], 
          Point[{-0.17430674563930493`, -0.6946412565878923`}], 
          Point[{0.06611250864166296`, -0.8760976688083804`}], 
          Point[{-0.3986435268294568`, -0.5183586080922935`}], 
          Point[{-0.10625943612419742`, 0.9566842912348965`}], 
          Point[{0.5172990971163227`, -0.12326633762322448`}], 
          Point[{-0.17753887775860977`, -0.3725568321223721`}], 
          Point[{0.1734917256456565`, -0.8982488080505602`}], 
          Point[{-0.23213632578301924`, 0.32224201178292167`}], 
          Point[{0.7639218883118875`, 0.9747887357329275`}], 
          Point[{-0.4083281248659839`, 0.25689022764649816`}], 
          Point[{-0.95424236801846`, -0.23482642110943608`}]};

Show[
        Graphics[{{RGBColor[0.698039,  0.92549,  0.156863], 
              Polygon[Flatten[
                  MapAt[Reverse, Outer[List, {-1, 1}, {-1, 1}], 2], 
                  1]]}, {RGBColor[0.219608,  0.321569,  0.501961], 
              PointSize[0.015], kb}, Text["KB", {0, 0}], 
            Text["Goal", {5, -0.3}], {PointSize[0.03], 
              RGBColor[0.831373,  0.0470588,  0.156863], Point[{5, 0}]}}], 
        PlotRange -> All, AspectRatio -> Automatic];

<< Graphics`Arrow`

Show[
        Graphics[{{RGBColor[0.698039,  0.92549,  0.156863], 
              Polygon[Flatten[
                  MapAt[Reverse, Outer[List, {-1, 1}, {-1, 1}], 2], 
                  1]]}, {RGBColor[0.219608,  0.321569,  0.501961], 
              PointSize[0.015], kb}, Text["KB", {0, 0}], 
            Text["Goal", {5, -0.3}], 
            Text["New\nGoal", {4, -0.4}], {GrayLevel[0.5], 
              Arrow[{5, 0}, {4, 0}]}, {PointSize[0.03], 
              RGBColor[0.831373,  0.0470588,  0.156863], Point[{5, 0}], 
              Point[{4, 0}]}}], PlotRange -> All, 
        AspectRatio -> Automatic];

Show[
        Graphics[{{RGBColor[0.878431,  0.956863,  0.501961], 
              Polygon[Flatten[
                  MapAt[Reverse, Outer[List, {-1, 1.8}, {-1, 1}], 2], 
                  1]], RGBColor[0.698039,  0.92549,  0.156863], 
              Polygon[Flatten[
                  MapAt[Reverse, Outer[List, {-1, 1}, {-1, 1}], 2], 
                  1]]}, {RGBColor[0.219608,  0.321569,  0.501961], 
              PointSize[0.015], kb, 
              Point[{1.7181642563303476`, 0.20961515684236365`}]}, {GrayLevel[
                0.5], Arrow[{0.7181642563303476`, 
                  0.20961515684236365`}, {1.7181642563303476`, 
                  0.20961515684236365`}]}, Text["KB", {0, 0}], 
            Text["Goal", {5, -0.3}], {PointSize[0.03], 
              RGBColor[0.831373,  0.0470588,  0.156863], Point[{5, 0}]}}], 
        PlotRange -> All, AspectRatio -> Automatic];

\(\(Show[
        Graphics[{{RGBColor[0.698039, \ 0.92549, \ 0.156863], 
              Polygon[Flatten[
                  MapAt[Reverse, Outer[List, {\(-1\), 1}, {\(-1\), 1}], 2], 
                  1]]}, {RGBColor[0.219608, \ 0.321569, \ 0.501961], 
              PointSize[0.015], kb, 
              Point[{1 - 
                    0.6561926285293338`, \(-0.2250175295726643`\)}]}, {GrayLevel[0.5], 
              Arrow[{\(-0.6561926285293338`\), \(-0.2250175295726643`\)}, {1 - 0.6561926285293338`, \(-0.2250175295726643`\)}]}, Text["KB", {0, 0}], 
            Text["Goal", {5, \(-0.3\)}], {PointSize[0.03], 
              RGBColor[0.831373, \ 0.0470588, \ 0.156863], Point[{5, 0}]}}], 
        PlotRange -> All, AspectRatio -> Automatic];\)\)