:: The Axiomatization of Propositional Logic
:: by Mariusz Giero
::
:: Received October 18, 2016
:: Copyright (c) 2016 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;
definitions TARSKI, ORDINAL1, INTPRO_1, HILBERT1;
equalities XBOOLEAN, HILBERT1, HILBERT2, FINSEQ_1;
expansions TARSKI, INTPRO_1;
theorems TARSKI, FINSEQ_1, XBOOLE_0, XBOOLE_1, XBOOLEAN, LTLAXIO5, NAT_1,
XXREAL_0, XREAL_1, NAT_D, FUNCT_1, RELAT_2, HILBERT2, RELAT_1, WELLORD1,
WELLORD2, ZFMISC_1, PARTFUN1, WELLFND1, PCOMPS_2, FUNCT_2, XTUPLE_0,
FINSEQ_3, ORDINAL1, FINSET_1, MARGREL1, INTPRO_1, HILBERT1;
schemes XFAMILY, NAT_1, FINSEQ_1, BINOP_1, WELLFND1, FRAENKEL, FUNCT_2,
HILBERT2, XBOOLE_0;
begin
theorem rnginc:
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
proof
let f,g be Function;
assume that A2: dom f c= dom g and A2a: for x be set st x in dom f
holds f.x = g.x;
let x be object;assume x in rng f;then
consider y be object such that A1: y in dom f & x = f.y by FUNCT_1:def 3;
x = g.y by A2a,A1;
hence x in rng g by FUNCT_1:3,A1,A2;
end;
theorem th1:
for p,q being boolean object holds (p '&' q) => p = TRUE
proof
let p,q be boolean object;
p = TRUE or p = FALSE by XBOOLEAN:def 3;
hence (p '&' q) => p = TRUE;
end;
theorem th2:
for p being boolean object holds ('not' 'not' p) <=> p = TRUE
proof
let p be boolean object;
p = TRUE or p = FALSE by XBOOLEAN:def 3;
hence ('not' 'not' p) <=> p = TRUE;
end;
theorem th3:
for p,q being boolean object holds
'not' (p '&' q) <=> ('not' p) 'or' ('not' q) = TRUE
proof
let p,q be boolean object;
A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;
q = TRUE or q = FALSE by XBOOLEAN:def 3;
hence 'not' (p '&' q) <=> ('not' p) 'or' ('not' q) = TRUE by A1;
end;
theorem th3a:
for p,q being boolean object holds
'not' (p 'or' q) <=> ('not' p) '&' ('not' q) = TRUE
proof
let p,q be boolean object;
A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;
q = TRUE or q = FALSE by XBOOLEAN:def 3;
hence 'not' (p 'or' q) <=> ('not' p) '&' ('not' q) = TRUE by A1;
end;
theorem th4:
for p,q be boolean object holds
(p => q) => (('not' q) => 'not' p) = TRUE
proof
let p,q be boolean object;
A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;
q = TRUE or q = FALSE by XBOOLEAN:def 3;
hence (p => q) => (('not' q) => 'not' p) = TRUE by A1;
end;
theorem th5:
for p,q,r be boolean object holds
p => q => (p => r => (p => (q '&' r))) = TRUE
proof
let p,q,r be boolean object;
A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;
A2: q = TRUE or q = FALSE by XBOOLEAN:def 3;
r = TRUE or r = FALSE by XBOOLEAN:def 3;
hence thesis by A1,A2;
end;
theorem th5a:
for p,q,r be boolean object holds
p => r => (q => r => ((p 'or' q) => r)) = TRUE
proof
let p,q,r be boolean object;
A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;
A2: q = TRUE or q = FALSE by XBOOLEAN:def 3;
r = TRUE or r = FALSE by XBOOLEAN:def 3;
hence thesis by A1,A2;
end;
theorem th6:
for p,q be boolean object holds (p '&' q) <=> (q '&' p) = TRUE
proof
let p,q be boolean object;
A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;
q = TRUE or q = FALSE by XBOOLEAN:def 3;
hence (p '&' q) <=> (q '&' p) = TRUE by A1;
end;
theorem th6a:
for p,q be boolean object holds (p 'or' q) <=> (q 'or' p) = TRUE
proof
let p,q be boolean object;
A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;
q = TRUE or q = FALSE by XBOOLEAN:def 3;
hence (p 'or' q) <=> (q 'or' p) = TRUE by A1;
end;
theorem th7:
for p,q,r be boolean object holds
(p '&' q '&' r) <=> (p '&' (q '&' r)) = TRUE
proof
let p,q,r be boolean object;
A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;
A2: q = TRUE or q = FALSE by XBOOLEAN:def 3;
r= TRUE or r = FALSE by XBOOLEAN:def 3;
hence thesis by A1,A2;
end;
theorem th7a:
for p,q,r be boolean object holds
(p 'or' q 'or' r) <=> (p 'or' (q 'or' r)) = TRUE
proof
let p,q,r be boolean object;
A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;
A2: q = TRUE or q = FALSE by XBOOLEAN:def 3;
r= TRUE or r = FALSE by XBOOLEAN:def 3;
hence thesis by A1,A2;
end;
theorem Th17a:
for p,q be boolean object holds
('not' q => 'not' p) => (('not' q => p) => q) = TRUE
proof
let p,q be boolean object;
A1: p = FALSE or p = TRUE by XBOOLEAN:def 3;
q = FALSE or q = TRUE by XBOOLEAN:def 3;
hence thesis by A1;
end;
theorem th8:
for p,q,r be boolean object holds
p '&' (q 'or' r) <=> ((p '&' q) 'or' (p '&' r)) = TRUE
proof
let p,q,r be boolean object;
A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;
A2: q = TRUE or q = FALSE by XBOOLEAN:def 3;
r= TRUE or r = FALSE by XBOOLEAN:def 3;
hence thesis by A1,A2;
end;
theorem th8a:
for p,q,r be boolean object holds
p 'or' (q '&' r) <=> ((p 'or' q) '&' (p 'or' r)) = TRUE
proof
let p,q,r be boolean object;
A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;
A2: q = TRUE or q = FALSE by XBOOLEAN:def 3;
r= TRUE or r = FALSE by XBOOLEAN:def 3;
hence thesis by A1,A2;
end;
theorem uniolinf:
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
proof
let X be finite set,Y be set;
assume
A0: Y is c=-linear & X c= union Y & Y <> {};
deffunc G(object) = {y where y is Element of Y: $1 in y};
deffunc F(object) = the Element of G($1);
A18: for x be object holds x in X implies G(x) is non empty
proof
let x be object;
assume x in X;then
consider y be set such that
A11: x in y & y in Y by TARSKI:def 4,A0;
reconsider y as Element of Y by A11;
y in G(x) by A11;
hence G(x) is non empty;
end;
per cases;
suppose
S1: X is empty;
consider Z be object such that
A15: Z in Y by A0,XBOOLE_0:def 1;
consider Z1 be set such that
A16: Z1 in Y & not ex x be object st x in Y & x in Z1 by TARSKI:3,A15;
X c= Z1 by S1;
hence thesis by A16;
end;
suppose
S2: not X is empty;
set Y1 = {F(x) where x is Element of X: x in X};
A20: X is finite;
A2: Y1 is finite from FRAENKEL:sch 21(A20);
A19: Y1 c= Y
proof
let x be object;
assume x in Y1;then
consider x1 be Element of X such that
A13: x = the Element of G(x1) & x1 in X;
G(x1) is non empty by A18,A13;then
x in G(x1) by A13;then
consider x2 be Element of Y such that
A14: x2 = x & x1 in x2;
thus x in Y by A0,A14;
end;
Y1 <> {}
proof
consider x be object such that
A15: x in X by XBOOLE_0:def 1,S2;
consider x1 be set such that
A16: x1 in X & not ex x be object st x in X & x in x1 by TARSKI:3,A15;
reconsider x1 as Element of X by A16;
the Element of G(x1) in Y1 by A16;
hence thesis;
end;then
consider Z being set such that
A1: Z in Y1 & for y being set st y in Y1 holds y c= Z
by FINSET_1:12,A0,A2,A19;
A4: X c= Z
proof
let x be object;
assume
A8: x in X;then
the Element of G(x) in Y1;then
A9: the Element of G(x) c= Z by A1;
G(x) is non empty by A8,A18;then
the Element of G(x) in G(x);then
consider y3 be Element of Y such that
A10: y3 = the Element of G(x) & x in y3;
thus x in Z by A10,A9;
end;
consider x be Element of X such that
A6: Z = the Element of G(x) & x in X by A1;
G(x) is non empty by A6,A18;then
Z in G(x) by A6;then
consider y be Element of Y such that
U1: y = Z & x in y;
thus ex Z be set st X c= Z & Z in Y by A4,A0,U1;
end;
end;
begin
definition
let D be set;
attr D is with_propositional_variables means
:Def4:
for n being Element of NAT holds <*3+n*> in D;
end;
definition
let D be set;
attr D is PL-closed means
:Def5:
D c= NAT* & D is with_FALSUM
with_implication with_propositional_variables;
end;
Lm1: for D be set st D is PL-closed holds D is non empty
proof
let D be set;
assume D is PL-closed;
then D is with_FALSUM;
hence thesis;
end;
registration
cluster PL-closed -> with_FALSUM with_implication
with_propositional_variables non empty for set;
coherence by Lm1;
cluster with_FALSUM with_implication
with_propositional_variables -> PL-closed for Subset of NAT*;
coherence;
end;
definition
func PL-WFF -> set means
:Def6:
it is PL-closed & for D being set st D is PL-closed holds it c= D;
existence
proof
A1: <*0 qua Element of NAT *> in NAT* by FINSEQ_1:def 11;
defpred P[set] means for D being set st D is PL-closed holds $1 in D;
consider D0 being set such that
A2: for x being set holds x in D0 iff x in NAT* & P[x] from XFAMILY:
sch 1;
A3: for D being set st D is PL-closed holds <*0*> in D by INTPRO_1:def 1;
then reconsider D0 as non empty set by A2,A1;
take D0;
A4: D0 c= NAT* by A2;
for p, q being FinSequence st p in D0 & q in D0 holds <*1*>^p^q in D0
proof
let p, q be FinSequence such that
A5: p in D0 and
A6: q in D0;
A7: q in NAT* by A2,A6;
A8: for D being set st D is PL-closed holds <*1*>^p^q in D
proof
let D be set;
assume
A9: D is PL-closed;
then
A10: q in D by A2,A6;
p in D by A2,A5,A9;
hence thesis by A9,A10,HILBERT1:def 2;
end;
p in NAT* by A2,A5;
then reconsider p9=p, q9=q as FinSequence of NAT by A7,FINSEQ_1:def 11;
<*1*>^p9^q9 in NAT* by FINSEQ_1:def 11;
hence thesis by A2,A8;
end;then
A11: D0 is with_implication by HILBERT1:def 2;
for n being Element of NAT holds <*3+n*> in D0
proof
let n be Element of NAT;
set p = 3+n;
reconsider h = <*p*> as FinSequence of NAT;
A19: h in NAT* by FINSEQ_1:def 11;
for D being set st D is PL-closed holds <*p*> in D by Def4;
hence thesis by A2,A19;
end;
then
A20: D0 is with_propositional_variables;
D0 is with_FALSUM by A2,A1,A3;
hence D0 is PL-closed by A4,A20,A11;
let D be set such that
A21: D is PL-closed;
let x be object;
assume x in D0;
hence thesis by A2,A21;
end;
uniqueness
proof
let D1, D2 be set such that
A22: D1 is PL-closed and
A23: for D being set st D is PL-closed holds D1 c= D and
A24: D2 is PL-closed and
A25: for D being set st D is PL-closed holds D2 c= D;
A26: D2 c= D1 by A22,A25;
D1 c= D2 by A23,A24;
hence thesis by A26,XBOOLE_0:def 10;
end;
end;
registration
cluster PL-WFF -> PL-closed;
coherence by Def6;
end;
registration
cluster PL-closed non empty for set;
existence
proof
take PL-WFF;
thus thesis;
end;
end;
registration
cluster PL-WFF -> functional;
coherence
proof
PL-WFF c= NAT* by Def5;
hence thesis;
end;
end;
registration
cluster -> FinSequence-like for Element of PL-WFF;
coherence
proof
let p be Element of PL-WFF;
PL-WFF c= NAT* by Def5;
hence thesis;
end;
end;
definition
func FaLSUM -> Element of PL-WFF equals
<*0*>;
correctness by INTPRO_1:def 1;
let p, q be Element of PL-WFF;
func p => q -> Element of PL-WFF equals
<*1*>^p^q;
coherence by HILBERT1:def 2;
end;
definition
let n be Element of NAT;
func Prop n -> Element of PL-WFF equals
<*(3 + n)*>;
coherence by Def4;
end;
definition
func props -> Subset of PL-WFF means :defprops:
for x be set holds x in it iff ex n be Element of NAT st x=Prop n;
existence
proof
defpred P1[object] means
ex n be Element of NAT st$1=Prop n;
consider X being set such that
A1: for x being object holds(x in X iff x in PL-WFF & P1[x])
from XBOOLE_0:sch 1;
X c=PL-WFF by A1;
then reconsider X as Subset of PL-WFF;
take X;
thus for x being set holds (x in X iff ex n be Element of NAT st x=Prop n)
by A1;
end;
uniqueness
proof
let A,B be Subset of PL-WFF such that
A2: for x be set holds x in A iff ex n be Element of NAT st x=Prop n and
A3: for x be set holds x in B iff ex n be Element of NAT st x=Prop n;
A4: B c= A
proof
let x be object;
assume x in B;
then consider n be Element of NAT such that
A5: x=Prop n by A3;
thus x in A by A2,A5;
end;
A c= B
proof
let x be object;
assume x in A;
then consider n be Element of NAT such that
A6: x=Prop n by A2;
thus x in B by A3,A6;
end;
hence A=B by A4,XBOOLE_0:def 10;
end;
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
for p, q st p in D & q in D holds p => q in D;
compatibility
proof
thus D is with_implication implies for p, q st p in D & q in D
holds p => q in D by HILBERT1:def 2;
assume
A1: for p, q st p in D & q in D holds p => q in D;
let p, q be FinSequence;
assume
A2: p in D & q in D;
then reconsider p9 = p, q9 = q as Element of PL-WFF;
p9 => q9 in D by A1,A2;
hence thesis;
end;
end;
scheme
PLInd { P[set] }: for r holds P[r]
provided
A1: P[FaLSUM] and
A2: for n holds P[Prop n] and
A3: for r,s st P[r] & P[s] holds P[r => s]
proof
set X = { p where p is Element of PL-WFF: P[p]};
X c= PL-WFF
proof
let x be object;
assume x in X;
then ex p being Element of PL-WFF st x = p & P[p];
hence thesis;
end;
then reconsider X as Subset of PL-WFF;
let r;
A4: X is with_propositional_variables
proof
let n;
P[Prop n] by A2;
hence thesis;
end;
A5: X is with_implication
proof
let p, q;
assume p in X;
then
A6: ex x being Element of PL-WFF st p = x & P[x];
assume q in X;
then ex x being Element of PL-WFF st q = x & P[x];
then P[p => q] by A3,A6;
hence thesis;
end;
PL-WFF c= NAT* by Def5;then
A8: X c= NAT*;
X is with_FALSUM by A1;
then PL-WFF c= X by A8,A5,A4,Def6;
then r in X;
then ex p being Element of PL-WFF st r = p & P[p];
hence thesis;
end;
theorem plhp:
PL-WFF c= HP-WFF
proof
let x be object;
assume
A0: x in PL-WFF;
defpred P[Element of PL-WFF] means $1 in HP-WFF;
VERUM = FaLSUM;
:: syntactically only,since represented by identical sequences
then A1: P[FaLSUM];
A2: for n holds P[Prop n]
proof
let n;
Prop n = prop n;
hence thesis;
end;
A3: for r,s st P[r] & P[s] holds P[r => s]
proof
let r,s;
assume P[r] & P[s];then
reconsider r1 = r, s1 = s as Element of HP-WFF;
r1 => s1 in HP-WFF;
hence P[r => s];
end;
A4: for A holds P[A] from PLInd(A1,A2,A3);
reconsider x1 = x as Element of PL-WFF by A0;
x1 in HP-WFF by A4;
hence x in HP-WFF;
end;
definition let p;
func 'not' p -> Element of PL-WFF equals
p => FaLSUM;
correctness;
end;
definition
func VeRUM -> Element of PL-WFF equals
'not' FaLSUM;
correctness;
end;
definition let p,q;
func p '&' q -> Element of PL-WFF equals
'not' (p => 'not' q);
coherence;
func p 'or' q -> Element of PL-WFF equals
('not' p) => q;
coherence;
end;
definition let p,q;
func p <=> q -> Element of PL-WFF equals
(p => q) '&' (q => p);
correctness;
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 :Def11:
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);
existence
proof
defpred P1[Element of NAT,Element of BOOLEAN] means
$2=1 iff Prop $1 in M;
A16: for x be Element of NAT
ex y being Element of BOOLEAN st P1[x,y]
proof
let x be Element of NAT;
defpred P2[Element of BOOLEAN] means
$1=1 iff Prop x in M;
per cases;
suppose prop x in M;
then P2[TRUE];
hence ex y being Element of BOOLEAN st P1[x,y];
end;
suppose not prop x in M;
then P2[FALSE];
hence ex y being Element of BOOLEAN st P1[x,y];
end;
end;
consider f1 be sequence of BOOLEAN such that
A19: for k holds P1[k,f1.k] from FUNCT_2:sch 3(A16);
deffunc P(Element of NAT)=f1.$1;
defpred C[Element of HP-WFF,Element of HP-WFF,set,set,set] means
ex s5 be Element of BOOLEAN st $5=FALSE;
defpred I[Element of HP-WFF,Element of HP-WFF,set,set,set] means
($3 is Element of BOOLEAN & $4 is Element of BOOLEAN implies ex s3,s4,s5
be Element of BOOLEAN st s3=$3 & s4=$4 & s5=$5 & s5=s3=>s4)
& (not($3 is Element of BOOLEAN & $4 is Element of BOOLEAN)
implies $5=FALSE);
A1: for p,q be Element of HP-WFF for a,b being set
ex c being set st C[p,q,a,b,c];
A2: for p,q be Element of HP-WFF for a,b being set
ex d being set st I[p,q,a,b,d]
proof
let p,q be Element of HP-WFF,a,b be set;
per cases;
suppose a is Element of BOOLEAN & b is Element of BOOLEAN;
then reconsider a1=a,b1=b as Element of BOOLEAN;
reconsider ab = a1 => b1 as Element of BOOLEAN by MARGREL1:def 12;
ab = a1 => b1;
hence thesis;
end;
suppose not(a is Element of BOOLEAN & b is Element of BOOLEAN);
hence thesis;
end;
end;
A3: for p,q be Element of HP-WFF for a,b,c,d being set
st C[p,q,a,b,c] & C[p,q,a,b,d] holds c = d;
A4: for p,q be Element of HP-WFF for a,b,c,d being set
st I[p,q,a,b,c] & I[p,q,a,b,d] holds c = d;
consider sat being ManySortedSet of HP-WFF such that
A34: sat.VERUM=0 &
(for n holds sat.(prop n)=P(n)) &
for p,q be Element of HP-WFF holds C[p,q,sat.p,sat.q,sat.(p '&' q)] &
I[p,q,sat.p,sat.q,sat.(p=>q)] from HILBERT2: sch 3(A1,A2,A3,A4);
A35: for x be object st x in HP-WFF holds sat.x in BOOLEAN
proof
let x be object;
assume x in HP-WFF;
then reconsider x1=x as Element of HP-WFF;
A42: now
let n;
sat.(prop n)=f1.n by A34;
hence sat.(prop n) in BOOLEAN;
end;
per cases by HILBERT2:9;
suppose x1 = VERUM;
hence sat.x in BOOLEAN by A34;
end;
suppose x1 is simple;then
ex n be Element of NAT st x1=prop n by HILBERT2:def 8;
hence sat.x in BOOLEAN by A42;
end;
suppose x1 is conjunctive;then
consider A,B be Element of HP-WFF such that
E2: x1=A '&' B by HILBERT2:def 6;
consider s5 be Element of BOOLEAN such that
E3: sat.(A '&' B)=FALSE by A34;
thus sat.x in BOOLEAN by E3,E2;
end;
suppose x1 is conditional;then
consider A,B be Element of HP-WFF such that
E1: x1=A=>B by HILBERT2:def 7;
A37: I[A,B,sat.A,sat.B,sat.(A=>B)] by A34;
thus sat.x in BOOLEAN by A37,E1;
end;
end;
dom sat=HP-WFF by PARTFUN1:def 2;then
reconsider sat as
Function of HP-WFF,BOOLEAN by A35,FUNCT_2:3;
set satc = sat | PL-WFF;
reconsider satc as Function of PL-WFF,BOOLEAN by FUNCT_2:32,plhp;
B1: satc.FaLSUM = 0 by A34,FUNCT_1:49;
B2: for k holds satc.Prop k=1 iff Prop k in M
proof
let k;
hereby
assume satc.Prop k=1;then
D2: sat.Prop k = 1 by FUNCT_1:49;
sat.prop k = f1.k by A34;
hence Prop k in M by A19,D2;
end;
assume Prop k in M;then
D1: f1.k = 1 by A19;
sat.prop k = f1.k by A34;
hence satc.Prop k=1 by D1,FUNCT_1:49;
end;
for p,q holds satc.(p=>q)=(satc.p)=>(satc.q)
proof
let p,q;
reconsider p1=p,q1=q as Element of HP-WFF by plhp;
consider s3,s4,s5 be Element of BOOLEAN such that
D4: s3=sat.p1 & s4=sat.q1 & s5=sat.(p1=>q1) & s5=s3=>s4 by A34;
thus satc.(p=>q)=sat.(p=>q) by FUNCT_1:49
.= (satc.p)=>(sat.q) by FUNCT_1:49,D4
.= (satc.p)=>(satc.q) by FUNCT_1:49;
end;
hence thesis by B1,B2;
end;
uniqueness
proof
let v1,v2 be Function of PL-WFF,BOOLEAN;
assume
A65: v1.FaLSUM=0 & (for k holds v1.
Prop k=1 iff Prop k in M) & for p,q holds v1.(p=>q)=v1.p=>v1.q;
assume
A66: v2.FaLSUM=0 & (for k holds v2.
Prop k=1 iff Prop k in M) & for p,q holds v2.(p=>q)=v2.p=>v2.q;
defpred P1[Element of PL-WFF] means v1.$1=v2.$1;
A67: P1[Prop n]
proof
per cases;
suppose A68: Prop n in M;
hence v1.Prop n=1 by A65
.=v2.Prop n by A66,A68;
end;
suppose A69: not Prop n in M;
then v1.Prop n=0 by XBOOLEAN:def 3,A65;
hence v1.Prop n = v2.Prop n by XBOOLEAN:def 3,A66,A69;
end;
end;
A70: for p,q st P1[p] & P1[q] holds P1[p=>q]
proof
let p,q;
assume that
A71: P1[p] and
A72: P1[q];
thus v1.(p=>q)=v1.p=>v1.q by A65
.=v2.(p=>q) by A66,A72,A71;
end;
A83: P1[FaLSUM] by A66,A65;
A84: for A holds P1[A] from PLInd(A83,A67,A70); then
A85: for x be Element of PL-WFF st x in dom v1 holds v1.x=v2.x;
dom v1=PL-WFF by FUNCT_2:def 1
.=dom v2 by FUNCT_2:def 1;
hence thesis by A85,PARTFUN1:5;
end;
end;
theorem
(SAT M).(A => B) = 1 iff (SAT M).A = 0 or (SAT M).B = 1
proof
A3: (SAT M).B = TRUE or (SAT M).B = FALSE by XBOOLEAN:def 3;
hereby
assume (SAT M).(A => B) = 1;then
(SAT M).A => (SAT M).B = 1 by Def11;
hence (SAT M).A = 0 or (SAT M).B = 1 by A3;
end;
assume
A4: (SAT M).A = 0 or (SAT M).B = 1;
thus (SAT M).(A => B) = (SAT M).A => (SAT M).B by Def11
.= 1 by A4;
end;
theorem semnot2:
(SAT M).('not' p) = 'not' (SAT M).p
proof
thus (SAT M).('not' p) = (SAT M).p => (SAT M).FaLSUM by Def11
.= (SAT M).p => FALSE by Def11
.= 'not' (SAT M).p;
end;
theorem semnot:
(SAT M).('not' A)=1 iff (SAT M).A=0
proof
hereby assume(SAT M).('not' A)=1;then
'not' (SAT M).A = 1 by semnot2;
hence (SAT M).A=0;
end;
assume A2: (SAT M).A=0;
thus(SAT M).('not' A)= 'not' (SAT M).A by semnot2 .=1 by A2;
end;
theorem semcon2:
(SAT M).(A '&' B) = (SAT M).A '&' (SAT M).B
proof
thus (SAT M).(A '&' B) = 'not' (SAT M).(A => 'not' B) by semnot2
.= 'not' ((SAT M).A => (SAT M).('not' B)) by Def11
.= 'not' ((SAT M).A => 'not' (SAT M).B) by semnot2
.= (SAT M).A '&' (SAT M).B;
end;
theorem
(SAT M).(A '&' B) = 1 iff (SAT M).A = 1 & (SAT M).B = 1
proof
hereby
assume (SAT M).(A '&' B) = 1;then
(SAT M).A '&' (SAT M).B = 1 by semcon2;
hence (SAT M).A = 1 & (SAT M).B = 1 by XBOOLEAN:101;
end;
assume A3:(SAT M).A = 1 & (SAT M).B = 1;
thus (SAT M).(A '&' B) = (SAT M).A '&' (SAT M).B by semcon2
.= 1 by A3;
end;
theorem semdis2:
(SAT M).(A 'or' B) = (SAT M).A 'or' (SAT M).B
proof
thus (SAT M).(A 'or' B) = (SAT M).('not' A) => (SAT M).B by Def11
.= (SAT M).A 'or' (SAT M).B by semnot2;
end;
theorem
(SAT M).(A 'or' B) = 1 iff (SAT M).A = 1 or (SAT M).B = 1
proof
A2: (SAT M).B = TRUE or (SAT M).B = FALSE by XBOOLEAN:def 3;
hereby
assume (SAT M).(A 'or' B) = 1;then
(SAT M).A 'or' (SAT M).B = 1 by semdis2;
hence (SAT M).A = 1 or (SAT M).B = 1 by A2;
end;
assume A3:(SAT M).A = 1 or (SAT M).B = 1;
thus (SAT M).(A 'or' B) = (SAT M).A 'or' (SAT M).B by semdis2
.= 1 by A3;
end;
theorem semequ2:
(SAT M).(A <=> B) = (SAT M).A <=> (SAT M).B
proof
thus (SAT M).(A <=> B) = (SAT M).(A => B) '&' (SAT M).(B => A) by semcon2
.= ((SAT M).A => (SAT M).B) '&' (SAT M).(B => A) by Def11
.= (SAT M).A <=> (SAT M).B by Def11;
end;
theorem
(SAT M).(A <=> B) = 1 iff (SAT M).A = (SAT M).B
proof
A2: (SAT M).B = TRUE or (SAT M).B = FALSE by XBOOLEAN:def 3;
hereby
assume (SAT M).(A <=> B) = 1;then
(SAT M).A <=> (SAT M).B = 1 by semequ2;
hence (SAT M).A = (SAT M).B by A2;
end;
assume A3:(SAT M).A = (SAT M).B;
thus (SAT M).(A <=> B) = (SAT M).A <=> (SAT M).B by semequ2
.=1 by A3,A2;
end;
definition let M,p;
pred M |= p means
(SAT M).p=1;
end;
definition let M,F;
pred M |= F means
for p st p in F holds M|=p;
end;
definition let F,p;
pred F |= p means
for M st M |= F holds M |= p;
end;
definition let A;
attr A is tautology means
for M holds (SAT M).A=1;
end;
theorem tautsat:
A is tautology iff {}PL-WFF |= A
proof
hereby
assume A1: A is tautology;
assume A2: not {}PL-WFF |= A; then
consider M such that
A3: M |= {}PL-WFF & not M |= A;
thus contradiction by A3,A1;
end;
assume
A4: {}PL-WFF |= A;
assume not A is tautology;then
consider M such that
A5: not (SAT M).A=1;
M |= {}PL-WFF;then
M |= A by A4;
hence contradiction by A5;
end;
theorem Th15:
p => (q => p) is tautology
proof
let M;
thus (SAT M).(p => (q => p)) = (SAT M).p => (SAT M).(q => p) by Def11
.= (SAT M).p => ((SAT M).q => (SAT M).p) by Def11
.= 1 by XBOOLEAN:104;
end;
theorem Th16:
(p => (q => r)) => ((p => q) => (p => r)) is tautology
proof
let M;
thus (SAT M).((p => (q => r)) => ((p=>q)=>(p=>r)))
= (SAT M).(p => (q => r)) => (SAT M).((p=>q)=>(p=>r)) by Def11
.= ((SAT M).p => (SAT M).(q => r)) => (SAT M).((p=>q)=>(p=>r)) by Def11
.= ((SAT M).p => ((SAT M).q => (SAT M).r))
=> (SAT M).((p=>q)=>(p=>r)) by Def11
.= ((SAT M).p => ((SAT M).q => (SAT M).r))
=> ((SAT M).(p=>q)=>(SAT M).(p=>r)) by Def11
.= ((SAT M).p => ((SAT M).q => (SAT M).r))
=> (((SAT M).p=>(SAT M).q)=>(SAT M).(p=>r)) by Def11
.= ((SAT M).p => ((SAT M).q => (SAT M).r))
=> (((SAT M).p=>(SAT M).q)=>((SAT M).p=>(SAT M).r)) by Def11
.= 1 by XBOOLEAN:109;
end;
theorem Th17:
('not' q => 'not' p) => (('not' q => p) => q) is tautology
proof
let M;
thus (SAT M).(('not' q => 'not' p) => (('not' q => p)=>q))
= (SAT M).('not' q => 'not' p) => (SAT M).(('not' q => p)=>q) by Def11
.= ((SAT M).('not' q) => (SAT M).('not' p)) =>
(SAT M).(('not' q => p)=>q) by Def11
.= (('not' (SAT M).q) => ((SAT M).('not' p))) =>
(SAT M).(('not' q => p)=>q) by semnot2
.= (('not' (SAT M).q) => ('not' (SAT M).p)) =>
(SAT M).(('not' q => p)=>q) by semnot2
.= (('not' (SAT M).q) => ('not' (SAT M).p)) =>
((SAT M).('not' q => p)=>(SAT M).q) by Def11
.= (('not' (SAT M).q) => ('not' (SAT M).p)) =>
(((SAT M).('not' q) => (SAT M).p)=>(SAT M).q) by Def11
.= (('not' (SAT M).q) => ('not' (SAT M).p)) =>
((('not' (SAT M).q) => (SAT M).p)=>(SAT M).q) by semnot2
.=1 by Th17a;
end;
theorem
(p => q) => (('not' q) => 'not' p) is tautology
proof
let M;
thus (SAT M).((p => q) => (('not' q) => 'not' p)) =
(SAT M).(p => q) => (SAT M).(('not' q) => 'not' p) by Def11
.= ((SAT M).p => (SAT M).q) => (SAT M).(('not' q) => 'not' p) by Def11
.= ((SAT M).p => (SAT M).q) => ((SAT M).('not' q) => (SAT M).('not' p))
by Def11
.= ((SAT M).p => (SAT M).q) => (('not' (SAT M).q) => (SAT M).('not' p))
by semnot2
.= ((SAT M).p => (SAT M).q) => (('not' (SAT M).q) => ('not' (SAT M).p))
by semnot2
.= 1 by th4;
end;
theorem
(p '&' q) => p is tautology
proof
let M;
thus (SAT M).((p '&' q) => p) = (SAT M).(p '&' q) => (SAT M).p by Def11
.= ((SAT M).p '&' (SAT M).q) => (SAT M).p by semcon2
.= 1 by th1;
end;
theorem
(p '&' q) => q is tautology
proof
let M;
thus (SAT M).((p '&' q) => q) = (SAT M).(p '&' q) => (SAT M).q by Def11
.= ((SAT M).p '&' (SAT M).q) => (SAT M).q by semcon2
.= 1 by th1;
end;
theorem
p => (p 'or' q) is tautology
proof
let M;
thus (SAT M).(p => (p 'or' q)) = (SAT M).p => (SAT M).(p 'or' q) by Def11
.= (SAT M).p => ((SAT M).p 'or' (SAT M).q) by semdis2
.= 1 by XBOOLEAN:123;
end;
theorem
q => (p 'or' q) is tautology
proof
let M;
thus (SAT M).(q => (p 'or' q)) = (SAT M).q => (SAT M).(p 'or' q) by Def11
.= (SAT M).q => ((SAT M).p 'or' (SAT M).q) by semdis2
.= 1 by XBOOLEAN:123;
end;
theorem
(p '&' q) <=> (q '&' p) is tautology
proof
let M;
thus (SAT M).((p '&' q) <=> (q '&' p)) =
(SAT M).(p '&' q) <=> (SAT M).(q '&' p) by semequ2
.= ((SAT M).p '&' (SAT M).q) <=> (SAT M).(q '&' p) by semcon2
.= ((SAT M).p '&' (SAT M).q) <=> ((SAT M).q '&' (SAT M).p) by semcon2
.= 1 by th6;
end;
theorem
(p 'or' q) <=> (q 'or' p) is tautology
proof
let M;
thus (SAT M).((p 'or' q) <=> (q 'or' p)) =
(SAT M).(p 'or' q) <=> (SAT M).(q 'or' p) by semequ2
.= ((SAT M).p 'or' (SAT M).q) <=> (SAT M).(q 'or' p) by semdis2
.= ((SAT M).p 'or' (SAT M).q) <=> ((SAT M).q 'or' (SAT M).p) by semdis2
.= 1 by th6a;
end;
theorem
(p '&' q '&' r) <=> (p '&' (q '&' r)) is tautology
proof
let M;
thus (SAT M).((p '&' q '&' r) <=> (p '&' (q '&' r)))
= (SAT M).(p '&' q '&' r) <=> (SAT M).(p '&' (q '&' r)) by semequ2
.= (SAT M).(p '&' q) '&' (SAT M).r <=> (SAT M).(p '&' (q '&' r))
by semcon2
.= (SAT M).(p '&' q) '&' (SAT M).r
<=> ((SAT M).p '&' (SAT M).(q '&' r)) by semcon2
.= (SAT M).(p '&' q) '&' (SAT M).r
<=> ((SAT M).p '&' ((SAT M).q '&' (SAT M).r)) by semcon2
.= (SAT M).p '&' (SAT M).q '&' (SAT M).r
<=> ((SAT M).p '&' ((SAT M).q '&' (SAT M).r)) by semcon2
.= 1 by th7;
end;
theorem
(p 'or' q 'or' r) <=> (p 'or' (q 'or' r)) is tautology
proof
let M;
thus (SAT M).((p 'or' q 'or' r) <=> (p 'or' (q 'or' r)))
= (SAT M).(p 'or' q 'or' r) <=> (SAT M).(p 'or' (q 'or' r)) by semequ2
.= (SAT M).(p 'or' q) 'or' (SAT M).r <=> (SAT M).(p 'or' (q 'or' r))
by semdis2
.= (SAT M).(p 'or' q) 'or' (SAT M).r
<=> ((SAT M).p 'or' (SAT M).(q 'or' r)) by semdis2
.= (SAT M).(p 'or' q) 'or' (SAT M).r
<=> ((SAT M).p 'or' ((SAT M).q 'or' (SAT M).r)) by semdis2
.= (SAT M).p 'or' (SAT M).q 'or' (SAT M).r
<=> ((SAT M).p 'or' ((SAT M).q 'or' (SAT M).r)) by semdis2
.= 1 by th7a;
end;
theorem
p '&' (q 'or' r) <=> ((p '&' q) 'or' (p '&' r)) is tautology
proof
let M;
thus (SAT M).(p '&' (q 'or' r) <=> ((p '&' q) 'or' (p '&' r)))
= (SAT M).(p '&' (q 'or' r)) <=>
(SAT M).((p '&' q) 'or' (p '&' r)) by semequ2
.= (SAT M).p '&' (SAT M).(q 'or' r) <=>
(SAT M).((p '&' q) 'or' (p '&' r)) by semcon2
.= (SAT M).p '&' ((SAT M).q 'or' (SAT M).r) <=>
(SAT M).((p '&' q) 'or' (p '&' r)) by semdis2
.= (SAT M).p '&' ((SAT M).q 'or' (SAT M).r) <=>
((SAT M).(p '&' q) 'or' (SAT M).(p '&' r)) by semdis2
.= (SAT M).p '&' ((SAT M).q 'or' (SAT M).r) <=>
((SAT M).p '&' (SAT M).q 'or' (SAT M).(p '&' r)) by semcon2
.= (SAT M).p '&' ((SAT M).q 'or' (SAT M).r) <=>
((SAT M).p '&' (SAT M).q 'or' ((SAT M).p '&' (SAT M).r)) by semcon2
.= 1 by th8;
end;
theorem
p 'or' (q '&' r) <=> ((p 'or' q) '&' (p 'or' r)) is tautology
proof
let M;
thus (SAT M).(p 'or' (q '&' r) <=> ((p 'or' q) '&' (p 'or' r)))
= (SAT M).(p 'or' (q '&' r)) <=>
(SAT M).((p 'or' q) '&' (p 'or' r)) by semequ2
.= (SAT M).p 'or' (SAT M).(q '&' r) <=>
(SAT M).((p 'or' q) '&' (p 'or' r)) by semdis2
.= (SAT M).p 'or' ((SAT M).q '&' (SAT M).r) <=>
(SAT M).((p 'or' q) '&' (p 'or' r)) by semcon2
.= (SAT M).p 'or' ((SAT M).q '&' (SAT M).r) <=>
((SAT M).(p 'or' q) '&' (SAT M).(p 'or' r)) by semcon2
.= (SAT M).p 'or' ((SAT M).q '&' (SAT M).r) <=>
(((SAT M).p 'or' (SAT M).q) '&' (SAT M).(p 'or' r)) by semdis2
.= (SAT M).p 'or' ((SAT M).q '&' (SAT M).r) <=>
(((SAT M).p 'or' (SAT M).q) '&' ((SAT M).p 'or' (SAT M).r)) by semdis2
.= 1 by th8a;
end;
theorem
('not' 'not' p) <=> p is tautology
proof
let M;
thus (SAT M).(('not' 'not' p) <=> p) =
(SAT M).('not' 'not' p) <=> (SAT M).p by semequ2
.= ('not' (SAT M).('not' p)) <=> (SAT M).p by semnot2
.= ('not' 'not' (SAT M).p) <=> (SAT M).p by semnot2
.=1 by th2;
end;
theorem
'not' (p '&' q) <=> ('not' p) 'or' ('not' q) is tautology
proof
let M;
thus (SAT M).('not' (p '&' q) <=> ('not' p) 'or' ('not' q)) =
(SAT M).('not' (p '&' q)) <=> (SAT M).(('not' p) 'or' ('not' q)) by semequ2
.= ('not' (SAT M).(p '&' q)) <=>
(SAT M).(('not' p) 'or' ('not' q)) by semnot2
.= ('not' ((SAT M).p '&' (SAT M).q)) <=>
(SAT M).(('not' p) 'or' ('not' q)) by semcon2
.= ('not' ((SAT M).p '&' (SAT M).q)) <=>
((SAT M).('not' p) 'or' (SAT M).('not' q)) by semdis2
.= ('not' ((SAT M).p '&' (SAT M).q)) <=>
('not' (SAT M).p 'or' (SAT M).('not' q)) by semnot2
.= ('not' ((SAT M).p '&' (SAT M).q)) <=>
('not' (SAT M).p 'or' 'not' (SAT M).q) by semnot2
.= 1 by th3;
end;
theorem
'not' (p 'or' q) <=> ('not' p) '&' ('not' q) is tautology
proof
let M;
thus (SAT M).('not' (p 'or' q) <=> ('not' p) '&' ('not' q)) =
(SAT M).('not' (p 'or' q)) <=> (SAT M).(('not' p) '&' ('not' q)) by semequ2
.= ('not' (SAT M).(p 'or' q)) <=>
(SAT M).(('not' p) '&' ('not' q)) by semnot2
.= ('not' ((SAT M).p 'or' (SAT M).q)) <=>
(SAT M).(('not' p) '&' ('not' q)) by semdis2
.= ('not' ((SAT M).p 'or' (SAT M).q)) <=>
((SAT M).('not' p) '&' (SAT M).('not' q)) by semcon2
.= ('not' ((SAT M).p 'or' (SAT M).q)) <=>
('not' (SAT M).p '&' (SAT M).('not' q)) by semnot2
.= ('not' ((SAT M).p 'or' (SAT M).q)) <=>
('not' (SAT M).p '&' 'not' (SAT M).q) by semnot2
.= 1 by th3a;
end;
theorem
p => q => (p => r => (p => (q '&' r))) is tautology
proof
let M;
thus (SAT M).(p => q => (p => r => (p => (q '&' r))))
= (SAT M).(p =>q) => (SAT M).(p => r => (p => (q '&' r))) by Def11
.= (SAT M).p => (SAT M).q => ((SAT M).(p => r => (p => (q '&' r)))) by Def11
.= (SAT M).p => (SAT M).q
=> ((SAT M).(p => r) => (SAT M).(p => (q '&' r))) by Def11
.= (SAT M).p => (SAT M).q =>
((SAT M).p => (SAT M).r => (SAT M).(p => (q '&' r))) by Def11
.= (SAT M).p => (SAT M).q =>
((SAT M).p => (SAT M).r => ((SAT M).p => (SAT M).(q '&' r))) by Def11
.= (SAT M).p => (SAT M).q =>
((SAT M).p => (SAT M).r => ((SAT M).p => ((SAT M).q '&' (SAT M).r))) by semcon2
.= 1 by th5;
end;
theorem
p => r => (q => r => ((p 'or' q) => r)) is tautology
proof
let M;
A3: (SAT M).(q => r => ((p 'or' q) => r))
= (SAT M).(q => r) => (SAT M).((p 'or' q) => r) by Def11
.= (SAT M).q => (SAT M).r => (SAT M).((p 'or' q) => r) by Def11
.= (SAT M).q => (SAT M).r => ((SAT M).(p 'or' q) => (SAT M).r) by Def11
.= (SAT M).q => (SAT M).r => (((SAT M).p 'or' (SAT M).q) => (SAT M).r)
by semdis2;
thus (SAT M).(p => r => (q => r => ((p 'or' q) => r)))
= (SAT M).(p => r) => (SAT M).(q => r => ((p 'or' q) => r)) by Def11
.= (SAT M).p => (SAT M).r => ((SAT M).q => (SAT M).r
=> (((SAT M).p 'or' (SAT M).q) => (SAT M).r)) by Def11,A3
.= 1 by th5a;
end;
theorem th24:
F |= A & F |= A => B implies F |= B
proof
assume that
A1: F|=A and
A2: F|=A=>B;
let M;
assume
A3: M|=F;then
M |= A=>B by A2;
then A4: (SAT M).A=>(SAT M).B=1 by Def11;
M |= A by A1,A3;
hence (SAT M).B=1 by A4;
end;
begin
definition let D be set;
attr D is with_PL_axioms means :withplax:
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 :defplax:
it is with_PL_axioms &
for D be Subset of PL-WFF st D is with_PL_axioms holds it c=D;
existence
proof
defpred S1[object] means
for D being set st D is with_PL_axioms holds$1 in D;
consider D0 being set such that
A1: for x being object
holds(x in D0 iff x in PL-WFF & S1[x]) from XBOOLE_0:sch 1;
D0 c=PL-WFF by A1;
then reconsider D0 as Subset of PL-WFF;
take D0;
thus D0 is with_PL_axioms
proof
let p,q,r be Element of PL-WFF;
for D being set st D is with_PL_axioms holds p => (q => p) in D;
hence p => (q => p) in D0 by A1;
for D being set st D is with_PL_axioms holds
(p => (q => r)) => ((p=>q)=>(p=>r)) in D;
hence (p => (q => r)) => ((p=>q)=>(p=>r)) in D0 by A1;
for D being set st D is with_PL_axioms holds
('not' q => 'not' p) => (('not' q => p)=>q) in D;
hence ('not' q => 'not' p) => (('not' q => p)=>q) in D0 by A1;
end;
let D be Subset of PL-WFF;
assume A2: D is with_PL_axioms;
let x be object;
assume x in D0;
hence x in D by A1,A2;
end;
uniqueness
proof
let D1,D2 be Subset of PL-WFF;
assume(D1 is with_PL_axioms) & (for D be Subset of PL-WFF st D is
with_PL_axioms holds D1 c=D) & D2 is with_PL_axioms & for D be Subset of
PL-WFF st D is with_PL_axioms holds D2 c=D;
then D1 c=D2 & D2 c=D1;
hence D1=D2 by XBOOLE_0:def 10;
end;
end;
registration
cluster PL_axioms -> with_PL_axioms;
coherence by defplax;
end;
definition let p,q,r;
pred p,q MP_rule r means
q = p => r;
end;
registration
cluster PL_axioms -> non empty;
coherence by withplax;
end;
definition let A;
attr A is axpl1 means :defaxpl1:
ex p,q st A = p => (q => p);
attr A is axpl2 means :defaxpl2:
ex p,q,r st A = (p => (q => r)) => ((p=>q)=>(p=>r));
attr A is axpl3 means :defaxpl3:
ex p,q st A = ('not' q => 'not' p) => (('not' q => p)=>q);
end;
theorem Th36:
for A be Element of PL_axioms holds
(A is axpl1 or A is axpl2 or A is axpl3)
proof
defpred P1[Element of PL_axioms] means
$1 is axpl1 or $1 is axpl2 or $1 is axpl3;
set X={p where p is Element of PL_axioms:P1[p]};
X c=PL-WFF
proof
let x be object;
assume x in X;
then ex p be Element of PL_axioms st x=p & P1[p];
hence x in PL-WFF;
end;
then reconsider X as Subset of PL-WFF;
let A be Element of PL_axioms;
X is with_PL_axioms
proof
let p,q,r;
thus p => (q => p) in X
proof
reconsider pp=p =>(q =>p) as Element of PL_axioms by withplax;
P1[pp] by defaxpl1;
hence thesis;
end;
thus (p => (q => r)) => ((p=>q)=>(p=>r)) in X
proof
reconsider pp=(p => (q => r)) => ((p=>q)=>(p=>r))
as Element of PL_axioms by withplax;
P1[pp] by defaxpl2;
hence thesis;
end;
thus ('not' q => 'not' p) => (('not' q => p)=>q) in X
proof
reconsider pp=('not' q => 'not' p) => (('not' q => p)=>q)
as Element of PL_axioms by withplax;
P1[pp] by defaxpl3;
hence thesis;
end;
end;
then A in PL_axioms & PL_axioms c=X by defplax;
then A in X;
then ex p be Element of PL_axioms st A=p & P1[p];
hence P1[A];
end;
theorem Th37:
A is axpl1 or A is axpl2 or A is axpl3 implies F |= A
proof
assume A1: A is axpl1 or A is axpl2 or A is axpl3;
let M;
assume M|=F;
per cases by A1;
suppose A is axpl1;
then consider p,q be Element of PL-WFF such that
A2: A=p => (q => p);
A is tautology by Th15,A2;
hence thesis;
end;
suppose A is axpl2;
then consider p,q,r be Element of PL-WFF such that
A3: A=(p => (q => r)) => ((p=>q)=>(p=>r));
A is tautology by Th16,A3;
hence thesis;
end;
suppose A is axpl3;
then consider p,q be Element of PL-WFF such that
A4: A=('not' q => 'not' p) => (('not' q => p)=>q);
A is tautology by Th17,A4;
hence thesis;
end;
end;
definition let i be Nat,f,F;
pred prc f,F,i means :defprc:
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
proof
assume that
A1: f=f1^<*p*> and
1<=len f1 and
A2: for i be Nat st 1<=i & i<=len f1 holds prc f1,F,i;
A3: len f=(len f1+len<*p*>) by A1,FINSEQ_1:22
.=len f1+1 by FINSEQ_1:39;
assume A4: prc f,F,len f;
A5: 0+len f1<=len f by A3,NAT_1:12;
A6: now let i be Nat;
assume that
A7: 1<=i and
A8: i<=len f;
A9: i) by A1,FINSEQ_1:22
.=f.(len f1+1) by FINSEQ_1:39
.=p by A1,FINSEQ_1:42;
hence F|-p by A3,XREAL_1:31,A6;
end;
theorem th42:
p in PL_axioms or p in F implies F |- p
proof
defpred P1[set,set] means $2=p;
A1: for k being Nat st k in Seg 1 holds ex x being Element of
PL-WFF st P1[k,x];
consider f such that
A2: dom f=Seg 1 & for k being Nat st k in Seg 1 holds P1[k,f.k]
from FINSEQ_1:sch 5(A1);
A3: len f=1 by A2,FINSEQ_1:def 3;
1 in Seg 1;
then A4: f.1=p by A2;
assume A5: p in PL_axioms or p in F;
for j be Nat st 1<=j & j<=len f holds prc f,F,j
proof
let j be Nat;
assume A6: 1<=j & j<=len f;
per cases by A5;
suppose p in PL_axioms;
hence thesis by A3,A4,A6,XXREAL_0:1;
end;
suppose p in F;
hence thesis by A3,A4,A6,XXREAL_0:1;
end;
end;
hence F|-p by A3,A4;
end;
theorem th43:
F |- p & F |- p => q implies F |- q
proof
assume F|-p;
then consider f such that
A1: f.len f=p and
A2: 1<=len f and
A3: for i be Nat st 1<=i & i<=len f holds prc f,F,i;
set j=len f;
assume F|-p=>q;
then consider f1 such that
A4: f1.len f1=p=>q and
A5: 1<=len f1 and
A6: for i be Nat st 1<=i & i<=len f1 holds prc f1,F,i;
A7: 1<=len f+len f1 by A2,NAT_1:12;
set g=f^f1^<*q*>;
A8: g=f^(f1^<*q*>) by FINSEQ_1:32;
A9: for i be Nat st 1<=i & i<=len f1 holds g.(len f+i)=f1.i
proof
let i be Nat;
assume that
A10: 1<=i and
A11: i<=len f1;
len(f1^<*q*>)=len f1+len<*q*> by FINSEQ_1:22
.=len f1+1 by FINSEQ_1:39;
then i<=len(f1^<*q*>) by A11,NAT_1:12;
hence g.(len f+i)=(f1^<*q*>).i by A8,A10,FINSEQ_1:65
.=f1.i by A10,A11,FINSEQ_1:64;
end;
A12: len g=len(f^f1)+len<*q*> by FINSEQ_1:22
.=len(f^f1)+1 by FINSEQ_1:39;
then A13: len g=len f+len f1+1 by FINSEQ_1:22;
then len g=len f+(len f1+1);
then A14: jq by A4,A5,A9;
then g/.j,g/.k MP_rule g/.len g by A15,LTLAXIO5:1,U1;
then A19: len(f^f1)=len f+len f1 & prc g,F,len g by A2,A14,A16,A18,
FINSEQ_1:22;
for i be Nat st 1<=i & i<=len(f^f1) holds prc f^f1,F,i by A2,A3,A5,A6,Th39;
hence F|-q by A7,A19,Th40;
end;
theorem monmp:
F c= G implies (F |- p implies G |- p)
proof
assume Z0: F c= G;
assume F |- p;then
consider f such that C1: f.len f = p & 1<=len f &
for k be Nat st 1<=k<=len f holds prc f,F,k;
C17: len f in dom f by C1,FINSEQ_3:25;
defpred P3[Nat] means 1 <= $1 <= len f implies G |- f/.$1;
C2: now
let s be Nat;
assume C5: for n being Nat st n < s holds P3[n];
per cases by NAT_1:14;
suppose s = 0;
hence P3[s];
end;
suppose not s < 1;
assume C7: 1 <= s <= len f;then
C3: prc f,F,s by C1;
C16: s in dom f by C7,FINSEQ_3:25;
thus G |- f/.s
proof
per cases by C3;
suppose f.s in PL_axioms;then
f/.s in PL_axioms by C16,PARTFUN1:def 6;
hence G |- f/.s by th42;
end;
suppose f.s in F;then
f/.s in F by C16,PARTFUN1:def 6;
hence G |- f/.s by th42,Z0;
end;
suppose ex j,k be Nat st 1<=j & j*~~f/.i by A5,A12,A13,A14,U1;
hence F|=f/.i by A5,A10,A11,A16,th24;
end;
end;
end;
A22: for i be Nat holds P[i] from NAT_1:sch 4(A4);
f/.len f=A by A1,A2,LTLAXIO5:1;
hence F|=A by A2,A22;
end;
theorem thaa:
F |- A => A
proof
A=>((A=>A)=>A) in PL_axioms by withplax;then
A1: F |- A=>((A=>A)=>A) by th42;
A=>(A=>A) in PL_axioms by withplax;then
A2: F |- A=>(A=>A) by th42;
(A=>((A=>A)=>A)) => ((A=>(A=>A))=>(A=>A)) in PL_axioms by withplax;then
F |- (A=>((A=>A)=>A)) => ((A=>(A=>A))=>(A=>A)) by th42;then
F |- (A=>(A=>A))=>(A=>A) by th43,A1;
hence F|- A=>A by th43,A2;
end;
::$N Deduction theorem
theorem ded:
F \/ {A} |- B implies F |- A => B
proof
assume F \/ {A} |- B;then
consider f such that
A1: f.len f = B and
A2: 1<=len f and
A3: for i be Nat st 1<=i & i<=len f holds prc f,F \/ {A},i;
defpred P[Nat] means
1<=$1 & $1<=len f implies F |- A => f/.$1;
A4: for i being Nat st for j being Nat st j~~* (A=>f/.i) in PL_axioms by withplax;then
A9: F |- f/.i => (A=>f/.i) by th42;
f/.i in PL_axioms by A6,A7,A8,LTLAXIO5:1;then
F |- f/.i by th42;
hence thesis by th43,A9;
end;
suppose A10: f.i in F \/ {A};
per cases by A10,XBOOLE_0:def 3;
suppose A11: f.i in F;
f/.i => (A=>f/.i) in PL_axioms by withplax;then
A12: F |- f/.i=>(A=>f/.i) by th42;
f/.i in F by A6,A7,A11,LTLAXIO5:1;then
F |- f/.i by th42;
hence thesis by th43,A12;
end;
suppose f.i in {A};then
f.i=A by TARSKI:def 1;then
f/.i=A by A6,A7,LTLAXIO5:1;
hence thesis by thaa;
end;
end;
suppose ex j,k be Nat st 1<=j & j** f/.j by A5,A15,A16;
k<=len f by A7,A18,XXREAL_0:2;then
A21: F|- A => f/.k by A5,A17,A18;
(A=>(f/.j=>f/.i))=>((A=>f/.j)=>(A=>f/.i)) in PL_axioms
by withplax;then
A23: F |- (A=>(f/.j=>f/.i))=>((A=>f/.j)=>(A=>f/.i)) by th42;
F|- (A=>f/.j)=>(A=>f/.i) by A23,th43,A21,A19;
hence F |- A => f/.i by A20,th43;
end;
end;
end;
A37: for i be Nat holds P[i] from NAT_1:sch 4(A4);
B = f/.len f by A1,A2,LTLAXIO5:1;
hence F |- A => B by A2,A37;
end;
theorem
F |- A => B implies F \/ {A} |- B
proof
A in {A} by TARSKI:def 1;
then A in F\/{A} by XBOOLE_0:def 3;
then A1: F\/{A}|-A by th42;
assume F|-A=>B;
then F\/{A}|-A=>B by monmp,XBOOLE_1:7;
hence F\/{A}|-B by A1,th43;
end;
theorem naab:
F |- ('not' A) => (A => B)
proof
set f = F \/ {'not' A} \/ {A};
A in f by ZFMISC_1:31,XBOOLE_1:11;then
A1: f |- A by th42;
f = F \/ {A} \/ {'not' A} by XBOOLE_1:4;then
'not' A in f by ZFMISC_1:31,XBOOLE_1:11;then
A2: f |- 'not' A by th42;
A => ('not' B => A) in PL_axioms by withplax;then
f |- A => ('not' B => A) by th42;then
A4: f |- ('not' B => A) by th43,A1;
'not' A => ('not' B => 'not' A) in PL_axioms by withplax;then
f |- 'not' A => ('not' B => 'not' A) by th42;then
A3: f |- 'not' B => 'not' A by th43,A2;
('not' B => 'not' A) => (('not' B => A)=>B) in PL_axioms by withplax;
then f |- ('not' B => 'not' A) => (('not' B => A)=>B) by th42;then
f |- ('not' B => A)=>B by th43,A3;then
f |- B by th43,A4;then
F \/ {'not' A} |- A => B by ded;
hence thesis by ded;
end;
theorem naa:
F |- ('not' A => A) => A
proof
'not' A => 'not' A => (('not' A => A)=>A) in PL_axioms by withplax;then
A1: F |- ('not' A => 'not' A) => (('not' A => A)=>A) by th42;
F |- 'not' A => 'not' A by thaa;
hence thesis by A1,th43;
end;
begin
definition
let F;
attr F is consistent means
not ex p st (F |- p & F |- 'not' p);
end;
theorem conco:
F is consistent iff ex A st not F |- A
proof
hereby assume
A0: F is consistent;
assume
A1: for A holds F |- A;then
A2: F |- Prop 0;
F |- 'not' Prop 0 by A1;
hence contradiction by A2,A0;
end;
assume
A4: ex A st not F |- A;
assume not F is consistent;then
consider A such that
A3: F |- A & F |- 'not' A;
now
let B;
F |- 'not' A => (A => B) by naab;then
F|- A => B by A3,th43;
hence F |- B by A3,th43;
end;
hence contradiction by A4;
end;
theorem th34:
not F |- A implies F \/ {'not' A} is consistent
proof
assume Z1: not F |- A;
assume not F \/ {'not' A} is consistent;then
A2: F |- 'not'A => A by ded,conco;
F |- ('not' A => A) => A by naa;
hence contradiction by Z1,A2,th43;
end;
theorem exfin:
for F,A holds
F |- A iff ex G st G c= F & G is finite & G |- A
proof
let F,A;
hereby
assume F |- A;then
consider f such that
A1: f.len f=A & 1<=len f &
for i be Nat st 1<=i & i<=len f holds prc f,F,i;
deffunc h(Nat) = f.$1;
set w2 = {i where i is Element of NAT: 1<=i & i<=len f};
set G = {h(i) where i is Element of NAT: i in w2};
F1: w2 c= Seg len f
proof
let x be object;
assume x in w2;then
consider i be Element of NAT such that
F2: i = x & 1<=i<=len f;
reconsider i1 = i as Nat;
thus x in Seg len f by F2;
end;
A8: w2 is finite by F1;
A4: G c= PL-WFF
proof
let x be object;
assume x in G;then
consider i be Element of NAT such that
A6: x = h(i) & i in w2;
consider j be Element of NAT such that
A9: j = i & 1<=j & j<=len f by A6;
i in dom f by FINSEQ_3:25,A9;then
A7: x in rng f by A6,FUNCT_1:def 3;
rng f c= PL-WFF by FINSEQ_1:def 4;
hence x in PL-WFF by A7;
end;
G is finite from FRAENKEL:sch 21(A8);then
reconsider G as finite Subset of PL-WFF by A4;
now
let i be Nat;
assume
A6: 1<=i<=len f;then
prc f,F,i by A1;then
per cases;
suppose f.i in PL_axioms;
hence prc f,F/\G,i;
end;
suppose
A5: f.i in F;
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
i1 in w2 by A6;then
f.i in G;
hence prc f,F/\G,i by A5,XBOOLE_0:def 4;
end;
suppose ex j,k be Nat
st 1<=j & j** A by ded,conco;
F |- (('not' A) => A) => A by naa;then
A6: F |- A by A2,th43;
F |- 'not' A by A1,conco,ded;
hence contradiction by A6,A1;
end;
reserve x,y for set;
::$N Lindenbaum's lemma
theorem th37:
for F st F is consistent ex G st F c= G & G is consistent & G is maximal
proof
let F;
assume Z0: F is consistent;
set L = PL-WFF;
consider R be Relation such that
A3: R well_orders L by WELLORD2:17;
R /\ [:L,L:]c=[:L,L:] by XBOOLE_1:17;
then reconsider R2 = R |_2 L as Relation of L by WELLORD1:def 6;
R2 well_orders L by A3,PCOMPS_2:1;then
A76: R2 is_connected_in L by WELLORD1:def 5;
reconsider RS = RelStr(#L,R2#) as non empty RelStr;
set cRS = the carrier of RS;
defpred H[object,object,object] means
for p for f be PartFunc of cRS,bool L st $1=p & $2=f holds
((union(rng (f qua bool L -valued Relation)) \/ F \/ {p} is consistent
implies $3=union (rng f) \/ F \/ {p}) &
(not union(rng (f qua bool L -valued Relation)) \/ F \/ {p} is consistent
implies $3=union (rng f) \/ F));
A4: for x,y be object st x in cRS & y in PFuncs(cRS, bool L)
ex z be object st z in bool L &
H[x,y,z]
proof
let x,y be object;
assume A6: x in cRS & y in PFuncs(cRS, bool L);
reconsider x1 = x as Element of L by A6;
reconsider y1 = y as PartFunc of cRS,bool L by A6,PARTFUN1:46;
per cases;
suppose
A7: union(rng (y1 qua bool L -valued Relation)) \/ F \/ {x1} is consistent;
take union(rng y1) \/ F \/ {x1};
thus thesis by A7;
end;
suppose
A7a:not union(rng (y1 qua bool L -valued Relation)) \/ F \/ {x1} is consistent;
take union(rng y1) \/ F;
thus thesis by A7a;
end;
end;
consider h be Function of [:cRS,PFuncs(cRS, bool L):],bool L such that
A9: for x,y be object st x in cRS & y in PFuncs(cRS, bool L)
holds H[x,y,h.(x,y)] from BINOP_1:sch 1(A4);
R2 well_orders L by A3,PCOMPS_2:1;then
R2 is_well_founded_in L by WELLORD1:def 5;then
A11: RS is well_founded by WELLFND1:def 2;then
consider f be Function of cRS, bool L such that
A12: f is_recursively_expressed_by h by WELLFND1:11;
A73: dom f = cRS by FUNCT_2:def 1;
reconsider G=union (rng (f qua bool L -valued Relation))
as Subset of PL-WFF;
set iRS = the InternalRel of RS;
F6: field R2 = L by A3,PCOMPS_2:1;
A17: for A,B holds [A,B] in R2 implies f.A c= f.B
proof
let A,B;assume F3: [A,B] in R2;
per cases;
suppose A = B;
hence thesis;
end;
suppose S2: A <> B;
set frA = f|iRS-Seg A;
set frB = f|iRS-Seg B;
iRS is well-ordering by A3,PCOMPS_2:1,WELLORD1:4,F6;then
F12: iRS-Seg A c= iRS-Seg B by F3,WELLORD1:29,F6;
iRS-Seg B c= field iRS by WELLORD1:9;then
F21: frB is Function of iRS-Seg B,bool L by FUNCT_2:32,F6;
iRS-Seg A c= field iRS by WELLORD1:9;then
frA is Function of iRS-Seg A,bool L by FUNCT_2:32,F6;then
F11: dom frA = iRS-Seg A by FUNCT_2:def 1;
F13: dom frB = iRS-Seg B by FUNCT_2:def 1,F21;
F18:
now
let x;assume F19: x in dom frA;
thus frA.x = f.x by F19,FUNCT_1:47
.= frB.x by F13,FUNCT_1:47,F12,F11,F19;
end;
E1: union rng frA c= union rng frB by ZFMISC_1:77,rnginc,F18,F11,F12,F13;then
F7: union rng frA \/ F c= union rng frB \/ F by XBOOLE_1:9;
F15: A in dom frB by F13,S2,F3,WELLORD1:1;
frB.A = f.A by FUNCT_1:47,F13,S2,F3,WELLORD1:1;then
F14: f.A c= union rng frB by ZFMISC_1:74,FUNCT_1:3,F15;
F18: dom frA c= cRS;
rng (frA qua bool L -valued Relation) c= bool L;then
E4: frA in PFuncs(cRS, bool L) by PARTFUN1:def 3,F18;
F18a: dom frB c= cRS;
rng (frB qua bool L -valued Relation) c= bool L;then
E2: frB in PFuncs(cRS, bool L) by PARTFUN1:def 3,F18a;
per cases;
suppose union(rng (frA qua bool L -valued Relation)) \/ F \/ {A}
is consistent;
per cases;
suppose
F2a: union(rng (frB qua bool L -valued Relation)) \/ F \/ {B}
is consistent;
F16: f.B = h.(B, frB) by WELLFND1:def 5,A12
.= union (rng frB) \/ F \/ {B} by A9,E2,F2a;
thus f.A c= f.B
proof
let x be object;assume x in f.A;then
x in union (rng frB) \/ (F \/ {B}) by XBOOLE_0:def 3,F14;
hence thesis by F16,XBOOLE_1:4;
end;
end;
suppose
F2b:not union(rng (frB qua bool L -valued Relation)) \/ F \/ {B} is consistent;
F16b: f.B = h.(B, frB) by WELLFND1:def 5,A12
.= union (rng frB) \/ F by A9,E2,F2b;
thus f.A c= f.B by F16b,XBOOLE_0:def 3,F14;
end;
end;
suppose
F2:not union(rng (frA qua bool L -valued Relation)) \/ F \/ {A} is consistent;
F8: f.A = h.(A, frA) by WELLFND1:def 5,A12
.= union (rng frA) \/ F by A9,E4,F2;
per cases;
suppose F2a: union(rng (frB qua bool L -valued Relation)) \/ F \/ {B}
is consistent;
F9: f.B = h.(B, frB) by WELLFND1:def 5,A12
.= union (rng frB) \/ F \/ {B} by A9,E2,F2a;
thus f.A c= f.B by F8,F9,XBOOLE_1:10,F7;
end;
suppose F2b:
not union(rng (frB qua bool L -valued Relation)) \/ F \/ {B} is consistent;
f.B = h.(B, frB) by WELLFND1:def 5,A12
.= union (rng frB) \/ F by A9,E2,F2b;
hence f.A c= f.B by F8,XBOOLE_1:9,E1;
end;
end;
end;
end;
A54: rng f is c=-linear
proof
let x,y;assume B2: x in rng f & y in rng f;then
consider x1 be object such that B3: x1 in dom f & f.x1 = x
by FUNCT_1:def 3;
consider y1 be object such that B4: y1 in dom f & f.y1 = y
by FUNCT_1:def 3,B2;
reconsider x1,y1 as Element of L by B3,B4;
per cases;
suppose x1 = y1;
hence thesis by B3,B4;
end;
suppose B1: x1 <> y1;
per cases by A76,RELAT_2:def 6,B1;
suppose [x1,y1] in R2;then
f.x1 c= f.y1 by A17;
hence x,y are_c=-comparable by XBOOLE_0:def 9,B3,B4;
end;
suppose [y1,x1] in R2;then
f.y1 c= f.x1 by A17;
hence x,y are_c=-comparable by XBOOLE_0:def 9,B3,B4;
end;
end;
end;
defpred S[Element of RS] means f.$1 is consistent;
A26: now
let x be Element of RS;
A20: f.x = h.(x, f|iRS-Seg x) by WELLFND1:def 5,A12;
f|iRS-Seg x in PFuncs(cRS, bool L) by PARTFUN1:45;
hence H[x,f|iRS-Seg x,f.x] by A20,A9;
end;
A27: now
let x be Element of RS;
reconsider x1 = {x} as Subset of L;
set fr = f|iRS-Seg x;
per cases;
suppose union(rng (fr qua bool L -valued Relation)) \/ F \/ x1
is consistent;then
f.x = union(rng fr) \/ F \/ x1 by A26
.= F \/ (union(rng fr) \/ x1) by XBOOLE_1:4;
hence F c= f.x by XBOOLE_1:7;
end;
suppose not union(rng (fr qua bool L -valued Relation)) \/ F \/ x1
is consistent;then
f.x = F \/ union(rng fr) by A26;
hence F c= f.x by XBOOLE_1:7;
end;
end;
A21: for x being Element of RS st
for y being Element of RS st y <> x & [y,x] in iRS holds S[y] holds S[x]
proof
let x be Element of RS;
assume A41: for y being Element of RS st y <> x & [y,x] in iRS
holds S[y];
set fr = f|iRS-Seg x;
iRS-Seg x c= field iRS by WELLORD1:9; then
C2: fr is Function of iRS-Seg x,bool L by FUNCT_2:32,F6; then
A39a: dom fr = iRS-Seg x by FUNCT_2:def 1;
reconsider x1 = {x} as Subset of L;
per cases;
suppose union(rng (fr qua bool L -valued Relation)) \/ F \/ x1
is consistent;
hence S[x] by A26;
end;
suppose C1:not union(rng (fr qua bool L -valued Relation)) \/ F \/ x1
is consistent;then
A22: f.x = union(rng fr) \/ F by A26;
per cases;
suppose S4: for y be object holds (not [y,x] in iRS or y = x);
iRS-Seg x = {}
proof
assume iRS-Seg x <> {};then
consider y be object such that
F19: y in iRS-Seg x by XBOOLE_0:7;
y <> x & [y,x] in iRS by WELLORD1:1,F19;
hence contradiction by S4;
end;then
dom fr = {} by FUNCT_2:def 1,C2;then
rng fr = {} by RELAT_1:42;
hence S[x] by Z0,ZFMISC_1:2,A26,C1;
end;
suppose A39: ex y be object st [y,x] in iRS & y <> x;
assume A30: not S[x];
consider y be object such that A29: [y,x] in iRS & y <> x by A39;
y in dom iRS by A29,XTUPLE_0:def 12;then
reconsider y as Element of RS;
fr.y in rng fr by FUNCT_1:3,A39a,WELLORD1:1,A29;then
A37: f.y in rng fr by WELLORD1:1,A29,A39a,FUNCT_1:47;
A37b: rng fr <> {} by WELLORD1:1,A29,A39a,FUNCT_1:3;
A37a: F c= f.y by A27;
F c= union rng fr by TARSKI:def 4,A37,A37a;then
A23: f.x = union(rng fr) by A22,XBOOLE_1:12;
consider F such that
A31: F is finite & not F is consistent & F c= f.x by A30,finin;
rng fr c= rng f by RELAT_1:70;then
consider z be set such that
A34: F c= z & z in rng fr by uniolinf,A23,A31,A54,A37b;
consider y be object such that
A36: y in dom fr & fr.y = z by A34,FUNCT_1:def 3;
A42: [y,x] in iRS by WELLORD1:1,A39a,A36;
A44: y <> x by WELLORD1:1,A39a,A36;
y in dom iRS by A42,XTUPLE_0:def 12;then
reconsider y as Element of RS;
f.y = fr.y by A36,FUNCT_1:47;
hence contradiction by A36,A34,A31,incsub,A44,A42,A41;
end;
end;
end;
A13a: for A be Element of RS holds S[A] from WELLFND1:sch 3(A21,A11);
take G;
thus F c= G
proof
let y be object;assume A46: y in F;
set z = the Element of RS;
A47: F c= f.z by A27;
f.z in rng f by FUNCT_1:3,A73;
hence y in G by A46,A47,TARSKI:def 4;
end;
thus G is consistent
proof
assume not G is consistent;then
consider F such that
A14: F is finite & not F is consistent & F c= G by finin;
consider z be set such that
A90: F c= z & z in rng f by uniolinf,A14,A54,RELAT_1:42,A73;
rng (f qua bool L -valued Relation) c= bool L;then
reconsider z as Subset of PL-WFF by A90;
consider x be object such that
A92: x in dom f & f.x = z by A90,FUNCT_1:def 3;
thus contradiction by A92,A13a,A90,A14,incsub;
end;
thus G is maximal
proof
given A such that A71: not A in G & not 'not' A in G;
reconsider ARS = A as Element of RS;
reconsider nA = 'not' A as Element of RS;
set fA = f|iRS-Seg A;
set fnA = f|iRS-Seg ('not' A);
reconsider A1 = {A} as Subset of L;
reconsider A1n = {'not' A} as Subset of L;
A74: not union rng (fA qua bool L -valued Relation) \/ F \/ A1
is consistent
proof
assume union rng (fA qua bool L -valued Relation) \/ F \/ A1
is consistent;then
A70: f.ARS = union rng fA \/ F \/ A1 by A26;
ARS in A1 by TARSKI:def 1;then
C1: ARS in union rng fA \/ F \/ A1 by XBOOLE_0:def 3;
f.ARS in rng f by FUNCT_1:3,A73;
hence contradiction by TARSKI:def 4,A71,A70,C1;
end;
A78: not union rng (fnA qua bool L -valued Relation) \/ F \/ A1n
is consistent
proof
assume union rng (fnA qua bool L -valued Relation) \/ F \/ A1n
is consistent;then
A70a: f.nA = union rng fnA \/ F \/ A1n by A26;
nA in A1n by TARSKI:def 1;then
A72a: nA in f.nA by A70a,XBOOLE_0:def 3;
f.nA in rng f by FUNCT_1:3,A73;
hence contradiction by TARSKI:def 4,A71,A72a;
end;then
A80: f.nA = union rng fnA \/ F by A26;
A79: f.A = union rng fA \/ F by A26,A74;
reconsider AAA = A as Element of HP-WFF by plhp;
reconsider fal=FaLSUM as Element of HP-WFF by plhp;
AAA=>fal = A => FaLSUM;then
len A <> len ('not' A) by HILBERT2:16;then
per cases by A76,RELAT_2:def 6;
suppose [A,'not' A] in R2;then
f.A c= f.nA by A17;then
not f.nA \/ A1 is consistent by A74,incsub,A79,XBOOLE_1:9;
hence contradiction by A13a,onecon,A78,A80;
end;
suppose ['not' A,A] in R2;then
f.nA c= f.A by A17;then
not f.ARS \/ A1n is consistent by A78,incsub,A80,XBOOLE_1:9;
hence contradiction by onecon,A74,A79,A13a;
end;
end;
end;
theorem inder:
F is maximal & F is consistent implies for p holds F |- p iff p in F
proof
assume A1: F is maximal & F is consistent;
let p;
hereby
assume A2: F |- p;
assume not p in F;then
'not' p in F by A1;then
F |- 'not' p by th42;
hence contradiction by A2,A1;
end;
assume p in F;
hence F |- p by th42;
end;
::#INSERT: Completeness theorem
theorem ct:
F |= A implies F |- A
proof
assume
A0: F |= A & not F |- A;then
consider G such that
A1: F \/ {'not' A} c= G and
A1a: G is consistent and
A1b: G is maximal by th37,th34;
set M = {Prop n where n is Element of NAT: Prop n in G};
M c= props
proof
let a be object;
assume a in M;then
consider k such that
A7: Prop k = a & Prop k in G;
thus a in props by A7,defprops;
end;then
reconsider M as PLModel;
defpred P[Element of PL-WFF] means ($1 in G iff M |= $1);
H0: P[FaLSUM]
proof
hereby assume FaLSUM in G;then
G |- FaLSUM & G |- 'not' FaLSUM by thaa,th42;
hence M |= FaLSUM by A1a;
end;
assume M |= FaLSUM;
hence thesis by Def11;
end;
H1: for n holds P[Prop n]
proof
let n;
hereby assume Prop n in G;then
Prop n in M;
hence M |= Prop n by Def11;
end;
assume M |= Prop n;then
Prop n in M by Def11;then
consider k such that
A6: Prop n = Prop k & Prop k in G;
thus Prop n in G by A6;
end;
H2: for r,s st P[r] & P[s] holds P[r => s]
proof
let r,s;
assume
A10: P[r] & P[s];
per cases;
suppose
S1: r => s in G;
hereby assume
A11: r=>s in G;
per cases;
suppose r in G;then
A12: G |- r by th42;
G |- r=>s by A11,th42;then
G |- s by A12,th43;then
M |= s by A10,inder,A1a,A1b;then
(SAT M).r => (SAT M).s = 1;
hence M |= r=>s by Def11;
end;
suppose not r in G;then
not M |= r by A10;then
(SAT M).r = 0 by XBOOLEAN:def 3;then
(SAT M).r => (SAT M).s = 1;
hence M |= r=>s by Def11;
end;
end;
assume M |= r=>s;
thus r=>s in G by S1;
end;
suppose
S2: not r => s in G;
thus r=>s in G implies M |= r=>s by S2;
assume
A14: M |= r=>s;
'not' (r=>s) in G by S2,A1b;then
A16: G |- 'not' (r=>s) by th42;
now
assume s in G;then
A17: G |- s by th42;
s=> (r=>s) in PL_axioms by withplax;then
G |- s=> (r=>s) by th42;then
G |- (r=>s) by th43,A17;
hence contradiction by A16,A1a;
end;then
A13: not M |= s by A10;
now
assume 'not' r in G;then
A15: G |- 'not' r by th42;
G |- 'not' r => (r =>s) by naab;then
G |- r=>s by th43,A15;
hence contradiction by A16,A1a;
end;then
M |= r by A10,A1b;then
not (SAT M).r => (SAT M).s = 1 by A13;
hence r=>s in G by A14,Def11;
end;
end;
A2: for B holds P[B] from PLInd(H0,H1,H2);
A4: F c= G by XBOOLE_1:11,A1;
A3: M |= F by A4,A2;
{'not' A} c= G by A1,XBOOLE_1:11;then
M |= 'not' A by A2,ZFMISC_1:31;then
not M |= A by semnot;
hence contradiction by A0,A3;
end;
theorem
A is tautology iff {}PL-WFF |- A by tautsat,sth,ct;
*