:: The Axiomatization of Propositional Logic
:: by Mariusz Giero
::
:: Received October 18, 2016
:: Copyright (c) 2016-2017 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;
*