TT2026 Introduction to Proof Systems notes


Remaining TODOs: 11


1. Logic

Definition 1.1: Logic is the study of the principles of correct reasoning.

This requires:

  • an unambiguous language in which we can formulate statements
  • a mathematical framework to determine the truth of a statement

Definition 1.2: A logical syllogism is an example of correct reasoning.

For example:

All beings are mortal;
All humans are beings;
Therefore all humans are mortal.

2. Propositional logic

2.1. Syntax

Definition 2.1.1: Basic sentences in propositional logic are atomic propositions.

For example, Alice is an architect.

Definition 2.1.2: Compound sentences can be formed by logical connectives: (negation), (disjunction), (conjunction).

e.g. ; .

Example:

“” means “entails”; we have some propositions and we draw a conclusion.

Definition 2.1.3: Let be a countably infinite set of propositional variables.

Formulas of propositional logic are defined inductively:

  1. (basis clause) true,false and every propositional variable are propositional formulae
  2. (inductive clause) If are formulae, then so are (negation), (disjunction, with and the disjuncts), and (conjunction, with and the conjuncts)
  3. (extremal clause) Nothing else is a formula
Remark: The extremal clause of the above definition ensures that the set of propositional formulae is the minimal set that satisfies the basis and inductive clauses.

Definition 2.1.4: There are some derived connectives:

  • implication: . Here is the antecedent and is the consequent
  • bi-implication:
  • Exclusive-OR:
  • Indexed conjunction:
  • Indexed disjunction:
Definition 2.1.5: The set of all formulae of proposition logic over is denoted by .

Definition 2.1.6: The operate precedence for propositional logic is:

Definition 2.1.7: A literal is an atomic proposition or its negation.

Definition 2.1.8: We say that is in conjunctive normal form (CNF) if

where each is a literal.

is in disjunctive normal form (DNF) if

Definition 2.1.9: is in -CNF if it is in CNF, and all the s are equal to some fixed .

is in -DNF if it is in DNF with all the s equal to fixed .

Remark: Normal forms are particularly well-suited for algorithmic treating.
Definition 2.1.10: Functions on formulae of propositional logic are uniquely defined by specifying the function values for “base cases” and “inductive steps”, following the cases in Definition 2.1.3. Such a definition is said to use structural induction.

Example: Suppose we want to define a function that returns the set of all subformulae of a formula .

We define using structural induction,

2.2. (Tarski-style) semantics

Definition 2.2.1: An assignment is a function that induces a function . That is maps propositional variables to truth values, and maps formulae to truth values.

We define using structural induction.

Note that we define in a kind of meta language - the “and” and “or” here are not the same as in propositional logic.

From now we write instead of for convenience.

Remark: We can construct truth tables for logical and derived connectives in the obvious manner. Implication may be surprising:
true true true
true false false
false false false
false true true

In particular this means that you can use false to show anything to be true, i.e. we should start with true assumptions when trying to prove something (obviously).

Definition 2.2.2: Let and . Then

  1. If then (“ is a model of “, or “ holds under “).
  2. If for all , then we write (“ models “)
  3. is satisfiable is there is some s.t. , or . Otherwise, is unsatisfiable.
  4. If holds under any assignment, we say that is valid, or that is a tautology.
  5. If, for all assignments , implies for some (not neccessarily an from statement 2), then entails , written . We write if .
  6. If and , then and are logically equivalent, .
  7. If is satisfiable iff is satisfiable, then and are equisatisfiable.

Example:

Example (Encoding constraint satisfaction problem - Hamiltonian path problem): For undirected graph , is there a path visiting every vertex exactly once?

Introduce propositional variables expressing whether a Hamiltonian path visits vertex at time in a Hamiltonian path.

Then iff has a Hamiltonian path.

This is a practical example of why satisfiable is an important concept.

Remark: This is nonconstructive, and also uses the law of the excluded middle; some claim that using the law of the excluded middle for nonconstructive proofs is invalid.

