Commit 724b7944 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

hol.md, suite

parent 0e7d57fe
......@@ -21,7 +21,7 @@ All starts with (polymorphic) simply-typed lambda-calculus.
- Two predifined constants : `(=) : α → α → bool` and `ε : (α → bool) → α` (Hilbert choice operator).
Syntax : `t = u` is just `(((=) t) u)`.
And when `p` and `q` are of type `bool` (hence propositions), `p = q` is rather written `p q`.
And when `p` and `q` are of type `bool` (hence propositions), `p = q` is rather written `p <=> q`.
#### The deducibility predicate
......@@ -58,13 +58,13 @@ This deducibility predicate is obtained through the following ten inference rule
----------- (ASSUME)
{p} ⊢ p
Γ ⊢ p q ∆ ⊢ p
--------------------- (EQ_MP)
Γ ⊢ p <=> q ∆ ⊢ p
----------------------- (EQ_MP)
Γ ∪ ∆ ⊢ q
Γ ⊢ p ∆ ⊢ q
------------------------------- (DEDUCT_ANTISYM_RULE)
(Γ − {q}) ∪ (∆ − {p}) ⊢ p q
--------------------------------- (DEDUCT_ANTISYM_RULE)
(Γ − {q}) ∪ (∆ − {p}) ⊢ p <=> q
Γ[x1,...,xn] ⊢ p[x1,...,xn]
---------------------------- (INST)
......@@ -76,21 +76,65 @@ This deducibility predicate is obtained through the following ten inference rule
```
Actually, three extra axioms :
- Extensionality via `ETA_AX` : `⊢ (λx.(t x)) = t`.
- `SELECT_AX` stating that Hilbert operator `ε` is a choice operator : `⊢ P x ==> P(ε(P))`. See below for the definition of implication `==>`. This axiom is the only one that implies that HOL-Light is a classical logic.
- `INFINITY_AX` stating that the `ind` type of individuals is infinite.
## The other logical connectives
On top of predefined equality `=` (and hence equivalence `⇔` on propositions), the other logical connectives are "syntactic sugar" :
On top of predefined equality `=` (and hence equivalence `<=>` on propositions), the other logical connectives are "syntactic sugar" :
```
T := (λp. p) = (λp. p)
p /\ q := (λf. f p q) = (λf. f T T)
p ==> q := (p /\ q) <=> p
∀P := P = (λx. T)
∃P := ∀q. (∀x. P(x) ==> q) ==> q
p ‌\/ q := ∀r. (p ==> r) ==> (q ==> r) ==> r
⊥ := ∀p. p
¬p := p ==> ⊥
```
Note that `∀x.P(x)` (actually written `!x.P(x)` in HOL-Light syntax) is a notation for `∀P` or equivalently `∀(λx.P(x))`. Similarly, `∃x.P(x)` (written `?x.P(x)` in HOL-Light) is `∃P` or `∃(λx.P(x))`.
The HOL-Light syntax for `⊥` is `F` and `¬` is `~`.
## Some elementary proofs
#### Symmetry of equality
The symmetry rule (`Γ ⊢ s = t` implies `Γ ⊢ t = s`) is admissible (i.e. can be "emulated" via the other rules).
```
T := (λp. p) = (λp. p)
p ∧ q := (λf. f p q) = (λf. f T T)
p ⇒ q := (p ∧ q) ⇔ p
∀P := P = (λx. T)
∃P := ∀q. (∀x. P (x) ⇒ q) ⇒ q
p ∨ q := ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊥ := ∀p. p
¬ := p ⇒ ⊥
∃!P := ∃P ∧ (∀x. ∀y. P x ∧ P y ⇒ x = y)
------------ REFL
⊢ (=) = (=) Γ ⊢ s = t
------------------------------ MK_COMB --------- REFL
Γ ⊢ ((=) s) = ((=) t) ⊢ s = s
-------------------------------------------------- MK_COMB --------- REFL
Γ ⊢ (s = s) <=> (t = s) ⊢ s = s
---------------------------------------------------------------------- EQ_MP
Γ ⊢ t = s
```
And `∀x.P x` is a notation for `∀(λx.(P x))`, and similarly `∃x.P x` is `∃(λx.(P x))`.
#### Transitivity
Transitivity is one of the basic rules (for efficiency reasons). But it can actually be derived from the other rules.
```
---------------------- REFL
⊢ ((=) s) = ((=) s) Δ ⊢ t = u
---------------------------------------- MK_COMB
Δ ⊢ (s = t) <=> (s = u) Γ ⊢ s = t
------------------------------------------------------------ EQ_MP
Γ ∪ ∆ ⊢ s = u
```
#### Natural deduction
Exercise : retreive the usual introduction and elimination rules for `T`, `/\`, `==>`, ``, ``, `\/`, ``, `¬`.
Exercise(++) : retreive at least one classical law from `SELECT_AX`.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment