HOLE Home Higher-Order Logic Explorer This is the GIF version.
Change to Unicode version
List of Syntax, Axioms (ax-) and Definitions (df-)
RefExpression (see link for any distinct variable requirements)
tv 1term x:al
ht 2type (al -> be)
hb 3type *
hi 4type iota
kc 5term (FT)
kl 6term \x:al T
ke 7term =
kt 8term T.
kbr 9term [AFB]
kct 10term (A, B)
wffMMJ2 11wff A |= B
wffMMJ2t 12wff A:al
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 |= T.
ax-cb1 29|- R |= A   =>   |- R:*
ax-cb2 30|- R |= A   =>   |- A:*
wctl 31|- (S, T):*   =>   |- S:*
wctr 32|- (S, T):*   =>   |- T:*
weq 38|- = :(al -> (al -> *))
ax-refl 39|- A:al   =>   |- T. |= (( = A)A)
ax-eqmp 42|- R |= A   &   |- R |= (( = A)B)   =>   |- R |= B
ax-ded 43|- (R, S) |= T   &   |- (R, T) |= S   =>   |- R |= (( = S)T)
wct 44|- S:*   &   |- T:*   =>   |- (S, T):*
wc 45|- F:(al -> be)   &   |- T:al   =>   |- (FT):be
ax-ceq 46|- F:(al -> be)   &   |- T:(al -> be)   &   |- A:al   &   |- B:al   =>   |- ((( = F)T), (( = A)B)) |= (( = (FA))(TB))
wv 58|- x:al:al
wl 59|- T:be   =>   |- \x:al T:(al -> be)
ax-beta 60|- A:be   =>   |- T. |= (( = (\x:al Ax:al))A)
ax-distrc 61|- A:be   &   |- B:al   &   |- F:(be -> ga)   =>   |- T. |= (( = (\x:al (FA)B))((\x:al FB)(\x:al AB)))
ax-leq 62|- A:be   &   |- B:be   &   |- R |= (( = A)B)   =>   |- R |= (( = \x:al A)\x:al B)
ax-distrl 63|- A:ga   &   |- B:al   =>   |- T. |= (( = (\x:al \y:be AB))\y:be (\x:al AB))
wov 64|- F:(al -> (be -> ga))   &   |- A:al   &   |- B:be   =>   |- [AFB]:ga
df-ov 65|- F:(al -> (be -> ga))   &   |- A:al   &   |- B:be   =>   |- T. |= (( = [AFB])((FA)B))
eqtypi 69|- A:al   &   |- R |= [A = B]   =>   |- B:al
eqtypri 71|- A:al   &   |- R |= [B = A]   =>   |- B:al
ax-hbl1 93|- A:ga   &   |- B:al   =>   |- T. |= [(\x:al \x:be AB) = \x:be A]
ax-17 95|- A:be   &   |- B:al   =>   |- T. |= [(\x:al AB) = A]
ax-inst 103|- R |= A   &   |- T. |= [(\x:al By:al) = B]   &   |- T. |= [(\x:al Sy:al) = S]   &   |- [x:al = C] |= [A = B]   &   |- [x:al = C] |= [R = S]   =>   |- S |= B
tfal 108term F.
tan 109term /\
tne 110term ~
tim 111term ==>
tal 112term A.
tex 113term E.
tor 114term \/
teu 115term E!
df-al 116|- T. |= [A. = \p:(al -> *) [p:(al -> *) = \x:al T.]]
df-fal 117|- T. |= [F. = (A.\p:* p:*)]
df-an 118|- T. |= [ /\ = \p:* \q:* [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]
df-im 119|- T. |= [ ==> = \p:* \q:* [[p:* /\ q:*] = p:*]]
df-not 120|- T. |= [~ = \p:* [p:* ==> F.]]
df-ex 121|- T. |= [E. = \p:(al -> *) (A.\q:* [(A.\x:al [(p:(al -> *)x:al) ==> q:*]) ==> q:*])]
df-or 122|- T. |= [ \/ = \p:* \q:* (A.\x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]])]
df-eu 123|- T. |= [E! = \p:(al -> *) (E.\y:al (A.\x:al [(p:(al -> *)x:al) = [x:al = y:al]]))]
wffMMJ2d 161wff typedef al(A, B)C
wabs 162|- B:al   &   |- F:(al -> *)   &   |- T. |= (FB)   &   |- typedef be(A, R)F   =>   |- A:(al -> be)
wrep 163|- B:al   &   |- F:(al -> *)   &   |- T. |= (FB)   &   |- typedef be(A, R)F   =>   |- R:(be -> al)
ax-tdef 164|- B:al   &   |- F:(al -> *)   &   |- T. |= (FB)   &   |- typedef be(A, R)F   =>   |- T. |= ((A.\x:be [(A(Rx:be)) = x:be]), (A.\x:al [(Fx:al) = [(R(Ax:al)) = x:al]]))
ax-eta 165|- T. |= (A.\f:(al -> be) [\x:al (f:(al -> be)x:al) = f:(al -> be)])
tf11 177term 1-1
tfo 178term onto
tat 179term @
wat 180|- @:((al -> *) -> al)
df-f11 181|- T. |= [1-1 = \f:(al -> be) (A.\x:al (A.\y:al [[(f:(al -> be)x:al) = (f:(al -> be)y:al)] ==> [x:al = y:al]]))]
df-fo 182|- T. |= [onto = \f:(al -> be) (A.\y:be (E.\x:al [y:be = (f:(al -> be)x:al)]))]
ax-ac 183|- T. |= (A.\p:(al -> *) (A.\x:al [(p:(al -> *)x:al) ==> (p:(al -> *)(@p:(al -> *)))]))
ax-inf 189|- T. |= (E.\f:(iota -> iota) [(1-1 f:(iota -> iota)) /\ (~ (onto f:(iota -> iota)))])
  Copyright terms: Public domain W3C validator