2.3. Minimal calculus (minimal logic)

Definition 2.3.1: The minimal calculus, consists of a finite number of axioms:

We also have a single inference rule, modus ponens: From and , infer .

Remark: Modus ponens is basically , but it allows us to actually perform pattern-matching on the proof and reduce it.
Remark:All of the axioms are also valid formulae in Tarski-style semantics
Remark: Implication needs to be a primitive in the minimal logic, so that we can deal very carefully with negation.
Remark: The subscript 0 in indicates that this is a propositional logic (as opposed to, e.g., predicate logic)

Definition 2.3.2: A derivation in the minimal calculus is a finite sequence of formulae , each being either an axiom, or obtained from by application of modus ponens. If some is neither an axiom nor MP-derived, it is a hypothesis.

We write if is derivable; then is a theorem or provable in .

Example:

This gives us a new proof rule, conjunction introduction:

Example:

  1. (hypothesis)
  2. (hyp)
  3. ( (1, 2))
  4. (PL4)
  5. (MP (3, 4))

This gives us a new rule, transitivity of implication,

Definition 2.3.3: Ex falso quodlibet (“from falsehood, anything follows”) is the principal that , i.e. anything is provable from a false hypothesis.
Definition 2.3.4: Tertium non datur (“no third [possibility] is given”) is the law of the excluded middle, (equivalently, is a tautology).

Remark: Not every valid statement in Tarski-style semantics is derivable using the minimal calculus.

In particular, it is not possible to derive ex falso quodlibet or tertium non datur.

Proposition 2.3.5:

Proof: Let be such that:

  • Propositional and template variables are given an arbitrary but fixed value

  • The remaining logical connectives are reduced inductively according to the following table
    0 0 1 0 0
    0 1 0 1 1
    1 0 0 1 0
    1 1 0 1 0

Then choose such that , and observe that all aaxioms of evaluate to 0 under , while .

Observe also that if , then applying modus ponens to get must have , otherwise would evaluate to 1 by the definition of .

Therefore, starting from axioms and using modus ponens, we cannot create a formula that evaluates to 1 under ; therefore is not derivable from the axioms and modus ponens.

Definition 2.3.6: If we add ex falso quodlibet as an extra axiom, PL11 , then we get intuitionistic logic, denoted .

If we add tertium non datur, the law of the excluded middle, as a 12th axiom, we get classical logic, denoted .

Theorem 2.3.7: For any formula , ( is valid) iff .
is soundness and is simple.
is completeness and is more difficult to prove.

2.4. Equational reasoning

Idea: substitute subformulae by equivalent ones, according to the axioms of Boolean algebras.

Definition 2.4.1: A Boolean algebra is a structure that satisfies the following axioms:

  • (idempotence)
  • (commutativity)
  • (associativity)
  • (absorption)
  • (distributivity)
  • (double negation)
  • (de Morgan)
  • (complementation)
  • (zero laws)
  • (identity laws)
Remark: Sets form a Boolean algebra.

Definition 2.4.2: We write to mean the formula obtained from by replacing every occurrence of in by .

This is a substitution.

Formally, if . For , we proceed by structural induction:

  • Base case: for all
  • Inductive steps:

Theorem 2.4.3 (Substitution theorem): Let be formulae s.t. and , then .

Proof: By structural induction on .

If then , hence .

Otherwise:

  • If , then , hence
  • If , then , by inductive hypothesis, where
  • Conjunction and disjunction follow similarly.

Definition 2.4.4: A proof by equational reasoning of is a sequence such that , , and is obtained from by a substitution according to the Boolean algebra axioms.

Theorem 2.4.5 (soundness): If we have an equational proof starting in and ending in , then .

Proof: Consequence of the substitution theorem.
Definition 2.4.6: A formula is in negation normal form if negation appears only in front of propositional variables.

