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:*
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 108	term F.
tan 109	term /\
tne 110	term ~
tim 111	term ==>
tal 112	term A.
tex 113	term E.
tor 114	term \/
teu 115	term 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 161	wff 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 177	term 1-1
tfo 178	term onto
tat 179	term @
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)))])