List of Syntax, Axioms (ax-) and
Definitions (df-)|
Ref | Expression (see link for any distinct variable requirements)
|
| tv 1 | term x:α |
| ht 2 | type (α →
β) |
| hb 3 | type ∗ |
| hi 4 | type ι |
| kc 5 | term (FT) |
| kl 6 | term λx:α
T |
| ke 7 | term = |
| kt 8 | term ⊤ |
| kbr 9 | term [AFB] |
| kct 10 | term (A, B) |
| wffMMJ2 11 | wff
A⊧B |
| wffMMJ2t 12 | wff
A:α |
| ax-syl 15 | ⊢ R⊧S
& ⊢ S⊧T ⇒ ⊢ R⊧T |
| ax-jca 17 | ⊢ R⊧S
& ⊢ R⊧T ⇒ ⊢ R⊧(S,
T) |
| ax-simpl 20 | ⊢ R:∗
& ⊢ S:∗ ⇒ ⊢ (R, S)⊧R |
| ax-simpr 21 | ⊢ R:∗
& ⊢ S:∗ ⇒ ⊢ (R, S)⊧S |
| ax-id 24 | ⊢ R:∗ ⇒ ⊢ R⊧R |
| ax-trud 26 | ⊢ R:∗ ⇒ ⊢ R⊧⊤ |
| ax-cb1 29 | ⊢ R⊧A ⇒ ⊢ R:∗ |
| ax-cb2 30 | ⊢ R⊧A ⇒ ⊢ A:∗ |
| ax-wctl 31 | ⊢ (S, T):∗ ⇒ ⊢ S:∗ |
| ax-wctr 32 | ⊢ (S, T):∗ ⇒ ⊢ T:∗ |
| ax-weq 40 | ⊢ = :(α
→ (α →
∗)) |
| ax-refl 42 | ⊢ A:α ⇒ ⊢ ⊤⊧(( = A)A) |
| ax-eqmp 45 | ⊢ R⊧A
& ⊢ R⊧(( =
A)B) ⇒ ⊢ R⊧B |
| ax-ded 46 | ⊢ (R, S)⊧T
& ⊢ (R, T)⊧S ⇒ ⊢ R⊧(( =
S)T) |
| ax-wct 47 | ⊢ S:∗
& ⊢ T:∗ ⇒ ⊢ (S, T):∗ |
| ax-wc 49 | ⊢ F:(α → β)
& ⊢ T:α ⇒ ⊢ (FT):β |
| ax-ceq 51 | ⊢ F:(α → β)
& ⊢ T:(α → β)
& ⊢ A:α
& ⊢ B:α ⇒ ⊢ ((( = F)T), (( =
A)B))⊧(( = (FA))(TB)) |
| ax-wv 63 | ⊢ x:α:α |
| ax-wl 65 | ⊢ T:β ⇒ ⊢ λx:α
T:(α → β) |
| ax-beta 67 | ⊢ A:β ⇒ ⊢ ⊤⊧(( = (λx:α
Ax:α))A) |
| ax-distrc 68 | ⊢ A:β
& ⊢ B:α
& ⊢ F:(β → γ) ⇒ ⊢ ⊤⊧(( = (λx:α
(FA)B))((λx:α
FB)(λx:α
AB))) |
| ax-leq 69 | ⊢ A:β
& ⊢ B:β
& ⊢ R⊧(( =
A)B) ⇒ ⊢ R⊧(( =
λx:α A)λx:α
B) |
| ax-distrl 70 | ⊢ A:γ
& ⊢ B:α ⇒ ⊢ ⊤⊧(( = (λx:α
λy:β AB))λy:β
(λx:α AB)) |
| ax-wov 71 | ⊢ F:(α → (β → γ))
& ⊢ A:α
& ⊢ B:β ⇒ ⊢ [AFB]:γ |
| df-ov 73 | ⊢ F:(α → (β → γ))
& ⊢ A:α
& ⊢ B:β ⇒ ⊢ ⊤⊧(( = [AFB])((FA)B)) |
| ax-eqtypi 77 | ⊢ A:α
& ⊢ R⊧[A =
B] ⇒ ⊢ B:α |
| ax-eqtypri 80 | ⊢ A:α
& ⊢ R⊧[B =
A] ⇒ ⊢ B:α |
| ax-hbl1 103 | ⊢ A:γ
& ⊢ B:α ⇒ ⊢ ⊤⊧[(λx:α
λx:β AB) =
λx:β A] |
| ax-17 105 | ⊢ A:β
& ⊢ B:α ⇒ ⊢ ⊤⊧[(λx:α
AB) =
A] |
| ax-inst 113 | ⊢ R⊧A
& ⊢ ⊤⊧[(λx:α
By:α) =
B]
& ⊢ ⊤⊧[(λx:α
Sy:α) =
S]
& ⊢ [x:α = C]⊧[A =
B]
& ⊢ [x:α = C]⊧[R =
S] ⇒ ⊢ S⊧B |
| tfal 118 | term ⊥ |
| tan 119 | term ∧ |
| tne 120 | term ¬ |
| tim 121 | term ⇒ |
| tal 122 | term ∀ |
| tex 123 | term ∃ |
| tor 124 | term
∨ |
| teu 125 | term ∃! |
| df-al 126 | ⊢ ⊤⊧[∀ = λp:(α
→ ∗) [p:(α → ∗) =
λx:α ⊤]] |
| df-fal 127 | ⊢ ⊤⊧[⊥ = (∀λp:∗ p:∗)] |
| df-an 128 | ⊢ ⊤⊧[ ∧ = λp:∗ λq:∗ [λf:(∗ → (∗ → ∗))
[p:∗f:(∗ → (∗ →
∗))q:∗] =
λf:(∗ → (∗
→ ∗)) [⊤f:(∗
→ (∗ → ∗))⊤]]] |
| df-im 129 | ⊢ ⊤⊧[ ⇒ =
λp:∗
λq:∗ [[p:∗ ∧
q:∗] = p:∗]] |
| df-not 130 | ⊢ ⊤⊧[¬ = λp:∗ [p:∗ ⇒ ⊥]] |
| df-ex 131 | ⊢ ⊤⊧[∃ = λp:(α
→ ∗) (∀λq:∗ [(∀λx:α
[(p:(α → ∗)x:α)
⇒ q:∗]) ⇒ q:∗])] |
| df-or 132 | ⊢ ⊤⊧[
∨ = λp:∗
λq:∗ (∀λx:∗ [[p:∗ ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]])] |
| df-eu 133 | ⊢ ⊤⊧[∃! = λp:(α
→ ∗) (∃λy:α (∀λx:α
[(p:(α → ∗)x:α) =
[x:α = y:α]]))] |
| wffMMJ2d 171 | wff
typedef α(A, B)C |
| ax-wabs 172 | ⊢ B:α
& ⊢ F:(α → ∗) & ⊢ ⊤⊧(FB) & ⊢ typedef β(A,
R)F ⇒ ⊢ A:(α → β) |
| ax-wrep 173 | ⊢ B:α
& ⊢ F:(α → ∗) & ⊢ ⊤⊧(FB) & ⊢ typedef β(A,
R)F ⇒ ⊢ R:(β → α) |
| ax-tdef 176 | ⊢ B:α
& ⊢ F:(α → ∗) & ⊢ ⊤⊧(FB) & ⊢ typedef β(A,
R)F ⇒ ⊢ ⊤⊧((∀λx:β
[(A(Rx:β)) = x:β]),
(∀λx:α
[(Fx:α) =
[(R(Ax:α)) = x:α]])) |
| ax-eta 177 | ⊢ ⊤⊧(∀λf:(α
→ β) [λx:α
(f:(α → β)x:α) =
f:(α → β)]) |
| tf11 189 | term 1-1 |
| tfo 190 | term onto |
| tat 191 | term ε |
| ax-wat 192 | ⊢ ε:((α → ∗) → α) |
| df-f11 194 | ⊢ ⊤⊧[1-1 = λf:(α
→ β) (∀λx:α (∀λy:α
[[(f:(α → β)x:α) =
(f:(α → β)y:α)]
⇒ [x:α = y:α]]))] |
| df-fo 195 | ⊢ ⊤⊧[onto = λf:(α
→ β) (∀λy:β (∃λx:α
[y:β = (f:(α
→ β)x:α)]))] |
| ax-ac 196 | ⊢ ⊤⊧(∀λp:(α
→ ∗) (∀λx:α
[(p:(α → ∗)x:α)
⇒ (p:(α → ∗)(εp:(α
→ ∗)))])) |
| ax-inf 202 | ⊢ ⊤⊧(∃λf:(ι → ι) [(1-1 f:(ι → ι)) ∧ (¬ (onto f:(ι → ι)))]) |
