let CX be Consistent Subset of CQC-WFF; :: thesis: ( CX is with_examples implies ex CY being Consistent Subset of CQC-WFF st
( CX c= CY & CY is negation_faithful & CY is with_examples ) )
assume A1: CX is with_examples ; :: thesis: ex CY being Consistent Subset of CQC-WFF st
( CX c= CY & CY is negation_faithful & CY is with_examples )
consider f being Function such that
A2: dom f = NAT and
A3: CQC-WFF = rng f by Lm1, Th18;
reconsider f = f as Function of NAT,CQC-WFF by A2, A3, FUNCT_2:2;
defpred S1[ set , set , set ] means ex X being Subset of CQC-WFF st
( X = $2 \/ {(f . $1)} & ( X is Consistent implies $3 = X ) & ( not X is Consistent implies $3 = $2 ) );
A4: for n being Element of NAT
for C being Subset of CQC-WFF ex D being Subset of CQC-WFF st S1[n,C,D]
proof
let n be Element of NAT ; :: thesis: for C being Subset of CQC-WFF ex D being Subset of CQC-WFF st S1[n,C,D]
reconsider p = f . n as Element of CQC-WFF ;
let C be Subset of CQC-WFF; :: thesis: ex D being Subset of CQC-WFF st S1[n,C,D]
set X = C \/ {p};
reconsider X = C \/ {p} as Subset of CQC-WFF ;
( not X is Consistent implies ex D being Subset of CQC-WFF st
( D = C & ex X being Subset of CQC-WFF st
( X = C \/ {p} & ( X is Consistent implies D = X ) & ( not X is Consistent implies D = C ) ) ) ) ;
hence ex D being Subset of CQC-WFF st S1[n,C,D] ; :: thesis: verum
end;
consider h being Function of NAT,(bool CQC-WFF) such that
A5: ( h . 0 = CX & ( for n being Element of NAT holds S1[n,h . n,h . (n + 1)] ) ) from RECDEF_1:sch 2(A4);
 set CY = union (rng h);
A6: now
let a be set ; :: thesis: ( a in CX implies a in union (rng h) )
assume A7: a in CX ; :: thesis: a in union (rng h)
dom h = NAT by FUNCT_2:def 1;
then h . 0 in rng h by FUNCT_1:3;
hence a in union (rng h) by A5, A7, TARSKI:def 4; :: thesis: verum
end;
then A8: CX c= union (rng h) by TARSKI:def 3;
A9: for n being Element of NAT holds h . n c= h . (n + 1)
proof
let n be Element of NAT ; :: thesis: h . n c= h . (n + 1)
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in h . n or a in h . (n + 1) )
assume A10: a in h . n ; :: thesis: a in h . (n + 1)
reconsider p = f . n as Element of CQC-WFF ;
set X = (h . n) \/ {p};
reconsider X = (h . n) \/ {p} as Subset of CQC-WFF ;
A11: h . n c= X by XBOOLE_1:7;
ex Y being Subset of CQC-WFF st
( Y = (h . n) \/ {(f . n)} & ( Y is Consistent implies h . (n + 1) = Y ) & ( not Y is Consistent implies h . (n + 1) = h . n ) ) by A5;
hence a in h . (n + 1) by A10, A11; :: thesis: verum
end;
A12: for n, m being Element of NAT st m in dom h & n in dom h & n < m holds
h . n c= h . m
proof
let n, m be Element of NAT ; :: thesis: ( m in dom h & n in dom h & n < m implies h . n c= h . m )
assume that
m in dom h and
n in dom h and
A13: n < m ; :: thesis: h . n c= h . m
defpred S2[ Element of NAT ] means ( n <= $1 implies h . n c= h . $1 );
A14: S2[ 0 ]
proof
assume n <= 0 ; :: thesis: h . n c= h . 0
then n = 0 by NAT_1:2;
hence h . n c= h . 0 ; :: thesis: verum
end;
A15: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S2[k] implies S2[k + 1] )
assume A16: S2[k] ; :: thesis: S2[k + 1]
assume A17: n <= k + 1 ; :: thesis: h . n c= h . (k + 1)
now
assume A18: n <= k ; :: thesis: h . n c= h . (k + 1)
h . k c= h . (k + 1) by A9;
hence h . n c= h . (k + 1) by A16, A18, XBOOLE_1:1; :: thesis: verum
end;
hence h . n c= h . (k + 1) by A17, NAT_1:8; :: thesis: verum
end;
for k being Element of NAT holds S2[k] from NAT_1:sch 1(A14, A15);
 hence h . n c= h . m by A13; :: thesis: verum
