:: The Fundamental Logic Structure in Quantum Mechanics
:: by Pawe{\l} Sadowski, Andrzej Trybulec and Konrad Raczkowski
::
:: Received December 18, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
let X be non empty set ;
let S be SigmaField of X;
func Probabilities S ->  set  means :Def1: :: QMAX_1:def 1
 for x being set holds
( x in it iff x is Probability of S );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff x is Probability of S )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is Probability of S ) ) & ( for x being set holds
( x in b2 iff x is Probability of S ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines Probabilities QMAX_1:def_1_:_
 for X being non empty set
for S being SigmaField of X
for b3 being set holds
( b3 = Probabilities S iff for x being set holds
( x in b3 iff x is Probability of S ) );

registration
let X be non empty set ;
let S be SigmaField of X;
cluster Probabilities S ->  non empty ;
coherence
 not Probabilities S is empty
proofend;
end;

definition
attrc1 is strict ;
struct QM_Str  -> ;
aggrQM_Str(# Observables, FStates, Quantum_Probability #) ->  QM_Str ;
sel Observables c1 ->  non empty set ;
sel FStates c1 ->  non empty set ;
sel Quantum_Probability c1 ->  Function of [: the Observables of c1, the FStates of c1:],(Probabilities Borel_Sets);
end;

definition
let Q be QM_Str ;
func Obs Q ->  set  equals :: QMAX_1:def 2
 the Observables of Q;
coherence
 the Observables of Q is set ;
func Sts Q ->  set  equals :: QMAX_1:def 3
 the FStates of Q;
coherence
 the FStates of Q is set ;
end;

:: deftheorem  defines Obs QMAX_1:def_2_:_
 for Q being QM_Str holds Obs Q = the Observables of Q;

:: deftheorem  defines Sts QMAX_1:def_3_:_
 for Q being QM_Str holds Sts Q = the FStates of Q;

registration
let Q be QM_Str ;
cluster Obs Q ->  non empty ;
coherence
 not Obs Q is empty ;
cluster Sts Q ->  non empty ;
coherence
 not Sts Q is empty ;
end;

definition
let Q be QM_Str ;
let A1 be Element of Obs Q;
let s be Element of Sts Q;
func Meas (A1,s) ->  Probability of Borel_Sets  equals :: QMAX_1:def 4
 the Quantum_Probability of Q . [A1,s];
coherence
 the Quantum_Probability of Q . [A1,s] is Probability of Borel_Sets
proofend;
end;

:: deftheorem  defines Meas QMAX_1:def_4_:_
 for Q being QM_Str
for A1 being Element of Obs Q
for s being Element of Sts Q holds Meas (A1,s) = the Quantum_Probability of Q . [A1,s];

set X = {0};

consider P being Function of Borel_Sets,REAL such that
Lm1:  for D being Subset of REAL 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 being Event of Borel_Sets holds 0 <= P . A
proofend;

Lm3:  P . REAL = 1
proofend;

Lm4:  for A, B being Event of Borel_Sets st A misses B holds
P . (A \/ B) = (P . A) + (P . B)
proofend;

 for ASeq being SetSequence of Borel_Sets st ASeq is non-ascending holds
( P * ASeq is convergent &amp; lim (P * ASeq) = P . (Intersection ASeq) )
proofend;

then reconsider P = P as Probability of Borel_Sets by Lm2, Lm3, Lm4, PROB_1:def_8;

set f = {[[0,0],P]};

 dom {[[0,0],P]} = {[0,0]}
by RELAT_1:9;

then Lm5:  dom {[[0,0],P]} = [:{0},{0}:]
by ZFMISC_1:29;

 ( rng {[[0,0],P]} = {P} &amp; P in Probabilities Borel_Sets )
by Def1, RELAT_1:9;

then  rng {[[0,0],P]} c= Probabilities Borel_Sets
by ZFMISC_1:31;

then reconsider Y = {[[0,0],P]} as Function of [:{0},{0}:],(Probabilities Borel_Sets) by Lm5, FUNCT_2:def_1, RELSET_1:4;

Lm6: now__::_thesis:_(_(_for_A1,_A2_being_Element_of_Obs_QM_Str(#_{0},{0},Y_#)_st_(_for_s_being_Element_of_Sts_QM_Str(#_{0},{0},Y_#)_holds_Meas_(A1,s)_=_Meas_(A2,s)_)_holds_
A1_=_A2_)_&amp;_(_for_s1,_s2_being_Element_of_Sts_QM_Str(#_{0},{0},Y_#)_st_(_for_A_being_Element_of_Obs_QM_Str(#_{0},{0},Y_#)_holds_Meas_(A,s1)_=_Meas_(A,s2)_)_holds_
s1_=_s2_)_&amp;_(_for_s1,_s2_being_Element_of_Sts_QM_Str(#_{0},{0},Y_#)
for_t_being_Real_st_0_<=_t_&amp;_t_<=_1_holds_
ex_s_being_Element_of_Sts_QM_Str(#_{0},{0},Y_#)_st_
for_A_being_Element_of_Obs_QM_Str(#_{0},{0},Y_#)
for_E_being_Event_of_Borel_Sets_holds_(Meas_(A,s))_._E_=_(t_*_((Meas_(A,s1))_._E))_+_((1_-_t)_*_((Meas_(A,s2))_._E))_)_)
thus  for A1, A2 being Element of Obs QM_Str(# {0},{0},Y #) st ( for s being Element of Sts QM_Str(# {0},{0},Y #) holds Meas (A1,s) = Meas (A2,s) ) holds
A1 = A2 ::_thesis: ( ( for s1, s2 being Element of Sts QM_Str(# {0},{0},Y #) st ( for A being Element of Obs QM_Str(# {0},{0},Y #) holds Meas (A,s1) = Meas (A,s2) ) holds
s1 = s2 ) &amp; ( for s1, s2 being Element of Sts QM_Str(# {0},{0},Y #)
for t being Real st 0 <= t &amp; t <= 1 holds
ex s being Element of Sts QM_Str(# {0},{0},Y #) st
for A being Element of Obs QM_Str(# {0},{0},Y #)
for E being Event of Borel_Sets holds (Meas (A,s)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E)) ) )
proof
let A1, A2 be Element of Obs QM_Str(# {0},{0},Y #); ::_thesis: ( ( for s being Element of Sts QM_Str(# {0},{0},Y #) holds Meas (A1,s) = Meas (A2,s) ) implies A1 = A2 )
 A1 = 0 by TARSKI:def_1;
hence  ( ( for s being Element of Sts QM_Str(# {0},{0},Y #) holds Meas (A1,s) = Meas (A2,s) ) implies A1 = A2 ) by TARSKI:def_1; ::_thesis: verum
end;
thus  for s1, s2 being Element of Sts QM_Str(# {0},{0},Y #) st ( for A being Element of Obs QM_Str(# {0},{0},Y #) holds Meas (A,s1) = Meas (A,s2) ) holds
s1 = s2 ::_thesis: for s1, s2 being Element of Sts QM_Str(# {0},{0},Y #)
for t being Real st 0 <= t &amp; t <= 1 holds
ex s being Element of Sts QM_Str(# {0},{0},Y #) st
for A being Element of Obs QM_Str(# {0},{0},Y #)
for E being Event of Borel_Sets 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(# {0},{0},Y #); ::_thesis: ( ( for A being Element of Obs QM_Str(# {0},{0},Y #) holds Meas (A,s1) = Meas (A,s2) ) implies s1 = s2 )
 s1 = 0 by TARSKI:def_1;
hence  ( ( for A being Element of Obs QM_Str(# {0},{0},Y #) holds Meas (A,s1) = Meas (A,s2) ) implies s1 = s2 ) by TARSKI:def_1; ::_thesis: verum
end;
thus  for s1, s2 being Element of Sts QM_Str(# {0},{0},Y #)
for t being Real st 0 <= t &amp; t <= 1 holds
ex s being Element of Sts QM_Str(# {0},{0},Y #) st
for A being Element of Obs QM_Str(# {0},{0},Y #)
for E being Event of Borel_Sets holds (Meas (A,s)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E)) ::_thesis: verum
proof
let s1, s2 be Element of Sts QM_Str(# {0},{0},Y #); ::_thesis: for t being Real st 0 <= t &amp; t <= 1 holds
ex s being Element of Sts QM_Str(# {0},{0},Y #) st
for A being Element of Obs QM_Str(# {0},{0},Y #)
for E being Event of Borel_Sets holds (Meas (A,s)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E))
let t be Real; ::_thesis: ( 0 <= t &amp; t <= 1 implies ex s being Element of Sts QM_Str(# {0},{0},Y #) st
for A being Element of Obs QM_Str(# {0},{0},Y #)
for E being Event of Borel_Sets holds (Meas (A,s)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E)) )
assume  ( 0 <= t &amp; t <= 1 ) ; ::_thesis: ex s being Element of Sts QM_Str(# {0},{0},Y #) st
for A being Element of Obs QM_Str(# {0},{0},Y #)
for E being Event of Borel_Sets holds (Meas (A,s)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E))
take  s2 ; ::_thesis: for A being Element of Obs QM_Str(# {0},{0},Y #)
for E being Event of Borel_Sets holds (Meas (A,s2)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E))
let A be Element of Obs QM_Str(# {0},{0},Y #); ::_thesis: for E being Event of Borel_Sets holds (Meas (A,s2)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E))
let E be Event of Borel_Sets ; ::_thesis: (Meas (A,s2)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E))
 ( s1 = 0 &amp; s2 = 0 ) by TARSKI:def_1;
hence  (Meas (A,s2)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E)) ; ::_thesis: verum
end;
end;

definition
let IT be QM_Str ;
attrIT is Quantum_Mechanics-like  means :Def5: :: QMAX_1:def 5
( ( 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 ) &amp; ( 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 ) &amp; ( for s1, s2 being Element of Sts IT
for t being Real st 0 <= t &amp; t <= 1 holds
ex s being Element of Sts IT st
for A being Element of Obs IT
for E being Event of Borel_Sets holds (Meas (A,s)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E)) ) );
end;

:: deftheorem Def5 defines Quantum_Mechanics-like QMAX_1:def_5_:_
 for IT being QM_Str holds
( IT is Quantum_Mechanics-like iff ( ( 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 ) &amp; ( 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 ) &amp; ( for s1, s2 being Element of Sts IT
for t being Real st 0 <= t &amp; t <= 1 holds
ex s being Element of Sts IT st
for A being Element of Obs IT
for E being Event of Borel_Sets holds (Meas (A,s)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E)) ) ) );

registration
cluster strict Quantum_Mechanics-like for QM_Str ;
existence
 ex b1 being QM_Str st
( b1 is strict &amp; b1 is Quantum_Mechanics-like )
proofend;
end;

definition
mode Quantum_Mechanics is Quantum_Mechanics-like QM_Str ;
end;

definition
attrc1 is strict ;
struct OrthoRelStr  ->  RelStr , ComplStr ;
aggrOrthoRelStr(# carrier, InternalRel, Compl #) ->  OrthoRelStr ;
end;

definition
let X1 be set ;
let Inv be Function of X1,X1;
predInv is_an_involution  means :: QMAX_1:def 6
 for x1 being Element of X1 holds Inv . (Inv . x1) = x1;
end;

:: deftheorem  defines is_an_involution QMAX_1:def_6_:_
 for X1 being set
for Inv being Function of X1,X1 holds
( Inv is_an_involution iff for x1 being Element of X1 holds Inv . (Inv . x1) = x1 );

definition
let W be OrthoRelStr ;
predW is_a_Quantum_Logic  means :Def7: :: QMAX_1:def 7
( the InternalRel of W partially_orders the carrier of W &amp; the Compl of W is_an_involution &amp; ( 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;

:: deftheorem Def7 defines is_a_Quantum_Logic QMAX_1:def_7_:_
 for W being OrthoRelStr holds
( W is_a_Quantum_Logic iff ( the InternalRel of W partially_orders the carrier of W &amp; the Compl of W is_an_involution &amp; ( 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 ) ) );

definition
let Q be Quantum_Mechanics;
func Prop Q ->  set  equals :: QMAX_1:def 8
[:(Obs Q),Borel_Sets:];
coherence
 [:(Obs Q),Borel_Sets:] is set ;
end;

:: deftheorem  defines Prop QMAX_1:def_8_:_
 for Q being Quantum_Mechanics holds Prop Q = [:(Obs Q),Borel_Sets:];

registration
let Q be Quantum_Mechanics;
cluster Prop Q ->  non empty ;
coherence
 not Prop Q is empty ;
end;

definition
let Q be Quantum_Mechanics;
let p be Element of Prop Q;
:: original:`1
redefine funcp `1  ->  Element of Obs Q;
coherence
 p `1 is Element of Obs Q by MCART_1:10;
:: original:`2
redefine funcp `2  ->  Event of Borel_Sets ;
coherence
 p `2 is Event of Borel_Sets by MCART_1:10;
end;

theorem Th1: :: QMAX_1:1
for Q being Quantum_Mechanics
for s being Element of Sts Q
for p being Element of Prop Q
for E being Event of Borel_Sets st E = (p `2) ` holds
(Meas ((p `1),s)) . (p `2) = 1 - ((Meas ((p `1),s)) . E)
proofend;

definition
let Q be Quantum_Mechanics;
let p be Element of Prop Q;
func 'not' p ->  Element of Prop Q equals :: QMAX_1:def 9
[(p `1),((p `2) `)];
coherence
 [(p `1),((p `2) `)] is Element of Prop Q
proofend;
involutiveness
 for b1, b2 being Element of Prop Q st b1 = [(b2 `1),((b2 `2) `)] holds
b2 = [(b1 `1),((b1 `2) `)]
proofend;
end;

:: deftheorem  defines 'not' QMAX_1:def_9_:_
 for Q being Quantum_Mechanics
for p being Element of Prop Q holds 'not' p = [(p `1),((p `2) `)];

definition
let Q be Quantum_Mechanics;
let p, q be Element of Prop Q;
predp |- q means :Def10: :: QMAX_1:def 10
 for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) <= (Meas ((q `1),s)) . (q `2);
reflexivity
 for p being Element of Prop Q
for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) <= (Meas ((p `1),s)) . (p `2) ;
end;

:: deftheorem Def10 defines |- QMAX_1:def_10_:_
 for Q being Quantum_Mechanics
for p, q being Element of Prop Q holds
( p |- q iff for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) <= (Meas ((q `1),s)) . (q `2) );

definition
let Q be Quantum_Mechanics;
let p, q be Element of Prop Q;
predp <==> q means :Def11: :: QMAX_1:def 11
( p |- q &amp; q |- p );
reflexivity
 for p being Element of Prop Q holds
( p |- p &amp; p |- p ) ;
symmetry
 for p, q being Element of Prop Q st p |- q &amp; q |- p holds
( q |- p &amp; p |- q ) ;
end;

:: deftheorem Def11 defines <==> QMAX_1:def_11_:_
 for Q being Quantum_Mechanics
for p, q being Element of Prop Q holds
( p <==> q iff ( p |- q &amp; q |- p ) );

theorem Th2: :: QMAX_1:2
for Q being Quantum_Mechanics
for p, q being Element of Prop Q holds
( p <==> q iff for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) = (Meas ((q `1),s)) . (q `2) )
proofend;

theorem :: QMAX_1:3
for Q being Quantum_Mechanics
for p being Element of Prop Q holds p |- p ;

theorem Th4: :: QMAX_1:4
for Q being Quantum_Mechanics
for p, q, r being Element of Prop Q st p |- q &amp; q |- r holds
p |- r
proofend;

theorem :: QMAX_1:5
for Q being Quantum_Mechanics
for p being Element of Prop Q holds p <==> p ;

theorem :: QMAX_1:6
for Q being Quantum_Mechanics
for p, q being Element of Prop Q st p <==> q holds
q <==> p ;

theorem Th7: :: QMAX_1:7
for Q being Quantum_Mechanics
for p, q, r being Element of Prop Q st p <==> q &amp; q <==> r holds
p <==> r
proofend;

theorem :: QMAX_1:8
canceled;

theorem Th9: :: QMAX_1:9
for Q being Quantum_Mechanics
for p, q being Element of Prop Q st p |- q holds
'not' q |- 'not' p
proofend;

definition
let Q be Quantum_Mechanics;
func PropRel Q ->  Equivalence_Relation of (Prop Q) means :Def12: :: QMAX_1:def 12
 for p, q being Element of Prop Q holds
( [p,q] in it iff p <==> q );
existence
 ex b1 being Equivalence_Relation of (Prop Q) st
for p, q being Element of Prop Q holds
( [p,q] in b1 iff p <==> q )
proofend;
uniqueness
 for b1, b2 being Equivalence_Relation of (Prop Q) st ( for p, q being Element of Prop Q holds
( [p,q] in b1 iff p <==> q ) ) &amp; ( for p, q being Element of Prop Q holds
( [p,q] in b2 iff p <==> q ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines PropRel QMAX_1:def_12_:_
 for Q being Quantum_Mechanics
for b2 being Equivalence_Relation of (Prop Q) holds
( b2 = PropRel Q iff for p, q being Element of Prop Q holds
( [p,q] in b2 iff p <==> q ) );

theorem Th10: :: QMAX_1:10
for Q being Quantum_Mechanics
for B, C being Subset of (Prop Q) st B in Class (PropRel Q) &amp; C in Class (PropRel Q) holds
for a, b, c, d being Element of Prop Q st a in B &amp; b in B &amp; c in C &amp; d in C &amp; a |- c holds
b |- d
proofend;

definition
let Q be Quantum_Mechanics;
func OrdRel Q ->  Relation of (Class (PropRel Q)) means :Def13: :: QMAX_1:def 13
 for B, C being Subset of (Prop Q) holds
( [B,C] in it iff ( B in Class (PropRel Q) &amp; C in Class (PropRel Q) &amp; ( for p, q being Element of Prop Q st p in B &amp; q in C holds
p |- q ) ) );
existence
 ex b1 being Relation of (Class (PropRel Q)) st
for B, C being Subset of (Prop Q) holds
( [B,C] in b1 iff ( B in Class (PropRel Q) &amp; C in Class (PropRel Q) &amp; ( for p, q being Element of Prop Q st p in B &amp; q in C holds
p |- q ) ) )
proofend;
uniqueness
 for b1, b2 being Relation of (Class (PropRel Q)) st ( for B, C being Subset of (Prop Q) holds
( [B,C] in b1 iff ( B in Class (PropRel Q) &amp; C in Class (PropRel Q) &amp; ( for p, q being Element of Prop Q st p in B &amp; q in C holds
p |- q ) ) ) ) &amp; ( for B, C being Subset of (Prop Q) holds
( [B,C] in b2 iff ( B in Class (PropRel Q) &amp; C in Class (PropRel Q) &amp; ( for p, q being Element of Prop Q st p in B &amp; q in C holds
p |- q ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def13 defines OrdRel QMAX_1:def_13_:_
 for Q being Quantum_Mechanics
for b2 being Relation of (Class (PropRel Q)) holds
( b2 = OrdRel Q iff for B, C being Subset of (Prop Q) holds
( [B,C] in b2 iff ( B in Class (PropRel Q) &amp; C in Class (PropRel Q) &amp; ( for p, q being Element of Prop Q st p in B &amp; q in C holds
p |- q ) ) ) );

theorem Th11: :: QMAX_1:11
for Q being Quantum_Mechanics
for p, q being Element of Prop Q holds
( p |- q iff [(Class ((PropRel Q),p)),(Class ((PropRel Q),q))] in OrdRel Q )
proofend;

theorem Th12: :: QMAX_1:12
for Q being Quantum_Mechanics
for B, C being Subset of (Prop Q) st B in Class (PropRel Q) &amp; C in Class (PropRel Q) holds
for p1, q1 being Element of Prop Q st p1 in B &amp; q1 in B &amp; 'not' p1 in C holds
'not' q1 in C
proofend;

theorem :: QMAX_1:13
for Q being Quantum_Mechanics
for B, C being Subset of (Prop Q) st B in Class (PropRel Q) &amp; C in Class (PropRel Q) holds
for p, q being Element of Prop Q st 'not' p in C &amp; 'not' q in C &amp; p in B holds
q in B
proofend;

definition
let Q be Quantum_Mechanics;
func InvRel Q ->  Function of (Class (PropRel Q)),(Class (PropRel Q)) means :Def14: :: QMAX_1:def 14
 for p being Element of Prop Q holds it . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p));
existence
 ex b1 being Function of (Class (PropRel Q)),(Class (PropRel Q)) st
for p being Element of Prop Q holds b1 . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p))
proofend;
uniqueness
 for b1, b2 being Function of (Class (PropRel Q)),(Class (PropRel Q)) st ( for p being Element of Prop Q holds b1 . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p)) ) &amp; ( for p being Element of Prop Q holds b2 . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def14 defines InvRel QMAX_1:def_14_:_
 for Q being Quantum_Mechanics
for b2 being Function of (Class (PropRel Q)),(Class (PropRel Q)) holds
( b2 = InvRel Q iff for p being Element of Prop Q holds b2 . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p)) );

theorem :: QMAX_1:14
for Q being Quantum_Mechanics holds OrthoRelStr(# (Class (PropRel Q)),(OrdRel Q),(InvRel Q) #) is_a_Quantum_Logic
proofend;