:: The Fundamental Logic Structure in Quantum Mechanics
:: by Pawe{\l} Sadowski, Andrzej Trybulec and Konrad Raczkowski
::
:: Received December 18, 1989
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines Probabilities QMAX_1:def 1 :
:: deftheorem defines Obs QMAX_1:def 2 :
:: deftheorem defines Sts QMAX_1:def 3 :
:: deftheorem defines Meas QMAX_1:def 4 :
reconsider X = {0 } as non empty set ;
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:60;
Lm2:
for A being Event of Borel_Sets holds 0 <= P . A
Lm3:
P . REAL = 1
Lm4:
for A, B being Event of Borel_Sets st A misses B holds
P . (A \/ B) = (P . A) + (P . B)
for ASeq being SetSequence of st ASeq is non-ascending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )
then reconsider P = P as Probability of Borel_Sets by Lm2, Lm3, Lm4, PROB_1:def 13;
reconsider f = {[[0 ,0 ],P]} as Function by GRFUNC_1:15;
dom f = {[0 ,0 ]}
by RELAT_1:23;
then Lm5:
dom f = [:X,X:]
by ZFMISC_1:35;
( rng f = {P} & P in Probabilities Borel_Sets )
by Def1, RELAT_1:23;
then
rng f c= Probabilities Borel_Sets
by ZFMISC_1:37;
then reconsider Y = f as Function of [:X,X:],(Probabilities Borel_Sets ) by Lm5, FUNCT_2:def 1, RELSET_1:11;
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
:: thesis: ( ( 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 ) & ( for s1, s2 being Element of Sts QM_Str(# X,X,Y #)
for t being Real st 0 <= t & t <= 1 holds
ex s being Element of Sts QM_Str(# X,X,Y #) st
for A being Element of Obs QM_Str(# X,X,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(#
X,
X,
Y #);
:: thesis: ( ( for s being Element of Sts QM_Str(# X,X,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(#
X,
X,
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(#
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
:: thesis: for s1, s2 being Element of Sts QM_Str(# X,X,Y #)
for t being Real st 0 <= t & t <= 1 holds
ex s being Element of Sts QM_Str(# X,X,Y #) st
for A being Element of Obs QM_Str(# X,X,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(#
X,
X,
Y #);
:: thesis: ( ( for A being Element of Obs QM_Str(# X,X,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(#
X,
X,
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(#
X,
X,
Y #)
for
t being
Real st
0 <= t &
t <= 1 holds
ex
s being
Element of
Sts QM_Str(#
X,
X,
Y #) st
for
A being
Element of
Obs QM_Str(#
X,
X,
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(#
X,
X,
Y #);
:: thesis: for t being Real st 0 <= t & t <= 1 holds
ex s being Element of Sts QM_Str(# X,X,Y #) st
for A being Element of Obs QM_Str(# X,X,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 & t <= 1 implies ex s being Element of Sts QM_Str(# X,X,Y #) st
for A being Element of Obs QM_Str(# X,X,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 that
0 <= t
and
t <= 1
;
:: thesis: ex s being Element of Sts QM_Str(# X,X,Y #) st
for A being Element of Obs QM_Str(# X,X,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(# X,X,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(#
X,
X,
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 &
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 ;
attr IT 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 ) & ( 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 for
t being
Real st
0 <= t &
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 ) & ( 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 for
t being
Real st
0 <= t &
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)) ) ) );
:: deftheorem defines is_an_involution_in QMAX_1:def 6 :
:: deftheorem Def7 defines is_a_Quantuum_Logic_on QMAX_1:def 7 :
:: deftheorem defines Prop QMAX_1:def 8 :
theorem :: QMAX_1:1
canceled;
theorem :: QMAX_1:2
canceled;
theorem :: QMAX_1:3
canceled;
theorem :: QMAX_1:4
canceled;
theorem :: QMAX_1:5
canceled;
theorem :: QMAX_1:6
canceled;
theorem :: QMAX_1:7
canceled;
theorem :: QMAX_1:8
canceled;
theorem :: QMAX_1:9
canceled;
theorem :: QMAX_1:10
canceled;
theorem :: QMAX_1:11
canceled;
theorem :: QMAX_1:12
canceled;
theorem :: QMAX_1:13
canceled;
theorem :: QMAX_1:14
canceled;
theorem :: QMAX_1:15
canceled;
theorem Th16: :: QMAX_1:16
:: deftheorem defines 'not' QMAX_1:def 9 :
:: deftheorem Def10 defines |- QMAX_1:def 10 :
:: deftheorem Def11 defines <==> QMAX_1:def 11 :
theorem :: QMAX_1:17
canceled;
theorem :: QMAX_1:18
canceled;
theorem :: QMAX_1:19
canceled;
theorem Th20: :: QMAX_1:20
theorem Th21: :: QMAX_1:21
theorem Th22: :: QMAX_1:22
theorem Th23: :: QMAX_1:23
theorem Th24: :: QMAX_1:24
theorem Th25: :: QMAX_1:25
theorem :: QMAX_1:26
canceled;
theorem Th27: :: QMAX_1:27
theorem Th28: :: QMAX_1:28
:: deftheorem Def12 defines PropRel QMAX_1:def 12 :
theorem :: QMAX_1:29
canceled;
theorem Th30: :: QMAX_1:30
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) &
C in Class (PropRel Q) & ( for
p,
q being
Element of
Prop Q st
p in B &
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) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) )
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) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) ) & ( for B, C being Subset of (Prop Q) holds
( [B,C] in b2 iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def13 defines OrdRel QMAX_1:def 13 :
theorem :: QMAX_1:31
canceled;
theorem Th32: :: QMAX_1:32
theorem Th33: :: QMAX_1:33
theorem :: QMAX_1:34
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)
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) ) & ( for p being Element of Prop Q holds b2 . (Class (PropRel Q),p) = Class (PropRel Q),('not' p) ) holds
b1 = b2
end;
:: deftheorem Def14 defines InvRel QMAX_1:def 14 :
theorem :: QMAX_1:35
canceled;
theorem :: QMAX_1:36