Filter
Top Products
9.1. LOGICAL RULES 73
#let th1 = REFL ‘x:num‘;;
th1 : thm = |- x = x
#let th2 = GEN ‘x:num‘ th1;;
th2 : thm = |- !x. x = x
#let th3 = GEN ‘y:num‘ th2;;
th3 : thm = |- !y x. x = x
#let th4 = ASSUME ‘x = 2‘;;
th4 : thm = x = 2 |- x = 2
#let th5 = GEN ‘x:num‘ th4;;
Uncaught exception: Failure "GEN"
#let th5 = GEN ‘y:num‘ th4;;
th5 : thm = x = 2 |- !y. x = 2
Γ p[t/x]
Γ ∃x. p
EXISTS
The ML invocations for this rule are relatively complicated; the function requires
the user to specify the desired form of the result and the term t to choose. It could
work out the latter for itself, but in general one can derive many existential theorems
from the same starting point, e.g.
#let th1 = REFL ‘1‘;;
th1 : thm = |- 1 = 1
#let th2 = EXISTS(‘?x. x = 1‘,‘1‘) th1;;
th2 : thm = |- ?x. x = 1
#let th3 = EXISTS(‘?x:num. x = x‘,‘1‘) th1;;
th3 : thm = |- ?x. x = x
#let th4 = EXISTS(‘?x:num. 1 = 1‘,‘23‘) th1;;
th4 : thm = |- ?x. 1 = 1
Γ q
Γ − {p} (∃x. p) ⇒ q
CHOOSE
This rule requires that x is not free in q nor in any of the Γ besides p.
Γ p
Γ p ∨ q
DISJ1
Γ q
Γ p ∨ q
DISJ2
Γ r Γ
r ∆ p ∨ q
(Γ − {p}) ∪ (Γ
− {q}) ∪ ∆ r
DISJ CASES
Γ ¬p
Γ p ⇒ ⊥
NOT ELIM
Γ p ⇒ ⊥
Γ ¬p
NOT INTRO
Γ p ≡ ⊥
Γ ¬p
EQF ELIM
Γ ¬p
Γ p ≡ ⊥
EQF INTRO