Lemma 2.4.7: Every formula can be transformed into DNF by equational reasoning.

Proof:

We exhaustively apply de Morgan’s laws, and rewrite and . This gives us the negation normal form of .

Then we exhaustively apply distributivity and the identity laws.

We can then reintroduce any variables that were eliminated, by replacing any disjunct with . Thus we obtain a canonical (up to disjunct ordering) DNF for the formula.

Theorem 2.4.8 (comleteness): If , then there is an equational proof starting in and ending in .

Proof: Given s.t. , then and have the same truth table, hence the same DNF . Then we apply Lemma 2.4.7 to to obtain by proof , and to to obtain by proof .

Then the equational proof of is concatenated with the reverse of .

2.5. Resolution

Use formulae in CNF, presented as sets.

E.g. if .

We represent this as .

We represent the empty clause as . .

Remark: The set representation naturally expresses commutativity, associativity and idempotence.

Definition 2.5.1: Given literal , we define

Definition 2.5.2: Let be clauses s.t. and . Then the resolvent of and is

We say that is derived by resolution from and ; we write

Definition 2.5.3: A derivation (or proof) of a clause from the set of clauses is a sequence of clauses such that

  • For each , either (an assumption), or is the resolvent of and , for some .
Definition 2.5.4: A derivation of demonstrates a refutation of .
Remark: To show that , we can demonstrate a refutation of .

Definition 2.5.5: Given , define

Also define ; .

Also . Note that this is computable in finite time. TODO is it?

Proposition 2.5.6: iff there exists a resolution derivation of from .

Lemma 2.5.7 (Resolution lemma): If is the resolvent of , then .

Proof: if we have that iff .

: If , then clearly .

: Let , . Then we have two cases:

  1. , then since , we have . Hence .
  2. , then since , we have , so .

Theorem 2.5.8 (soundness): If can be derived by resolution from , then is unsatisfiable.

Proof: By induction on the length of the resolution proof.

.

Theorem 2.5.9 (completeness): If is unsatisfiable, then can be derived from by resolution.

Proof: By induction on the number of propositional variables that appear in , .

If , then . Trivial.

Then suppose true for , and consider .

mentions prop. vars. . Let .

Since is unsatisfiable, both and are unsatisfiable. By the inductive hypothesis, we have being a refutation of .

Note that or are already in . By reintroducing , we either obtain a proof of , or of .

In the latter case, we can apply the same reasoning to and obtain a proof of . Then the final resolution step gives us .

Remark: Constructing equivalent CNF formulae can be expensive. But because resolution only checks unsatisfiability, we only need an equisatisfiable formula.

Give , do the following:

  • Introduce fresh prop. vars for every subformula of , whenever is not a literal; call it
  • Introduce , where is , with the top-level subformulae replaced by the new prop. vars.
  • Use equational transformation to transform all of the s into CNF
  • The final formula is all new CNF formulae, plus .

Example: Consider the formula . The subformulae of , excluding literals, are . Then we introduce new propositional variables , , , and say that:

We then transform these into CNF:

  • and combine them all with to get:

2.6. Natural deduction

Definition 2.6.1: The calculus of natural deduction has no axioms. Proofs begin by assumptions, and we use rules for Boolean connectives. A proof is a tree.

Temporary assumptions that are discharged are denoted by square brackets in the proof rules. If, at the end of a proof, all assumptions are discharged, the proof is valid.

Definition 2.6.2: The natural deduction rules are as follows:

  • Conjunction introduction:

  • Conjunction elimination:

  • Disjunction introduction:

  • Disjunction elimination:

    This says that, in order to derive from , it is sufficient to derive from and also from . Then both assumptions and are discharged. This is informally proof by cases.

  • Implication introduction:

  • Implication elimination:

  • Negation introduction:

  • Negation elimination:

  • Ex falso quodlibet:

  • Reductio ad absurdum:

