Type  Label  Description 
Statement 

0.1 Ortholattices


0.1.1 Basic syntax and axioms


Syntax  wb 1 
If a and b are terms, a = b is
a wff.

wff
a = b 

Syntax  wle 2 
If a and b are terms, a ≤ b
is a wff.

wff
a ≤ b 

Syntax  wc 3 
If a and b are terms, a C b is a wff.

wff
a C b 

Syntax  wn 4 
If a is a term, so is a^{⊥}.

term a^{⊥} 

Syntax  tb 5 
If a and b are terms, so is (a ≡ b).

term (a
≡ b) 

Syntax  wo 6 
If a and b are terms, so is (a ∪ b).

term (a ∪
b) 

Syntax  wa 7 
If a and b are terms, so is (a ∩ b).

term (a ∩
b) 

Syntax  wt 8 
The logical true constant is a term.

term 1 

Syntax  wf 9 
The logical false constant is a term.

term 0 

Syntax  wle2 10 
If a and b are terms, so is (a ≤_{2 }b).

term (a
≤_{2 }b) 

Syntax  wi0 11 
If a and b are terms, so is (a →_{0 }b).

term (a
→_{0 }b) 

Syntax  wi1 12 
If a and b are terms, so is (a →_{1 }b).

term (a
→_{1 }b) 

Syntax  wi2 13 
If a and b are terms, so is (a →_{2 }b).

term (a
→_{2 }b) 

Syntax  wi3 14 
If a and b are terms, so is (a →_{3 }b).

term (a
→_{3 }b) 

Syntax  wi4 15 
If a and b are terms, so is (a →_{4 }b).

term (a
→_{4 }b) 

Syntax  wi5 16 
If a and b are terms, so is (a →_{5 }b).

term (a
→_{5 }b) 

Syntax  wid0 17 
If a and b are terms, so is (a ≡_{0 } b).

term (a
≡_{0 } b) 

Syntax  wid1 18 
If a and b are terms, so is (a ≡_{1 }b).

term (a
≡_{1 }b) 

Syntax  wid2 19 
If a and b are terms, so is (a ≡_{2 }b).

term (a
≡_{2 }b) 

Syntax  wid3 20 
If a and b are terms, so is (a ≡_{3 }b).

term (a
≡_{3 }b) 

Syntax  wid4 21 
If a and b are terms, so is (a ≡_{4 }b).

term (a
≡_{4 }b) 

Syntax  wid5 22 
If a and b are terms, so is (a ≡_{5 }b).

term (a
≡_{5 }b) 

Syntax  wb3 23 
If a and b are terms, so is (a ↔_{3 } b).

term (a
↔_{3 } b) 

Syntax  wb1 24 
If a and b are terms, so is (a ↔_{3 } b).

term (a
↔_{1 } b) 

Syntax  wo3 25 
If a and b are terms, so is (a ∪_{3 } b).

term (a
∪_{3 } b) 

Syntax  wan3 26 
If a and b are terms, so is (a ∩_{3 } b).

term (a
∩_{3 } b) 

Syntax  wid3oa 27 
If a, b, and c are terms, so is (a ≡ c
≡_{OA }b).

term (a
≡ c ≡_{OA }b) 

Syntax  wid4oa 28 
If a, b, c, and d are terms, so is
(a ≡ c, d
≡_{OA }b).

term (a
≡ c, d ≡_{OA }b) 

Syntax  wcmtr 29 
If a and b are terms, so is C (a, b).

term C (a, b) 

Axiom  axa1 30 
Axiom for ortholattices. (Contributed by NM, 9Aug1997.)

a = a^{⊥}
^{⊥} 

Axiom  axa2 31 
Axiom for ortholattices. (Contributed by NM, 9Aug1997.)

(a ∪ b) =
(b ∪ a) 

Axiom  axa3 32 
Axiom for ortholattices. (Contributed by NM, 9Aug1997.)

((a ∪ b)
∪ c) = (a ∪ (b
∪ c)) 

Axiom  axa4 33 
Axiom for ortholattices. (Contributed by NM, 9Aug1997.)

(a ∪ (b
∪ b^{⊥} )) = (b ∪ b^{⊥} ) 

Axiom  axa5 34 
Axiom for ortholattices. (Contributed by NM, 9Aug1997.)

(a ∪ (a^{⊥} ∪ b)^{⊥} ) = a 

Axiom  axr1 35 
Inference rule for ortholattices. (Contributed by NM, 9Aug1997.)

