Hilbert proof systems

also known as Frege systems or axiom systems

method of entailment (not refutation)

refutation
prove (un)satisfiability
tableaux, resolution
entailment
derive consequences
natural deduction, Hilbert proof systems

Hilbert systems vs. natural deduction

similar, but:

natural deduction:
assumptions
Hilbert proof systems:
axioms
axioms=some formulae that are valid in the considered logic

chosen in such a way they allow to derive any other valid formula


An Hilbert system for propositional logic

axioms
  1. x→(y→x)
  2. (x→(y→z))→((x→y)→(x→z))
rules
A   A→B modus ponens
B
A substitution (x variable, B formula)
A[B/x]

How it works

proof=sequence of formulae

where each formula is either:


Example

prove that x→x holds


Example: proof

1. (x→(y→z))→((x→y)→(x→z)) axiom 2
2. (w→((w→w)→w))→((w→(w→w))→(w→w)) from 1. by substitution [w/x, w→w/y, w/z]
3. x→(y→x) axiom 1
4. w→((w→w)→w) from 3. by substitution [w/x, w→w/y]
5. (w→(w→w))→(w→w) from 2. and 4. by modus ponens
6. w→(w→w) from 3. by substitution [w/x, w/y]
7. w→w from 5. and 6. by modus ponens
8. x→x from 7. by substitution [x/w]

Pros and cons

cons:

pros:


Axioms for the other connectives

  1. ⊥→x
  2. x→⊤
  3. ¬¬x→x
  4. x→(¬x→y)
  5. (x∧y)→x
  6. (x∧y)→y
  7. (x→z)→((y→z)→((x∨y)→z))

Several Hilbert systems

not just a method, rather a family of methods

same mechanism, different variants

several exists just for propositional logic

some employ axioms, other axiom schemes (next slide)


Substitution vs. axiom scheme

use axiom schemes instead of axioms

axiom
a formula
axiom scheme
an infinite set of formulae
specified by a single formula in which each variable can be replaced by an arbitrary formula

axiom schemes makes substitution unnecessary


Other Hilbert systems

Frege
uses only and ¬
  1. six axioms
  2. modus ponens + substitution
Russell (principia mathematica)
only and ¬

A minimalistic system

see (Fitting):