HOLE Home Higher-Order Logic Explorer This is the Unicode version.
Change to GIF version

List of Syntax, Axioms (ax-) and Definitions (df-)
RefExpression (see link for any distinct variable requirements)
tv 1term x:α
ht 2type (αβ)
hb 3type
hi 4type ι
kc 5term (FT)
kl 6term λx:α T
ke 7term =
kt 8term
kbr 9term [AFB]
kct 10term (A, B)
wffMMJ2 11wff AB
wffMMJ2t 12wff A:α
ax-syl 15RS    &   ST       RT
ax-jca 17RS    &   RT       R⊧(S, T)
ax-simpl 20R:∗    &   S:∗       (R, S)⊧R
ax-simpr 21R:∗    &   S:∗       (R, S)⊧S
ax-id 24R:∗       RR
ax-trud 26R:∗       R⊧⊤
ax-cb1 29RA       R:∗
ax-cb2 30RA       A:∗
wctl 31(S, T):∗       S:∗
wctr 32(S, T):∗       T:∗
weq 38 = :(α → (α → ∗))
ax-refl 39A:α       ⊤⊧(( = A)A)
ax-eqmp 42RA    &   R⊧(( = A)B)       RB
ax-ded 43(R, S)⊧T    &   (R, T)⊧S       R⊧(( = S)T)
wct 44S:∗    &   T:∗       (S, T):∗
wc 45F:(αβ)    &   T:α       (FT):β
ax-ceq 46F:(αβ)    &   T:(αβ)    &   A:α    &   B:α       ((( = F)T), (( = A)B))⊧(( = (FA))(TB))
wv 58x:α:α
wl 59T:β       λx:α T:(αβ)
ax-beta 60A:β       ⊤⊧(( = (λx:α Ax:α))A)
ax-distrc 61A:β    &   B:α    &   F:(βγ)       ⊤⊧(( = (λx:α (FA)B))((λx:α FB)(λx:α AB)))
ax-leq 62A:β    &   B:β    &   R⊧(( = A)B)       R⊧(( = λx:α A)λx:α B)
ax-distrl 63A:γ    &   B:α       ⊤⊧(( = (λx:α λy:β AB))λy:β (λx:α AB))
wov 64F:(α → (βγ))    &   A:α    &   B:β       [AFB]:γ
df-ov 65F:(α → (βγ))    &   A:α    &   B:β       ⊤⊧(( = [AFB])((FA)B))
eqtypi 69A:α    &   R⊧[A = B]       B:α
eqtypri 71A:α    &   R⊧[B = A]       B:α
ax-hbl1 93A:γ    &   B:α       ⊤⊧[(λx:α λx:β AB) = λx:β A]
ax-17 95A:β    &   B:α       ⊤⊧[(λx:α AB) = A]
ax-inst 103RA    &   ⊤⊧[(λx:α By:α) = B]    &   ⊤⊧[(λx:α Sy:α) = S]    &   [x:α = C]⊧[A = B]    &   [x:α = C]⊧[R = S]       SB
tfal 108term
tan 109term
tne 110term ¬
tim 111term
tal 112term
tex 113term
tor 114term
teu 115term ∃!
df-al 116⊤⊧[ = λp:(α → ∗) [p:(α → ∗) = λx:α ⊤]]
df-fal 117⊤⊧[⊥ = (λp:∗ p:∗)]
df-an 118⊤⊧[ = λp:∗ λq:∗ [λf:(∗ → (∗ → ∗)) [p:∗f:(∗ → (∗ → ∗))q:∗] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]]
df-im 119⊤⊧[ ⇒ = λp:∗ λq:∗ [[p:∗ q:∗] = p:∗]]
df-not 120⊤⊧[¬ = λp:∗ [p:∗ ⇒ ⊥]]
df-ex 121⊤⊧[ = λp:(α → ∗) (λq:∗ [(λx:α [(p:(α → ∗)x:α) ⇒ q:∗]) ⇒ q:∗])]
df-or 122⊤⊧[ = λp:∗ λq:∗ (λx:∗ [[p:∗ ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]])]
df-eu 123⊤⊧[∃! = λp:(α → ∗) (λy:α (λx:α [(p:(α → ∗)x:α) = [x:α = y:α]]))]
wffMMJ2d 161wff typedef α(A, B)C
wabs 162B:α    &   F:(α → ∗)    &   ⊤⊧(FB)    &   typedef β(A, R)F       A:(αβ)
wrep 163B:α    &   F:(α → ∗)    &   ⊤⊧(FB)    &   typedef β(A, R)F       R:(βα)
ax-tdef 164B:α    &   F:(α → ∗)    &   ⊤⊧(FB)    &   typedef β(A, R)F       ⊤⊧((λx:β [(A(Rx:β)) = x:β]), (λx:α [(Fx:α) = [(R(Ax:α)) = x:α]]))
ax-eta 165⊤⊧(λf:(αβ) [λx:α (f:(αβ)x:α) = f:(αβ)])
tf11 177term 1-1
tfo 178term onto
tat 179term ε
wat 180ε:((α → ∗) → α)
df-f11 181⊤⊧[1-1 = λf:(αβ) (λx:α (λy:α [[(f:(αβ)x:α) = (f:(αβ)y:α)] ⇒ [x:α = y:α]]))]
df-fo 182⊤⊧[onto = λf:(αβ) (λy:β (λx:α [y:β = (f:(αβ)x:α)]))]
ax-ac 183⊤⊧(λp:(α → ∗) (λx:α [(p:(α → ∗)x:α) ⇒ (p:(α → ∗)(εp:(α → ∗)))]))
ax-inf 189⊤⊧(λf:(ιι) [(1-1 f:(ιι)) (¬ (onto f:(ιι)))])
  Copyright terms: Public domain W3C validator