:: The Fundamental Logic Structure in Quantum Mechanics :: by Pawe{\l} Sadowski, Andrzej Trybulec and Konrad Raczkowski :: :: Received December 18, 1989 :: Copyright (c) 1990-2021 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; 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 :: QMAX_1:def 1 for x being object holds x in it iff x is Probability of S; end; registration let X; let S be SigmaField of X; cluster Probabilities(S) -> non empty; 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 :: QMAX_1:def 2 the Observables of Q; func Sts Q -> set equals :: QMAX_1:def 3 the FStates of Q; end; registration let Q; cluster Obs Q -> non empty; cluster Sts Q -> non empty; 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 :: QMAX_1:def 4 (the Quantum_Probability of Q).[A1,s]; end; definition let IT be QM_Str; attr IT is Quantum_Mechanics-like means :: 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, 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; 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 :: QMAX_1:def 6 Inv.(Inv.x1) = x1; end; definition let W be OrthoRelStr; pred W is_a_Quantum_Logic means :: QMAX_1:def 7 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 :: QMAX_1:def 8 [:Obs Q,Borel_Sets:]; end; registration let Q; cluster Prop Q -> non empty; end; reserve p,q,r,p1,q1 for Element of Prop Q; definition let Q,p; redefine func p`1 -> Element of Obs Q; redefine func p`2 -> Event of Borel_Sets; end; theorem :: QMAX_1:1 for E st E = p`2` holds Meas(p`1,s).p`2 = 1 - Meas(p`1,s).E; definition let Q,p; func 'not' p -> Element of Prop Q equals :: QMAX_1:def 9 [p`1,(p`2)`]; involutiveness; end; definition let Q,p,q; pred p |- q means :: QMAX_1:def 10 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 :: QMAX_1:def 11 p |- q & q |- p; reflexivity; symmetry; end; theorem :: QMAX_1:2 p <==> q iff for s holds Meas(p`1,s).p`2 = Meas(q`1,s).q`2; theorem :: QMAX_1:3 p |- p; theorem :: QMAX_1:4 p |- q & q |- r implies p |- r; theorem :: QMAX_1:5 p <==> p; theorem :: QMAX_1:6 p <==> q implies q <==> p; theorem :: QMAX_1:7 p <==> q & q <==> r implies p <==> r; ::$CT theorem :: QMAX_1:9 p |- q implies 'not' q |- 'not' p; definition let Q; func PropRel Q -> Equivalence_Relation of Prop Q means :: QMAX_1:def 12 [p,q] in it iff p <==> q; end; reserve B,C for Subset of Prop Q; theorem :: QMAX_1:10 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; definition let Q; func OrdRel Q -> Relation of Class PropRel (Q) means :: QMAX_1:def 13 [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; end; theorem :: QMAX_1:11 p |- q iff [Class(PropRel Q,p),Class(PropRel Q,q)] in OrdRel Q; theorem :: QMAX_1:12 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; theorem :: QMAX_1:13 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; definition let Q; func InvRel Q -> Function of Class PropRel Q,Class PropRel Q means :: QMAX_1:def 14 it.Class(PropRel Q,p) = Class(PropRel Q,'not' p); end; theorem :: QMAX_1:14 :: Main Theorem for Q holds OrthoRelStr(#Class PropRel Q,OrdRel Q,InvRel Q#) is_a_Quantum_Logic;