end;
defpred S2[ Element of NAT ] means h . $1 is Consistent ;
A19: S2[ 0 ] by A5;
A20: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let n be Element of NAT ; :: thesis: ( S2[n] implies S2[n + 1] )
assume A21: S2[n] ; :: thesis: S2[n + 1]
ex Y being Subset of CQC-WFF st
( Y = (h . n) \/ {(f . n)} & ( Y is Consistent implies h . (n + 1) = Y ) & ( not Y is Consistent implies h . (n + 1) = h . n ) ) by A5;
hence S2[n + 1] by A21; :: thesis: verum
end;
set CY = union (rng h);
for n being Element of NAT holds S2[n] from NAT_1:sch 1(A19, A20);
 then for n, m being Element of NAT st m in dom h & n in dom h & n < m holds
( h . n is Consistent & h . n c= h . m ) by A12;
then reconsider CY = union (rng h) as Consistent Subset of CQC-WFF by HENMODEL:11;
A22: CY is negation_faithful
proof
let p be Element of CQC-WFF ; :: according to GOEDELCP:def 1 :: thesis: ( CY |- p or CY |- 'not' p )
consider a being set such that
A23: a in dom f and
A24: f . a = p by A3, FUNCT_1:def 3;
reconsider n = a as Element of NAT by A23;
now
assume not CY |- 'not' p ; :: thesis: CY |- p
then A25: CY \/ {p} is Consistent by HENMODEL:10;
A26: now
assume not (h . n) \/ {p} is Consistent ; :: thesis: contradiction
then A27: (h . n) \/ {p} |- 'not' VERUM by Th24;
now
let a be set ; :: thesis: ( a in h . n implies a in CY )
assume A28: a in h . n ; :: thesis: a in CY
dom h = NAT by FUNCT_2:def 1;
then h . n in rng h by FUNCT_1:3;
hence a in CY by A28, TARSKI:def 4; :: thesis: verum
end;
then h . n c= CY by TARSKI:def 3;
then CY \/ {p} |- 'not' VERUM by A27, Th32, XBOOLE_1:9;
hence contradiction by A25, Th24; :: thesis: verum
end;
A29: ex Y being Subset of CQC-WFF st
( Y = (h . n) \/ {(f . n)} & ( Y is Consistent implies h . (n + 1) = Y ) & ( not Y is Consistent implies h . (n + 1) = h . n ) ) by A5;
now
let a be set ; :: thesis: ( a in h . (n + 1) implies a in CY )
assume A30: a in h . (n + 1) ; :: thesis: a in CY
dom h = NAT by FUNCT_2:def 1;
then h . (n + 1) in rng h by FUNCT_1:3;
hence a in CY by A30, TARSKI:def 4; :: thesis: verum
end;
then A31: h . (n + 1) c= CY by TARSKI:def 3;
{p} c= h . (n + 1) by A24, A26, A29, XBOOLE_1:7;
then {p} c= CY by A31, XBOOLE_1:1;
then p in CY by ZFMISC_1:31;
hence CY |- p by Th21; :: thesis: verum
end;
hence ( CY |- p or CY |- 'not' p ) ; :: thesis: verum
end;
A32: CY is with_examples
proof
let x be bound_QC-variable; :: according to GOEDELCP:def 2 :: thesis: for p being Element of CQC-WFF ex y being bound_QC-variable st CY |- ('not' (Ex (x,p))) 'or' (p . (x,y))
let p be Element of CQC-WFF ; :: thesis: ex y being bound_QC-variable st CY |- ('not' (Ex (x,p))) 'or' (p . (x,y))
consider y being bound_QC-variable such that
A33: CX |- ('not' (Ex (x,p))) 'or' (p . (x,y)) by A1, Def2;
take y ; :: thesis: CY |- ('not' (Ex (x,p))) 'or' (p . (x,y))
thus CY |- ('not' (Ex (x,p))) 'or' (p . (x,y)) by A8, A33, Th32; :: thesis: verum
end;
take CY ; :: thesis: ( CX c= CY & CY is negation_faithful & CY is with_examples )
thus ( CX c= CY & CY is negation_faithful & CY is with_examples ) by A6, A22, A32, TARSKI:def 3; :: thesis: verum