a = b ⇒ b = a 

Axiom  axr2 36 
Inference rule for ortholattices. (Contributed by NM, 9Aug1997.)

a = b
& b =
c ⇒ a = c 

Axiom  axr4 37 
Inference rule for ortholattices. (Contributed by NM, 9Aug1997.)

a = b ⇒ a^{⊥} = b^{⊥} 

Axiom  axr5 38 
Inference rule for ortholattices. (Contributed by NM, 9Aug1997.)

a = b ⇒ (a ∪ c) =
(b ∪ c) 

Definition  dfb 39 
Define biconditional. (Contributed by NM, 9Aug1997.)

(a ≡ b) =
((a^{⊥} ∪ b^{⊥} )^{⊥} ∪
(a ∪ b)^{⊥} ) 

Definition  dfa 40 
Define conjunction. (Contributed by NM, 9Aug1997.)

(a ∩ b) =
(a^{⊥} ∪ b^{⊥}
)^{⊥} 

Definition  dft 41 
Define true. (Contributed by NM, 9Aug1997.)

1 = (a ∪ a^{⊥} ) 

Definition  dff 42 
Define false. (Contributed by NM, 9Aug1997.)

0 =
1^{⊥} 

Definition  dfi0 43 
Define classical conditional. (Contributed by NM, 31Oct1998.)

(a →_{0 }b) = (a^{⊥} ∪ b) 

Definition  dfi1 44 
Define Sasaki (Mittelstaedt) conditional. (Contributed by NM,
23Nov1997.)

(a →_{1 }b) = (a^{⊥} ∪ (a ∩ b)) 

Definition  dfi2 45 
Define Dishkant conditional. (Contributed by NM, 23Nov1997.)

(a →_{2 }b) = (b ∪
(a^{⊥} ∩ b^{⊥} )) 

Definition  dfi3 46 
Define Kalmbach conditional. (Contributed by NM, 2Nov1997.)

(a →_{3 }b) = (((a^{⊥} ∩ b) ∪ (a^{⊥} ∩ b^{⊥} )) ∪ (a ∩ (a^{⊥} ∪ b))) 

Definition  dfi4 47 
Define nontollens conditional. (Contributed by NM, 23Nov1997.)

(a →_{4 }b) = (((a ∩
b) ∪ (a^{⊥} ∩ b)) ∪ ((a^{⊥} ∪ b) ∩ b^{⊥} )) 

Definition  dfi5 48 
Define relevance conditional. (Contributed by NM, 23Nov1997.)

(a →_{5 }b) = (((a ∩
b) ∪ (a^{⊥} ∩ b)) ∪ (a^{⊥} ∩ b^{⊥} )) 

Definition  dfid0 49 
Define classical identity. (Contributed by NM, 7Feb1999.)

(a ≡_{0 } b) = ((a^{⊥} ∪ b) ∩ (b^{⊥} ∪ a)) 

Definition  dfid1 50 
Define asymmetrical identity (for "NonOrthomodular Models..."
paper).
(Contributed by NM, 7Feb1999.)

(a ≡_{1 }b) = ((a ∪
b^{⊥} ) ∩ (a^{⊥} ∪ (a ∩ b))) 

Definition  dfid2 51 
Define asymmetrical identity (for "NonOrthomodular Models..."
paper).
(Contributed by NM, 7Feb1999.)

(a ≡_{2 }b) = ((a ∪
b^{⊥} ) ∩ (b ∪ (a^{⊥} ∩ b^{⊥} ))) 

Definition  dfid3 52 
Define asymmetrical identity (for "NonOrthomodular Models..."
paper).
(Contributed by NM, 7Feb1999.)

(a ≡_{3 }b) = ((a^{⊥} ∪ b) ∩ (a
∪ (a^{⊥} ∩ b^{⊥} ))) 

Definition  dfid4 53 
Define asymmetrical identity (for "NonOrthomodular Models..."
paper).
(Contributed by NM, 7Feb1999.)

(a ≡_{4 }b) = ((a^{⊥} ∪ b) ∩ (b^{⊥} ∪ (a ∩ b))) 

Definition  dfo3 54 
Defined disjunction. (Contributed by NM, 2Nov1997.)

(a ∪_{3 } b) = (a^{⊥} →_{3 }(a^{⊥} →_{3 }b)) 

Definition  dfa3 55 
Defined conjunction. (Contributed by NM, 2Nov1997.)

