[Lattice L46-7]Home PageHome Quantum Logic Explorer
Theorem List (p. 3 of 13) 		< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  QLE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for Quantum Logic Explorer - 201-300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremwa5c 201 Absorption law.
((a ^ (a v b)) == a) = 1
 
Theoremwcon 202 Contraposition law.
((a == b) == (a' == b')) = 1
 
Theoremwancom 203 Commutative law.
((a ^ b) == (b ^ a)) = 1
 
Theoremwanass 204 Associative law.
(((a ^ b) ^ c) == (a ^ (b ^ c))) = 1
 
Theoremwwbmp 205 Weak weak equivalential detachment (WBMP).
a = 1   &   (a == b) = 1   =>   b = 1
 
Theoremwwbmpr 206 Weak weak equivalential detachment (WBMP).
b = 1   &   (a == b) = 1   =>   a = 1
 
Theoremwcon1 207 Weak contraposition.
(a' == b') = 1   =>   (a == b) = 1
 
Theoremwcon2 208 Weak contraposition.
(a == b') = 1   =>   (a' == b) = 1
 
Theoremwcon3 209 Weak contraposition.
(a' == b) = 1   =>   (a == b') = 1
 
Theoremwlem3.1 210 Weak analogue to lemma used in proof of Th. 3.1 of Pavicic 1993.
(a v b) = b   &   (b' v a) = 1   =>   (a == b) = 1
 
Theoremwoml 211 Theorem structurally similar to orthomodular law but does not require R3.
((a v (a' ^ (a v b))) == (a v b)) = 1
 
Theoremwwoml2 212 Weak orthomodular law.
a =< b   =>   ((a v (a' ^ b)) == b) = 1
 
Theoremwwoml3 213 Weak orthomodular law.
a =< b   &   (b ^ a') = 0   =>   (a == b) = 1
 
Theoremwwcomd 214 Commutation dual (weak). Kalmbach 83 p. 23.
a' C b   =>   a = ((a v b) ^ (a v b'))
 
Theoremwwcom3ii 215 Lemma 3(ii) (weak) of Kalmbach 83 p. 23.
b' C a   =>   (a ^ (a' v b)) = (a ^ b)
 
Theoremwwfh1 216 Foulis-Holland Theorem (weak).
b C a   &   c C a   =>   ((a ^ (b v c)) == ((a ^ b) v (a ^ c))) = 1
 
Theoremwwfh2 217 Foulis-Holland Theorem (weak).
a C b   &   c' C a   =>   ((b ^ (a v c)) == ((b ^ a) v (b ^ c))) = 1
 
Theoremwwfh3 218 Foulis-Holland Theorem (weak).
b' C a   &   c' C a   =>   ((a v (b ^ c)) == ((a v b) ^ (a v c))) = 1
 
Theoremwwfh4 219 Foulis-Holland Theorem (weak).
a' C b   &   c C a   =>   ((b v (a ^ c)) == ((b v a) ^ (b v c))) = 1
 
Theoremwomao 220 Weak OM-like absorption law for ortholattices.
(a' ^ (a v (a' ^ (a v b)))) = (a' ^ (a v b))
 
Theoremwomaon 221 Weak OM-like absorption law for ortholattices.
(a ^ (a' v (a ^ (a' v b)))) = (a ^ (a' v b))
 
Theoremwomaa 222 Weak OM-like absorption law for ortholattices.
(a' v (a ^ (a' v (a ^ b)))) = (a' v (a ^ b))
 
Theoremwomaan 223 Weak OM-like absorption law for ortholattices.
(a v (a' ^ (a v (a' ^ b)))) = (a v (a' ^ b))
 
Theoremanorabs2 224 Absorption law for ortholattices.
(a ^ (b v (a ^ (b v c)))) = (a ^ (b v c))
 
Theoremanorabs 225 Absorption law for ortholattices.
(a' ^ (b v (a' ^ (a v b)))) = (a' ^ (a v b))
 
Theoremska2a 226 Axiom KA2a in Pavicic and Megill, 1998
(((a v c) == (b v c)) == ((c v a) == (c v b))) = 1
 
Theoremska2b 227 Axiom KA2b in Pavicic and Megill, 1998
(((a v c) == (b v c)) == ((a' ^ c')' == (b' ^ c')')) = 1
 
Theoremka4lemo 228 Lemma for KA4 soundness (OR version) - uses OL only.
((a v b) v ((a v c) == (b v c))) = 1
 
Theoremka4lem 229 Lemma for KA4 soundness (AND version) - uses OL only.
((a ^ b)' v ((a ^ c) == (b ^ c))) = 1
 
0.1.6  Kalmbach axioms (soundness proofs) that are true in all ortholattices
 
Theoremsklem 230 Soundness lemma.
a =< b   =>   (a' v b) = 1
 
Theoremska1 231 Soundness theorem for Kalmbach's quantum propositional logic axiom KA1.
(a == a) = 1
 
Theoremska3 232 Soundness theorem for Kalmbach's quantum propositional logic axiom KA3.
((a == b)' v (a' == b')) = 1
 
Theoremska5 233 Soundness theorem for Kalmbach's quantum propositional logic axiom KA5.
((a ^ b) == (b ^ a)) = 1
 
Theoremska6 234 Soundness theorem for Kalmbach's quantum propositional logic axiom KA6.
((a ^ (b ^ c)) == ((a ^ b) ^ c)) = 1
 
Theoremska7 235 Soundness theorem for Kalmbach's quantum propositional logic axiom KA7.
((a ^ (a v b)) == a) = 1
 
Theoremska8 236 Soundness theorem for Kalmbach's quantum propositional logic axiom KA8.
((a' ^ a) == ((a' ^ a) ^ b)) = 1
 
Theoremska9 237 Soundness theorem for Kalmbach's quantum propositional logic axiom KA9.
(a == a'') = 1
 
Theoremska10 238 Soundness theorem for Kalmbach's quantum propositional logic axiom KA10.
((a v b)' == (a' ^ b')) = 1
 
Theoremska11 239 Soundness theorem for Kalmbach's quantum propositional logic axiom KA11.
((a v (a' ^ (a v b))) == (a v b)) = 1
 
Theoremska12 240 Soundness theorem for Kalmbach's quantum propositional logic axiom KA12.
((a == b) == (b == a)) = 1
 
Theoremska13 241 Soundness theorem for Kalmbach's quantum propositional logic axiom KA13.
((a == b)' v (a' v b)) = 1
 
Theoremskr0 242 Soundness theorem for Kalmbach's quantum propositional logic axiom KR0.
a = 1   &   (a' v b) = 1   =>   b = 1
 
Theoremwlem1 243 Lemma for 2-variable WOML proof.
((a == b)' v ((a ->1 b) ^ (b ->1 a))) = 1
 
Theoremska15 244 Soundness theorem for Kalmbach's quantum propositional logic axiom KA15.
((a ->3 b)' v (a' v b)) = 1
 
Theoremskmp3 245 Soundness proof for KMP3.
a = 1   &   (a ->3 b) = 1   =>   b = 1
 
Theoremlei3 246 L.e. to Kalmbach implication.
a =< b   =>   (a ->3 b) = 1
 
Theoremmccune2 247 E2 - OL theorem proved by EQP
(a v ((a' ^ ((a v b') ^ (a v b))) v (a' ^ ((a' ^ b) v (a' ^ b'))))) = 1
 
Theoremmccune3 248 E3 - OL theorem proved by EQP
((((a' ^ b) v (a' ^ b')) v (a ^ (a' v b)))' v (a' v b)) = 1
 
Theoremi3n1 249 Equivalence for Kalmbach implication.
(a' ->3 b') = (((a ^ b') v (a ^ b)) v (a' ^ (a v b')))
 
Theoremni31 250 Equivalence for Kalmbach implication.
(a ->3 b)' = (((a v b') ^ (a v b)) ^ (a' v (a ^ b')))
 
Theoremi3id 251 Identity for Kalmbach implication.
(a ->3 a) = 1
 
Theoremli3 252 Introduce Kalmbach implication to the left.
a = b   =>   (c ->3 a) = (c ->3 b)
 
Theoremri3 253 Introduce Kalmbach implication to the right.
a = b   =>   (a ->3 c) = (b ->3 c)
 
Theorem2i3 254 Join both sides with Kalmbach implication.
a = b   &   c = d   =>   (a ->3 c) = (b ->3 d)
 
Theoremud1lem0a 255 Introduce ->1 to the left.
a = b   =>   (c ->1 a) = (c ->1 b)
 
Theoremud1lem0b 256 Introduce ->1 to the right.
a = b   =>   (a ->1 c) = (b ->1 c)
 
Theoremud1lem0ab 257 Join both sides of hypotheses with ->1.
a = b   &   c = d   =>   (a ->1 c) = (b ->1 d)
 
Theoremud2lem0a 258 Introduce ->2 to the left.
a = b   =>   (c ->2 a) = (c ->2 b)
 
Theoremud2lem0b 259 Introduce ->2 to the right.
a = b   =>   (a ->2 c) = (b ->2 c)
 
Theoremud3lem0a 260 Introduce Kalmbach implication to the left.
a = b   =>   (c ->3 a) = (c ->3 b)
 
Theoremud3lem0b 261 Introduce Kalmbach implication to the right.
a = b   =>   (a ->3 c) = (b ->3 c)
 
Theoremud4lem0a 262 Introduce ->4 to the left.
a = b   =>   (c ->4 a) = (c ->4 b)
 
Theoremud4lem0b 263 Introduce ->4 to the right.
a = b   =>   (a ->4 c) = (b ->4 c)
 
Theoremud5lem0a 264 Introduce ->5 to the left.
a = b   =>   (c ->5 a) = (c ->5 b)
 
Theoremud5lem0b 265 Introduce ->5 to the right.
a = b   =>   (a ->5 c) = (b ->5 c)
 
Theoremi1i2 266 Correspondence between Sasaki and Dishkant conditionals.
(a ->1 b) = (b' ->2 a')
 
Theoremi2i1 267 Correspondence between Sasaki and Dishkant conditionals.
(a ->2 b) = (b' ->1 a')
 
Theoremi1i2con1 268 Correspondence between Sasaki and Dishkant conditionals.
(a ->1 b') = (b ->2 a')
 
Theoremi1i2con2 269 Correspondence between Sasaki and Dishkant conditionals.
(a' ->1 b) = (b' ->2 a)
 
Theoremi3i4 270 Correspondence between Kalmbach and non-tollens conditionals.
(a ->3 b) = (b' ->4 a')
 
Theoremi4i3 271 Correspondence between Kalmbach and non-tollens conditionals.
(a ->4 b) = (b' ->3 a')
 
Theoremi5con 272 Converse of ->5.
(a ->5 b) = (b' ->5 a')
 
Theorem0i1 273 Antecedent of 0 on Sasaki conditional.
(0 ->1 a) = 1
 
Theorem1i1 274 Antecedent of 1 on Sasaki conditional.
(1 ->1 a) = a
 
Theoremi1id 275 Identity law for Sasaki conditional.
(a ->1 a) = 1
 
Theoremi2id 276 Identity law for Dishkant conditional.
(a ->2 a) = 1
 
Theoremud1lem0c 277 Lemma for unified disjunction.
(a ->1 b)' = (a ^ (a' v b'))
 
Theoremud2lem0c 278 Lemma for unified disjunction.
(a ->2 b)' = (b' ^ (a v b))
 
Theoremud3lem0c 279 Lemma for unified disjunction.
(a ->3 b)' = (((a v b') ^ (a v b)) ^ (a' v (a ^ b')))
 