Remark: Without J or K, natural deduction is equivalent to ; with J it is equivalent to ; and with K, it is equivalent to .
Definition 2.6.3: A deduction of a formula is a finite tree of formulae in which every leaf is an assumption, and every other formula is the conclusion of an application of one of the inference rules. The open assumptions of a deduction are those that are not discharged by any rule in the tree. A deduction of with no open assumptions is a proof of , and is a theorem if such a proof exists.
Remark: Natural deduction is sound and complete.

2.7. Sequent calculus

Definition 2.7.1: A sequent is an expression of the form

where the s and s are propositional forumlae.

Such a sequent is valid if the following is valid in classical logic:

  • , if
  • , if
  • , if ,
  • false otherwise.

The left-hand side of the sequent is the antecedent, and the right-hand side is the succedent.

Remark: The sequent with an empty antecedent and empty succedent is the empty sequent and is always invalid, by the last case in the definition above.
Remark: is a tautology/axiom.
Remark: In declarations of sequent inference rules, we use the Greek letters to denote (possibly empty) ordered lists of propositional formulae.

Definition 2.7.2: The inference rules of sequent calculus are either structural rules, which manipulate the list structure of a sequent, and operational rules, which provide rules for introducing logical connectives in the antecent or succedent. Inference rules take one or more premises from which a conclusion is drawn.

Definition 2.7.3: The structural rules are as follows:

  • Interchange allows consecutive formulae to be swapped, on both the left and right-hand sides:

  • Weakening allows formulae to be added to the left or right:

  • Contraction allows duplicate formulae to be merged:

Definition 2.7.4: The operational rules are as follows:

  • Conjunction:

  • Disjunction:

  • Conditional:

  • Negation:

Definition 2.7.5: A proof in the sequent calculus is a finite tree of sequents in which every leaf is an axiom (), and every other node is obtained from its children (where children are written above their parent) by an inference rule.

A sequent is provable or derivable if it is the root of such a proof.

Remark: To prove validity of in the sequent calculus, we want to obtain an empty left-hand side, with on the right:

Example: To prove that :

Example: To prove

Theorem 2.7.6: The sequent calculus is a sound and complete proof system for classical logic.

2.8. The compactness theorem

Theorem 2.8.1 (compactness theorem):

A set of formulae is satisfiable iff every finite subset of is satisfiable.

Equivalently, a set of formulae is unsatisfiable iff there is some unsatisfiable finite .

Proof:

“”: Suppose that is satisfiable, then there exists s.t. for all , hence for all for any finite subset .

“”:

Define a partial assignment to be a function , where .

We say that a partial assignment is good if for all s.t. only mentions the variables in .

Suppose that every finite subset of is satisfiable, then for every , there is a partial assignment s.t. that is good:

  • Let be all formulae over .
  • might be infinite, but contains only finitely many formulae, up to logical equivalence.
  • Choose representatives for each equivalence class and put them in , finite.
  • By assumption, there is some such that for all . Moreover, will satisfy every formula in , because they are all logically equivalent to a formula in

Now we plan to construct a sequence of partial assignments that are good, and such that extends ; that is, , and for all .

We do this while maintaining the invariant that, for all , there are infinitely many good extensions of .

We construct the s by induction on .

The base case is clear: is the empty assignment, which vacuously satisfies the empty subset of , and there are clearly an infinite number of good assignments that extend the empty assignment, since every finite subset of is satisfiable.

Then suppose we constructed , and consider two assignments that extend , with . Since has infinitely many good extensions, one of and must have infinitely many good extensions. Pick the or that has infinitely many good extensions to be . Then by induction we have constructed our sequence .

Now we take such that for all . Then for all , because we can take the largest index of a prop. var. that appears in , and we know that extends a model of , so .

Example (an application of the compactness theorem):

Proposition: Let be a graph with , and suppose that every finite subgraph of is -colourable, then is -colourable.

Proof: For every , introduce a propositional variabel ( has colour ).