(a ∩_{3 } b) = (a^{⊥} ∪_{3 } b^{⊥}
)^{⊥} 

Definition  dfb3 56 
Defined biconditional. (Contributed by NM, 2Nov1997.)

(a ↔_{3 } b) = ((a
→_{3 }b) ∩ (b →_{3 }a)) 

Definition  dfid3oa 57 
The 3variable orthoarguesian identity term. (Contributed by NM,
22Sep1998.)

(a ≡ c
≡_{OA }b) = (((a →_{1 }c) ∩ (b
→_{1 }c)) ∪ ((a^{⊥} →_{1 }c) ∩ (b^{⊥} →_{1 }c))) 

Definition  dfid4oa 58 
The 4variable orthoarguesian identity term. (Contributed by NM,
28Nov1998.)

(a ≡ c,
d ≡_{OA }b) = ((a
≡ d ≡_{OA }b) ∪ ((a
≡ d ≡_{OA }c) ∩ (b
≡ d ≡_{OA }c))) 

0.1.2 Basic lemmas


Theorem  id 59 
Identity law. (Contributed by NM, 9Aug1997.)

a = a 

Theorem  tt 60 
Justification of definition dft 41 of true (1). This shows that the
definition is independent of the variable used to define it. (Contributed
by NM, 9Aug1997.)

(a ∪ a^{⊥} ) = (b ∪ b^{⊥} ) 

Theorem  cm 61 
Commutative inference rule for ortholattices. (Contributed by NM,
26May2008.)

a = b ⇒ b = a 

Theorem  tr 62 
Transitive inference rule for ortholattices. (Contributed by NM,
26May2008.)

a = b
& b =
c ⇒ a = c 

Theorem  3tr1 63 
Transitive inference useful for introducing definitions. (Contributed
by NM, 10Aug1997.)

a = b
& c =
a
& d =
b ⇒ c = d 

Theorem  3tr2 64 
Transitive inference useful for eliminating definitions. (Contributed
by NM, 10Aug1997.)

a = b
& a =
c
& b =
d ⇒ c = d 

Theorem  3tr 65 
Triple transitive inference. (Contributed by NM, 20Sep1998.)

a = b
& b =
c
& c =
d ⇒ a = d 

Theorem  con1 66 
Contraposition inference. (Contributed by NM, 10Aug1997.)

a^{⊥} = b^{⊥} ⇒ a = b 

Theorem  con2 67 
Contraposition inference. (Contributed by NM, 10Aug1997.)

a = b^{⊥} ⇒ a^{⊥} = b 

Theorem  con3 68 
Contraposition inference. (Contributed by NM, 10Aug1997.)

a^{⊥} = b ⇒ a = b^{⊥} 

Theorem  con4 69 
Contraposition inference. (Contributed by NM, 26May2008.) (Revised
by NM, 31Mar2011.)

a = b ⇒ a^{⊥} = b^{⊥} 

Theorem  lor 70 
Inference introducing disjunct to left. (Contributed by NM,
10Aug1997.)

a = b ⇒ (c ∪ a) =
(c ∪ b) 

Theorem  ror 71 
Inference introducing disjunct to right. (Contributed by NM,
26May2008.) (Revised by NM, 31Mar2011.)

a = b ⇒ (a ∪ c) =
(b ∪ c) 

Theorem  2or 72 
Join both sides with disjunction. (Contributed by NM, 10Aug1997.)

a = b
& c =
d ⇒ (a ∪ c) =
(b ∪ d) 

Theorem  orcom 73 
Commutative law. (Contributed by NM, 27May2008.) (Revised by NM,
31Mar2011.)

(a ∪ b) =
(b ∪ a) 

Theorem  ancom 74 
Commutative law. (Contributed by NM, 10Aug1997.)

(a ∩ b) =
(b ∩ a) 

Theorem  orass 75 
Associative law. (Contributed by NM, 27May2008.) (Revised by NM,
31Mar2011.)

((a ∪ b)
∪ c) = (a ∪ (b
∪ c)) 

Theorem  anass 76 
Associative law. (Contributed by NM, 12Aug1997.)

((a ∩ b)
∩ c) = (a ∩ (b
∩ c)) 

Theorem  lan 77 
Introduce conjunct on left. (Contributed by NM, 10Aug1997.)

a = b ⇒ (c ∩ a) =
(c ∩ b) 

Theorem  ran 78 
Introduce conjunct on right. (Contributed by NM, 10Aug1997.)

