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:*
ax-wctl 31|- (S, T):*   =>   |- S:*
ax-wctr 32|- (S, T):*   =>   |- T:*
ax-weq 40|- = :(al -> (al -> *))
ax-refl 42|- A:al   =>   |- T. |= (( = 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:(al -> be)   &   |- T:al   =>   |- (FT):be
ax-ceq 51|- F:(al -> be)   &   |- T:(al -> be)   &   |- A:al   &   |- B:al   =>   |- ((( = F)T), (( = A)B)) |= (( = (FA))(TB))
ax-wv 63|- x:al:al
ax-wl 65|- T:be   =>   |- \x:al T:(al -> be)
ax-beta 67|- A:be   =>   |- T. |= (( = (\x:al Ax:al))A)
ax-distrc 68|- A:be   &   |- B:al   &   |- F:(be -> ga)   =>   |- T. |= (( = (\x:al (FA)B))((\x:al FB)(\x:al AB)))
ax-leq 69|- A:be   &   |- B:be   &   |- R |= (( = A)B)   =>   |- R |= (( = \x:al A)\x:al B)
ax-distrl 70|- A:ga   &   |- B:al   =>   |- T. |= (( = (\x:al \y:be AB))\y:be (\x:al AB))
ax-wov 71|- F:(al -> (be -> ga))   &   |- A:al   &   |- B:be   =>   |- [AFB]:ga
df-ov 73|- F:(al -> (be -> ga))   &   |- A:al   &   |- B:be   =>   |- T. |= (( = [AFB])((FA)B))
ax-eqtypi 77|- A:al   &   |- R |= [A = B]   =>   |- B:al
ax-eqtypri 80|- A:al   &   |- R |= [B = A]   =>   |- B:al
ax-hbl1 103|- A:ga   &   |- B:al   =>   |- T. |= [(\x:al \x:be AB) = \x:be A]
ax-17 105|- A:be   &   |- B:al   =>   |- T. |= [(\x:al AB) = A]
ax-inst 113|- 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 118term F.
tan 119term /\
tne 120term ~
tim 121term ==>
tal 122term A.
tex 123term E.
tor 124term \/
teu 125term E!
df-al 126|- T. |= [A. = \p:(al -> *) [p:(al -> *) = \x:al T.]]
df-fal 127|- T. |= [F. = (A.\p:* p:*)]
df-an 128|- T. |= [ /\ = \p:* \q:* [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]
df-im 129|- T. |= [ ==> = \p:* \q:* [[p:* /\ q:*] = p:*]]
df-not 130|- T. |= [~ = \p:* [p:* ==> F.]]
df-ex 131|- T. |= [E. = \p:(al -> *) (A.\q:* [(A.\x:al [(p:(al -> *)x:al) ==> q:*]) ==> q:*])]
df-or 132|- T. |= [ \/ = \p:* \q:* (A.\x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]])]
df-eu 133|- T. |= [E! = \p:(al -> *) (E.\y:al (A.\x:al [(p:(al -> *)x:al) = [x:al = y:al]]))]
wffMMJ2d 171wff typedef al(A, B)C
ax-wabs 172|- B:al   &   |- F:(al -> *)   &   |- T. |= (FB)   &   |- typedef be(A, R)F   =>   |- A:(al -> be)
ax-wrep 173|- B:al   &   |- F:(al -> *)   &   |- T. |= (FB)   &   |- typedef be(A, R)F   =>   |- R:(be -> al)
ax-tdef 176|- 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 177|- T. |= (A.\f:(al -> be) [\x:al (f:(al -> be)x:al) = f:(al -> be)])
tf11 189term 1-1
tfo 190term onto
tat 191term @
ax-wat 192|- @:((al -> *) -> al)
df-f11 194|- 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 195|- T. |= [onto = \f:(al -> be) (A.\y:be (E.\x:al [y:be = (f:(al -> be)x:al)]))]
ax-ac 196|- T. |= (A.\p:(al -> *) (A.\x:al [(p:(al -> *)x:al) ==> (p:(al -> *)(@p:(al -> *)))]))
ax-inf 202|- T. |= (E.\f:(iota -> iota) [(1-1 f:(iota -> iota)) /\ (~ (onto f:(iota -> iota)))])
  Copyright terms: Public domain W3C validator