mmdefinitions - Higher-Order Logic Explorer

List of Syntax, Axioms (ax-) and Definitions (df-)

Ref	Expression (see link for any distinct variable requirements)
tv 1	term x:al
ht 2	type (al -> be)
hb 3	type *
hi 4	type iota
kc 5	term (FT)
kl 6	term \x:al T
ke 7	term =
kt 8	term T.
kbr 9	term [AFB]
kct 10	term (A, B)
wffMMJ2 11	wff A |= B
wffMMJ2t 12	wff 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 118	term F.
tan 119	term /\
tne 120	term ~
tim 121	term ==>
tal 122	term A.
tex 123	term E.
tor 124	term \/
teu 125	term 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 171	wff 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 189	term 1-1
tfo 190	term onto
tat 191	term @
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)))])