a = b ⇒ (a ∩ c) =
(b ∩ c) 

Theorem  2an 79 
Conjoin both sides of hypotheses. (Contributed by NM, 10Aug1997.)

a = b
& c =
d ⇒ (a ∩ c) =
(b ∩ d) 

Theorem  or12 80 
Swap disjuncts. (Contributed by NM, 27Aug1997.)

(a ∪ (b
∪ c)) = (b ∪ (a
∪ c)) 

Theorem  an12 81 
Swap conjuncts. (Contributed by NM, 27Aug1997.)

(a ∩ (b
∩ c)) = (b ∩ (a
∩ c)) 

Theorem  or32 82 
Swap disjuncts. (Contributed by NM, 27Aug1997.)

((a ∪ b)
∪ c) = ((a ∪ c)
∪ b) 

Theorem  an32 83 
Swap conjuncts. (Contributed by NM, 27Aug1997.)

((a ∩ b)
∩ c) = ((a ∩ c)
∩ b) 

Theorem  or4 84 
Swap disjuncts. (Contributed by NM, 27Aug1997.)

((a ∪ b)
∪ (c ∪ d)) = ((a ∪
c) ∪ (b ∪ d)) 

Theorem  or42 85 
Rearrange disjuncts. (Contributed by NM, 4Mar2006.)

((a ∪ b)
∪ (c ∪ d)) = ((a ∪
d) ∪ (b ∪ c)) 

Theorem  an4 86 
Swap conjuncts. (Contributed by NM, 27Aug1997.)

((a ∩ b)
∩ (c ∩ d)) = ((a ∩
c) ∩ (b ∩ d)) 

Theorem  oran 87 
Disjunction expressed with conjunction. (Contributed by NM,
10Aug1997.)

(a ∪ b) =
(a^{⊥} ∩ b^{⊥}
)^{⊥} 

Theorem  anor1 88 
Conjunction expressed with disjunction. (Contributed by NM,
12Aug1997.)

(a ∩ b^{⊥} ) = (a^{⊥} ∪ b)^{⊥} 

Theorem  anor2 89 
Conjunction expressed with disjunction. (Contributed by NM,
12Aug1997.)

(a^{⊥} ∩ b) = (a ∪
b^{⊥}
)^{⊥} 

Theorem  anor3 90 
Conjunction expressed with disjunction. (Contributed by NM,
15Dec1997.)

(a^{⊥} ∩ b^{⊥} ) = (a ∪ b)^{⊥} 

Theorem  oran1 91 
Disjunction expressed with conjunction. (Contributed by NM,
15Dec1997.)

(a ∪ b^{⊥} ) = (a^{⊥} ∩ b)^{⊥} 

Theorem  oran2 92 
Disjunction expressed with conjunction. (Contributed by NM,
15Dec1997.)

(a^{⊥} ∪ b) = (a ∩
b^{⊥}
)^{⊥} 

Theorem  oran3 93 
Disjunction expressed with conjunction. (Contributed by NM,
15Dec1997.)

(a^{⊥} ∪ b^{⊥} ) = (a ∩ b)^{⊥} 

Theorem  dfb 94 
Biconditional expressed with others. (Contributed by NM, 10Aug1997.)

(a ≡ b) =
((a ∩ b) ∪ (a^{⊥} ∩ b^{⊥} )) 

Theorem  dfnb 95 
Negated biconditional. (Contributed by NM, 30Aug1997.)

(a ≡ b)^{⊥} = ((a ∪ b)
∩ (a^{⊥} ∪ b^{⊥} )) 

Theorem  bicom 96 
Commutative law. (Contributed by NM, 10Aug1997.)

(a ≡ b) =
(b ≡ a) 

Theorem  lbi 97 
Introduce biconditional to the left. (Contributed by NM,
10Aug1997.)

a = b ⇒ (c ≡ a) =
(c ≡ b) 

Theorem  rbi 98 
Introduce biconditional to the right. (Contributed by NM,
10Aug1997.)

a = b ⇒ (a ≡ c) =
(b ≡ c) 

Theorem  2bi 99 
Join both sides with biconditional. (Contributed by NM,
10Aug1997.)

a = b
& c =
d ⇒ (a ≡ c) =
(b ≡ d) 

Theorem  dff2 100 
Alternate definition of "false". (Contributed by NM, 10Aug1997.)

0 = (a ∪ a^{⊥}
)^{⊥} 