Then let

and we claim that is satisfiable iff has a colouring (proof is easy).

Observe that any finite “talks about” a finite subgraph of ; by assumption, is satisfiable. By the compactness theorem, is satisfiable; therefore is -colourable.

3. 1st-order logic

3.1. Syntax

Definition 3.1.1: A signature, , is a tuple of

  • constant symbols ()
  • function symbols ()
  • predicate symbols ()

with function and predicate symbols each having nonzero arity .

We also keep a set of variables , independently from the signature.

Definition 3.1.2: A -term is defined by structural induction:

  • every is a term
  • every is a term
  • if are terms, then is a term (assuming has arity )
  • nothing else is a term

Definition 3.1.3: A formula of 1st-order logic over is defined by structural induction.

  • is an atomic formula for a -ary relation symbol and terms
  • If are formulae, and , then the following are formulae:
    • , ,
    • (existential quantifier)
    • (universal quantifier)
  • Nothing else is a formula

Definition 3.1.4: For existential/universal quanitifiers / , we say that is in the scope of / , and moreover is bound by / .

If a variable is not bound, it is free.

A formula with no free variables is a sentence, or closed.

TODO quantifier depth

3.2. Semantics

Definition 3.2.1: A -structure or -assignment is a tuple consisting of:

  • A non-empty universe
  • For every -ary function symbol , a function
  • For every -ary predicate symbol , a -ary relation
  • For every constant , a
  • For every variable , a .

Definition 3.2.2: For -structure and term , we define the value of under by structural induction:

Definition 3.2.3: We define the satisfaction relation by structural induction:

  • iff
  • iff
  • iff and
  • iff or
  • iff there is s.t.
  • iff for all ,

Definition 3.2.4: A 1st-order logic formula is satisfiable if there is a -structure s.t. .

is unsatisfiable if there is no such structure.

Definition 3.2.5: 1st-order logic formulae are equivalent () if for all .
Definition 3.2.6: 1st-order formulae are equisatisfiable if is satisfiable iff is satisfiable.

3.3. Equivalences & Skolem form

Definition 3.3.1: A formula is in Skolem form if , where is quantifier-free.
Lemma 3.3.2 (Relevance Lemma): Let be a formula, and assignments coinciding on their interpretation of constants, function symbols, predicate symbols and variables that are free in . Then iff .

Remark: Propositional logic laws for logical equivalence still carry over, e.g. .

Moreover, logical equivalence is still a congruence, e.g. iff and .

Also, if , then , and .

Theorem 3.3.3:

Let be formulae, then the following equivalences hold in 1st-order logic:

  1. , (these allow us to establish a negation-normal form for 1st-order logic)

  2. If does not appear free in , then

    • ,
    • ,
  3. ,
  4. ,

Proof:

  1. iff

    iff for some

    iff for some

    iff

    and similar for the second equivalence.

  2. iff and

    iff, for all , and

    iff, for all , and

    (by the Relevance Lemma, since does not appear free in )

    iff, for all ,

    iff

    and similarly for the other equivalences.

  3. TODO exercise
  4. TODO exercise

Definition 3.3.4: A formula is in prenex form if

where is quantifier-free.

Lemma 3.3.5: Any formula is equivalent to one in prenex form.

Definition 3.3.6: Let be a formula, a variable, and a term, then is a substitution obtained by replacing every free occurrence of in with .

TODO define by structural induction.

Lemma 3.3.7 (translation-lemma): If is a term and a formula such that no variable in occurs bound in , then we have that iff .

Proof:TODO, optional

Lemma 3.3.8: Let with a quantifier, and a variable not occurring in . Then .

Proof:TODO
Definition 3.3.9: A formula is rectified if no variable occurs both bound and free at the same time, and all quantifiers refer to different variables.

Lemma 3.3.10: Every formula is equivalent to a rectified formula, and moreover one in rectified prenex form.