Theoremud4lem0c 280 Lemma for unified disjunction.
(a ->4 b)' = (((a' v b') ^ (a v b')) ^ ((a ^ b') v b))
 
Theoremud5lem0c 281 Lemma for unified disjunction.
(a ->5 b)' = (((a' v b') ^ (a v b')) ^ (a v b))
 
Theorembina1 282 Pavicic binary logic ax-a1 analog.
(a ->3 a'') = 1
 
Theorembina2 283 Pavicic binary logic ax-a2 analog.
(a'' ->3 a) = 1
 
Theorembina3 284 Pavicic binary logic ax-a3 analog.
(a ->3 (a v b)) = 1
 
Theorembina4 285 Pavicic binary logic ax-a4 analog.
(b ->3 (a v b)) = 1
 
Theorembina5 286 Pavicic binary logic ax-a5 analog.
(b ->3 (a v a')) = 1
 
Theoremwql1lem 287 Classical implication inferred from Sakaki implication.
(a ->1 b) = 1   =>   (a' v b) = 1
 
Theoremwql2lem 288 Classical implication inferred from Dishkant implication.
(a ->2 b) = 1   =>   (a' v b) = 1
 
Theoremwql2lem2 289 Lemma for ->2 WQL axiom.
((a v c) ->2 (b v c)) = 1   =>   ((a v (b v c))' v (b v c)) = 1
 
Theoremwql2lem3 290 Lemma for ->2 WQL axiom.
(a ->2 b) = 1   =>   ((a ^ b') ->2 a') = 1
 
Theoremwql2lem4 291 Lemma for ->2 WQL axiom.
(((a ^ b') v (a ^ b)) ->2 (a' v (a ^ b))) = 1   &   ((a ->1 b) v (a ^ b')) = 1   =>   (a ->1 b) = 1
 
Theoremwql2lem5 292 Lemma for ->2 WQL axiom.
(a ->2 b) = 1   =>   ((b' ^ (a v b)) ->2 a') = 1
 
Theoremwql1 293 The 2nd hypothesis is the first ->1 WQL axiom. We show it implies the WOM law.
(a ->1 b) = 1   &   ((a v c) ->1 (b v c)) = 1   &   c = b   =>   (a ->2 b) = 1
 
Theoremoaidlem1 294 Lemma for OA identity-like law.
(a ^ b) =< c   =>   (a' v (b ->1 c)) = 1
 
Theoremwomle2a 295 An equivalent to the WOM law.
(a ^ (a ->2 b)) =< ((a ->2 b)' v (a ->1 b))   =>   ((a ->2 b)' v (a ->1 b)) = 1
 
Theoremwomle2b 296 An equivalent to the WOM law.
((a ->2 b)' v (a ->1 b)) = 1   =>   (a ^ (a ->2 b)) =< ((a ->2 b)' v (a ->1 b))
 
Theoremwomle3b 297 Implied by the WOM law.
((a ->1 b)' v (a ->2 b)) = 1   =>   (a ^ (a ->1 b)) =< ((a ->1 b)' v (a ->2 b))
 
Theoremwomle 298 An equality implying the WOM law.
(a ^ (a ->1 b)) = (a ^ (a ->2 b))   =>   ((a ->2 b)' v (a ->1 b)) = 1
 
Theoremnomb41 299 Lemma for "Non-Orthomodular Models..." paper.
(a ==4 b) = (b ==1 a)
 
Theoremnomb32 300 Lemma for "Non-Orthomodular Models..." paper.
(a ==3 b) = (b ==2 a)
    < Previous  Next >
Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1215
  Copyright terms: Public domain < Previous  Next >