Detailed syntax breakdown of Definition df-ex
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | kt 8 |
. 2
term ⊤ |
| 2 | | tex 123 |
. . 3
term ∃ |
| 3 | | hal |
. . . . 5
type α |
| 4 | | hb 3 |
. . . . 5
type ∗ |
| 5 | 3, 4 | ht 2 |
. . . 4
type (α → ∗) |
| 6 | | vp |
. . . 4
var p |
| 7 | | tal 122 |
. . . . 5
term ∀ |
| 8 | | vq |
. . . . . 6
var q |
| 9 | | vx |
. . . . . . . . 9
var x |
| 10 | 5, 6 | tv 1 |
. . . . . . . . . . 11
term p:(α
→ ∗) |
| 11 | 3, 9 | tv 1 |
. . . . . . . . . . 11
term x:α |
| 12 | 10, 11 | kc 5 |
. . . . . . . . . 10
term (p:(α
→ ∗)x:α) |
| 13 | 4, 8 | tv 1 |
. . . . . . . . . 10
term q:∗ |
| 14 | | tim 121 |
. . . . . . . . . 10
term ⇒ |
| 15 | 12, 13, 14 | kbr 9 |
. . . . . . . . 9
term [(p:(α
→ ∗)x:α) ⇒ q:∗] |
| 16 | 3, 9, 15 | kl 6 |
. . . . . . . 8
term λx:α
[(p:(α → ∗)x:α)
⇒ q:∗] |
| 17 | 7, 16 | kc 5 |
. . . . . . 7
term (∀λx:α
[(p:(α → ∗)x:α)
⇒ q:∗]) |
| 18 | 17, 13, 14 | kbr 9 |
. . . . . 6
term [(∀λx:α
[(p:(α → ∗)x:α)
⇒ q:∗]) ⇒ q:∗] |
| 19 | 4, 8, 18 | kl 6 |
. . . . 5
term λq:∗ [(∀λx:α
[(p:(α → ∗)x:α)
⇒ q:∗]) ⇒ q:∗] |
| 20 | 7, 19 | kc 5 |
. . . 4
term (∀λq:∗ [(∀λx:α
[(p:(α → ∗)x:α)
⇒ q:∗]) ⇒ q:∗]) |
| 21 | 5, 6, 20 | kl 6 |
. . 3
term λp:(α
→ ∗) (∀λq:∗ [(∀λx:α
[(p:(α → ∗)x:α)
⇒ q:∗]) ⇒ q:∗]) |
| 22 | | ke 7 |
. . 3
term = |
| 23 | 2, 21, 22 | kbr 9 |
. 2
term [∃
= λp:(α → ∗) (∀λq:∗ [(∀λx:α
[(p:(α → ∗)x:α)
⇒ q:∗]) ⇒ q:∗])] |
| 24 | 1, 23 | wffMMJ2 11 |
1
wff ⊤⊧[∃ = λp:(α
→ ∗) (∀λq:∗ [(∀λx:α
[(p:(α → ∗)x:α)
⇒ q:∗]) ⇒ q:∗])] |