Proof: TODO by the lemmas above.

Lemma 3.3.11: Let where is rectified. Let be a fresh function symbol of arity , then is equisatisfiable with .

Proof sketch: Suppose . We define extending such that , where is such that .

Then .

Remark: If , then is a constant symbol.

Theorem 3.3.12: Any 1st-order formula is equisatisfiable with a formula in Skolem form.

Proof: We get in prenex form, and utilise Lemma 3.3.11 to eliminate existential quanitifiers from left to right.
Remark: The quantifier-free part of a Skolem-form formula is sometimes known as the matrix of the formula.

3.4. Herbrand’s Theorem & Ground Resolution

Definition 3.4.1: A ground term (of ) is a variable-free term.

Definition 3.4.2: A -structure is a Herband structure if the following are true:

  • is the set of ground terms
  • for every constant symbol
  • For every -ary function symbol and ground terms ,
Remark: The interpretations of constant and function symbols are just strings of symbols.
Remark: The only thing we are free to choose is the interpretation of predicate symbols.
Remark: The interpretation of a term in a Herbrand structure is .

Corollary 3.4.3 (translation lemma for Herbrand structures):

iff .

Theorem 3.4.4 (Herbrand's theorem): Let be a closed formula in Skolem form. Then is satisfiable iff has a Herbrand model.

Proof:

“”: obvious.

“”: Suppose . We define iff . Then we show that is a model of by induction on the number of quantifiers .

If , then is a Boolean combination of atomic formulae for ground terms . By construction, iff , so , iff .

Then suppose true for Skolem-form sentences with quantifiers, and consider with quantifiers, where . By the translation lemma, iff . Hence for all ground terms . is closed, so by the i.h. for all ground terms . By the translation lemma, for all , hence , .

Corollary 3.4.5: For any formula with an uncountable model, there is a countable model.

Definition 3.4.6: Let be closed in Skolem form, and define the Herbrand expansion to be

Remark: Each formula in is a Boolean combination of atomic formulae. This means that has a Herbrand model iff it is propositionally satisfiable, i.e. there is an assignment to the set of closed atomic formulae that makes all formulae in evaluate to true.

Theorem 3.4.7: A closed Skolem-form formula is satisfiable iff is satisfiable when viewing atomic formulae as propositional variables.

Proof:

sat. iff exists a Herbrand model of , by Herbrand’s Theorem
iff
iff for all ground terms
iff , by the Translation Lemma for Herbrand structures
iff by defn of Herbrand expansion
iff is satisfiable, by Herbrand’s Theorem.

Theorem 3.4.8 (Ground Resolution): A closed Skolem-form formula is unsatisfiable iff there is a propositional resolution refutation of .

Proof: TODO

Remark:

To prove validity of , we can provide a ground resolution refutation of .

  • Transform into negation normal form
  • Transform into rectified prenex form
  • Skolemise
  • Transform into CNF
  • Do a propositional resolution proof on the Herband expansion
  • If is derived, then is unsatisfiable, so is valid

Example:

Let , .

Note that the set of ground terms is empty because there are no constant symbols. However, we can introduce a fresh constant symbol , and now the set of ground terms is .

TODO resolution refutation

3.5. Natural deduction and sequent calculus in 1st-order logic

Definition 3.5.1: We introduce new natural deduction proof rules for quantifiers:

  • Universal elimination:

  • Universal introduction:

    where is free and must not occur in any undischarged assumption on which the deduction of relies.

  • Existential introduction:

  • Existential elimination:

    provided that does not occur in , and all assumptions must be discharged when E is applied.

Example:

Definition 3.5.2: We extend the sequent calculus with new proof rules for quantifier.

  • Universal quantification:

    where the exclamation mark (!) indicates that must not occur in .

    • Existential quantification:

Example:

TODO IMPORTANT: exercise 22 (ground resolution), 23 (natural deduction), 26 (sequent calculus)