Difference between revisions of "Hilbert System"
m |
m (→Extension Axioms) |
||
| Line 221: | Line 221: | ||
*<math>\,\phi\wedge\psi \to\psi</math> ( \wedge -elimination) | *<math>\,\phi\wedge\psi \to\psi</math> ( \wedge -elimination) | ||
| − | * | + | * ψ → φ ∨ ψ |
| − | * | + | * φ ∨ ψ → ψ ( ∨-introduction) |
| − | * | + | * (φ → α) → ((ψ → α) → ((φ ∨ ψ) → α)) ( ∨-elimination) |
==A Final Note== | ==A Final Note== | ||
Revision as of 14:01, 15 June 2010
This page summarizes the basics of the Hilbert-style proof system. You may be interested in Natural Deduction, and an extension of this proof theory to the normal Modal Logic K, and to the Predicate Logic.
Contents
Overview
A Hilbert-style proof is just a sequence of formulas with justifications. Each line in a proof must be one of the following:
- an (instance of) axiom
- the result of applying Modus Ponens
- a hypothesis (i.e., a given formula, a.k.a. an assumption)
- a theorem (i.e., any theorem derived in class or by you)
<math>\Phi\vdash\phi</math> reads <math>\,\phi</math> is provable from <math>\,\Phi</math>.
<math>\vdash\phi</math> simply reads <math>\,\phi</math> is provable.
The Hilbert system is sound (if <math>\,\vdash\phi</math> then <math>\,\phi</math> is a tautology) and complete (if <math>\,\phi</math> is a tautology then <math>\,\vdash\phi</math>).
Axiom Schema
Hilbert system (denoted as H) provides rules for implication only. Only negation (<math>\lnot</math>) and implication (<math>\to</math>) are considered primitive, other connectives can occur in proofs only when the standard Hilbert system is extended (as shown in later sections on Conservative Extensions). Obviously, we know the two connectives form an adequate set of connectives for boolean logic.
We have three axioms (some textbooks may employ different axioms) in an axiom schema (which are tautologies) as follows in a standard H system.
- Axiom 1: A <math>\to</math> (B <math>\to</math> A)
- Axiom 2: (A <math>\to</math> (B <math>\to</math> C)) <math>\to</math> ((A <math>\to</math> B) <math>\to</math> (A <math>\to</math> C))
- Axiom 3: (<math>\neg</math>A <math>\to</math> <math>\neg</math>B) <math>\to</math> (B <math>\to</math> A)
They are considered axiom schema because we assume all instances of them that can be obtained by uniformly substituting formulae for A, B and C. For instance, we can get P <math>\to</math> (P <math>\to</math> P) from axiom 1. Every axiom above denotes essentially an infinite set of formulae.
Axioms
Axioms are rules without any premises. For example, we have the following rule (MP) in the Hilbert system, but we have many rules in Natural Deduction. On the contrary, we have three axioms in the Hilbert system, but only have one axiom (LEM) in Natural Deduction.
- Modus Ponens: <math>\frac{A \to B, A}{B}</math>.
MP together with three axioms suffice to prove all tautologies of propositional logic.
Proofs and Theorems
Lemmas
Lemmas are just theorems, so they can be used in proofs. However, if you have not proven them, you cannot take them for granted!
Lemma 0.1
If <math>\,\phi</math> is an axiom, then <math>\,\Phi\vdash\phi</math>.
Lemma 0.2
If <math>\,\phi\in\Phi</math>, then <math>\,\Phi\vdash\phi</math>.
Lemma 0.3
If <math>\,\Gamma \vdash \phi</math>, then <math>\,\Gamma\cup\Delta\vdash\phi</math>
The First Proof
- Theorem 1: <math>\quad\vdash_H A\to A</math>
1. A <math>\to</math> ((A<math>\to</math>A) <math>\to</math> A) <math>\quad</math> Axiom 1
2. (A <math>\to</math> ((A<math>\to</math>A) <math>\to</math> A)) <math>\to</math> ((A <math>\to</math> (A <math>\to</math> A)) <math>\to</math> (A <math>\to</math> A)) <math>\quad</math> Axiom 2
3. (A <math>\to</math> (A <math>\to</math> A)) <math>\to</math> (A <math>\to</math> A) <math>\quad</math> Modus Ponens, 1,2.
4. A <math>\to</math> (A <math>\to</math> A) <math>\quad</math> Axiom 1
5. A <math>\to</math> A <math>\quad</math> Modus Ponens, 3,4.
<math>\blacksquare</math>
We have proven <math>\vdash_H A\to A</math>, and any instance of it can be used in future proofs.
Proof using Hypotheses
Hypotheses (or Given, or Assumption) must be used exactly as stated, i.e., they can not be instantiated. This is different from the application of axioms.
Let's do a proof for this theorem:
- Theorem 2: <math>\quad A \to (B \to C), A \to B \vdash_H A \to C</math>
1. A <math>\to</math> (B <math>\to</math> C) <math>\quad</math> Hypotheses (or Given/Assumption)
2. A <math>\to</math> B <math>\quad</math> Hypotheses
3. (A <math>\to</math> (B <math>\to</math> C)) <math>\to</math> ((A <math>\to</math> B) <math>\to</math> (A <math>\to</math> C)) <math>\quad</math> Axiom 2
4. (A <math>\to</math> B) <math>\to</math> (A <math>\to</math> C) <math>\quad</math> Modus Ponens, 1,3.
5. A <math>\to</math> C <math>\quad</math> Modus Ponens, 2,4.
<math>\blacksquare</math>
Note that if you can prove a formula with less hypotheses than given, it is fine, as shown in Lemma 0.3. E.g., if we can prove <math>A\vdash A</math>, then we can conclude <math>A\cup\Phi\vdash A</math> with <math>\,\Phi</math> being any set of formulas.
Deduction Theorem
- Deduction Theorem (Herbrand 1930). <math>\quad \Phi \cup \{\phi\} \vdash_H \psi</math> <math>\quad\quad</math>iff<math>\quad\quad</math> <math>\Phi \vdash_H \phi \to \psi</math>.
Note that <math>\Phi\,</math> refers to a set of formulas. This theorem is an elegant shortcut to prove Theorem 2, for we can do the following (an informal proof of Theorem 2 above):
1. (A <math>\to</math> (B <math>\to</math> C)) <math>\to</math> ((A <math>\to</math> B) <math>\to</math> (A <math>\to</math> C)) <math>\quad</math> Axiom 2
2. A <math>\to</math> (B <math>\to</math> C) <math>\vdash_H</math> (A <math>\to</math> B) <math>\to</math> (A <math>\to</math> C) <math>\quad</math> Deduction Theorem
3. A <math>\to</math> (B <math>\to</math> C), A <math>\to</math> B <math>\vdash_H</math> (A <math>\to</math> B) <math>\to</math> (A <math>\to</math> C) <math>\quad</math> Deduction Theorem
Remarks about Deduction Theorem
The deduction theorem is not a theorem of the Hilbert system, so it is called a meta-theorem, meaning that it is a theorem about the Hilbert system.
This theorem says that if we have a proof of <math>p \vdash_H q</math>, then we are guaranteed that a proof of <math>\vdash_H p \to q</math> exists. Since the deduction theorem is not really a rule, an axiom, or a theorem of L, it is technically incorrect to use it as a justification for a line in a formal proof. However, we allow this sometimes.
If we use the deduction theorem to show that a proof <math>\vdash_H p \to q</math> exists, then sure enough, a formal proof in H of <math>p \to q</math> does exist, which doesn't use the deduction theorem. The deduction theorem does save time for proofs.
The Semantics behind Deduction Theorem
Without loss of generality, we want to show that a given set of formulas, say <math>\Phi\,</math>, entails <math>\phi\,</math>, i.e., <math>\underbrace{\Phi\vDash\phi}_{}</math>.
In fact, we know that <math>\Phi\vDash\phi</math> holds IFF <math>\Phi_{\land}\land\neg\phi</math> is unsatisfiable, where the subscript symbol in <math>\Phi_{\land}</math> means the conjunction of all formulas in <math>\Phi</math>. To wit, we want to show <math>\neg(\Phi_{\land}\land\neg\phi)</math> is a tautology. That is, IFF (<math>\,\neg\Phi_{\land}\lor\phi</math>) is a tautology, which can be denoted as <math>\vDash(\,\neg\Phi_{\land}\lor\phi)</math>. Note that this is exactly <math>\underbrace{\,\vDash(\,\Phi_{\land}\to\phi)}_{}</math>.
More Proofs/Theorems
- Theorem 3: <math>\{A\to B, B\to C\}\quad\vdash_H\quad A\to C </math>
1. B <math>\to</math> C Hypotheses
2. (B <math>\to</math> C) <math>\to</math> (A <math>\to</math> (B <math>\to</math> C)) Axiom 1
3. A <math>\to</math> (B <math>\to</math> C) Modus Ponens, 1,2.
4. (A <math>\to</math> (B <math>\to</math> C)) <math>\to</math> ((A <math>\to</math> B) <math>\to</math> (A <math>\to</math> C)) Axiom 2
5. (A <math>\to</math> B) <math>\to</math> (A <math>\to</math> C) Modus Ponens, 3,4.
6. A <math>\to</math> B Hypotheses
7. A <math>\to</math> C Modus Ponens, 5, 6.
<math>\blacksquare</math>
- Theorem 4: <math>\vdash_H\quad \neg A\to(A\to B)</math>
1. <math>\neg</math>A <math>\to</math> (<math>\neg</math>B <math>\to</math> <math>\neg</math>A) Axiom 1
2. (<math>\neg</math>B <math>\to</math> <math>\neg</math>A) <math>\to</math> (A <math>\to</math> B) Axiom 3
3. <math>\neg</math>A <math>\to</math> (A <math>\to</math> B) Theorem 3, 1,3.
<math>\blacksquare</math>
Note that Theorem 3 is applied to the last line in the above proof, as it is a theorem proven in the Hilbert system.
- Another proof for Theorem 4: <math>\vdash_H\quad \neg A\to(A\to B)</math>
Proof.
1. <math>\neg A\vdash_H\quad (A\to B)</math> Deduction Theorem
2. <math>\neg A\to (\neg B\to \neg A)</math> Axiom 1
3. <math>\neg A</math> Hypotheses, line 1
4. <math>\neg B\to \neg A</math> Modus Ponens
5. <math>A\to B</math> Axiom 3
<math>\blacksquare</math>
- Theorem 5: <math>\vdash_H\quad (\neg\phi\to\phi)\to\phi</math>
1. By deduction theorem, we are to prove <math>(\neg\phi\to\phi)\vdash_H\phi</math>.
2. <math>\neg\phi\to(\phi\to\neg(\neg\phi\to\phi))</math> Theorem 4
3. <math>\neg\phi\to(\phi\to\neg(\neg\phi\to\phi)) \to (\neg\phi\to\phi)\to(\neg\phi\to\neg(\neg\phi\to\phi))</math> Axiom 2
4. <math>(\neg\phi\to\phi)\to(\neg\phi\to\neg(\neg\phi\to\phi))</math> Modus Ponens
5. <math>\neg\phi\to\phi</math> Hypothesis
6. <math>\neg\phi\to\neg(\neg\phi\to\phi)</math> Modus Ponens, 4,5.
7. <math>\neg\phi\to\neg(\neg\phi\to\phi) \to ((\neg\phi\to\phi)\to\phi)</math> Axiom 3
8. <math>(\neg\phi\to\phi)\to\phi</math> Modus Ponens, 6,7.
9. <math>\,\phi\,</math> Modus Ponens, 5,8.
<math>\blacksquare</math>
- Theorem 6: <math>\vdash_H\neg\neg\phi\to\phi</math>
Proof.
By deduction theorem, we are to prove: <math>\neg\neg\phi\vdash_H\phi</math>
1. <math>\neg\neg\phi\to(\neg\neg\neg\neg\phi\to\neg\neg\phi)</math> Axiom 1
2. <math>\neg\neg\neg\neg\phi\to\neg\neg\phi</math> Modus Ponens, hypothesis and line 1
3. <math>\neg\phi\to\neg\neg\neg\phi</math> Axiom 3 and Modus Ponens, 2.
4. <math>\neg\neg\phi\to\phi</math> Axiom 3 and Modus Ponens, line 3
<math>\blacksquare</math>
Modifying the Hilbert System
We can modify the three axioms in our previously defined H system to obtain a new system, still retaining soundness and completeness. We can discard, add axioms or starting from scratch.
Adding tautologies to H will still get H, but adding non-tautologies to H will return us a garbage system. To discard an axiom, we have to observe that the axiom is dependent of the other axioms. Here, we look at a new H system, with only one axiom that is sufficient to prove all the tautologies.
Meredith's Axiom
This is the only axiom to be used with Modus Ponens. The theorems of this system are the tautologies, so it is very elegant. But it is too hard to prove theorems in this system.
[((A <math>\to</math> B) <math>\to</math> (<math>\neg</math> C <math>\to</math> <math>\neg</math> D)) <math>\to</math> C ] <math>\to</math> E
<math>\to</math>
[(E <math>\to</math> A) <math>\to</math> (D <math>\to</math> A)]
Conservative Extension
Extension Axioms
If you want to deal with conjunctions in Hilbert systems, the following axioms can be legitimately used.
- <math>\,\phi\to(\psi\to(\phi\wedge\psi))</math> ( \wedge -introduction)
- <math>\,\phi\wedge\psi \to\phi</math>
- <math>\,\phi\wedge\psi \to\psi</math> ( \wedge -elimination)
- ψ → φ ∨ ψ
- φ ∨ ψ → ψ ( ∨-introduction)
- (φ → α) → ((ψ → α) → ((φ ∨ ψ) → α)) ( ∨-elimination)
A Final Note
Compared to Natural Deduction, the Hilbert system is scheme/pattern based, and there is no algorithm showing how to apply the three axioms in order to complete the proof. However, natural deduction rules always provide some clues as they have premises (except the axiom LEM).
The Hilbert system is a human-style way to conduct reasoning, but is not easy to implement for automated reasoning systems. In other words, natural deduction seems to be more amenable to computer applications.
