:: The Fundamental Logic Structure in Quantum Mechanics
:: by Pawe{\l} Sadowski, Andrzej Trybulec and Konrad Raczkowski
::
:: Received December 18, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, XBOOLE_0, RPR_1, PROB_1, FUNCT_2, FUNCT_1,
ZFMISC_1, CARD_1, XXREAL_0, TARSKI, ARYTM_3, RELAT_1, SEQ_2, ORDINAL2,
EQREL_1, REAL_1, ARYTM_1, STRUCT_0, ORDERS_2, ROBBINS1, ORDERS_1,
MCART_1, XBOOLEAN, CQC_THE1, ZFREFLE1, RELAT_2, QMAX_1, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS,
RELAT_1, RELSET_1, RELAT_2, FUNCT_1, XCMPLX_0, XREAL_0, FUNCT_2,
ORDERS_1, DOMAIN_1, SEQ_2, PROB_1, MCART_1, EQREL_1, XXREAL_0, STRUCT_0,
ORDERS_2, ROBBINS1;
constructors DOMAIN_1, XXREAL_0, EQREL_1, SEQ_2, PROB_1, ORDERS_2, ROBBINS1,
REAL_1, VALUED_1, RELSET_1, FINSUB_1, COMSEQ_2, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, PARTFUN1, NUMBERS, EQREL_1,
PROB_1, RELAT_1, FUNCT_1, XREAL_0, XTUPLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions RELAT_2;
equalities SUBSET_1;
theorems ORDERS_1, TARSKI, FUNCT_1, ZFMISC_1, FUNCT_2, PROB_1, MCART_1,
EQREL_1, RELAT_1, RELSET_1, XBOOLE_0, XREAL_1, XXREAL_0, NAT_1, XREAL_0,
ORDINAL1;
schemes EQREL_1, RELSET_1, FUNCT_2, XBOOLE_0;
begin
reserve X1,x,y,z for set,
n,m for Nat,
X for non empty set;
reserve A,B for Event of Borel_Sets,
D for Subset of REAL;
definition let X;
let S be SigmaField of X;
func Probabilities(S) -> set means
:Def1:
for x being object holds x in it iff x is Probability of S;
existence
proof
defpred P[object] means $1 is Probability of S;
consider X being set such that
A1: for x being object holds x in X iff x in Funcs(S,REAL) & P[x]
from XBOOLE_0:sch 1;
take X;
let x be object;
x is Probability of S implies x in Funcs(S,REAL) by FUNCT_2:8;
hence thesis by A1;
end;
uniqueness
proof
let A1,A2 be set;
assume that
A2: for x being object holds x in A1 iff x is Probability of S and
A3: for x being object holds x in A2 iff x is Probability of S;
now
let y be object;
y in A1 iff y is Probability of S by A2;
hence y in A1 iff y in A2 by A3;
end;
hence thesis by TARSKI:2;
end;
end;
registration let X;
let S be SigmaField of X;
cluster Probabilities(S) -> non empty;
coherence
proof
set x = the Probability of S;
x in Probabilities(S) by Def1;
hence thesis;
end;
end;
definition
struct QM_Str (# Observables, FStates -> non empty set,
Quantum_Probability -> Function of [:the Observables, the FStates:],
Probabilities(Borel_Sets) #);
end;
reserve Q for QM_Str;
definition let Q;
func Obs Q -> set equals
the Observables of Q;
coherence;
func Sts Q -> set equals
the FStates of Q;
coherence;
end;
registration let Q;
cluster Obs Q -> non empty;
coherence;
cluster Sts Q -> non empty;
coherence;
end;
reserve A1 for Element of Obs Q;
reserve s for Element of Sts Q;
reserve E for Event of Borel_Sets;
reserve ASeq for SetSequence of Borel_Sets;
definition let Q,A1,s;
func Meas(A1,s) -> Probability of Borel_Sets equals
(the Quantum_Probability of Q).[A1,s];
coherence
proof
reconsider A1s = [A1,s] as Element of [:the Observables of Q,
the FStates of Q:];
(the Quantum_Probability of Q).A1s is Element of Probabilities Borel_Sets;
hence thesis by Def1;
end;
end;
set X = {0};
consider P being Function of Borel_Sets,REAL such that
Lm1: for D st D in Borel_Sets holds (0 in D implies P.D = 1) & (not 0 in D
implies P.D = 0) by PROB_1:28;
Lm2: for A holds 0 <= P.A
proof
let A;
now per cases;
suppose 0 in A;
then P.A = 1 by Lm1;
hence thesis;
end;
suppose not 0 in A;
hence thesis by Lm1;
end;
end;
hence thesis;
end;
Lm3: P.REAL = 1
proof
A1: 0 in REAL by XREAL_0:def 1;
[#]REAL in Borel_Sets by PROB_1:5;
hence thesis by Lm1,A1;
end;
Lm4: for A,B st A misses B holds P.(A \/ B) = P.A + P.B
proof
let A,B such that
A1: A misses B;
now
per cases by A1,XBOOLE_0:3;
suppose
A2: 0 in A & not 0 in B; then
A3: 0 in A \/ B by XBOOLE_0:def 3;
P.A = 1 & P.B = 0 by A2,Lm1;
hence thesis by A3,Lm1;
end;
suppose
A4: not 0 in A & 0 in B;
then
A5: 0 in A \/ B by XBOOLE_0:def 3;
P.A = 0 & P.B = 1 by A4,Lm1;
hence thesis by A5,Lm1;
end;
suppose
A6: not 0 in A & not 0 in B;
then
A7: not 0 in (A \/ B) by XBOOLE_0:def 3;
P.A = 0 & P.B = 0 by A6,Lm1;
hence thesis by A7,Lm1;
end;
end;
hence thesis;
end;
for ASeq st ASeq is non-ascending holds P * ASeq is convergent & lim (P *
ASeq) = P.Intersection ASeq
proof
let ASeq;
A1: now
let n;
A2: n in NAT by ORDINAL1:def 12;
dom (P * ASeq) = NAT by FUNCT_2:def 1;
hence (P * ASeq).n = P.(ASeq.n) by A2,FUNCT_1:12;
end;
assume
A3: ASeq is non-ascending;
now
per cases;
suppose
A4: for n holds 0 in ASeq.n;
rng ASeq c= Borel_Sets by RELAT_1:def 19;
then
A5: Intersection ASeq in Borel_Sets by PROB_1:def 6;
A6: 0 in Intersection ASeq by A4,PROB_1:13;
A7: now
let n;
A8: rng ASeq c= Borel_Sets & ASeq.n in rng ASeq by NAT_1:51,RELAT_1:def 19;
A9: ASeq.n in Borel_Sets by A8;
0 in ASeq.n by A4;
then P.(ASeq.n) = 1 by Lm1,A9;
hence (P * ASeq).n = 1 by A1;
end;
A10: ex m st for n st m <= n holds (P * ASeq).n = 1
proof
take 0;
thus thesis by A7;
end;
then lim (P * ASeq) = 1 by PROB_1:1;
hence thesis by A10,A6,A5,Lm1,PROB_1:1;
end;
suppose
A11: not (for n holds 0 in ASeq.n);
rng ASeq c= Borel_Sets by RELAT_1:def 19;
then
A12: Intersection ASeq in Borel_Sets by PROB_1:def 6;
A13: not 0 in Intersection ASeq by A11,PROB_1:13;
A14: ex m st for n st m <= n holds (P * ASeq).n = 0
proof
consider m such that
A15: not 0 in ASeq.m by A11;
take m;
for n st m <= n holds (P * ASeq).n = 0
proof
let n;
assume m <= n;
then ASeq.n c= ASeq.m by A3,PROB_1:def 4;
then
A16: not 0 in ASeq.n by A15;
rng ASeq c= Borel_Sets & ASeq.n in rng ASeq
by NAT_1:51,RELAT_1:def 19;
then ASeq.n in Borel_Sets;
then P.(ASeq.n) = 0 by A16,Lm1;
hence thesis by A1;
end;
hence thesis;
end;
then lim (P * ASeq) = 0 by PROB_1:1;
hence thesis by A14,A13,A12,Lm1,PROB_1:1;
end;
end;
hence thesis;
end;
then reconsider P as Probability of Borel_Sets by Lm2,Lm3,Lm4,PROB_1:def 8;
set f = { [ [0,0], P] };
dom f = { [0,0] } by RELAT_1:9;
then
Lm5: dom f = [:X,X:] by ZFMISC_1:29;
rng f = {P} & P in Probabilities(Borel_Sets) by Def1,RELAT_1:9;
then rng f c= Probabilities(Borel_Sets) by ZFMISC_1:31;
then reconsider
Y = f as Function of [:X, X:], Probabilities(Borel_Sets) by Lm5,FUNCT_2:def 1
,RELSET_1:4;
Lm6: now
thus for A1,A2 being Element of Obs QM_Str(#X,X,Y#) st for s being Element
of Sts QM_Str(#X,X,Y#) holds Meas(A1,s)=Meas(A2,s) holds A1=A2
proof
let A1,A2 be Element of Obs QM_Str(#X,X,Y#);
A1=0 by TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
thus for s1,s2 being Element of Sts QM_Str(#X,X,Y#) st for A being Element
of Obs QM_Str(#X,X,Y#) holds Meas(A,s1)=Meas(A,s2) holds s1=s2
proof
let s1,s2 be Element of Sts QM_Str(#X,X,Y#);
s1=0 by TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
thus for s1,s2 being Element of Sts QM_Str(#X,X,Y#), t being Real st 0<=t &
t<=1 ex s being Element of Sts QM_Str(#X,X,Y#) st for A being Element of Obs
QM_Str(#X,X,Y#), E holds Meas(A,s).E=t*(Meas(A,s1).E) + ((1-t)*Meas(A,s2).E)
proof
let s1,s2 be Element of Sts QM_Str(#X,X,Y#);
let t be Real;
assume 0<=t & t<=1;
take s2;
let A be Element of Obs QM_Str(#X,X,Y#), E;
s1=0 & s2=0 by TARSKI:def 1;
hence thesis;
end;
end;
definition let IT be QM_Str;
attr IT is Quantum_Mechanics-like means
:Def5:
(for A1,A2 being Element of Obs IT st
for s being Element of Sts IT holds Meas(A1,s)=Meas(A2,s) holds A1=A2) &
(for s1,s2 being Element of Sts IT st for A being Element of Obs IT holds
Meas(A,s1)=Meas(A,s2) holds s1=s2) &
for s1,s2 being Element of Sts IT, t being Real st 0<=t & t<=1
ex s being Element of Sts IT st for A being Element of Obs IT, E holds
Meas(A,s).E=t*(Meas(A,s1).E) + ((1-t)*Meas(A,s2).E);
end;
registration
cluster strict Quantum_Mechanics-like for QM_Str;
existence
by Def5,Lm6;
end;
definition
mode Quantum_Mechanics is Quantum_Mechanics-like QM_Str;
end;
reserve Q for Quantum_Mechanics;
reserve s for Element of Sts Q;
definition
struct(RelStr,ComplStr) OrthoRelStr(# carrier -> set,
InternalRel -> (Relation of the carrier),
Compl -> Function of the carrier,the carrier #);
end;
reserve x1 for Element of X1;
reserve Inv for Function of X1,X1;
definition let X1, Inv;
pred Inv is_an_involution means
Inv.(Inv.x1) = x1;
end;
definition let W be OrthoRelStr;
pred W is_a_Quantum_Logic means
the InternalRel of W partially_orders the carrier of W &
the Compl of W is_an_involution &
for x,y being Element of W st
[x,y] in the InternalRel of W holds
[(the Compl of W).y,(the Compl of W).x] in the InternalRel of W;
end;
definition let Q;
func Prop Q -> set equals
[:Obs Q,Borel_Sets:];
coherence;
end;
registration let Q;
cluster Prop Q -> non empty;
coherence;
end;
reserve p,q,r,p1,q1 for Element of Prop Q;
definition let Q,p;
redefine func p`1 -> Element of Obs Q; :: redefines `1 (XTUPLE_0, definition)
coherence by MCART_1:10;
redefine func p`2 -> Event of Borel_Sets; :: redefines `2 (XTUPLE_0, definition)
coherence by MCART_1:10;
end;
theorem Th1:
for E st E = p`2` holds Meas(p`1,s).p`2 = 1 - Meas(p`1,s).E
proof
let E such that
A1: E = p`2`;
[#] Borel_Sets = REAL & REAL \ E = E` by PROB_1:def 7;
hence thesis by A1,PROB_1:32;
end;
definition let Q,p;
func 'not' p -> Element of Prop Q equals
[p`1,(p`2)`];
coherence
proof
reconsider x = p`2` as Event of Borel_Sets by PROB_1:20;
x in Borel_Sets;
hence thesis by ZFMISC_1:87;
end;
involutiveness by MCART_1:21;
end;
definition let Q,p,q;
pred p |- q means
for s holds Meas(p`1,s).p`2 <= Meas(q`1,s).q`2;
reflexivity;
end;
definition let Q,p,q;
pred p <==> q means
p |- q & q |- p;
reflexivity;
symmetry;
end;
theorem Th2:
p <==> q iff for s holds Meas(p`1,s).p`2 = Meas(q`1,s).q`2
proof
thus p <==> q implies for s holds Meas(p`1,s).p`2 = Meas(q`1,s).q`2
proof
assume
A1: p <==> q;
let s;
q |- p by A1; then
A2: Meas(q`1,s).q`2 <= Meas(p`1,s).p`2;
p |- q by A1;
then Meas(p`1,s).p`2 <= Meas(q`1,s).q`2;
hence thesis by A2,XXREAL_0:1;
end;
assume
A3: for s holds Meas(p`1,s).p`2 = Meas(q`1,s).q`2;
thus p |- q
by A3;
let s;
thus thesis by A3;
end;
theorem
p |- p;
theorem Th4:
p |- q & q |- r implies p |- r
proof
assume
A1: p |- q & q |- r;
let s;
Meas(p`1,s).p`2 <= Meas(q`1,s).q`2 & Meas(q`1,s).q`2 <= Meas(r`1,s).r`2
by A1;
hence thesis by XXREAL_0:2;
end;
theorem
p <==> p;
theorem
p <==> q implies q <==> p;
theorem Th7:
p <==> q & q <==> r implies p <==> r
by Th4;
::$CT
theorem Th8:
p |- q implies 'not' q |- 'not' p
proof
assume
A1: p |- q;
let s;
reconsider E1 = q`2` as Event of Borel_Sets by PROB_1:20;
reconsider E = p`2` as Event of Borel_Sets by PROB_1:20;
set p1 = Meas(p`1,s).E, p2 = Meas(q`1,s).E1;
A2: -(1-p1) = p1 -1 & -(1-p2) = p2 -1;
A4: Meas(q`1,s).q`2 = 1 - p2 & Meas(p`1,s).p`2 = 1 - p1 by Th1;
Meas(p`1,s).p`2 <= Meas(q`1,s).q`2 by A1;
then p2 -1 <= p1 - 1 by A4,A2,XREAL_1:24;
hence thesis by XREAL_1:9;
end;
definition let Q;
func PropRel Q -> Equivalence_Relation of Prop Q means
:Def12:
[p,q] in it iff p <==> q;
existence
proof
defpred P[object,object] means ex p,q st p=$1 & q = $2 & p <==> q;
A1: for x,y being object st P[x,y] holds P[y,x];
A2: for x,y,z being object st P[x,y] & P[y,z] holds P[x,z] by Th7;
A3: for x being object st x in Prop Q holds P[x,x];
consider R being Equivalence_Relation of Prop Q such that
A4: for x,y being object
holds [x,y] in R iff x in Prop Q & y in Prop Q & P[x,y]
from EQREL_1:sch 1(A3,A1,A2);
take R;
[p,q] in R iff p <==> q
proof
thus [p,q] in R implies p <==> q
proof
assume [p,q] in R;
then ex p1,q1 st p1=p & q1=q & p1 <==> q1 by A4;
hence thesis;
end;
assume p <==> q;
hence thesis by A4;
end;
hence thesis;
end;
uniqueness
proof
let R1,R2 be Equivalence_Relation of Prop Q;
assume that
A5: for p,q holds [p,q] in R1 iff p <==> q and
A6: for p,q holds [p,q] in R2 iff p <==> q;
A7: for p,q holds [p,q] in R1 iff [p,q] in R2 by A5,A6;
for x,y being object holds [x,y] in R1 iff [x,y] in R2
proof
let x,y be object;
thus [x,y] in R1 implies [x,y] in R2
proof
assume
A8: [x,y] in R1;
then x is Element of Prop Q & y is Element of Prop Q by ZFMISC_1:87;
hence thesis by A7,A8;
end;
assume
A9: [x,y] in R2;
then x is Element of Prop Q & y is Element of Prop Q by ZFMISC_1:87;
hence thesis by A7,A9;
end;
hence thesis by RELAT_1:def 2;
end;
end;
reserve B,C for Subset of Prop Q;
theorem Th9:
for B,C st B in Class PropRel Q & C in Class PropRel Q for a,b,c
,d being Element of Prop Q holds a in B & b in B & c in C & d in C & a |- c
implies b |- d
proof
let B,C such that
A1: B in Class PropRel Q and
A2: C in Class PropRel Q;
let a,b,c,d be Element of Prop Q;
assume that
A3: a in B & b in B and
A4: c in C & d in C;
assume
A5: a |- c;
let s;
ex y being object st y in Prop Q & C = Class(PropRel Q,y)
by A2,EQREL_1:def 3;
then [c,d] in PropRel Q by A4,EQREL_1:22;
then c <==> d by Def12;
then
A6: Meas(c`1,s).c`2 = Meas(d`1,s).d`2 by Th2;
ex x being object st x in Prop Q & B = Class(PropRel Q,x)
by A1,EQREL_1:def 3;
then [a,b] in PropRel Q by A3,EQREL_1:22;
then a <==> b by Def12;
then Meas(a`1,s).a`2 = Meas(b`1,s).b`2 by Th2;
hence thesis by A5,A6;
end;
definition let Q;
func OrdRel Q -> Relation of Class PropRel (Q) means
:Def13:
[B,C] in it iff B in Class PropRel Q & C in Class PropRel Q &
for p,q st p in B & q in C holds p |- q;
existence
proof
defpred P[object,object] means
ex B,C st $1 = B & $2 = C & for p,q st p in B & q
in C holds p |- q;
consider R being Relation of Class PropRel Q,Class PropRel Q such that
A1: for x,y being object
holds [x,y] in R iff x in Class PropRel Q & y in Class
PropRel Q & P[x,y] from RELSET_1:sch 1;
[B,C] in R iff B in Class PropRel Q & C in Class PropRel Q & for p,q
st p in B & q in C holds p |- q
proof
thus [B,C] in R implies B in Class PropRel Q & C in Class PropRel Q &
for p,q st p in B & q in C holds p |- q
proof
assume
A2: [B,C] in R; then
ex B9,C9 being Subset of Prop Q st B = B9 & C = C9 & for p,q st p
in B9 & q in C9 holds p |- q by A1;
hence thesis by A1,A2;
end;
assume B in Class PropRel Q & C in Class PropRel Q & for p,q st p in B
& q in C holds p |- q;
hence thesis by A1;
end;
hence thesis;
end;
uniqueness
proof
let R1,R2 be Relation of Class PropRel Q;
assume that
A3: for B,C holds [B,C] in R1 iff B in Class PropRel Q & C in Class
PropRel Q & for p,q st p in B & q in C holds p |- q and
A4: for B,C holds [B,C] in R2 iff B in Class PropRel Q & C in Class
PropRel Q & for p,q st p in B & q in C holds p |- q;
A5: now
let B,C;
[B,C] in R1 iff B in Class PropRel Q & C in Class PropRel Q & for p
,q st p in B & q in C holds p |- q by A3;
hence [B,C] in R1 iff [B,C] in R2 by A4;
end;
for x,y being object holds [x,y] in R1 iff [x,y] in R2
proof
let x,y be object;
thus [x,y] in R1 implies [x,y] in R2
proof
assume
A6: [x,y] in R1;
then x in Class PropRel Q & y in Class PropRel Q by ZFMISC_1:87;
hence thesis by A5,A6;
end;
assume
A7: [x,y] in R2;
then x in Class PropRel Q & y in Class PropRel Q by ZFMISC_1:87;
hence thesis by A5,A7;
end;
hence thesis by RELAT_1:def 2;
end;
end;
theorem Th10:
p |- q iff [Class(PropRel Q,p),Class(PropRel Q,q)] in OrdRel Q
proof
[p,p] in PropRel Q by Def12;
then
A1: p in Class(PropRel Q,p) by EQREL_1:19;
[q,q] in PropRel Q by Def12;
then
A2: q in Class(PropRel Q,q) by EQREL_1:19;
A3: Class(PropRel Q,p) in Class PropRel Q & Class(PropRel Q,q) in Class
PropRel Q by EQREL_1:def 3;
thus p |- q implies [Class(PropRel Q,p),Class(PropRel Q,q)] in OrdRel Q
proof
assume p |- q;
then for p1,q1 holds p1 in Class(PropRel Q,p) & q1 in Class(PropRel Q,q)
implies p1 |- q1 by A1,A2,A3,Th9;
hence thesis by A3,Def13;
end;
thus thesis by A1,A2,Def13;
end;
theorem Th11:
for B,C st B in Class PropRel Q & C in Class PropRel Q for p1,q1
holds p1 in B & q1 in B & 'not' p1 in C implies 'not' q1 in C
proof
let B,C such that
A1: B in Class PropRel Q and
A2: C in Class PropRel Q;
consider y being object such that
A3: y in Prop Q and
A4: C = Class(PropRel Q,y) by A2,EQREL_1:def 3;
let p1,q1;
assume that
A5: p1 in B & q1 in B and
A6: 'not' p1 in C;
ex x being object st x in Prop Q & B = Class(PropRel Q,x)
by A1,EQREL_1:def 3;
then [p1,q1] in PropRel Q by A5,EQREL_1:22;
then
A7: p1 <==> q1 by Def12;
now
reconsider E1 = q1`2`, E = p1`2` as Event of Borel_Sets
by PROB_1:20;
let s;
set r1 = Meas(p1`1,s).E, r2 = Meas(q1`1,s).E1;
1 - r1 = Meas(p1`1,s).p1`2 by Th1
.= Meas(q1`1,s).q1`2 by A7,Th2
.= 1 - r2 by Th1;
hence
Meas(('not' p1)`1,s).('not' p1)`2 = Meas(('not' q1)`1,s).('not' q1)`2
;
end;
then
A10: 'not' p1 <==> 'not' q1 by Th2;
reconsider q = y as Element of Prop Q by A3;
['not' p1,q] in PropRel Q by A4,A6,EQREL_1:19;
then 'not' p1 <==> q by Def12;
then q <==> 'not' q1 by A10,Th7;
then ['not' q1,q] in PropRel Q by Def12;
hence thesis by A4,EQREL_1:19;
end;
theorem
for B,C st B in Class PropRel Q & C in Class PropRel Q for p,q holds
'not' p in C & 'not' q in C & p in B implies q in B
proof
let B,C such that
A1: B in Class PropRel Q & C in Class PropRel Q;
let p,q;
'not'('not' p) = p & 'not'('not' q) =q;
hence thesis by A1,Th11;
end;
definition let Q;
func InvRel Q -> Function of Class PropRel Q,Class PropRel Q means
:Def14:
it.Class(PropRel Q,p) = Class(PropRel Q,'not' p);
existence
proof
defpred P[object,object] means
for p st $1 = Class(PropRel Q,p) holds $2 = Class
(PropRel Q,'not' p);
A1: for x being object st x in Class PropRel Q
ex y being object st y in Class PropRel Q & P[x,y]
proof
let x be object;
assume
A2: x in Class PropRel Q;
then consider q such that
A3: x = Class(PropRel Q,q) by EQREL_1:36;
reconsider y = Class(PropRel Q,'not' q) as set;
take y;
thus
A4: y in Class PropRel Q by EQREL_1:def 3;
let p;
assume
A5: x = Class(PropRel Q,p);
then reconsider x as Subset of Prop Q;
A6: q in x by A3,EQREL_1:20;
reconsider y9=y as Subset of Prop Q;
A7: 'not' q in y9 by EQREL_1:20;
p in x by A5,EQREL_1:20;
then 'not' p in y9 by A2,A4,A6,A7,Th11;
hence thesis by EQREL_1:23;
end;
consider F being Function of Class PropRel Q,Class PropRel Q such that
A8: for x being object st x in Class PropRel Q holds P[x,F.x]
from FUNCT_2:sch 1(
A1);
take F;
let p;
Class(PropRel Q,p) in Class PropRel Q by EQREL_1:def 3;
hence thesis by A8;
end;
uniqueness
proof
let F1,F2 be Function of Class PropRel Q,Class PropRel Q;
assume that
A9: for p holds F1.Class(PropRel Q,p) = Class(PropRel Q,'not' p) and
A10: for p holds F2.Class(PropRel Q,p) = Class(PropRel Q,'not' p);
now let x be object;
assume x in Class PropRel Q;
then consider p such that
A11: x = Class(PropRel Q, p) by EQREL_1:36;
F1.x = Class(PropRel Q,'not' p) by A9,A11;
hence F1.x = F2.x by A10,A11;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem :: Main Theorem
for Q holds OrthoRelStr(#Class PropRel Q,OrdRel Q,InvRel Q#)
is_a_Quantum_Logic
proof
let Q;
A1: OrdRel Q is_transitive_in Class PropRel Q
proof
let x,y,z be object;
assume that
A2: x in Class PropRel Q and
A3: y in Class PropRel Q and
A4: z in Class PropRel Q and
A5: [x,y] in OrdRel Q & [y,z] in OrdRel Q;
consider p such that
A6: x = Class(PropRel Q,p) by A2,EQREL_1:36;
consider r such that
A7: z = Class(PropRel Q,r) by A4,EQREL_1:36;
consider q such that
A8: y = Class(PropRel Q,q) by A3,EQREL_1:36;
p |- q & q |- r implies p |- r by Th4;
hence thesis by A5,A6,A8,A7,Th10;
end;
A9: OrdRel Q is_antisymmetric_in Class PropRel Q
proof
let x,y be object;
assume that
A10: x in Class PropRel Q and
A11: y in Class PropRel Q and
A12: [x,y] in OrdRel Q & [y,x] in OrdRel Q;
consider p such that
A13: x = Class(PropRel Q,p) by A10,EQREL_1:36;
consider q such that
A14: y = Class(PropRel Q,q) by A11,EQREL_1:36;
A15: p <==> q implies [p,q] in PropRel Q by Def12;
thus thesis by A12,A13,A14,A15,Th10,EQREL_1:35;
end;
A16: for x,y being Element of Class PropRel Q st [x,y] in OrdRel Q holds
[(InvRel Q).y,(InvRel Q).x] in OrdRel Q
proof
let x,y be Element of Class PropRel Q;
consider p such that
A17: x = Class(PropRel Q,p) by EQREL_1:36;
consider q such that
A18: y = Class(PropRel Q,q) by EQREL_1:36;
A19: p |- q implies 'not' q |- 'not' p by Th8;
(InvRel Q).Class(PropRel Q,p) = Class(PropRel Q,'not' p) & (InvRel Q)
.Class( PropRel Q,q) = Class(PropRel Q,'not' q) by Def14;
hence thesis by A17,A18,A19,Th10;
end;
A20: InvRel Q is_an_involution
proof
let x be Element of Class PropRel Q;
consider p such that
A21: x = Class(PropRel Q,p) by EQREL_1:36;
(InvRel Q).((InvRel Q).x) = (InvRel Q).Class(PropRel Q,'not' p) by A21
,Def14
.= Class(PropRel Q,'not'('not' p)) by Def14;
hence thesis by A21;
end;
OrdRel Q is_reflexive_in Class PropRel Q
proof
let x be object;
assume x in Class PropRel Q;
then ex p st x = Class(PropRel Q,p) by EQREL_1:36;
hence thesis by Th10;
end;
then OrdRel Q partially_orders Class PropRel Q by A1,A9,ORDERS_1:def 8;
hence thesis by A20,A16;
end;