### The Mizar article:

### The Fundamental Logic Structure in Quantum Mechanics

**by****Pawel Sadowski,****Andrzej Trybulec, and****Konrad Raczkowski**

- Received December 18, 1989
Copyright (c) 1989 Association of Mizar Users

- MML identifier: QMAX_1
- [ MML identifier index ]

environ vocabulary PROB_1, FUNCT_2, FUNCT_1, BOOLE, SEQ_2, ORDINAL2, RELAT_1, ARYTM_1, ORDERS_2, MCART_1, SUBSET_1, ZF_LANG, EQREL_1, RELAT_2, QMAX_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, RELAT_1, RELSET_1, RELAT_2, FUNCT_1, REAL_1, FUNCT_2, ORDERS_2, DOMAIN_1, SEQ_2, PROB_1, MCART_1, EQREL_1; constructors RELAT_2, ORDERS_2, DOMAIN_1, SEQ_2, PROB_1, EQREL_1, XCMPLX_0, MEMBERED, XBOOLE_0; clusters RELSET_1, XREAL_0, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2, EQREL_1, PARTFUN1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions RELAT_2, ORDERS_2; theorems TARSKI, FUNCT_1, GRFUNC_1, REAL_1, ZFMISC_1, SUBSET_1, FUNCT_2, PROB_1, MCART_1, EQREL_1, RELAT_1, AXIOMS, RELSET_1, XBOOLE_0, XCMPLX_1; 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: x in it iff x is Probability of S; existence proof defpred P[set] means $1 is Probability of S; consider X being set such that A1: x in X iff x in Funcs(S,REAL) & P[x] from Separation; take X; let x; x is Probability of S implies x in Funcs(S,REAL) by FUNCT_2:11; hence thesis by A1; end; uniqueness proof let A1,A2 be set; assume that A2: x in A1 iff x is Probability of S and A3: x in A2 iff x is Probability of S; now let y; 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; definition let X; let S be SigmaField of X; cluster Probabilities(S) -> non empty; coherence proof consider x being Probability of S; x in Probabilities(S) by Def1; hence thesis; end; end; definition struct QM_Str (# Observables, States -> non empty set, Quantum_Probability -> Function of [:the Observables, the States:], Probabilities(Borel_Sets) #); end; reserve Q for QM_Str; definition let Q; func Obs Q -> set equals :Def2: the Observables of Q; coherence; func Sts Q -> set equals :Def3: the States of Q; coherence; end; definition let Q; cluster Obs Q -> non empty; coherence proof the Observables of Q is non empty; hence thesis by Def2; end; cluster Sts Q -> non empty; coherence proof the States of Q is non empty; hence thesis by Def3; end; 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 Obs Q = the Observables of Q & Sts Q = the States of Q by Def2,Def3; then reconsider A1s = [A1,s] as Element of [:the Observables of Q, the States of Q:]; (the Quantum_Probability of Q).A1s is Element of Probabilities Borel_Sets; hence thesis by Def1; end; end; reconsider X = {0} as non empty set; 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:60; Lm2: for A holds (0 in A implies P.A = 1) & (not 0 in A implies P.A = 0) proof let A; A in Borel_Sets by PROB_1:def 10; hence thesis by Lm1; end; Lm3: for A holds 0 <= P.A proof let A; now per cases; suppose 0 in A; then P.A = 1 by Lm2;hence 0 <= P.A; suppose not 0 in A; hence 0 <= P.A by Lm2; end; hence thesis; end; Lm4: P.REAL = 1 proof REAL c= REAL; then reconsider Omega = REAL as Subset of REAL; Omega in Borel_Sets by PROB_1:43; hence thesis by Lm1; end; Lm5: 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: P.A = 1 & P.B = 0 by Lm2; 0 in A \/ B by A2,XBOOLE_0:def 2; hence P.(A \/ B) = P.A + P.B by A3,Lm2; suppose A4: not 0 in A & 0 in B; then A5: P.A = 0 & P.B = 1 by Lm2; 0 in A \/ B by A4,XBOOLE_0:def 2; hence P.(A \/ B) = P.A + P.B by A5,Lm2; suppose A6: not 0 in A & not 0 in B; then A7: P.A = 0 & P.B = 0 by Lm2; not 0 in (A \/ B) by A6,XBOOLE_0:def 2; hence P.(A \/ B)=P.A + P.B by A7,Lm2; end; hence thesis; end; for ASeq st ASeq is non-increasing holds P * ASeq is convergent & lim (P * ASeq) = P.Intersection ASeq proof let ASeq; assume A1: ASeq is non-increasing; A2: now let n; dom (P * ASeq) = NAT by FUNCT_2:def 1; hence (P * ASeq).n = P.(ASeq.n) by FUNCT_1:22; end; now per cases; suppose A3: for n holds 0 in ASeq.n; A4: now let n; A5: ASeq.n in Borel_Sets by PROB_1:def 9; 0 in ASeq.n by A3; then P.(ASeq.n) = 1 by A5,Lm1; hence (P * ASeq).n = 1 by A2; end; reconsider r = 1 as Real; ex m st for n st m <= n holds (P * ASeq).n = r proof take 0; thus thesis by A4; end; then A6: P * ASeq is convergent & lim (P * ASeq) = 1 by PROB_1:3; A7: 0 in Intersection ASeq by A3,PROB_1:29; for n holds ASeq.n in Borel_Sets by PROB_1:def 9; then Intersection ASeq in Borel_Sets by PROB_1:def 8; hence P * ASeq is convergent & lim (P * ASeq) = P.Intersection ASeq by A6,A7,Lm1; suppose A8: not (for n holds 0 in ASeq.n); ex m st (for n st m <= n holds (P * ASeq).n = 0) proof consider m such that A9: not 0 in ASeq.m by A8; 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 A1,PROB_1:def 6; then A10: not 0 in ASeq.n by A9; ASeq.n in Borel_Sets by PROB_1:def 9; then P.(ASeq.n) = 0 by A10,Lm1; hence thesis by A2; end; hence thesis; end; then A11: P * ASeq is convergent & lim (P * ASeq) = 0 by PROB_1:3; A12: not 0 in Intersection ASeq by A8,PROB_1:29; for n holds ASeq.n in Borel_Sets by PROB_1:def 9; then Intersection ASeq in Borel_Sets by PROB_1:def 8; hence P * ASeq is convergent & lim (P * ASeq) = P.Intersection ASeq by A11,A12 ,Lm1; end; hence thesis; end; then reconsider P as Probability of Borel_Sets by Lm3,Lm4,Lm5,PROB_1:def 13; reconsider f = { [ [0,0], P] } as Function by GRFUNC_1:15; Lm6: dom f = { [0,0] } & rng f = {P} by RELAT_1:23; then Lm7: dom f = [:X,X:] by ZFMISC_1:35; P in Probabilities(Borel_Sets) by Def1; then rng f c= Probabilities(Borel_Sets) by Lm6,ZFMISC_1:37; then reconsider Y = f as Function of [:X, X:], Probabilities(Borel_Sets) by Lm7,FUNCT_2:def 1,RELSET_1:11; Lm8: 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 A1: Obs QM_Str(#X,X,Y#) = X by Def2; let A1,A2 be Element of Obs QM_Str(#X,X,Y#); A1=0 & A2=0 by A1,TARSKI:def 1; hence thesis; end; A2: Sts QM_Str(#X,X,Y#) = X by Def3; 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 & s2=0 by A2,TARSKI:def 1; hence thesis; 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#); A3: s1=0 & s2=0 by A2,TARSKI:def 1; let t be Real; assume 0<=t & t<=1; take s2; let A be Element of Obs QM_Str(#X,X,Y#), E; thus Meas(A,s2).E = 1*Meas(A,s2).E .= (t + (1-t))*Meas(A,s2).E by XCMPLX_1:27 .= t*Meas(A,s1).E + (1-t)*Meas(A,s2).E by A3,XCMPLX_1:8; 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; definition cluster strict Quantum_Mechanics-like QM_Str; existence proof QM_Str(#X,X,Y#) is Quantum_Mechanics-like by Def5,Lm8; hence thesis; end; 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 let X be set; struct POI_Str over X (# Ordering -> (Relation of X), Involution -> Function of X,X #); end; reserve x1 for Element of X1; reserve Inv for Function of X1,X1; definition let X1, Inv; pred Inv is_an_involution_in X1 means Inv.(Inv.x1) = x1; end; definition let X1; let W be POI_Str over X1; pred W is_a_Quantuum_Logic_on X1 means :Def7: ex Ord being (Relation of X1), Inv being Function of X1,X1 st W = POI_Str(#Ord,Inv#) & Ord partially_orders X1 & Inv is_an_involution_in X1 & for x,y being Element of X1 st [x,y] in Ord holds [Inv.y,Inv.x] in Ord; end; definition let Q; func Prop Q -> set equals :Def8: [:Obs Q,Borel_Sets:]; coherence; end; definition let Q; cluster Prop Q -> non empty; coherence proof Prop Q = [:Obs Q,Borel_Sets:] by Def8; hence thesis; end; end; reserve p,q,r,p1,q1 for Element of Prop Q; definition let Q,p; redefine func p`1 -> Element of Obs Q; coherence proof Prop Q = [:Obs Q,Borel_Sets:] by Def8; hence thesis by MCART_1:10; end; func p`2 -> Event of Borel_Sets; coherence proof Prop Q = [:Obs Q,Borel_Sets:] by Def8; then p`2 in Borel_Sets by MCART_1:10; hence thesis by PROB_1:48; end; end; canceled 13; theorem Th14: p = [p`1,p`2] proof Prop Q = [:Obs Q,Borel_Sets:] by Def8; hence thesis by MCART_1:23; end; canceled; theorem Th16: 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`; A2: [#] Borel_Sets = REAL by PROB_1:def 11; REAL \ E = E` by SUBSET_1:def 5; hence thesis by A1,A2,PROB_1:68; end; definition let Q,p; func 'not' p -> Element of Prop Q equals :Def9: [p`1,(p`2)`]; coherence proof A1: Prop Q = [:Obs Q,Borel_Sets:] by Def8; reconsider x = p`2` as Event of Borel_Sets by PROB_1:50; x in Borel_Sets by PROB_1:def 10; hence thesis by A1,ZFMISC_1:106; end; end; definition let Q,p,q; pred p |- q means :Def10: for s holds Meas(p`1,s).p`2 <= Meas(q`1,s).q`2; end; definition let Q,p,q; pred p <==> q means :Def11: p |- q & q |- p; end; canceled 3; theorem Th20: 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 p <==> q; then A1: p |- q & q |- p by Def11; let s; Meas(p`1,s).p`2 <= Meas(q`1,s).q`2 & Meas(q`1,s).q`2 <= Meas(p`1,s).p`2 by A1,Def10; hence thesis by AXIOMS:21; end; assume A2: for s holds Meas(p`1,s).p`2 = Meas(q`1,s).q`2; thus p |- q proof let s; thus thesis by A2; end; let s; thus thesis by A2; end; theorem Th21: p |- p proof let s; thus thesis; end; theorem Th22: 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,Def10; hence thesis by AXIOMS:22; end; theorem Th23: p <==> p proof p |- p by Th21; hence thesis by Def11; end; theorem Th24: p <==> q implies q <==> p proof assume p |- q & q |- p; hence thesis by Def11; end; theorem Th25: p <==> q & q <==> r implies p <==> r proof assume p |- q & q |- p & q |- r & r |- q; hence p |- r & r |- p by Th22; end; theorem Th26: ('not' p)`1 = p`1 & ('not' p)`2 = (p`2)` proof 'not' p = [p`1,(p`2)`] by Def9; hence thesis by MCART_1:7; end; theorem Th27: 'not'('not' p) = p proof thus 'not'('not' p) = [('not' p)`1,(('not' p)`2)`] by Def9 .= [p`1,(('not' p)`2)`] by Th26 .= [p`1,((p`2)`)`] by Th26 .= p by Th14; end; theorem Th28: p |- q implies 'not' q |- 'not' p proof assume A1: p |- q; reconsider E = p`2` as Event of Borel_Sets by PROB_1:50; reconsider E1 = q`2` as Event of Borel_Sets by PROB_1:50; let s; set p1 = Meas(p`1,s).E, p2 = Meas(q`1,s).E1; A2: Meas(q`1,s).q`2 = 1 - p2 & Meas(p`1,s).p`2 = 1 - p1 by Th16; A3: -(1-p1) = p1 -1 & -(1-p2) = p2 -1 by XCMPLX_1:143; Meas(p`1,s).p`2 <= Meas(q`1,s).q`2 by A1,Def10; then A4: p2 -1 <= p1 - 1 by A2,A3,REAL_1:50; ('not' q)`1 = q`1 & ('not' q)`2 = (q`2)` & ('not' p)`1 = p`1 & ('not' p)`2 = (p`2)` by Th26; hence thesis by A4,REAL_1:54; 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[set,set] means ex p,q st p=$1 & q = $2 & p <==> q; A1: for x st x in Prop Q holds P[x,x] proof let x; assume x in Prop Q; then reconsider x as Element of Prop Q; A2: x<==>x by Th23; take x; thus thesis by A2; end; A3: for x,y st P[x,y] holds P[y,x] proof let x,y; given p1,q1 such that A4: p1=x & q1=y & p1<==>q1; take q1,p1; thus thesis by A4,Th24; end; A5: for x,y,z st P[x,y] & P[y,z] holds P[x,z] proof let x,y,z; assume that A6: ex p,q st p=x & q=y & p <==> q and A7: ex p1,q1 st p1=y & q1=z & p1 <==> q1; consider p,q such that A8: p=x & q=y & p <==> q by A6; consider p1,q1 such that A9: p1=y & q1=z & p1 <==> q1 by A7; take p,q1; thus thesis by A8,A9,Th25; end; consider R being Equivalence_Relation of Prop Q such that A10: for x,y holds [x,y] in R iff x in Prop Q & y in Prop Q & P[x,y] from Ex_Eq_Rel(A1,A3,A5); 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 A10; hence thesis; end; assume p <==> q; hence thesis by A10; end; hence thesis; end; uniqueness proof let R1,R2 be Equivalence_Relation of Prop Q; assume A11: (for p,q holds [p,q] in R1 iff p <==> q) & (for p,q holds [p,q] in R2 iff p <==> q); A12: now let p,q; ([p,q] in R1 iff p <==> q) & ([p,q] in R2 iff p <==> q) by A11; hence [p,q] in R1 iff [p,q] in R2; end; for x,y holds [x,y] in R1 iff [x,y] in R2 proof let x,y; thus [x,y] in R1 implies [x,y] in R2 proof assume A13: [x,y] in R1; then x is Element of Prop Q & y is Element of Prop Q by ZFMISC_1:106 ; hence thesis by A12,A13; end; assume A14: [x,y] in R2; then x is Element of Prop Q & y is Element of Prop Q by ZFMISC_1:106; hence thesis by A12,A14; end; hence thesis by RELAT_1:def 2; end; end; reserve B,C for Subset of Prop Q; canceled; theorem Th30: 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) & C in Class PropRel(Q); let a,b,c,d be Element of Prop Q; A2: ex x st x in Prop Q & B = Class(PropRel(Q),x) by A1,EQREL_1:def 5; A3: ex y st y in Prop Q & C = Class(PropRel(Q),y) by A1,EQREL_1:def 5; assume a in B & b in B & c in C & d in C; then [a,b] in PropRel(Q) & [c,d] in PropRel(Q) by A2,A3,EQREL_1:30; then A4: a <==> b & c <==> d by Def12; assume A5: a |- c; let s; Meas(a`1,s).a`2 = Meas(b`1,s).b`2 & Meas(c`1,s).c`2 = Meas(d`1,s).d`2 by A4,Th20; hence thesis by A5,Def10; 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[set,set] 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 holds [x,y] in R iff x in Class PropRel(Q) & y in Class PropRel(Q) & P[x,y] from Rel_On_Set_Ex; [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 [B,C] in R; then B in Class PropRel(Q) & C in Class PropRel(Q) & ex B',C' being Subset of Prop Q st B = B' & C = C' & for p,q st p in B' & q in C' holds p |- q by A1; hence thesis; 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 A2: 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 A3: 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; A4: 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 A2; hence [B,C] in R1 iff [B,C] in R2 by A3; end; for x,y holds [x,y] in R1 iff [x,y] in R2 proof let x,y; thus [x,y] in R1 implies [x,y] in R2 proof assume A5: [x,y] in R1; then x in Class PropRel(Q) & y in Class PropRel(Q) by ZFMISC_1:106; hence thesis by A4,A5; end; assume A6: [x,y] in R2; then x in Class PropRel(Q) & y in Class PropRel(Q) by ZFMISC_1:106; hence thesis by A4,A6; end; hence thesis by RELAT_1:def 2; end; end; canceled; theorem Th32: p |- q iff [Class(PropRel(Q),p),Class(PropRel(Q),q)] in OrdRel(Q) proof p <==> p & q <==> q by Th23; then [p,p] in PropRel(Q) & [q,q] in PropRel(Q) by Def12; then A1: p in Class(PropRel(Q),p) & q in Class(PropRel(Q),q) by EQREL_1:27; A2: Class(PropRel(Q),p) in Class PropRel(Q) & Class(PropRel(Q),q) in Class PropRel(Q) by EQREL_1:def 5; 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,Th30; hence thesis by A2,Def13; end; assume [Class(PropRel(Q),p),Class(PropRel(Q),q)] in OrdRel(Q); hence thesis by A1,Def13; end; theorem Th33: 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) & C in Class PropRel(Q); let p1,q1; consider x such that A2: x in Prop Q & B = Class(PropRel(Q),x) by A1,EQREL_1:def 5; consider y such that A3: y in Prop Q & C = Class(PropRel(Q),y) by A1,EQREL_1:def 5; reconsider q = y as Element of Prop Q by A3; assume p1 in B & q1 in B & 'not' p1 in C; then [p1,q1] in PropRel(Q) & ['not' p1,q] in PropRel(Q) by A2,A3,EQREL_1:27,30 ; then A4: p1 <==> q1 & 'not' p1 <==> q by Def12; then A5: p1 <==> q1 & q <==> 'not' p1 by Th24; now let s; A6: 1 - 1 = 0; reconsider E = p1`2` as Event of Borel_Sets by PROB_1:50; reconsider E1 = q1`2` as Event of Borel_Sets by PROB_1:50; set r1 = Meas(p1`1,s).E, r2 = Meas(q1`1,s).E1; A7: 1 - r1 = Meas(p1`1,s).p1`2 by Th16 .= Meas(q1`1,s).q1`2 by A4,Th20 .= 1 - r2 by Th16; A8: ('not' p1)`1 = p1`1 & ('not' p1)`2 = (p1`2)` & ('not' q1)`1 = q1`1 & ('not' q1)`2 = (q1`2)` by Th26; hence Meas(('not' p1)`1,s).('not' p1)`2 = 0 + r1 .= 1 - (1 - r1) by A6,XCMPLX_1:37 .= 0 + r2 by A6,A7,XCMPLX_1:37 .= Meas(('not' q1)`1,s).('not' q1)`2 by A8; end; then 'not' p1 <==> 'not' q1 by Th20; then q <==> 'not' q1 by A5,Th25; then [q,'not' q1] in PropRel(Q) by Def12; then ['not' q1,q] in PropRel(Q) by EQREL_1:12; hence thesis by A3,EQREL_1:27; 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 by Th27; hence thesis by A1,Th33; 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[set,set] means for p st $1 = Class(PropRel(Q),p) holds $2 = Class(PropRel(Q),'not' p); A1: for x st x in Class PropRel(Q) ex y st y in Class PropRel(Q) & P[x,y] proof let x; assume A2: x in Class PropRel(Q); then consider q such that A3: x = Class(PropRel(Q),q) by EQREL_1:45; reconsider y = Class(PropRel(Q),'not' q) as set; take y; thus A4: y in Class PropRel(Q) by EQREL_1:def 5; reconsider y'=y as Subset of Prop Q; let p; assume A5: x = Class(PropRel(Q),p); then reconsider x as Subset of Prop Q; p in x & q in x & 'not' q in y' by A3,A5,EQREL_1:28; then 'not' p in y' by A2,A4,Th33; hence y = Class(PropRel(Q),'not' p) by EQREL_1:31; end; consider F being Function of Class PropRel(Q),Class PropRel(Q) such that A6: for x st x in Class PropRel(Q) holds P[x,F.x] from FuncEx1(A1); take F; let p; Class(PropRel(Q),p) in Class PropRel(Q) by EQREL_1:def 5; hence F.Class(PropRel(Q),p) = Class(PropRel(Q),'not' p) by A6; end; uniqueness proof let F1,F2 be Function of Class PropRel(Q),Class PropRel(Q); assume that A7: for p holds F1.Class(PropRel(Q),p) = Class(PropRel(Q),'not' p) and A8: for p holds F2.Class(PropRel(Q),p) = Class(PropRel(Q),'not' p); now let x; assume x in Class PropRel(Q); then consider p such that A9: x = Class(PropRel Q, p) by EQREL_1:45; F1.x = Class(PropRel(Q),'not' p) & F2.x = Class(PropRel(Q),'not' p) by A7,A8,A9; hence F1.x = F2.x; end; hence thesis by FUNCT_2:18; end; end; canceled; theorem ::Main Theorem for Q holds POI_Str(#OrdRel(Q),InvRel(Q)#) is_a_Quantuum_Logic_on Class PropRel(Q) proof let Q; A1: OrdRel(Q) partially_orders Class PropRel(Q) proof thus OrdRel(Q) is_reflexive_in Class PropRel(Q) proof let x; assume x in Class PropRel(Q); then consider p such that A2: x = Class(PropRel(Q),p) by EQREL_1:45; p |- p by Th21; hence thesis by A2,Th32; end; thus OrdRel(Q) is_transitive_in Class PropRel(Q) proof let x,y,z; assume that A3: x in Class PropRel(Q) & y in Class PropRel(Q) & z in Class PropRel(Q) and A4: [x,y] in OrdRel(Q) & [y,z] in OrdRel(Q); consider p such that A5: x = Class(PropRel(Q),p) by A3,EQREL_1:45; consider q such that A6: y = Class(PropRel(Q),q) by A3,EQREL_1:45; consider r such that A7: z = Class(PropRel(Q),r) by A3,EQREL_1:45; p |- q & q |- r implies p |- r by Th22; hence thesis by A4,A5,A6,A7,Th32; end; thus OrdRel(Q) is_antisymmetric_in Class PropRel(Q) proof let x,y; assume that A8: x in Class PropRel(Q) & y in Class PropRel(Q) and A9: [x,y] in OrdRel(Q) & [y,x] in OrdRel(Q); consider p such that A10: x = Class(PropRel(Q),p) by A8,EQREL_1:45; consider q such that A11: y = Class(PropRel(Q),q) by A8,EQREL_1:45; (p |- q & q |- p implies p <==> q) & (p <==> q implies [p,q] in PropRel(Q)) by Def11,Def12; hence thesis by A9,A10,A11,Th32,EQREL_1:44; end; end; A12: InvRel(Q) is_an_involution_in Class PropRel(Q) proof let x be Element of Class PropRel(Q); consider r; Class(PropRel Q,r) in Class PropRel Q by EQREL_1:def 5; then reconsider D = Class PropRel(Q) as non empty set; x in D; then consider p such that A13: x = Class(PropRel(Q),p) by EQREL_1:45; (InvRel(Q)).((InvRel(Q)).x) = (InvRel(Q)).Class(PropRel(Q),'not' p) by A13,Def14 .= Class(PropRel(Q),'not'('not' p)) by Def14; hence thesis by A13,Th27; end; 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 r; Class(PropRel Q,r) in Class PropRel Q by EQREL_1:def 5; then reconsider D = Class PropRel(Q) as non empty set; x in D; then consider p such that A14: x = Class(PropRel(Q),p) by EQREL_1:45; y in D; then consider q such that A15: y = Class(PropRel(Q),q) by EQREL_1:45; A16: (InvRel(Q)).Class(PropRel(Q),p) = Class(PropRel(Q),'not' p) & (InvRel(Q)).Class(PropRel(Q),q) = Class(PropRel(Q),'not' q) by Def14; p |- q implies 'not' q |- 'not' p by Th28; hence thesis by A14,A15,A16,Th32; end; hence thesis by A1,A12,Def7; end;

Back to top