let A be Element of PL-WFF ; for F being Subset of PL-WFF st F |= A holds
F |- A
let F be Subset of PL-WFF; ( F |= A implies F |- A )
assume A0:
( F |= A & not F |- A )
; 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
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 ]
H1:
for n being Element of NAT holds S1[ Prop n]
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 ;
( S1[r] & S1[s] implies S1[r => s] )
assume A10:
(
S1[
r] &
S1[
s] )
;
S1[r => s]
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; verum