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
-
- x→(y→x)
- (x→(y→z))→((x→y)→(x→z))
- rules
-
A |
substitution |
(x variable, B formula) |
A[B/x] |
How it works
proof=sequence of formulae
where each formula is either:
- an axiom
- obtained by applying a rule to some previous ones
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:
- which axioms to use?
- which rules to apply?
- possible to keep running forever
pros:
- proof relatively easy to understand
- only known method for some logics
- shortest proofs
(in theory: proof complexity)
Axioms for the other connectives
- ⊥→x
- x→⊤
- ¬¬x→x
- x→(¬x→y)
- (x∧y)→x
- (x∧y)→y
- (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 ¬
- six axioms
- modus ponens + substitution
- Russell (principia mathematica)
- only ∨ and ¬
- five axioms
(the fourth was later proved to be consequence of the others)
- substitution + variant of modus ponens:
A minimalistic system
see (Fitting):
- only ↑
("nand": x↑y=¬(x∧y))
- rule:
- axiom scheme:
(x↑(y↑z)) ↑
( ((w↑z)↑((x↑w)↑(x↑w)))
↑
(x↑(x↑y))
)