:: The Axiomatization of Propositional Logic :: by Mariusz Giero :: :: Received October 18, 2016 :: Copyright (c) 2016-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 FINSEQ_1, CARD_1, ORDINAL4, SUBSET_1, NUMBERS, ARYTM_3, TARSKI, RELAT_1, RELAT_2, XBOOLE_0, FUNCT_1, QC_LANG1, XBOOLEAN, HILBERT1, CQC_THE1, NAT_1, XXREAL_0, LTLAXIO1, ARYTM_1, ZF_LANG, PARTFUN1, WELLFND1, ORDERS_2, ORDINAL1, STRUCT_0, MARGREL1, HILBERT2, ZFMISC_1, ZF_MODEL, PBOOLE, GLIB_000, INTPRO_1, ABCMIZ_0, GROUP_4, WELLORD1, FINSET_1, QMAX_1, PL_AXIOM; notations TARSKI, XBOOLE_0, ZFMISC_1, DOMAIN_1, SUBSET_1, SETFAM_1, RELAT_1, RELAT_2, RELSET_1, PARTFUN1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, XXREAL_0, NAT_D, FUNCT_1, WELLORD1, STRUCT_0, ORDERS_2, FUNCT_2, FINSET_1, WELLFND1, BINOP_1, FINSEQ_1, HILBERT1, HILBERT2, PBOOLE, XBOOLEAN, MARGREL1, INTPRO_1; constructors NAT_D, RELSET_1, AOFA_I00, HILBERT2, DOMAIN_1, WELLORD1, WELLFND1, SETFAM_1, INTPRO_1; registrations SUBSET_1, ORDINAL1, FUNCT_1, FINSEQ_1, NAT_1, XBOOLEAN, RELSET_1, MARGREL1, XBOOLE_0, XREAL_0, HILBERT1, STRUCT_0, FINSET_1, ORDERS_2; requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL; begin theorem :: PL_AXIOM:1 for f,g be Function holds (dom f c= dom g & for x be set st x in dom f holds f.x = g.x) implies rng f c= rng g; theorem :: PL_AXIOM:2 for p,q being boolean object holds (p '&' q) => p = TRUE; theorem :: PL_AXIOM:3 for p being boolean object holds ('not' 'not' p) <=> p = TRUE; theorem :: PL_AXIOM:4 for p,q being boolean object holds 'not' (p '&' q) <=> ('not' p) 'or' ('not' q) = TRUE; theorem :: PL_AXIOM:5 for p,q being boolean object holds 'not' (p 'or' q) <=> ('not' p) '&' ('not' q) = TRUE; theorem :: PL_AXIOM:6 for p,q be boolean object holds (p => q) => (('not' q) => 'not' p) = TRUE; theorem :: PL_AXIOM:7 for p,q,r be boolean object holds p => q => (p => r => (p => (q '&' r))) = TRUE; theorem :: PL_AXIOM:8 for p,q,r be boolean object holds p => r => (q => r => ((p 'or' q) => r)) = TRUE; theorem :: PL_AXIOM:9 for p,q be boolean object holds (p '&' q) <=> (q '&' p) = TRUE; theorem :: PL_AXIOM:10 for p,q be boolean object holds (p 'or' q) <=> (q 'or' p) = TRUE; theorem :: PL_AXIOM:11 for p,q,r be boolean object holds (p '&' q '&' r) <=> (p '&' (q '&' r)) = TRUE; theorem :: PL_AXIOM:12 for p,q,r be boolean object holds (p 'or' q 'or' r) <=> (p 'or' (q 'or' r)) = TRUE; theorem :: PL_AXIOM:13 for p,q be boolean object holds ('not' q => 'not' p) => (('not' q => p) => q) = TRUE; theorem :: PL_AXIOM:14 for p,q,r be boolean object holds p '&' (q 'or' r) <=> ((p '&' q) 'or' (p '&' r)) = TRUE; theorem :: PL_AXIOM:15 for p,q,r be boolean object holds p 'or' (q '&' r) <=> ((p 'or' q) '&' (p 'or' r)) = TRUE; theorem :: PL_AXIOM:16 for X be finite set,Y be set holds Y is c=-linear & X c= union Y & Y <> {} implies ex Z be set st X c= Z & Z in Y; begin definition let D be set; attr D is with_propositional_variables means :: PL_AXIOM:def 1 for n being Element of NAT holds <*3+n*> in D; end; definition let D be set; attr D is PL-closed means :: PL_AXIOM:def 2 D c= NAT* & D is with_FALSUM with_implication with_propositional_variables; end; registration cluster PL-closed -> with_FALSUM with_implication with_propositional_variables non empty for set; cluster with_FALSUM with_implication with_propositional_variables -> PL-closed for Subset of NAT*; end; definition func PL-WFF -> set means :: PL_AXIOM:def 3 it is PL-closed & for D being set st D is PL-closed holds it c= D; end; registration cluster PL-WFF -> PL-closed; end; registration cluster PL-closed non empty for set; end; registration cluster PL-WFF -> functional; end; registration cluster -> FinSequence-like for Element of PL-WFF; end; definition func FaLSUM -> Element of PL-WFF equals :: PL_AXIOM:def 4 <*0*>; let p, q be Element of PL-WFF; func p => q -> Element of PL-WFF equals :: PL_AXIOM:def 5 <*1*>^p^q; end; definition let n be Element of NAT; func Prop n -> Element of PL-WFF equals :: PL_AXIOM:def 6 <*(3 + n)*>; end; definition func props -> Subset of PL-WFF means :: PL_AXIOM:def 7 for x be set holds x in it iff ex n be Element of NAT st x=Prop n; end; reserve p,q,r,s,A,B for Element of PL-WFF, F,G,H for Subset of PL-WFF, k,n for Element of NAT, f,f1,f2 for FinSequence of PL-WFF; definition let D be Subset of PL-WFF; redefine attr D is with_implication means :: PL_AXIOM:def 8 for p, q st p in D & q in D holds p => q in D; end; scheme :: PL_AXIOM:sch 1 PLInd { P[set] }: for r holds P[r] provided P[FaLSUM] and for n holds P[Prop n] and for r,s st P[r] & P[s] holds P[r => s]; theorem :: PL_AXIOM:17 PL-WFF c= HP-WFF; definition let p; func 'not' p -> Element of PL-WFF equals :: PL_AXIOM:def 9 p => FaLSUM; end; definition func VeRUM -> Element of PL-WFF equals :: PL_AXIOM:def 10 'not' FaLSUM; end; definition let p,q; func p '&' q -> Element of PL-WFF equals :: PL_AXIOM:def 11 'not' (p => 'not' q); func p 'or' q -> Element of PL-WFF equals :: PL_AXIOM:def 12 ('not' p) => q; end; definition let p,q; func p <=> q -> Element of PL-WFF equals :: PL_AXIOM:def 13 (p => q) '&' (q => p); end; begin definition mode PLModel is Subset of props; end; reserve M for PLModel; definition let M be PLModel; func SAT M -> Function of PL-WFF,BOOLEAN means :: PL_AXIOM:def 14 it.FaLSUM=0 & (for k holds it.Prop k=1 iff Prop k in M) & for p,q holds it.(p=>q)=(it.p)=>(it.q); end; theorem :: PL_AXIOM:18 (SAT M).(A => B) = 1 iff (SAT M).A = 0 or (SAT M).B = 1; theorem :: PL_AXIOM:19 (SAT M).('not' p) = 'not' (SAT M).p; theorem :: PL_AXIOM:20 (SAT M).('not' A)=1 iff (SAT M).A=0; theorem :: PL_AXIOM:21 (SAT M).(A '&' B) = (SAT M).A '&' (SAT M).B; theorem :: PL_AXIOM:22 (SAT M).(A '&' B) = 1 iff (SAT M).A = 1 & (SAT M).B = 1; theorem :: PL_AXIOM:23 (SAT M).(A 'or' B) = (SAT M).A 'or' (SAT M).B; theorem :: PL_AXIOM:24 (SAT M).(A 'or' B) = 1 iff (SAT M).A = 1 or (SAT M).B = 1; theorem :: PL_AXIOM:25 (SAT M).(A <=> B) = (SAT M).A <=> (SAT M).B; theorem :: PL_AXIOM:26 (SAT M).(A <=> B) = 1 iff (SAT M).A = (SAT M).B; definition let M,p; pred M |= p means :: PL_AXIOM:def 15 (SAT M).p=1; end; definition let M,F; pred M |= F means :: PL_AXIOM:def 16 for p st p in F holds M|=p; end; definition let F,p; pred F |= p means :: PL_AXIOM:def 17 for M st M |= F holds M |= p; end; definition let A; attr A is tautology means :: PL_AXIOM:def 18 for M holds (SAT M).A=1; end; theorem :: PL_AXIOM:27 A is tautology iff {}PL-WFF |= A; theorem :: PL_AXIOM:28 p => (q => p) is tautology; theorem :: PL_AXIOM:29 (p => (q => r)) => ((p => q) => (p => r)) is tautology; theorem :: PL_AXIOM:30 ('not' q => 'not' p) => (('not' q => p) => q) is tautology; theorem :: PL_AXIOM:31 (p => q) => (('not' q) => 'not' p) is tautology; theorem :: PL_AXIOM:32 (p '&' q) => p is tautology; theorem :: PL_AXIOM:33 (p '&' q) => q is tautology; theorem :: PL_AXIOM:34 p => (p 'or' q) is tautology; theorem :: PL_AXIOM:35 q => (p 'or' q) is tautology; theorem :: PL_AXIOM:36 (p '&' q) <=> (q '&' p) is tautology; theorem :: PL_AXIOM:37 (p 'or' q) <=> (q 'or' p) is tautology; theorem :: PL_AXIOM:38 (p '&' q '&' r) <=> (p '&' (q '&' r)) is tautology; theorem :: PL_AXIOM:39 (p 'or' q 'or' r) <=> (p 'or' (q 'or' r)) is tautology; theorem :: PL_AXIOM:40 p '&' (q 'or' r) <=> ((p '&' q) 'or' (p '&' r)) is tautology; theorem :: PL_AXIOM:41 p 'or' (q '&' r) <=> ((p 'or' q) '&' (p 'or' r)) is tautology; theorem :: PL_AXIOM:42 ('not' 'not' p) <=> p is tautology; theorem :: PL_AXIOM:43 'not' (p '&' q) <=> ('not' p) 'or' ('not' q) is tautology; theorem :: PL_AXIOM:44 'not' (p 'or' q) <=> ('not' p) '&' ('not' q) is tautology; theorem :: PL_AXIOM:45 p => q => (p => r => (p => (q '&' r))) is tautology; theorem :: PL_AXIOM:46 p => r => (q => r => ((p 'or' q) => r)) is tautology; theorem :: PL_AXIOM:47 F |= A & F |= A => B implies F |= B; begin definition let D be set; attr D is with_PL_axioms means :: PL_AXIOM:def 19 for p,q,r holds (p => (q => p) in D & (p => (q => r)) => ((p=>q)=>(p=>r)) in D & ('not' q => 'not' p) => (('not' q => p)=>q) in D); end; definition func PL_axioms -> Subset of PL-WFF means :: PL_AXIOM:def 20 it is with_PL_axioms & for D be Subset of PL-WFF st D is with_PL_axioms holds it c=D; end; registration cluster PL_axioms -> with_PL_axioms; end; definition let p,q,r; pred p,q MP_rule r means :: PL_AXIOM:def 21 q = p => r; end; registration cluster PL_axioms -> non empty; end; definition let A; attr A is axpl1 means :: PL_AXIOM:def 22 ex p,q st A = p => (q => p); attr A is axpl2 means :: PL_AXIOM:def 23 ex p,q,r st A = (p => (q => r)) => ((p=>q)=>(p=>r)); attr A is axpl3 means :: PL_AXIOM:def 24 ex p,q st A = ('not' q => 'not' p) => (('not' q => p)=>q); end; theorem :: PL_AXIOM:48 for A be Element of PL_axioms holds (A is axpl1 or A is axpl2 or A is axpl3); theorem :: PL_AXIOM:49 A is axpl1 or A is axpl2 or A is axpl3 implies F |= A; definition let i be Nat,f,F; pred prc f,F,i means :: PL_AXIOM:def 25 f.i in PL_axioms or f.i in F or (ex j,k be Nat st 1<=j & j & 1<=len f1 & for i be Nat st 1<=i & i<=len f1 holds prc f1,F,i) & prc f,F,len f implies (for i be Nat st 1<=i & i<=len f holds prc f,F,i) & F|-p; theorem :: PL_AXIOM:53 p in PL_axioms or p in F implies F |- p; theorem :: PL_AXIOM:54 F |- p & F |- p => q implies F |- q; theorem :: PL_AXIOM:55 F c= G implies (F |- p implies G |- p); begin ::#INSERT: Soundness theorem theorem :: PL_AXIOM:56 F |- A implies F |= A; theorem :: PL_AXIOM:57 F |- A => A; ::$N Deduction theorem theorem :: PL_AXIOM:58 F \/ {A} |- B implies F |- A => B; theorem :: PL_AXIOM:59 F |- A => B implies F \/ {A} |- B; theorem :: PL_AXIOM:60 F |- ('not' A) => (A => B); theorem :: PL_AXIOM:61 F |- ('not' A => A) => A; begin definition let F; attr F is consistent means :: PL_AXIOM:def 27 not ex p st (F |- p & F |- 'not' p); end; theorem :: PL_AXIOM:62 F is consistent iff ex A st not F |- A; theorem :: PL_AXIOM:63 not F |- A implies F \/ {'not' A} is consistent; theorem :: PL_AXIOM:64 for F,A holds F |- A iff ex G st G c= F & G is finite & G |- A; theorem :: PL_AXIOM:65 for F st not F is consistent ex G st G is finite & not G is consistent & G c= F; definition let F; attr F is maximal means :: PL_AXIOM:def 28 for p holds (p in F or 'not' p in F); end; theorem :: PL_AXIOM:66 F c= G & not F is consistent implies not G is consistent; theorem :: PL_AXIOM:67 F is consistent & not F \/ {A} is consistent implies F \/ {'not' A} is consistent; reserve x,y for set; ::$N Lindenbaum's lemma theorem :: PL_AXIOM:68 for F st F is consistent ex G st F c= G & G is consistent & G is maximal; theorem :: PL_AXIOM:69 F is maximal & F is consistent implies for p holds F |- p iff p in F; ::#INSERT: Completeness theorem theorem :: PL_AXIOM:70 F |= A implies F |- A; theorem :: PL_AXIOM:71 A is tautology iff {}PL-WFF |- A;