let Z be set ; :: thesis: for S being countable Language
for phi being wff string of S st Z c= AllFormulasOf S & xnot phi is Z -implied holds
xnot phi is Z,S -rules -provable
let S be countable Language; :: thesis: for phi being wff string of S st Z c= AllFormulasOf S & xnot phi is Z -implied holds
xnot phi is Z,S -rules -provable
set D = S -rules ;
set FF = AllFormulasOf S;
let phi be wff string of S; :: thesis: ( Z c= AllFormulasOf S & xnot phi is Z -implied implies xnot phi is Z,S -rules -provable )
assume Z c= AllFormulasOf S ; :: thesis: ( not xnot phi is Z -implied or xnot phi is Z,S -rules -provable )
then reconsider X = Z as Subset of (AllFormulasOf S) ;
set psi = xnot phi;
reconsider Phi = {phi} as non empty Subset of (AllFormulasOf S) by FOMODEL2:16, ZFMISC_1:31;
reconsider Y = X \/ Phi as non empty Subset of (AllFormulasOf S) ;
reconsider XX = X null Phi as Subset of Y ;
reconsider Phii = Phi null X as non empty Subset of Y ;
assume A1: xnot phi is Z -implied ; :: thesis: xnot phi is Z,S -rules -provable
assume not xnot phi is Z,S -rules -provable ; :: thesis: contradiction
then ( S -rules is isotone & R#1 S in S -rules & R#8 S in S -rules & not xnot phi is Z,S -rules -provable ) by Def62;
then consider U being non empty countable set , I being Element of U -InterpretersOf S such that
A2: Y is I -satisfied by Th19, Lm47;
(I -TruthEval (xnot phi)) \+\ ('not' (I -TruthEval phi)) = {} ;
then A3: I -TruthEval (xnot phi) = 'not' (I -TruthEval phi) by FOMODEL0:29;
A4: Y /\ XX is I -satisfied by A2;
phi in Phii by TARSKI:def 1;
then 1 = 'not' (I -TruthEval (xnot phi)) by A3, A2;
hence contradiction by A4, A1; :: thesis: verum