let A be Element of PL-WFF ; :: thesis: for F being Subset of PL-WFF st F |= A holds
F |- A
let F be Subset of PL-WFF; :: thesis: ( F |= A implies F |- A )
assume A0: ( F |= A & not F |- A ) ; :: thesis: contradiction
then consider G being Subset of PL-WFF 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 } ;
{ (Prop n) where n is Element of NAT : Prop n in G } c= props
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (Prop n) where n is Element of NAT : Prop n in G } or a in props )
assume a in { (Prop n) where n is Element of NAT : Prop n in G } ; :: thesis: a in props
then consider k being Element of NAT such that
A7: ( Prop k = a & Prop k in G ) ;
thus a in props by A7, defprops; :: thesis: verum
end;
then reconsider M = { (Prop n) where n is Element of NAT : Prop n in G } as PLModel ;
defpred S1[ Element of PL-WFF ] means ( $1 in G iff M |= $1 );
H0: S1[ FaLSUM ]
proof
hereby :: thesis: ( M |= FaLSUM implies FaLSUM in G )
assume FaLSUM in G ; :: thesis: M |= FaLSUM
then ( G |- FaLSUM & G |- 'not' FaLSUM ) by thaa, th42;
hence M |= FaLSUM by A1a; :: thesis: verum
end;
assume M |= FaLSUM ; :: thesis: FaLSUM in G
hence FaLSUM in G by Def11; :: thesis: verum
end;
H1: for n being Element of NAT holds S1[ Prop n]
proof
let n be Element of NAT ; :: thesis: S1[ Prop n]
hereby :: thesis: ( M |= Prop n implies Prop n in G )
assume Prop n in G ; :: thesis: M |= Prop n
then Prop n in M ;
hence M |= Prop n by Def11; :: thesis: verum
end;
assume M |= Prop n ; :: thesis: Prop n in G
then Prop n in M by Def11;
then consider k being Element of NAT such that
A6: ( Prop n = Prop k & Prop k in G ) ;
thus Prop n in G by A6; :: thesis: verum
end;
H2: for r, s being Element of PL-WFF st S1[r] & S1[s] holds
S1[r => s]
proof
let r, s be Element of PL-WFF ; :: thesis: ( S1[r] & S1[s] implies S1[r => s] )
assume A10: ( S1[r] & S1[s] ) ; :: thesis: S1[r => s]
per cases ( r => s in G or not r => s in G ) ;
suppose S1: r => s in G ; :: thesis: S1[r => s]
hereby :: thesis: ( M |= r => s implies r => s in G )
assume A11: r => s in G ; :: thesis: M |= r => s
per cases ( r in G or not r in G ) ;
suppose r in G ; :: thesis: M |= r => s
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; :: thesis: verum
end;
suppose not r in G ; :: thesis: M |= r => s
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; :: thesis: verum
end;
end;
end;
assume M |= r => s ; :: thesis: r => s in G
thus r => s in G by S1; :: thesis: verum
end;
suppose S2: not r => s in G ; :: thesis: S1[r => s]
thus ( r => s in G implies M |= r => s ) by S2; :: thesis: ( M |= r => s implies r => s in G )
assume A14: M |= r => s ; :: thesis: r => s in G
'not' (r => s) in G by S2, A1b;
then A16: G |- 'not' (r => s) by th42;
now :: thesis: not s in G
assume s in G ; :: thesis: contradiction
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; :: thesis: verum
end;
then A13: not M |= s by A10;
now :: thesis: not 'not' r in G
assume 'not' r in G ; :: thesis: contradiction
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; :: thesis: verum
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; :: thesis: verum
end;
end;
end;
A2: for B being Element of PL-WFF holds S1[B] from PL_AXIOM:sch 1(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; :: thesis: verum