QLE Home Quantum 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)
wb 1wff a = b
wle 2wff a =< b
wc 3wff a C b
wn 4term a'
tb 5term (a == b)
wo 6term (a v b)
wa 7term (a ^ b)
wt 8term 1
wf 9term 0
wle2 10term (a =<2 b)
wi0 11term (a ->0 b)
wi1 12term (a ->1 b)
wi2 13term (a ->2 b)
wi3 14term (a ->3 b)
wi4 15term (a ->4 b)
wi5 16term (a ->5 b)
wid0 17term (a ==0 b)
wid1 18term (a ==1 b)
wid2 19term (a ==2 b)
wid3 20term (a ==3 b)
wid4 21term (a ==4 b)
wid5 22term (a ==5 b)
wb3 23term (a <->3 b)
wb1 24term (a <->1 b)
wo3 25term (a u3 b)
wan3 26term (a ^3 b)
wid3oa 27term (a == c ==OA b)
wid4oa 28term (a == c, d ==OA b)
wcmtr 29term C (a, b)
ax-a1 30a = a''
ax-a2 31(a v b) = (b v a)
ax-a3 32((a v b) v c) = (a v (b v c))
ax-a4 33(a v (b v b')) = (b v b')
ax-a5 34(a v (a' v b)') = a
ax-r1 35a = b   =>   b = a
ax-r2 36a = b   &   b = c   =>   a = c
ax-r4 37a = b   =>   a' = b'
ax-r5 38a = b   =>   (a v c) = (b v c)
df-b 39(a == b) = ((a' v b')' v (a v b)')
df-a 40(a ^ b) = (a' v b')'
df-t 411 = (a v a')
df-f 420 = 1'
df-i0 43(a ->0 b) = (a' v b)
df-i1 44(a ->1 b) = (a' v (a ^ b))
df-i2 45(a ->2 b) = (b v (a' ^ b'))
df-i3 46(a ->3 b) = (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b)))
df-i4 47(a ->4 b) = (((a ^ b) v (a' ^ b)) v ((a' v b) ^ b'))
df-i5 48(a ->5 b) = (((a ^ b) v (a' ^ b)) v (a' ^ b'))
df-id0 49(a ==0 b) = ((a' v b) ^ (b' v a))
df-id1 50(a ==1 b) = ((a v b') ^ (a' v (a ^ b)))
df-id2 51(a ==2 b) = ((a v b') ^ (b v (a' ^ b')))
df-id3 52(a ==3 b) = ((a' v b) ^ (a v (a' ^ b')))
df-id4 53(a ==4 b) = ((a' v b) ^ (b' v (a ^ b)))
df-o3 54(a u3 b) = (a' ->3 (a' ->3 b))
df-a3 55(a ^3 b) = (a' u3 b')'
df-b3 56(a <->3 b) = ((a ->3 b) ^ (b ->3 a))
df-id3oa 57(a == c ==OA b) = (((a ->1 c) ^ (b ->1 c)) v ((a' ->1 c) ^ (b' ->1 c)))
df-id4oa 58(a == c, d ==OA b) = ((a == d ==OA b) v ((a == d ==OA c) ^ (b == d ==OA c)))
df-le 129(a =<2 b) = ((a v b) == b)
df-le1 130(a v b) = b   =>   a =< b
df-le2 131a =< b   =>   (a v b) = b
df-c1 132a = ((a ^ b) v (a ^ b'))   =>   a C b
df-c2 133a C b   =>   a = ((a ^ b) v (a ^ b'))
df-cmtr 134C (a, b) = (((a ^ b) v (a ^ b')) v ((a' ^ b) v (a' ^ b')))
ax-wom 361(a' v (a ^ b)) = 1   =>   (b v (a' ^ b')) = 1
ax-r3 439(c v c') = ((a' v b')' v (a v b)')   =>   a = b
ax-oadist 994e = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))   &   f = (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e)   &   h =< (a ->1 d)   &   j =< f   &   k =< f   &   (h ^ (b ->1 d)) =< k   =>   (h ^ (j v k)) = ((h ^ j) v (h ^ k))
ax-3oa 998((a ->1 c) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))) =< (b ->1 c)
ax-oal4 1026a =< b'   &   c =< d'   =>   ((a v b) ^ (c v d)) =< (b v (a ^ (c v ((a v c) ^ (b v d)))))
ax-oa6 1030a =< b'   &   c =< d'   &   e =< f'   =>   (((a v b) ^ (c v d)) ^ (e v f)) =< (b v (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))))))
ax-4oa 1033((a ->1 d) ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d)))))) =< (b ->1 d)
ax-newstateeq 1045(((a ->1 b) ->1 (c ->1 b)) ^ ((a ->1 c) ^ (b ->1 a))) =< (c ->1 a)
df-id5 1047(a ==5 b) = ((a ^ b) v (a' ^ b'))
df-b1 1048(a <->1 b) = ((a ->1 b) ^ (b ->1 a))
ax-wdol 1102((a == b) v (a == b')) = 1
ax-ml 1120((a v b) ^ (a v c)) =< (a v (b ^ (a v c)))
ax-arg 1151((a0 v b0) ^ (a1 v b1)) =< (a2 v b2)   =>   ((a0 v a1) ^ (b0 v b1)) =< (((a0 v a2) ^ (b0 v b2)) v ((a1 v a2) ^ (b1 v b2)))
  Copyright terms: Public domain W3C validator