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:∗
ax-wctl 31(S, T):∗       S:∗
ax-wctr 32(S, T):∗       T:∗
ax-weq 40 = :(α → (α → ∗))
ax-refl 42A:α       ⊤⊧(( = A)A)
ax-eqmp 45RA    &   R⊧(( = A)B)       RB
ax-ded 46(R, S)⊧T    &   (R, T)⊧S       R⊧(( = S)T)
ax-wct 47S:∗    &   T:∗       (S, T):∗
ax-wc 49F:(αβ)    &   T:α       (FT):β
ax-ceq 51F:(αβ)    &   T:(αβ)    &   A:α    &   B:α       ((( = F)T), (( = A)B))⊧(( = (FA))(TB))
ax-wv 63x:α:α
ax-wl 65T:β       λx:α T:(αβ)
ax-beta 67A:β       ⊤⊧(( = (λx:α Ax:α))A)
ax-distrc 68A:β    &   B:α    &   F:(βγ)       ⊤⊧(( = (λx:α (FA)B))((λx:α FB)(λx:α AB)))
ax-leq 69A:β    &   B:β    &   R⊧(( = A)B)       R⊧(( = λx:α A)λx:α B)
ax-distrl 70A:γ    &   B:α       ⊤⊧(( = (λx:α λy:β AB))λy:β (λx:α AB))
ax-wov 71F:(α → (βγ))    &   A:α    &   B:β       [AFB]:γ
df-ov 73F:(α → (βγ))    &   A:α    &   B:β       ⊤⊧(( = [AFB])((FA)B))
ax-eqtypi 77A:α    &   R⊧[A = B]       B:α
ax-eqtypri 80A:α    &   R⊧[B = A]       B:α
ax-hbl1 103A:γ    &   B:α       ⊤⊧[(λx:α λx:β AB) = λx:β A]
ax-17 105A:β    &   B:α       ⊤⊧[(λx:α AB) = A]
ax-inst 113RA    &   ⊤⊧[(λx:α By:α) = B]    &   ⊤⊧[(λx:α Sy:α) = S]    &   [x:α = C]⊧[A = B]    &   [x:α = C]⊧[R = S]       SB
tfal 118term
tan 119term
tne 120term ¬
tim 121term
tal 122term
tex 123term
tor 124term
teu 125term ∃!
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 171wff typedef α(A, B)C
ax-wabs 172B:α    &   F:(α → ∗)    &   ⊤⊧(FB)    &   typedef β(A, R)F       A:(αβ)
ax-wrep 173B:α    &   F:(α → ∗)    &   ⊤⊧(FB)    &   typedef β(A, R)F       R:(βα)
ax-tdef 176B:α    &   F:(α → ∗)    &   ⊤⊧(FB)    &   typedef β(A, R)F       ⊤⊧((λx:β [(A(Rx:β)) = x:β]), (λx:α [(Fx:α) = [(R(Ax:α)) = x:α]]))
ax-eta 177⊤⊧(λf:(αβ) [λx:α (f:(αβ)x:α) = f:(αβ)])
tf11 189term 1-1
tfo 190term onto
tat 191term ε
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:(ιι)))])
  Copyright terms: Public domain W3C validator