:: Transition of Consistency and Satisfiability under Language Extensions
:: by Julian J. Schl\"oder and Peter Koepke
::
:: Received May 7, 2012
:: Copyright (c) 2012-2026 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 NUMBERS, SUBSET_1, QC_LANG1, CQC_LANG, XBOOLE_0, VALUAT_1,
FINSEQ_1, HENMODEL, CQC_THE1, XBOOLEAN, BVFUNC_2, FUNCT_1, ORDINAL4,
CALCUL_1, ARYTM_3, RELAT_1, CARD_1, XXREAL_0, TARSKI, ZF_MODEL, REALSET1,
SUBSTUT1, SUBSTUT2, ZF_LANG, ARYTM_1, CARD_3, ZFMISC_1, FINSET_1,
MCART_1, NAT_1, MARGREL1, FUNCT_2, FUNCOP_1, QC_TRANS, FUNCT_4, CLASSES2,
SUBLEMMA;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XXREAL_0, NAT_1,
ORDINAL1, CARD_3, FINSEQ_1, FUNCT_1, QC_LANG1, QC_LANG2, QC_LANG3,
NUMBERS, CQC_LANG, RELAT_1, FINSET_1, VALUAT_1, RELSET_1, FUNCT_2,
CQC_SIM1, DOMAIN_1, XTUPLE_0, MCART_1, SUBSTUT1, SUBLEMMA, SUBSTUT2,
CALCUL_1, CQC_THE1, GOEDELCP, MARGREL1, FUNCT_4, FUNCOP_1, HENMODEL;
constructors SETFAM_1, DOMAIN_1, XXREAL_0, NAT_1, NAT_D, FINSEQ_2, QC_LANG1,
CQC_THE1, CQC_SIM1, SUBLEMMA, SUBSTUT2, CALCUL_1, HENMODEL, CARD_3,
RELSET_1, CARD_1, WELLORD2, GOEDELCP, VALUAT_1, MARGREL1, CQC_LANG,
QC_LANG3, FUNCT_4, FUNCOP_1, SUBSTUT1, PARTFUN1;
registrations SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, HENMODEL,
FINSEQ_1, FINSET_1, CARD_3, XBOOLE_0, QC_LANG1, CQC_LANG, MARGREL1,
CARD_1, GOEDELCP, FUNCOP_1, SUBLEMMA, SUBSTUT1, XTUPLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities QC_LANG1;
expansions TARSKI, QC_LANG1;
theorems TARSKI, FUNCT_1, MCART_1, XBOOLE_0, XBOOLE_1, CQC_LANG, QC_LANG1,
ZFMISC_1, RELAT_1, QC_LANG3, QC_LANG2, HENMODEL, CALCUL_1, SUBLEMMA,
NAT_1, FINSEQ_1, VALUAT_1, FUNCT_2, SUBSTUT2, CQC_SIM1, CARD_2, ORDINAL1,
CARD_1, GOEDELCP, FUNCOP_1, FINSEQ_2, FINSET_1, SUBSTUT1, FUNCT_4,
CARD_4, XTUPLE_0, XXREAL_0;
schemes CQC_LANG, FINSET_1, FRAENKEL;
begin :: Language Extensions
reserve Al for QC-alphabet;
reserve PHI for Consistent Subset of CQC-WFF(Al),
p,q,r,s for Element of CQC-WFF(Al),
A for non empty set,
J for interpretation of Al,A,
v for Element of Valuations_in(Al,A),
m,n,i,j,k for Nat,
l for CQC-variable_list of k,Al,
P for QC-pred_symbol of k,Al,
x,y,z for bound_QC-variable of Al,
b for QC-symbol of Al,
PR for FinSequence of [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:];
definition
let Al;
let Al2 be QC-alphabet;
attr Al2 is Al-expanding means
:Def1:
Al c= Al2;
end;
registration
let Al;
cluster Al-expanding for QC-alphabet;
existence by Def1;
end;
registration
let Al1,Al2 be countable QC-alphabet;
cluster countable Al1-expanding Al2-expanding for QC-alphabet;
existence
proof
set Al3 = Al1 \/ Al2;
Al1 = [:NAT,QC-symbols(Al1):] & Al2 =[:NAT,QC-symbols(Al2):] by QC_LANG1:5;
then
A1: Al3 = [:NAT, QC-symbols(Al1) \/ QC-symbols(Al2):] by ZFMISC_1:97;
NAT c= QC-symbols(Al1) \/ QC-symbols(Al2) by XBOOLE_1:10,QC_LANG1:3;
then reconsider Al3 as QC-alphabet by A1,QC_LANG1:def 1;
take Al3;
thus thesis by CARD_2:85,XBOOLE_1:7;
end;
end;
definition
let Al,Al2 be QC-alphabet;
let P be Subset of CQC-WFF(Al);
attr P is Al2-Consistent means
for S being Subset of CQC-WFF(Al2) st P=S holds S is Consistent;
end;
registration
let Al;
cluster non empty Consistent for Subset of CQC-WFF(Al);
existence
proof
{VERUM(Al)} is Consistent by HENMODEL:13;
hence thesis;
end;
end;
registration
let Al;
cluster Consistent -> Al-Consistent for Subset of CQC-WFF(Al);
coherence;
cluster Al-Consistent -> Consistent for Subset of CQC-WFF(Al);
coherence;
end;
reserve Al2 for Al-expanding QC-alphabet,
J2 for interpretation of Al2,A,
Jp for interpretation of Al,A,
v2 for Element of Valuations_in(Al2,A),
vp for Element of Valuations_in(Al,A);
theorem Th1:
the_arity_of P = len l
proof
thus len l = k by CARD_1:def 7 .= the_arity_of P by QC_LANG1:11;
end;
theorem Th2:
QC-symbols(Al) c= QC-symbols(Al2)
proof
Al c= Al2 & Al = [: NAT, QC-symbols(Al) :] &
Al2 = [:NAT,QC-symbols(Al2) :] by Def1, QC_LANG1:5;
hence QC-symbols(Al) c= QC-symbols(Al2) by ZFMISC_1:115;
end;
theorem Th3:
QC-pred_symbols(Al) c= QC-pred_symbols(Al2)
proof
for Q being object st Q in QC-pred_symbols(Al)
holds Q in QC-pred_symbols(Al2)
proof
let Q be object such that
A1: Q in QC-pred_symbols(Al);
set preds = { [k,b] : 7 <= k };
set preds2 = { [k,b2] where b2 is QC-symbol of Al2 : 7 <= k };
consider k,b such that
A2: Q=[k,b] & 7 <= k by A1;
b in QC-symbols(Al2) by Th2,TARSKI:def 3;
hence Q in QC-pred_symbols(Al2) by A2;
end;
hence thesis;
end;
theorem Th4:
bound_QC-variables(Al) c= bound_QC-variables(Al2)
proof
A1: QC-symbols(Al) c= QC-symbols(Al2) by Th2;
thus thesis by A1, ZFMISC_1:96;
end;
theorem Th5:
for k,l holds l is CQC-variable_list of k,Al2
proof
let k,l;
rng l c= bound_QC-variables(Al) &
bound_QC-variables(Al) c= bound_QC-variables(Al2) by Th4;
then rng l c= bound_QC-variables(Al2);
hence thesis by FINSEQ_1:def 4, XBOOLE_1:1;
end;
theorem Th6:
P is QC-pred_symbol of k,Al2
proof
the_arity_of P = k by QC_LANG1:11;
then
A1: P`1 = 7+k by QC_LANG1:def 8;
reconsider P as QC-pred_symbol of Al2 by Th3,TARSKI:def 3;
the_arity_of P = k by QC_LANG1:def 8, A1;
hence thesis by QC_LANG3:1;
end;
theorem Th7:
for Al2 being Al-expanding QC-alphabet
for p holds p is Element of CQC-WFF(Al2)
proof
let Al2 be Al-expanding QC-alphabet;
defpred P[Element of CQC-WFF(Al)] means $1 is Element of CQC-WFF(Al2);
A1: P[VERUM(Al)]
proof
VERUM(Al) = VERUM(Al2);
hence thesis;
end;
A2: for k,P,l holds P[P!l]
proof
let k,P,l;
A3: the_arity_of P = len l by Th1;
P is QC-pred_symbol of k,Al2 & l is CQC-variable_list of k,Al2 by Th5,Th6;
then consider P2 being QC-pred_symbol of k,Al2,
l2 being CQC-variable_list of k,Al2 such that
A4: P=P2 & l=l2;
the_arity_of P2 = len l2 by Th1;
then P2!l2 = <*P2*>^l2 by QC_LANG1:def 12;
hence thesis by A3,A4,QC_LANG1:def 12;
end;
A5: P[p] implies P['not' p]
proof
assume P[p];
then consider q being Element of CQC-WFF(Al2) such that
A6: p = q;
'not' p = 'not' q by A6;
hence thesis;
end;
A7: P[p] & P[q] implies P[p '&' q]
proof
assume P[p] & P[q];
then consider t,u being Element of CQC-WFF(Al2) such that
A8: p = t & q = u;
p '&' q = t '&' u by A8;
hence thesis;
end;
A9: for x holds P[p] implies P[All(x,p)]
proof
let x;
assume P[p];
then consider q being Element of CQC-WFF(Al2) such that
A10: p = q;
x is bound_QC-variable of Al2 by Th4,TARSKI:def 3;
then consider y being bound_QC-variable of Al2 such that
A11: x = y;
All(x,p) = All(y,q) by A10,A11;
hence thesis;
end;
A12: for r,s being Element of CQC-WFF(Al)
for x being bound_QC-variable of Al for k
for l being CQC-variable_list of k, Al for P being
QC-pred_symbol of k,Al holds P[VERUM(Al)] & P[P!l] &
(P[r] implies P['not' r]) & (P[r] & P[s] implies P[r '&' s]) &
(P[r] implies P[All(x, r)]) by A1,A2,A5,A7,A9;
for p holds P[p] from CQC_LANG:sch 1(A12);
hence for p holds p is Element of CQC-WFF(Al2);
end;
definition
let Al;
let Al2 be Al-expanding QC-alphabet;
let p be Element of CQC-WFF(Al);
func Al2-Cast(p) -> Element of CQC-WFF(Al2) equals p;
coherence by Th7;
end;
definition
let Al;
let Al2 be Al-expanding QC-alphabet;
let x be bound_QC-variable of Al;
func Al2-Cast(x) -> bound_QC-variable of Al2 equals x;
coherence by Th4,TARSKI:def 3;
end;
definition
let Al;
let Al2 be Al-expanding QC-alphabet;
let k;
let P be QC-pred_symbol of k,Al;
func Al2-Cast(P) -> QC-pred_symbol of k,Al2 equals P;
coherence by Th6;
end;
definition
let Al;
let Al2 be Al-expanding QC-alphabet;
let k;
let l be CQC-variable_list of k,Al;
func Al2-Cast(l) -> CQC-variable_list of k,Al2 equals l;
coherence by Th5;
end;
theorem Th8:
for p,r,x,P,l for Al2 being Al-expanding QC-alphabet
holds Al2-Cast(VERUM(Al)) = VERUM(Al2) &
Al2-Cast(P!l) = Al2-Cast(P)!Al2-Cast(l) &
Al2-Cast('not' p) = 'not' (Al2-Cast(p)) &
Al2-Cast(p '&' r) = (Al2-Cast(p)) '&' (Al2-Cast(r)) &
Al2-Cast(All(x,p)) = All(Al2-Cast(x),Al2-Cast(p))
proof
let p,r,x,P,l;
let Al2 be Al-expanding QC-alphabet;
A1: the_arity_of P = len l by Th1;
A2: the_arity_of Al2-Cast(P) = len (Al2-Cast(l)) by Th1;
thus Al2-Cast(VERUM(Al)) = VERUM(Al2);
thus Al2-Cast(P!l) = <*P*>^l by A1,QC_LANG1:def 12
.= Al2-Cast(P)!Al2-Cast(l) by A2,QC_LANG1:def 12;
thus Al2-Cast('not' p) = 'not' (Al2-Cast(p));
thus Al2-Cast(p '&' r) = (Al2-Cast(p)) '&' (Al2-Cast(r));
thus Al2-Cast(All(x,p)) = All(Al2-Cast(x),Al2-Cast(p));
end;
begin :: Downward Transfer of Consistency and Satisfiability
theorem Th9:
Jp = J2|QC-pred_symbols(Al) & vp = v2|bound_QC-variables(Al)
implies (J2,v2 |= Al2-Cast(r) iff Jp,vp |= r)
proof
defpred T[Element of CQC-WFF(Al)] means
for J2,Jp,v2,vp holds
Jp = J2|QC-pred_symbols(Al) & vp = v2|bound_QC-variables(Al) implies
(( J2,v2 |= Al2-Cast($1) ) iff Jp,vp |= $1);
A1: T[VERUM(Al)]
proof
let J2, Jp, v2, vp;
J2,v2 |= VERUM(Al2) by VALUAT_1:32;
hence thesis by VALUAT_1:32;
end;
A2: for k,P,l holds T[P!l]
proof
let k,P,l;
let J2, Jp, v2, vp;
assume
A3: Jp = J2|QC-pred_symbols(Al) & vp = v2|bound_QC-variables(Al);
set p = P!l;
the_arity_of P = len l by Th1;
then
A4: P!l = <*P*>^l by QC_LANG1:def 12;
P is QC-pred_symbol of k,Al2 & l is CQC-variable_list of k,Al2
by Th5, Th6;
then consider P2 being QC-pred_symbol of k,Al2,
l2 being CQC-variable_list of k,Al2 such that
A5: P=P2 & l=l2;
A6: the_arity_of P2 = len l2 by Th1;
A7: v2*'l2 = vp*'l
proof
A8: bound_QC-variables(Al) c= bound_QC-variables(Al2) by Th4;
A9: for j st 1 <= j & j <= len l holds l.j in bound_QC-variables(Al) iff
l.j in bound_QC-variables(Al2)
proof
let j such that
A10: 1 <= j & j <= len l;
thus l.j in bound_QC-variables(Al) implies
l.j in bound_QC-variables(Al2) by A8;
hereby
assume l.j in bound_QC-variables(Al2);
len l = k by CARD_1:def 7;
then j in Seg k by A10, FINSEQ_1:1;
then j in dom l by FINSEQ_1:89;
hence l.j in bound_QC-variables(Al) by FUNCT_1:102;
end;
end;
set t1 ={l.i: 1 <= i & i <= len l & l.i in bound_QC-variables(Al)};
set t2 ={l.i: 1 <= i & i <= len l & l.i in bound_QC-variables(Al2)};
A11: t1=t2
proof
thus t1 c= t2
proof
let x be object;
assume x in t1;
then consider i such that
A12: x = l.i & 1 <= i & i <= len l & l.i in bound_QC-variables(Al);
x = l.i & 1 <= i & i <= len l & l.i in bound_QC-variables(Al2)
by A9,A12;
hence x in t2;
end;
thus t2 c= t1
proof
let x be object;
assume x in t2;
then consider i such that
A13: x = l.i & 1 <= i & i <= len l & l.i in bound_QC-variables(Al2);
x = l.i & 1 <= i & i <= len l & l.i in bound_QC-variables(Al)
by A9,A13;
hence x in t1;
end;
end;
A14: still_not-bound_in l = still_not-bound_in l2 by A5,A11;
A15: vp|still_not-bound_in l
= v2|(bound_QC-variables(Al) /\ still_not-bound_in l) by A3,RELAT_1:71
.= v2|still_not-bound_in l by XBOOLE_1:28;
v2*'l2 = l*(vp|still_not-bound_in l) by A5,A14,A15,SUBLEMMA:59
.= vp*'l by SUBLEMMA:59;
hence thesis;
end;
A16:J2,v2 |= Al2-Cast(P!l) implies Jp,vp |= P!l
proof
assume J2,v2 |= Al2-Cast(P!l);
then J2,v2 |= P2!l2 by A4,A5,A6,QC_LANG1:def 12;
then Valid(P2!l2,J2).v2 = TRUE by VALUAT_1:def 7;
then (l2 'in' (J2.P2)).v2 = TRUE by VALUAT_1:6;
then
A17: vp*'l in (J2.P2) by A7,VALUAT_1:def 4;
vp*'l in (Jp.P) by FUNCT_1:49,A3,A5,A17;
then (l 'in' (Jp.P)).vp = TRUE by VALUAT_1:def 4;
then Valid(P!l,Jp).vp = TRUE by VALUAT_1:6;
hence thesis by VALUAT_1:def 7;
end;
(not J2,v2 |= Al2-Cast(P!l)) implies (not Jp,vp |= P!l)
proof
assume not J2,v2 |= Al2-Cast(P!l);
then not J2,v2 |= P2!l2 by A4,A5,A6,QC_LANG1:def 12;
then not Valid(P2!l2,J2).v2 = TRUE by VALUAT_1:def 7;
then not (l2 'in' (J2.P2)).v2 = TRUE by VALUAT_1:6;
then
A18: not vp*'l in (J2.P2) by A7,VALUAT_1:def 4;
not vp*'l in (Jp.P) by FUNCT_1:49,A3,A5,A18;
then not (l 'in' (Jp.P)).vp = TRUE by VALUAT_1:def 4;
then not Valid(P!l,Jp).vp = TRUE by VALUAT_1:6;
hence thesis by VALUAT_1:def 7;
end;
hence thesis by A16;
end;
A19: for p holds T[p] implies T['not' p]
proof
let p;
assume
A20:T[p];
let J2, Jp, v2, vp;
assume
A21:Jp = J2|QC-pred_symbols(Al) & vp = v2|bound_QC-variables(Al);
per cases;
suppose
A22: not J2,v2 |= Al2-Cast(p);
then
A23: not Jp,vp |= p by A20,A21;
J2,v2 |= 'not' (Al2-Cast(p)) by A22, VALUAT_1:17;
hence thesis by A23,VALUAT_1:17;
end;
suppose
A24: J2,v2 |= Al2-Cast(p);
then
A25: Jp,vp |= p by A20,A21;
not J2,v2 |= 'not' (Al2-Cast(p)) by VALUAT_1:17, A24;
hence thesis by A25,VALUAT_1:17;
end;
end;
A26: for p,r holds (T[p] & T[r]) implies T[p '&' r]
proof
let p,r;
assume
A27:T[p] & T[r];
let J2, Jp, v2, vp;
assume
A28: Jp = J2|QC-pred_symbols(Al) & vp = v2|bound_QC-variables(Al);
A29:J2,v2 |= (Al2-Cast(p '&' r)) implies Jp,vp |= p '&' r
proof
assume J2,v2 |= Al2-Cast(p '&' r);
then J2,v2 |= (Al2-Cast(p)) '&' (Al2-Cast(r));
then J2,v2 |= Al2-Cast(p) & J2,v2 |= Al2-Cast(r) by VALUAT_1:18;
then Jp,vp |= p & Jp,vp |= r by A27, A28;
hence Jp,vp |= p '&' r by VALUAT_1:18;
end;
Jp,vp |= p '&' r implies J2,v2 |= (Al2-Cast(p '&' r))
proof
assume Jp,vp |= p '&' r;
then Jp,vp |= p & Jp,vp |= r by VALUAT_1:18;
then J2,v2 |= Al2-Cast(p) & J2,v2 |= Al2-Cast(r) by A27,A28;
then J2,v2 |= (Al2-Cast(p)) '&' (Al2-Cast(r)) by VALUAT_1:18;
hence J2,v2 |= Al2-Cast(p '&' r);
end;
hence thesis by A29;
end;
A30: for x,r holds T[r] implies T[All(x,r)]
proof
let x,r;
assume
A31:T[r];
let J2, Jp, v2, vp;
assume
A32: Jp = J2|QC-pred_symbols(Al) & vp = v2|bound_QC-variables(Al);
A33:J2,v2 |= Al2-Cast(All(x,r)) implies Jp,vp |= All(x,r)
proof
assume J2,v2 |= Al2-Cast(All(x,r));
then
A34: J2,v2 |= All(Al2-Cast(x),Al2-Cast(r));
for vp1 being Element of Valuations_in(Al,A) st
for y being bound_QC-variable of Al st x <> y holds vp1.y = vp.y
holds Jp,vp1 |= r
proof
let vp1 be Element of Valuations_in(Al,A) such that
A35: for y being bound_QC-variable of Al st x <> y holds vp1.y = vp.y;
set s = Al2-Cast(x) .--> vp1.x;
A36: s = {Al2-Cast(x)} --> vp1.x by FUNCOP_1:def 9;
set v21 = v2 +* s;
v2 is Element of Funcs(bound_QC-variables(Al2),A) by VALUAT_1:def 1;
then
A37: dom v2 = bound_QC-variables(Al2) & rng v2 c= A by FUNCT_2:92;
dom s = {Al2-Cast(x)} by A36;
then dom v21 = dom v2 \/ {Al2-Cast(x)} by FUNCT_4:def 1;
then
A38: dom v21 = bound_QC-variables(Al2) by A37,XBOOLE_1:12;
A39: rng v2 \/ {vp1.x} c= A by A37, XBOOLE_1:8;
rng s = {vp1.x} by A36, FUNCOP_1:8;
then rng v21 c= rng v2 \/ {vp1.x} by FUNCT_4:17;
then rng v21 c= A by A39;
then v21 is Element of Funcs(bound_QC-variables(Al2),A)
by A38, FUNCT_2:def 2;
then reconsider v21 as Element of Valuations_in(Al2,A)
by VALUAT_1:def 1;
for y being bound_QC-variable of Al2 st Al2-Cast(x) <> y
holds v21.y = v2.y by FUNCT_4:83;
then
A40: J2,v21 |= Al2-Cast(r) by A34,VALUAT_1:29;
vp1 is Element of Funcs(bound_QC-variables(Al),A) by VALUAT_1:def 1;
then
A41: dom vp1 = bound_QC-variables(Al) by FUNCT_2:92
.= (dom v21) /\ bound_QC-variables(Al) by A38, Th4, XBOOLE_1:28;
for c being object st c in dom vp1 holds vp1.c = v21.c
proof
let c be object such that
A42: c in dom vp1;
per cases;
suppose
A43: c = Al2-Cast(x);
then c in dom s by FUNCOP_1:74;
hence v21.c = s.c by FUNCT_4:13
.= vp1.c by A43,FUNCOP_1:72;
end;
suppose
A44: c <> Al2-Cast(x);
reconsider c as bound_QC-variable of Al by A41,A42,XBOOLE_0:def 4;
v21.c = v2.c by A44,FUNCT_4:83
.= (v2|bound_QC-variables(Al)).c by FUNCT_1:49
.= vp1.c by A32,A35,A44;
hence thesis;
end;
end;
then v21|bound_QC-variables(Al) = vp1 by FUNCT_1:46, A41;
hence Jp,vp1 |= r by A32,A31,A40;
end;
hence Jp,vp |= All(x,r) by VALUAT_1:29;
end;
Jp,vp |= All(x,r) implies J2,v2 |= Al2-Cast(All(x,r))
proof
assume
A45: Jp,vp |= All(x,r);
for v21 being Element of Valuations_in(Al2,A) st
for y being bound_QC-variable of Al2 st Al2-Cast(x) <> y holds
v21.y = v2.y holds J2,v21 |= Al2-Cast(r)
proof
let v21 be Element of Valuations_in(Al2,A) such that
A46: for y being bound_QC-variable of Al2 st Al2-Cast(x) <> y holds
v21.y = v2.y;
set s = x .--> v21.(Al2-Cast(x));
A47: s = {x} --> v21.(Al2-Cast(x)) by FUNCOP_1:def 9;
set vp1 = vp +* s;
vp is Element of Funcs(bound_QC-variables(Al),A) by VALUAT_1:def 1;
then
A48: dom vp = bound_QC-variables(Al) & rng vp c= A by FUNCT_2:92;
dom s = {x} by A47;
then dom vp1 = dom vp \/ {x} by FUNCT_4:def 1;
then
A49: dom vp1 = bound_QC-variables(Al) by A48,XBOOLE_1:12;
A50: rng vp \/ {v21.(Al2-Cast(x))} c= A by A48, XBOOLE_1:8;
rng s = {v21.(Al2-Cast(x))} by A47, FUNCOP_1:8;
then rng vp1 c= rng vp \/ {v21.(Al2-Cast(x))} by FUNCT_4:17;
then rng vp1 c= A by A50;
then vp1 is Element of Funcs(bound_QC-variables(Al),A)
by A49, FUNCT_2:def 2;
then reconsider vp1 as Element of Valuations_in(Al,A)
by VALUAT_1:def 1;
for y being bound_QC-variable of Al st x <> y
holds vp1.y = vp.y by FUNCT_4:83;
then
A51: Jp,vp1 |= r by A45,VALUAT_1:29;
v21 is Element of Funcs(bound_QC-variables(Al2),A) by VALUAT_1:def 1;
then
A52: dom v21 = bound_QC-variables(Al2) by FUNCT_2:92;
vp1 is Element of Funcs(bound_QC-variables(Al),A) by VALUAT_1:def 1;
then
A53: dom vp1 = bound_QC-variables(Al) by FUNCT_2:92
.= (dom v21) /\ bound_QC-variables(Al) by A52, Th4, XBOOLE_1:28;
for c being object st c in dom vp1 holds vp1.c = v21.c
proof
let c be object such that
A54: c in dom vp1;
per cases;
suppose
A55: c = x;
then c in dom s by FUNCOP_1:74;
then vp1.c = s.x by A55,FUNCT_4:13 .= v21.c by A55,FUNCOP_1:72;
hence vp1.c = v21.c;
end;
suppose
A56: c <> x;
A57: c in bound_QC-variables(Al) by A53,A54,XBOOLE_0:def 4;
vp1 is Element of Funcs(bound_QC-variables(Al),A)
by VALUAT_1:def 1;
then dom vp1 = bound_QC-variables(Al) by FUNCT_2:92;
then
A58: dom vp1 c= bound_QC-variables(Al2) by Th4;
vp1.c = vp.c by A56,FUNCT_4:83
.= v2.c by A32,A57,FUNCT_1:49
.= v21.c by A56,A46,A54,A58;
hence thesis;
end;
end;
then v21|bound_QC-variables(Al) = vp1 by FUNCT_1:46, A53;
hence J2,v21 |= Al2-Cast(r) by A32,A31,A51;
end;
then J2,v2 |= All(Al2-Cast(x),Al2-Cast(r)) by VALUAT_1:29;
hence J2,v2 |= Al2-Cast(All(x,r));
end;
hence thesis by A33;
end;
A59: for r,s being Element of CQC-WFF(Al)
for x being bound_QC-variable of Al for k
for l being CQC-variable_list of k, Al for P being
QC-pred_symbol of k,Al holds T[VERUM(Al)] & T[P!l] &
(T[r] implies T['not' r]) & (T[r] & T[s] implies T[r '&' s]) &
(T[r] implies T[All(x, r)]) by A1,A2,A19,A26,A30;
for r being Element of CQC-WFF(Al) holds T[r] from CQC_LANG:sch 1(A59);
hence thesis;
end;
theorem
for Al2 being Al-expanding QC-alphabet,
THETA being Subset of CQC-WFF(Al2) st PHI c= THETA holds
for A2 being non empty set, J2 being interpretation of Al2,A2,
v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA holds
ex A,J,v st J,v |= PHI
proof
let Al2 be Al-expanding QC-alphabet,
THETA be Subset of CQC-WFF(Al2) such that
A1: PHI c= THETA;
let A2 be non empty set, J2 be interpretation of Al2,A2,
v2 be Element of Valuations_in(Al2,A2) such that
A2: J2,v2 |= THETA;
set A = A2;
A3: QC-pred_symbols(Al) c= QC-pred_symbols(Al2) by Th3;
set Jp = J2|QC-pred_symbols(Al);
reconsider Jp as Function of QC-pred_symbols(Al),relations_on A
by A3,FUNCT_2:32;
for P being Element of QC-pred_symbols(Al),
r being Element of relations_on A st Jp.P = r holds
r = empty_rel(A) or the_arity_of P = the_arity_of r
proof
let P be Element of QC-pred_symbols(Al),
r be Element of relations_on A such that
A4: Jp.P = r;
P is Element of QC-pred_symbols(Al2) by Th3,TARSKI:def 3;
then consider Q being Element of QC-pred_symbols(Al2) such that
A5: P = Q;
A6: P`1 = 7+the_arity_of P & Q`1 = 7+the_arity_of Q by QC_LANG1:def 8;
Jp.P = J2.Q by A5,FUNCT_1:49;
hence thesis by A4,A5,A6,VALUAT_1:def 5;
end;
then reconsider Jp as interpretation of Al,A by VALUAT_1:def 5;
A7: bound_QC-variables(Al) c= bound_QC-variables(Al2) by Th4;
set vp = v2|bound_QC-variables(Al);
reconsider vp as Function of bound_QC-variables(Al),A
by A7, FUNCT_2:32;
A8: Funcs(bound_QC-variables(Al),A) = Valuations_in(Al,A) by VALUAT_1:def 1;
reconsider vp as Element of Valuations_in(Al,A) by A8,FUNCT_2:8;
for r being Element of CQC-WFF(Al) holds
r in PHI implies Jp,vp |= r
proof
let r be Element of CQC-WFF(Al) such that
A9: r in PHI;
J2,v2 |= Al2-Cast(r) by A1,A2,A9,CALCUL_1:def 11;
hence thesis by Th9;
end;
hence thesis by CALCUL_1:def 11;
end;
theorem Th11:
for f being FinSequence of CQC-WFF(Al2),g being FinSequence of CQC-WFF(Al)
st f=g holds Ant f = Ant g & Suc f = Suc g
proof
let f be FinSequence of CQC-WFF(Al2),g be FinSequence of CQC-WFF(Al) such that
A1: f = g;
per cases;
suppose
A2: len f > 0;
then consider k being Nat such that
A3: len f = k + 1 by NAT_1:6;
reconsider k as Element of NAT by ORDINAL1:def 12;
thus Ant f = g|(Seg k) by A1,A2,A3,CALCUL_1:def 1
.= Ant g by A1,A2,A3,CALCUL_1:def 1;
Suc f = g.(len g) by A1,A2,CALCUL_1:def 2
.= Suc g by A1,A2,CALCUL_1:def 2;
hence thesis;
end;
suppose
A4: not len f > 0;
thus Ant f = {} by A4,CALCUL_1:def 1
.= Ant g by A1,A4,CALCUL_1:def 1;
thus Suc f = VERUM(Al2) by A4, CALCUL_1:def 2
.= VERUM(Al)
.= Suc g by A1,A4, CALCUL_1:def 2;
end;
end;
theorem Th12:
for p holds still_not-bound_in p = still_not-bound_in (Al2-Cast(p))
proof
defpred A[Element of CQC-WFF(Al)] means still_not-bound_in $1 =
still_not-bound_in (Al2-Cast($1));
A1: A[VERUM(Al)]
proof
thus still_not-bound_in VERUM(Al) = {} by QC_LANG3:3
.= still_not-bound_in VERUM(Al2) by QC_LANG3:3
.= still_not-bound_in (Al2-Cast(VERUM(Al)));
end;
A2: for k,P,l holds A[P!l]
proof
let k,P,l;
A3: still_not-bound_in l = still_not-bound_in Al2-Cast(l)
proof
for x being object st x in still_not-bound_in l holds
x in still_not-bound_in Al2-Cast(l)
proof
let x be object such that
A4: x in still_not-bound_in l;
consider n such that
A5: x = l.n & 1 <= n & n <= len l & l.n in bound_QC-variables(Al) by A4;
set y = l.n;
reconsider y as bound_QC-variable of Al by A5;
y = Al2-Cast(y);
hence thesis by A5;
end;
hence still_not-bound_in l c= still_not-bound_in Al2-Cast(l);
for x being object st x in still_not-bound_in Al2-Cast(l) holds
x in still_not-bound_in l
proof
let x be object such that
A6: x in still_not-bound_in Al2-Cast(l);
consider n such that
A7: x = Al2-Cast(l).n & 1 <= n & n <= len (Al2-Cast(l)) &
Al2-Cast(l).n in bound_QC-variables(Al2) by A6;
set y = Al2-Cast(l).n;
rng l c= bound_QC-variables(Al) & dom l = Seg (len l) by FINSEQ_1:def 3;
then y = l.n & n in dom l & l is FinSequence of bound_QC-variables(Al)
by A7,FINSEQ_1:1,def 4;
then y in bound_QC-variables(Al) by FINSEQ_2:11;
hence thesis by A7;
end;
hence still_not-bound_in Al2-Cast(l) c= still_not-bound_in l;
end;
thus still_not-bound_in (P!l) = still_not-bound_in l by QC_LANG3:5
.= still_not-bound_in (Al2-Cast(P)!Al2-Cast(l)) by A3,QC_LANG3:5
.= still_not-bound_in Al2-Cast(P!l) by Th8;
end;
A8: for p holds A[p] implies A['not' p]
proof
let p such that
A9: A[p];
thus still_not-bound_in 'not' p
= still_not-bound_in p by QC_LANG3:7
.= still_not-bound_in 'not' Al2-Cast(p) by A9,QC_LANG3:7
.= still_not-bound_in Al2-Cast('not' p);
end;
A10: for p,q holds A[p] & A[q] implies A[p '&' q]
proof
let p,q such that
A11: A[p] & A[q];
set p2 = Al2-Cast(p);
set q2 = Al2-Cast(q);
reconsider p2,q2 as Element of CQC-WFF(Al2);
p '&' q is conjunctive & p2 '&' q2 is conjunctive;
then
A12: p = the_left_argument_of p '&' q & q = the_right_argument_of p '&' q &
p2 = the_left_argument_of p2 '&' q2 &
q2 = the_right_argument_of p2 '&' q2 by QC_LANG1:def 25,def 26;
hence still_not-bound_in p '&' q
= still_not-bound_in p \/ still_not-bound_in q
by QC_LANG1:def 20,QC_LANG3:9
.= still_not-bound_in Al2-Cast(p '&' q)
by A11,A12,QC_LANG1:def 20,QC_LANG3:9;
end;
for x,p holds A[p] implies A[All(x,p)]
proof
let x,p such that
A13: A[p];
set x2 = Al2-Cast(x);
set p2 = Al2-Cast(p);
reconsider p2 as Element of CQC-WFF(Al2);
reconsider x2 as bound_QC-variable of Al2;
All(x,p) is universal & All(x2,p2) is universal;
then
A14: p = the_scope_of All(x,p) & x = bound_in All(x,p) & p2 = the_scope_of
All(x2,p2) & x2 = bound_in All(x2,p2) by QC_LANG1:def 27, def 28;
then still_not-bound_in All(x,p)
= still_not-bound_in p \ {x} by QC_LANG3:11, QC_LANG1:def 21
.= still_not-bound_in Al2-Cast(All(x,p))
by A13,A14,QC_LANG1:def 21,QC_LANG3:11;
hence thesis;
end;
then
A15: for p, q, x, k, l, P holds A[VERUM(Al)] & A[P!l] &
(A[p] implies A['not' p]) & (A[p] & A[q] implies A[p '&' q]) &
(A[p] implies A[All(x, p)]) by A1,A2,A8,A10;
for p holds A[p] from CQC_LANG:sch 1(A15);
hence thesis;
end;
theorem Th13:
for p2 being Element of CQC-WFF(Al2), S being CQC_Substitution of Al,
S2 being CQC_Substitution of Al2, x2 being bound_QC-variable of Al2, x, p
st p = p2 & S = S2 & x = x2 holds RestrictSub(x,p,S) = RestrictSub(x2,p2,S2)
proof
let p2 be Element of CQC-WFF(Al2), S be CQC_Substitution of Al, S2 be
CQC_Substitution of Al2, x2 be bound_QC-variable of Al2, x, p such that
A1: p = p2 & S = S2 & x = x2;
set rset = {y where y is bound_QC-variable of Al : y in still_not-bound_in p
& y is Element of dom S & y <> x & y <> S.y};
set rset2 = {y2 where y2 is bound_QC-variable of Al2 : y2 in
still_not-bound_in p2 & y2 is Element of dom S2 & y2 <> x2 & y2 <> S2.y2};
rset = rset2
proof
for s being object st s in rset holds s in rset2
proof
let s be object such that
A2: s in rset;
consider y being bound_QC-variable of Al such that
A3: s = y & y in still_not-bound_in p & y is Element of dom S & y <> x &
y <> S.y by A2;
reconsider y as bound_QC-variable of Al2 by Th4,TARSKI:def 3;
p2 = Al2-Cast(p) by A1;
then y in still_not-bound_in p2 & y is Element of dom S2 & y <> x2 &
y <> S2.y by A1,A3,Th12;
hence s in rset2 by A3;
end;
hence rset c= rset2;
for s2 being object st s2 in rset2 holds s2 in rset
proof
let s2 be object such that
A4: s2 in rset2;
consider y2 being bound_QC-variable of Al2 such that
A5: s2 = y2 & y2 in still_not-bound_in p2 & y2 is Element of dom S2 &
y2 <> x2 & y2 <> S2.y2 by A4;
p2 = Al2-Cast(p) by A1;
then
A6: y2 in still_not-bound_in p by A5,Th12;
then reconsider y2 as bound_QC-variable of Al;
thus s2 in rset by A1,A5,A6;
end;
hence rset2 c= rset;
end;
then S|rset = S2|rset2 & S|rset = RestrictSub(x,p,S) &
S2|rset2 = RestrictSub(x2,p2,S2) by A1,SUBSTUT1:def 6;
hence thesis;
end;
theorem Th14:
for p2 being Element of CQC-WFF(Al2), S being finite CQC_Substitution of Al,
S2 being finite CQC_Substitution of Al2, p st S = S2 & p = p2 holds
upVar(S,p) = upVar(S2,p2)
proof
let p2 be Element of CQC-WFF(Al2), S be finite CQC_Substitution of
Al, S2 being finite CQC_Substitution of Al2, p such that
A1: S = S2 & p = p2;
A2: Sub_Var(S) = Sub_Var(S2)
proof
for s being object st s in Sub_Var(S) holds s in Sub_Var(S2)
proof
let s be object such that
A3: s in Sub_Var(S);
s in {t where t is QC-symbol of Al : x.t in rng S} by A3,SUBSTUT1:def 10;
then consider s2 being QC-symbol of Al such that
A4: s = s2 & x.s2 in rng S;
s2 in QC-symbols(Al) & QC-symbols(Al) c= QC-symbols(Al2) by Th2;
then consider s3 being QC-symbol of Al2 such that
A5: s3 = s2;
x.s2 =[4,s2] by QC_LANG3:def 2 .= x.s3 by A5,QC_LANG3:def 2;
then s3 in {t where t is QC-symbol of Al2 : x.t in rng S2} by A1,A4;
hence thesis by A4,A5,SUBSTUT1:def 10;
end;
hence Sub_Var(S) c= Sub_Var(S2);
for s being object st s in Sub_Var(S2) holds s in Sub_Var(S)
proof
let s be object such that
A6: s in Sub_Var(S2);
s in {t where t is QC-symbol of Al2:x.t in rng S2} by A6,SUBSTUT1:def 10;
then consider s2 being QC-symbol of Al2 such that
A7: s = s2 & x.s2 in rng S2;
A8: rng @S c= bound_QC-variables(Al) by SUBSTUT1:39;
x.s2 in rng @S by A1,A7,SUBSTUT1:def 2;
then x.s2 in bound_QC-variables(Al) by A8;
then [4,s2] in [:{4},QC-symbols(Al):] by QC_LANG3:def 2;
then s2 in QC-symbols(Al) by ZFMISC_1:87;
then consider s3 being QC-symbol of Al such that
A9: s3 = s2;
x.s2 =[4,s2] by QC_LANG3:def 2.= x.s3 by A9,QC_LANG3:def 2;
then s3 in {t where t is QC-symbol of Al : x.t in rng S} by A1,A7;
hence thesis by A7,A9,SUBSTUT1:def 10;
end;
hence Sub_Var(S2) c= Sub_Var(S);
end;
defpred P[Element of QC-WFF(Al)] means for q2 being Element of CQC-WFF(Al2)
st $1 = q2 holds Bound_Vars($1) = Bound_Vars(q2);
A10: P[VERUM(Al)]
proof
let q2 be Element of CQC-WFF(Al2) such that
A11: q2 = VERUM(Al);
q2 = VERUM(Al2) by A11;
hence Bound_Vars(q2)={} by SUBSTUT1:2.=Bound_Vars(VERUM(Al)) by SUBSTUT1:2;
end;
A12: for k,P,l holds P[P!l]
proof
let k,P,l;
set P2 = Al2-Cast(P);
set l2 = Al2-Cast(l);
let q2 be Element of CQC-WFF(Al2) such that
A13: P!l = q2;
A14: q2 = Al2-Cast(P!l) by A13 .= P2!l2 by Th8;
thus Bound_Vars(P!l) = still_not-bound_in (P!l) by SUBLEMMA:43
.= still_not-bound_in (Al2-Cast(P!l)) by Th12
.= still_not-bound_in (P2!l2) by Th8
.= Bound_Vars(q2) by A14,SUBLEMMA:43;
end;
A15: for r,s st P[r] & P[s] holds P[r '&' s]
proof
let r,s such that
A16: P[r] & P[s];
set q = r '&' s;
set r2 = Al2-Cast(r);
set s2 = Al2-Cast(s);
let q2 be Element of CQC-WFF(Al2) such that
A17: r '&' s = q2;
A18: q2 = r2 '&' s2 by A17;
then q is conjunctive & q2 is conjunctive;
then
A19: the_left_argument_of q = r & the_right_argument_of q = s &
the_left_argument_of q2 = r2 & the_right_argument_of q2 = s2
by A18,QC_LANG1:def 25, def 26;
A20: Bound_Vars(r) = Bound_Vars(r2) & Bound_Vars(s) = Bound_Vars(s2) by A16;
thus Bound_Vars(q) = Bound_Vars(r) \/ Bound_Vars(s)
by A19,SUBSTUT1:5,QC_LANG1:def 20
.= Bound_Vars(q2) by A18,A19,A20,SUBSTUT1:5,QC_LANG1:def 20;
end;
A21: for r st P[r] holds P['not' r]
proof
let r such that
A22: P[r];
set q = 'not' r;
set r2 = Al2-Cast(r);
let q2 be Element of CQC-WFF(Al2) such that
A23: q = q2;
A24: q2 = 'not' r2 by A23;
then q is negative & q2 is negative;
then
A25: the_argument_of q = r & the_argument_of q2 = r2 by A24,QC_LANG1:def 24;
thus Bound_Vars(q) = Bound_Vars(r) by A25,SUBSTUT1:4,QC_LANG1:def 19
.= Bound_Vars(r2) by A22 .= Bound_Vars(q2)
by A24,A25,SUBSTUT1:4,QC_LANG1:def 19;
end;
A26: for x,r st P[r] holds P[All(x,r)]
proof
let x,r such that
A27: P[r];
set q = All(x,r);
set r2 = Al2-Cast(r);
set x2 = Al2-Cast(x);
let q2 be Element of CQC-WFF(Al2) such that
A28: q = q2;
A29: q2 = All(x2,r2) by A28;
then q is universal & q2 is universal;
then
A30: the_scope_of q = r & bound_in q = x & the_scope_of q2 = r2 &
bound_in q2 = x2 by A29,QC_LANG1:def 27,def 28;
thus Bound_Vars(q) = Bound_Vars(r) \/ {x}
by A30,SUBSTUT1:6,QC_LANG1:def 21
.= Bound_Vars(r2) \/ {x2} by A27 .= Bound_Vars(q2)
by A29,A30,SUBSTUT1:6,QC_LANG1:def 21;
end;
A31: for r,s,x,k,l,P holds P[VERUM(Al)] & P[P!l] & (P[r] implies P['not' r]) &
(P[r] & P[s] implies P[r '&' s]) & (P[r] implies P[All(x, r)])
by A10,A12,A15,A21,A26;
A32: for q being Element of CQC-WFF(Al) holds P[q] from CQC_LANG:sch 1(A31);
A33: Dom_Bound_Vars p = Dom_Bound_Vars p2
proof
for s being object st s in Dom_Bound_Vars p holds s in Dom_Bound_Vars p2
proof
let s be object such that
A34: s in Dom_Bound_Vars p;
s in {b where b is QC-symbol of Al : x.b in Bound_Vars p}
by A34,SUBSTUT1:def 9;
then consider s2 being QC-symbol of Al such that
A35: s = s2 & x.s2 in Bound_Vars p;
x.s2 in Bound_Vars p2 by A1,A32,A35;
then x.s2 in bound_QC-variables(Al2);
then [4,s2] in [:{4},QC-symbols(Al2):] by QC_LANG3:def 2;
then s2 in QC-symbols(Al2) by ZFMISC_1:87;
then consider s3 being QC-symbol of Al2 such that
A36: s3 = s2;
x.s2 =[4,s2] by QC_LANG3:def 2 .= x.s3 by A36,QC_LANG3:def 2;
then x.s3 in Bound_Vars p2 by A1,A32,A35;
then s3 in {b where b is QC-symbol of Al2 : x.b in Bound_Vars p2};
hence thesis by A35,A36,SUBSTUT1:def 9;
end;
hence Dom_Bound_Vars p c= Dom_Bound_Vars p2;
for s being object st s in Dom_Bound_Vars p2 holds s in Dom_Bound_Vars p
proof
let s be object such that
A37: s in Dom_Bound_Vars p2;
s in {b where b is QC-symbol of Al2 : x.b in Bound_Vars p2}
by A37,SUBSTUT1:def 9;
then consider s2 being QC-symbol of Al2 such that
A38: s = s2 & x.s2 in Bound_Vars p2;
x.s2 in Bound_Vars p by A1,A32,A38;
then x.s2 in bound_QC-variables(Al);
then [4,s2] in [:{4},QC-symbols(Al):] by QC_LANG3:def 2;
then s2 in QC-symbols(Al) by ZFMISC_1:87;
then consider s3 being QC-symbol of Al such that
A39: s3 = s2;
x.s2 =[4,s2] by QC_LANG3:def 2 .= x.s3 by A39,QC_LANG3:def 2;
then x.s3 in Bound_Vars p by A1,A32,A38;
then s3 in {b where b is QC-symbol of Al : x.b in Bound_Vars p};
hence thesis by A38,A39,SUBSTUT1:def 9;
end;
hence Dom_Bound_Vars p2 c= Dom_Bound_Vars p;
end;
A40: NSub(p,S) = NAT\(Dom_Bound_Vars(p)\/Sub_Var(S)) by SUBSTUT1:def 11
.= NSub(p2,S2) by A2,A33,SUBSTUT1:def 11;
thus upVar(S,p) = the Element of NSub(p,S) by SUBSTUT1:def 12
.= upVar(S2,p2) by A40,SUBSTUT1:def 12;
end;
theorem Th15:
for p2 being Element of CQC-WFF(Al2), S being CQC_Substitution of Al,
S2 being CQC_Substitution of Al2, x2 being bound_QC-variable of Al2, x, p
st p = p2 & S = S2 & x = x2 holds ExpandSub(x,p,RestrictSub(x,All(x,p),S))
= ExpandSub(x2,p2,RestrictSub(x2,All(x2,p2),S2))
proof
let p2 be Element of CQC-WFF(Al2), S being CQC_Substitution of Al,
S2 being CQC_Substitution of Al2, x2 being bound_QC-variable of Al2, x, p
such that
A1: p = p2 & S = S2 & x = x2;
set rsub = RestrictSub(x,All(x,p),S);
set rsub2 = RestrictSub(x2,All(x2,p2),S2);
set esub = ExpandSub(x,p,rsub);
set esub2 = ExpandSub(x2,p2,rsub2);
set uv = upVar(rsub,p);
set uv2 = upVar(rsub2,p2);
A2: x.uv =[4,uv] by QC_LANG3:def 2 .= [4,uv2] by A1,Th13,Th14
.= x.uv2 by QC_LANG3:def 2;
per cases;
suppose
A3: not x in rng rsub;
then not x2 in rng rsub2 by A1,Th13;
hence esub2 = rsub2 \/ {[x2,x2]} by SUBSTUT1:def 13
.= rsub \/ {[x,x]} by A1,Th13 .= esub by A3,SUBSTUT1:def 13;
end;
suppose
A4: x in rng rsub;
then x2 in rng rsub2 by A1,Th13;
hence esub2 = rsub2 \/ {[x2,(x.uv2)]} by SUBSTUT1:def 13
.= rsub \/ {[x,(x.uv)]} by A1,Th13,A2
.= esub by A4,SUBSTUT1:def 13;
end;
end;
theorem Th16:
for Z being Element of CQC-Sub-WFF(Al), Z2 being Element of CQC-Sub-WFF(Al2)
st Z`1 is universal & Z2`1 is universal & bound_in Z`1 = bound_in Z2`1 &
the_scope_of Z`1 = the_scope_of Z2`1 & Z = Z2 holds S_Bound(@Z) = S_Bound(@Z2)
proof
let Z be Element of CQC-Sub-WFF(Al), Z2 be Element of CQC-Sub-WFF(Al2)
such that
A1: Z`1 is universal & Z2`1 is universal & bound_in Z`1 = bound_in Z2`1 &
the_scope_of Z`1 = the_scope_of Z2`1 & Z = Z2;
set p = (@Z)`1;
set p2 = (@Z2)`1;
set S = (@Z)`2;
set S2 = (@Z2)`2;
reconsider p as Element of CQC-WFF(Al) by A1,SUBSTUT1:def 35;
reconsider p2 as Element of CQC-WFF(Al2) by A1,SUBSTUT1:def 35;
reconsider S as CQC_Substitution of Al;
reconsider S2 as CQC_Substitution of Al2;
set x = bound_in p;
set x2 = bound_in p2;
set q = the_scope_of p;
set q2 = the_scope_of p2;
p is universal by A1,SUBSTUT1:def 35;
then p = All(x,q) by QC_LANG2:6;
then reconsider q as Element of CQC-WFF(Al) by CQC_LANG:13;
p2 is universal by A1,SUBSTUT1:def 35;
then p2 = All(x2,q2) by QC_LANG2:6;
then reconsider q2 as Element of CQC-WFF(Al2) by CQC_LANG:13;
reconsider x as bound_QC-variable of Al;
reconsider x2 as bound_QC-variable of Al2;
A2: p =Z`1 by SUBSTUT1:def 35 .= p2 by A1,SUBSTUT1:def 35;
A3: S =Z`2 by SUBSTUT1:def 35 .= S2 by A1,SUBSTUT1:def 35;
A4: x = bound_in Z`1 by SUBSTUT1:def 35 .= x2 by A1,SUBSTUT1:def 35;
A5: q = the_scope_of Z`1 by SUBSTUT1:def 35 .= q2 by A1,SUBSTUT1:def 35;
set rsub = RestrictSub(x,p,S);
set rsub2 = RestrictSub(x2,p2,S2);
per cases;
suppose
A6: not x in rng rsub;
then not x2 in rng rsub2 by A2,A3,A4,Th13;
hence S_Bound @Z2 = x2 by SUBSTUT1:def 36
.= S_Bound @Z by A4,A6,SUBSTUT1:def 36;
end;
suppose
A7: x in rng rsub;
then x2 in rng rsub2 by A2,A3,A4,Th13;
then S_Bound @Z2 = x.(upVar(rsub2,q2)) by SUBSTUT1:def 36
.= [4,upVar(rsub2,q2)] by QC_LANG3:def 2
.= [4,upVar(rsub,q)] by A5,A2,A3,A4,Th13,Th14
.= x.(upVar(rsub,q)) by QC_LANG3:def 2
.= S_Bound @Z by A7,SUBSTUT1:def 36;
hence thesis;
end;
end;
theorem Th17:
for p2 being Element of CQC-WFF(Al2),x2,y2 being bound_QC-variable of Al2,
p,x,y st p=p2 & x=x2 & y=y2 holds p.(x,y) = p2.(x2,y2)
proof
defpred P[Element of CQC-WFF(Al)] means for p2 being Element of CQC-WFF(Al2),
S being CQC_Substitution of Al, S2 being CQC_Substitution of Al2
st $1 = p2 & S = S2 holds CQC_Sub [$1,S] = CQC_Sub [p2,S2];
A1: P[VERUM(Al)]
proof
set p = VERUM(Al);
let p2 be Element of CQC-WFF(Al2), S be CQC_Substitution of Al,
S2 be CQC_Substitution of Al2 such that
A2: p = p2 & S = S2;
A3: VERUM(Al2) = p2 by A2;
A4: [p,S] is Al-Sub_VERUM & [p2,S2] is Al2-Sub_VERUM by A3,SUBSTUT1:def 19;
thus CQC_Sub [p,S] = VERUM(Al2) by A4,SUBLEMMA:3
.= CQC_Sub [p2,S2] by A4,SUBLEMMA:3;
end;
A5: for k,P,l holds P[P!l]
proof
let k,P,l;
set P2 = Al2-Cast(P);
set l2 = Al2-Cast(l);
reconsider P2 as QC-pred_symbol of k,Al2;
reconsider l2 as CQC-variable_list of k,Al2;
let p2 be Element of CQC-WFF(Al2), S be CQC_Substitution of Al,
S2 be CQC_Substitution of Al2 such that
A6: P!l = p2 & S = S2;
A7: p2 = Al2-Cast(P!l) by A6 .= P2!l2 by Th8;
set p = P!l;
reconsider p as Element of CQC-WFF(Al);
set sub = CQC_Subst(l,S);
A8: sub = CQC_Subst(Al2-Cast(l),S2)
proof
A9: len sub = len l by SUBSTUT1:def 3
.= len CQC_Subst(Al2-Cast(l),S2) by SUBSTUT1:def 3;
for n being Nat st n in dom sub holds
sub.n = (CQC_Subst(Al2-Cast(l),S2)).n
proof
let n be Nat such that
A10: n in dom sub;
n in Seg len sub by A10,FINSEQ_1:def 3;
then 1 <= n & n <= len sub by FINSEQ_1:1;
then
A11: 1 <= n & n <= len l by SUBSTUT1:def 3;
reconsider n as Element of NAT by ORDINAL1:def 12;
per cases;
suppose
A12: l.n in dom S;
sub.n = S.(l.n) by A11,A12,SUBSTUT1:def 3
.= CQC_Subst(Al2-Cast(l),S2).n by A6,A11,A12,SUBSTUT1:def 3;
hence thesis;
end;
suppose
A13: not l.n in dom S;
sub.n = l.n by A11,A13,SUBSTUT1:def 3
.= CQC_Subst(Al2-Cast(l),S2).n by A6,A11,A13,SUBSTUT1:def 3;
hence thesis;
end;
end;
hence thesis by A9,FINSEQ_2:9;
end;
the_arity_of P = len l & the_arity_of P2 = len l2 by Th1;
then
A14: [P!l,S] = Sub_P(P,l,S) & [P2!l2,S2] = Sub_P(P2,l2,S2)
by SUBSTUT1:def 18;
P!l is atomic & P2!l2 is atomic;
then
A15: P = the_pred_symbol_of P!l & P2 = the_pred_symbol_of P2!l2
by QC_LANG1:def 22;
A16: [P!l,S]`1 = P!l & [P!l,S]`2 = S & [P2!l2,S2]`1 = P2!l2 & [P2!l2,S2]`2 = S2
& Sub_the_arguments_of [P!l,S] = l & Sub_the_arguments_of [P2!l2,S2] = l2
by A14,SUBSTUT1:def 29;
thus CQC_Sub [P!l,S] = Al2-Cast(P!CQC_Subst(l,S)) by A14,A15,A16,SUBLEMMA:6
.= (Al2-Cast(P))!(Al2-Cast(CQC_Subst(l,S))) by Th8
.= CQC_Sub [p2,S2] by A7,A8,A14,A15,A16,SUBLEMMA:6;
end;
A17: for q st P[q] holds P['not' q]
proof
let q such that
A18: P[q];
set p = 'not' q;
reconsider p as Element of CQC-WFF(Al);
set q2 = Al2-Cast(q);
reconsider q2 as Element of CQC-WFF(Al2);
let p2 be Element of CQC-WFF(Al2), S being CQC_Substitution of Al,
S2 being CQC_Substitution of Al2 such that
A19: 'not' q = p2 & S = S2;
A20: [q,S]`1 = q & [q,S]`2 = S & [q2,S2]`1 = q2 & [q2,S2]`2 = S2;
thus CQC_Sub ['not' q, S] = CQC_Sub Sub_not [q,S] by A20,SUBSTUT1:def 20
.= Al2-Cast('not' CQC_Sub [q,S]) by SUBSTUT1:29
.= 'not' CQC_Sub [q2,S2] by A18,A19
.= CQC_Sub Sub_not [q2,S2] by SUBSTUT1:29 .= CQC_Sub ['not' q2,S2]
by A20,SUBSTUT1:def 20
.= CQC_Sub [p2,S2] by A19;
end;
A21: for r,s st P[r] & P[s] holds P[r '&' s]
proof
let r,s such that
A22: P[r] & P[s];
set r2 = Al2-Cast(r);
set s2 = Al2-Cast(s);
reconsider r2,s2 as Element of CQC-WFF(Al2);
let p2 be Element of CQC-WFF(Al2), S be CQC_Substitution of Al,
S2 be CQC_Substitution of Al2 such that
A23: r '&' s = p2 & S = S2;
A24: CQC_Sub[r,S] = CQC_Sub[r2,S2] & CQC_Sub[s,S] = CQC_Sub[s2,S2] by A22,A23;
A25: [r,S]`1 = r & [r,S]`2 = S & [s,S]`1 = s & [s,S]`2 = S & [r2,S2]`1 = r2 &
[r2,S2]`2 = S2 & [s2,S2]`1 = s2 & [s2,S2]`2 = S2;
thus CQC_Sub[r '&' s,S] = CQC_Sub CQCSub_&([r,S],[s,S]) by SUBSTUT2:19
.= Al2-Cast((CQC_Sub [r,S]) '&' (CQC_Sub[s,S])) by A25,SUBLEMMA:23
.= Al2-Cast(CQC_Sub [r,S]) '&' Al2-Cast(CQC_Sub[s,S])
.= CQC_Sub CQCSub_&([r2,S2],[s2,S2]) by A24,A25,SUBLEMMA:23
.= CQC_Sub [r2 '&' s2,S2] by SUBSTUT2:19
.= CQC_Sub [p2,S2] by A23;
end;
for z being bound_QC-variable of Al,q st P[q] holds P[All(z,q)]
proof
let z be bound_QC-variable of Al,q such that
A26: P[q];
set p = All(z,q);
set q2 = Al2-Cast(q);
set z2 = Al2-Cast(z);
reconsider p as Element of CQC-WFF(Al);
let p2 be Element of CQC-WFF(Al2), S be CQC_Substitution of Al,
S2 be CQC_Substitution of Al2 such that
A27: All(z,q) = p2 & S = S2;
set qsc = Qsc(q,z,S);
set qsc2 = Qsc(q2,z2,S2);
set sub = [All(z,q),S];
set sub2 = [All(z2,q2),S2];
set qscope = [q,(CFQ(Al)).sub];
set qscope2 = [q2,(CFQ(Al2)).sub2];
A28: QScope(q,z,S) = [qscope,z] by SUBSTUT2:def 3;
reconsider qscope as Element of CQC-Sub-WFF(Al);
reconsider qsc as second_Q_comp of [qscope,z] by SUBSTUT2:def 3;
A29: QScope(q2,z2,S2) = [qscope2,z2] by SUBSTUT2:def 3;
reconsider qscope2 as Element of CQC-Sub-WFF(Al2);
reconsider qsc2 as second_Q_comp of [qscope2,z2] by SUBSTUT2:def 3;
A30: sub = CQCSub_All([qscope,z],qsc) & [qscope,z] is quantifiable &
sub2 = CQCSub_All([qscope2,z2],qsc2) & [qscope2,z2] is quantifiable
by A28,A29,SUBSTUT2:22;
set expandsub = ExpandSub(z,q,RestrictSub(z,All(z,q),S));
set expandsub2 = ExpandSub(z2,q2,RestrictSub(z2,All(z2,q2),S2));
A31: All(z,q) is universal & All(z2,q2) is universal;
then z = bound_in All(z,q) & q = the_scope_of All(z,q) &
z2 = bound_in All(z2,q2) & q2 = the_scope_of All(z2,q2)
by QC_LANG1:def 27, def 28;
then All(z,q),S PQSub expandsub &
All(z2,q2),S2 PQSub expandsub2 by A31,SUBSTUT1:def 14;
then [sub,expandsub] in QSub(Al) & [sub2,expandsub2] in QSub(Al2)
by SUBSTUT1:def 15;
then [sub,expandsub] in (QSub(Al))|(CQC-Sub-WFF(Al)) &
[sub2,expandsub2] in (QSub(Al2))|(CQC-Sub-WFF(Al2)) by RELAT_1:def 11;
then
A32:[sub,expandsub] in CFQ(Al) & [sub2,expandsub2] in CFQ(Al2)
by SUBSTUT2:def 2;
set scope = CQCSub_the_scope_of sub;
set scope2 = CQCSub_the_scope_of sub2;
A33: bound_in sub`1 = z by A31,QC_LANG1:def 27
.= bound_in sub2`1 by A31,QC_LANG1:def 27;
A34: the_scope_of sub`1 = q by A31,QC_LANG1:def 28
.= the_scope_of sub2`1 by A31,QC_LANG1:def 28;
A35: expandsub = expandsub2 by A27,Th15;
A36: CQC_Sub qscope = CQC_Sub[q,expandsub] by A32,FUNCT_1:1
.= CQC_Sub qscope2 by A26,A32,A35,FUNCT_1:1;
CQC_Sub [p,S] = CQCQuant(sub, CQC_Sub scope) by A30,SUBLEMMA:27,28
.= Quant(sub,CQC_Sub scope) by A30,SUBLEMMA:27,def 7
.= All(S_Bound(@sub),CQC_Sub scope) by SUBSTUT1:def 37
.= Al2-Cast(All(S_Bound(@sub),CQC_Sub qscope)) by A30,SUBLEMMA:30
.= All(S_Bound(@sub2),CQC_Sub qscope2) by A36,A27,A31,A33,A34,Th16
.= All(S_Bound(@sub2),CQC_Sub scope2) by A30,SUBLEMMA:30
.= Quant(sub2,CQC_Sub scope2) by SUBSTUT1:def 37
.= CQCQuant(sub2, CQC_Sub scope2) by A30,SUBLEMMA:27,def 7
.= CQC_Sub [p2,S2] by A27,A30,SUBLEMMA:27,28;
hence thesis;
end;
then
A37: for r,s,x,k,l,P holds P[VERUM(Al)] & P[P!l] & (P[r] implies P['not' r]) &
(P[r] & P[s] implies P[r '&' s]) & (P[r] implies P[All(x, r)])
by A1,A5,A17,A21;
A38: for p being Element of CQC-WFF(Al) holds P[p] from CQC_LANG:sch 1(A37);
let p2 be Element of CQC-WFF(Al2),x2,y2 be bound_QC-variable of Al2 ,p,x,y
such that
A39: p=p2 & x=x2 & y=y2;
thus p.(x,y) = CQC_Sub [p,Sbst(x,y)] by SUBSTUT2:def 1
.= CQC_Sub [p2,Sbst(x2,y2)] by A38,A39 .= p2.(x2,y2) by SUBSTUT2:def 1;
end;
theorem Th18:
for PHI being Consistent Subset of CQC-WFF(Al2) st
PHI is Subset of CQC-WFF(Al) holds PHI is Al-Consistent
proof
let PHI be Consistent Subset of CQC-WFF(Al2) such that
PHI is Subset of CQC-WFF(Al);
for S being Subset of CQC-WFF(Al) st PHI=S holds S is Consistent
proof
let S be Subset of CQC-WFF(Al) such that
A1: PHI=S;
assume
A2: S is Inconsistent;
PHI |- 'not' VERUM(Al2)
proof
consider f being FinSequence of CQC-WFF(Al) such that
A3: rng f c= S & |- f^<*'not' VERUM(Al)*> by A2,GOEDELCP:24,HENMODEL:def 1;
set f2 = f;
for x being object st x in rng f2 holds x in CQC-WFF(Al2)
proof
let x be object such that
A4: x in rng f2;
x in PHI by A1,A3,A4;
hence x in CQC-WFF(Al2);
end;
then reconsider f2 as FinSequence of CQC-WFF(Al2)
by FINSEQ_1:def 4,TARSKI:def 3;
consider PR such that
A5: PR is a_proof & f^<*'not' VERUM(Al)*> = (PR.(len PR))`1
by A3,CALCUL_1:def 9;
A6: PR <> {} & for n being Nat st 1 <= n & n <= len PR holds
PR,n is_a_correct_step by A5,CALCUL_1:def 8;
set PR2 = PR;
PR2 is FinSequence of [:set_of_CQC-WFF-seq(Al2),Proof_Step_Kinds:]
proof
for p being object holds p in CQC-WFF(Al) implies p in CQC-WFF(Al2)
proof
let p be object;
assume p in CQC-WFF(Al);
then p is Element of CQC-WFF(Al2) by Th7;
hence thesis;
end;
then
A7: CQC-WFF(Al) c= CQC-WFF(Al2) &
rng PR2 c= [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:];
for x being object holds x in set_of_CQC-WFF-seq(Al) implies
x in set_of_CQC-WFF-seq(Al2)
proof
let x be object;
assume x in set_of_CQC-WFF-seq(Al);
then reconsider x as FinSequence of CQC-WFF(Al) by CALCUL_1:def 6;
rng x c= CQC-WFF(Al2) by A7;
then x is FinSequence of CQC-WFF(Al2) by FINSEQ_1:def 4;
hence thesis by CALCUL_1:def 6;
end;
then set_of_CQC-WFF-seq(Al) c= set_of_CQC-WFF-seq(Al2);
then [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:] c=
[:set_of_CQC-WFF-seq(Al2),Proof_Step_Kinds:] by ZFMISC_1:95;
then rng PR2 c= [:set_of_CQC-WFF-seq(Al2),Proof_Step_Kinds:];
hence thesis by FINSEQ_1:def 4;
end;
then reconsider PR2 as FinSequence of
[:set_of_CQC-WFF-seq(Al2),Proof_Step_Kinds:];
A8: PR2 is a_proof
proof
for n being Nat st 1 <= n & n <= len PR2 holds PR2,n is_a_correct_step
proof
let n be Nat such that
A9: 1 <= n & n <= len PR2;
A10: (for i st 1 <= i & i<n holds (PR2.i)`1 in set_of_CQC-WFF-seq(Al2)) &
((PR2.n)`1 in set_of_CQC-WFF-seq(Al2))
proof
thus for i st 1 <= i & i < n holds
(PR2.i)`1 in set_of_CQC-WFF-seq(Al2)
proof
let i such that
A11: 1 <= i & i < n;
set k = len PR2 - n;
reconsider k as Element of NAT by A9,NAT_1:21;
len PR2 = n + k;
then
A12: 1 <= i & i <= len PR2 by A11, NAT_1:12;
dom PR2 = Seg (len PR2) by FINSEQ_1:def 3;
then i in dom PR2 by A12,FINSEQ_1:1;
then PR2.i in rng PR2 by FUNCT_1:def 3;
hence (PR2.i)`1 in set_of_CQC-WFF-seq(Al2) by MCART_1:10;
end;
dom PR2 = Seg (len PR2) by FINSEQ_1:def 3;
then n in dom PR2 by A9,FINSEQ_1:1;
then PR2.n in rng PR2 by FUNCT_1:def 3;
hence (PR2.n)`1 in set_of_CQC-WFF-seq(Al2) by MCART_1:10;
end;
A13: PR,n is_a_correct_step by A5,CALCUL_1:def 8,A9;
(PR.n)`2 = 0 or ... or (PR.n)`2 = 9 by CALCUL_1:31,A9;
then per cases;
suppose
A14: (PR2.n)`2 = 0;
then consider g2 being FinSequence of CQC-WFF(Al) such that
A15: (Suc g2 is_tail_of Ant g2 & (PR2.n)`1 = g2) by A13,CALCUL_1:def 7;
g2 is FinSequence of CQC-WFF(Al2) by A10,A15,CALCUL_1:def 6;
then consider g being FinSequence of CQC-WFF(Al2) such that
A16: g=g2;
A17: Suc g = Suc g2 & Ant g = Ant g2 by A16,Th11;
thus thesis by A14,A15,A16,A17,CALCUL_1:def 7;
end;
suppose
A18: (PR2.n)`2 = 1;
then consider g2 being FinSequence of CQC-WFF(Al) such that
A19: ((PR.n)`1 = g2^<*VERUM(Al)*>) by A13,CALCUL_1:def 7;
g2^<*VERUM(Al)*> is FinSequence of CQC-WFF(Al2)
by A10,A19,CALCUL_1:def 6;
then consider gp being FinSequence of CQC-WFF(Al2) such that
A20: gp=g2^<*VERUM(Al)*>;
len gp <> 0 by A20;
then consider g being FinSequence of CQC-WFF(Al2),
v being Element of CQC-WFF(Al2) such that
A21: gp = g^<*v*> by FINSEQ_2:19;
v = VERUM(Al2) by A20,A21,FINSEQ_2:17;
hence thesis by A18,A19,A20,A21,CALCUL_1:def 7;
end;
suppose
A22: (PR2.n)`2 = 2;
then consider i being Nat, g2,h2 being
FinSequence of CQC-WFF(Al) such that
A23: (1 <= i & i<n & Ant g2 is_Subsequence_of Ant h2 & Suc g2 = Suc h2
& (PR2.i)`1 = g2 & (PR2.n)`1 = h2) by A13,CALCUL_1:def 7;
g2 in set_of_CQC-WFF-seq(Al2) & h2 in set_of_CQC-WFF-seq(Al2)
by A10,A23;
then h2 is FinSequence of CQC-WFF(Al2) &
g2 is FinSequence of CQC-WFF(Al2) by CALCUL_1:def 6;
then consider g,h being FinSequence of CQC-WFF(Al2) such that
A24: g=g2 & h=h2;
A25: Suc g = Suc g2 by A24,Th11
.= Suc h by A23,A24,Th11;
consider N being Subset of NAT such that
A26: (Ant g2) c= Seq((Ant h2)|N) by A23,CALCUL_1:def 4;
(Ant h2)|N = (Ant h)|N by A24,Th11;
then (Ant g) c= Seq((Ant h)|N) by A24,A26,Th11;
then
A27: Ant g is_Subsequence_of Ant h by CALCUL_1:def 4;
thus thesis by A22,A23,A24,A25,A27,CALCUL_1:def 7;
end;
suppose
A28: (PR2.n)`2 = 3;
then consider i,j being Nat, g,h being
FinSequence of CQC-WFF(Al) such that
A29: (1 <= i & i < n & 1 <= j & j < i & len g > 1 & len h > 1 &
Ant (Ant g) = Ant (Ant h) & 'not' (Suc (Ant g)) = Suc (Ant h)
& Suc g = Suc h & g = (PR2.j) `1 & h = (PR2.i)`1 &
(Ant (Ant g))^<*(Suc g)*> = (PR2.n)`1) by A13,CALCUL_1:def 7;
(PR2.j)`1 = g & (PR2.i)`1 = h & j < n by A29,XXREAL_0:2;
then g in set_of_CQC-WFF-seq(Al2) & h in set_of_CQC-WFF-seq(Al2)
by A10,A29;
then h is FinSequence of CQC-WFF(Al2) &
g is FinSequence of CQC-WFF(Al2) by CALCUL_1:def 6;
then consider g2,h2 being FinSequence of CQC-WFF(Al2) such that
A30: g2=g & h2=h;
A31: Ant g2 = Ant g & Ant h2 = Ant h by A30,Th11;
then
A32: Ant (Ant g2) = Ant (Ant g) by Th11
.= Ant (Ant h2) by A29,A31,Th11;
A33: 'not' (Suc (Ant g2)) = 'not' (Al2-Cast(Suc (Ant g))) by A31,Th11
.= Suc (Ant h2) by A29,A31,Th11;
A34: Suc g2 = Suc g by A30,Th11
.= Suc h2 by A29,A30,Th11;
A35: (PR2.n)`1 = (Ant (Ant g))^<*(Suc g2)*> by A29,A30,Th11
.= (Ant (Ant g2))^<*Suc g2*> by A31,Th11;
thus thesis by A28,A29,A30,A32,A33,A34,A35,CALCUL_1:def 7;
end;
suppose
A36: (PR2.n)`2 = 4;
then consider i,j being Nat, g,h being FinSequence of
CQC-WFF(Al), p being Element of CQC-WFF(Al) such that
A37: (1 <= i & i < n & 1 <= j & j < i & len g > 1 & Ant g = Ant h &
Suc (Ant g) = 'not' p & 'not' (Suc g) = Suc h & g = (PR2.j)`1
& h = (PR2.i)`1 & (Ant (Ant g))^<*p*> = (PR2.n)`1)
by A13,CALCUL_1:def 7;
(PR2.j)`1 = g & (PR2.i)`1 = h & j < n by A37,XXREAL_0:2;
then g in set_of_CQC-WFF-seq(Al2) & h in set_of_CQC-WFF-seq(Al2)
by A10,A37;
then h is FinSequence of CQC-WFF(Al2) &
g is FinSequence of CQC-WFF(Al2) by CALCUL_1:def 6;
then consider g2,h2 being FinSequence of CQC-WFF(Al2) such that
A38: g2=g & h2=h;
A39: Ant g2 = Ant g by A38,Th11 .= Ant h2 by A37,A38,Th11;
Ant g2 = Ant g by A38,Th11;
then
A40: Suc (Ant g2) = 'not' Al2-Cast(p) by A37,Th11;
A41: 'not' (Suc g2) = 'not' (Al2-Cast((Suc g))) by A38,Th11
.= Suc h2 by A37,A38,Th11;
Ant g2 = Ant g by A38,Th11;
then (Ant (Ant g2))^<*Al2-Cast(p)*> = (PR2.n)`1 by Th11,A37;
hence thesis by A36,A37,A38,A39,A40,A41,CALCUL_1:def 7;
end;
suppose
A42: (PR2.n)`2 = 5;
then consider i,j being Nat, g,h being FinSequence of
CQC-WFF(Al) such that
A43: (1 <= i & i < n & 1<=j & j<i & Ant g = Ant h & g = (PR2.j)`1 &
h = (PR2.i)`1 & (Ant g)^<*((Suc g) '&' (Suc h))*> =(PR2.n)`1)
by A13,CALCUL_1:def 7;
(PR2.j)`1 = g & (PR2.i)`1 = h & j < n by A43,XXREAL_0:2;
then g in set_of_CQC-WFF-seq(Al2) & h in set_of_CQC-WFF-seq(Al2)
by A10,A43;
then h is FinSequence of CQC-WFF(Al2) &
g is FinSequence of CQC-WFF(Al2) by CALCUL_1:def 6;
then consider g2,h2 being FinSequence of CQC-WFF(Al2) such that
A44: g=g2 & h=h2;
Al2-Cast(Suc g) = Suc g2 & Al2-Cast(Suc h) = Suc h2 by A44,Th11;
then
A45: (Ant g2)^<*((Suc g2) '&' (Suc h2))*> = (PR2.n)`1 by A43,A44,Th11;
Ant g2 = Ant g by A44,Th11 .= Ant h2 by A43,A44,Th11;
hence thesis by A42,A43,A44,A45,CALCUL_1:def 7;
end;
suppose
A46: (PR2.n)`2 = 6;
then consider i being Nat, g being FinSequence of
CQC-WFF(Al), p,q being Element of CQC-WFF(Al) such that
A47: (1 <= i & i < n & p '&' q = Suc g & g = (PR2.i)`1 &
(Ant g)^<*p*> = (PR2.n)`1) by A13,CALCUL_1:def 7;
g in set_of_CQC-WFF-seq(Al2) by A10,A47;
then g is FinSequence of CQC-WFF(Al2) by CALCUL_1:def 6;
then consider g2 being FinSequence of CQC-WFF(Al2) such that
A48: g=g2;
A49: Suc g2 = (Al2-Cast(p)) '&' (Al2-Cast(q)) by A47,A48,Th11;
(Ant g2)^<*p*> = (PR2.n)`1 by A47,A48,Th11;
hence thesis by A46,A47,A48,A49,CALCUL_1:def 7;
end;
suppose
A50: (PR2.n)`2 = 7;
then consider i being Nat, g being FinSequence of
CQC-WFF(Al), p,q being Element of CQC-WFF(Al) such that
A51: (1 <= i & i < n & p '&' q = Suc g & g = (PR2.i)`1 &
(Ant g)^<*q*> = (PR2.n)`1) by A13,CALCUL_1:def 7;
g in set_of_CQC-WFF-seq(Al2) by A10,A51;
then g is FinSequence of CQC-WFF(Al2) by CALCUL_1:def 6;
then reconsider g2 = g as FinSequence of CQC-WFF(Al2);
A52: Suc g2 = (Al2-Cast(p)) '&' (Al2-Cast(q)) by A51,Th11;
(Ant g2)^<*Al2-Cast(q)*> = (PR2.n)`1 by A51,Th11;
hence thesis by A50,A51,A52,CALCUL_1:def 7;
end;
suppose
A53: (PR2.n)`2 = 8;
then consider i being Nat, g being FinSequence of
CQC-WFF(Al), p being Element of CQC-WFF(Al), x,y being
bound_QC-variable of Al such that
A54: (1 <= i & i < n & Suc g = All(x,p) & g = (PR2.i)`1 &
(Ant g)^<*(p.(x,y))*> = (PR2.n)`1 ) by A13,CALCUL_1:def 7;
g in set_of_CQC-WFF-seq(Al2) by A10,A54;
then g is FinSequence of CQC-WFF(Al2) by CALCUL_1:def 6;
then consider g2 being FinSequence of CQC-WFF(Al2) such that
A55: g=g2;
p is Element of CQC-WFF(Al2) & x is bound_QC-variable of Al2 &
y is bound_QC-variable of Al2 by Th4,Th7,TARSKI:def 3;
then consider q being Element of CQC-WFF(Al2),
a,b being bound_QC-variable of Al2 such that
A56: a = x & b = y & q = p;
A57: (PR2.n)`1 = (Ant g)^<*(q.(a,b))*> by A54,A56,Th17
.= (Ant g2)^<*(q.(a,b))*> by A55,Th11;
Suc g2 = All(a,q) by A54,A55,A56,Th11;
hence thesis by A53,A54,A55,A57,CALCUL_1:def 7;
end;
suppose
A58: (PR2.n)`2 = 9;
then consider i being Nat, g being FinSequence of
CQC-WFF(Al), p being Element of CQC-WFF(Al), x,y being
bound_QC-variable of Al such that
A59: (1 <= i & i < n & Suc g = p.(x,y) & not y in still_not-bound_in
(Ant g) & not y in still_not-bound_in (All(x,p)) & g=(PR2.i)`1 &
(Ant g)^<*(All(x,p))*> = (PR2.n)`1) by A13,CALCUL_1:def 7;
g in set_of_CQC-WFF-seq(Al2) by A10,A59;
then g is FinSequence of CQC-WFF(Al2) by CALCUL_1:def 6;
then consider g2 being FinSequence of CQC-WFF(Al2) such that
A60: g=g2;
p is Element of CQC-WFF(Al2) & x is bound_QC-variable of Al2 &
y is bound_QC-variable of Al2 by Th4,Th7,TARSKI:def 3;
then consider q being Element of CQC-WFF(Al2),
a,b being bound_QC-variable of Al2 such that
A61: q = p & a = x & b = y;
A62: Suc g2 = Suc g by A60,Th11 .= q.(a,b) by A59,A61,Th17;
A63: still_not-bound_in All(x,p) =
still_not-bound_in (Al2-Cast(All(x,p))) by Th12
.= still_not-bound_in All(a,q) by A61;
A64: not b in still_not-bound_in (Ant g2)
proof
assume b in still_not-bound_in (Ant g2);
then consider i being Nat,
r being Element of CQC-WFF(Al2) such that
A65: i in dom (Ant g2) & r = (Ant g2).i & b in still_not-bound_in r
by CALCUL_1:def 5;
A66: dom (Ant g2) = dom (Ant g) by A60,Th11;
r = (Ant g).i by A60,A65,Th11;
then reconsider r as Element of CQC-WFF(Al)
by A65,A66,FINSEQ_2:11;
i in dom (Ant g) & Al2-Cast(r) = (Ant g).i &
b in still_not-bound_in (Al2-Cast(r)) by A60,A65,Th11;
then i in dom (Ant g) & r = (Ant g).i &
y in still_not-bound_in r by A61,Th12;
hence contradiction by A59,CALCUL_1:def 5;
end;
(Ant g2)^<*(All(a,q))*> = (PR2.n)`1 by A59,A60,A61,Th11;
hence thesis by A58,A59,A60,A61,A62,A63,A64,CALCUL_1:def 7;
end;
end;
hence thesis by A6,CALCUL_1:def 8;
end;
|- f2^<*('not' VERUM(Al2))*> by A5,A8,CALCUL_1:def 9;
hence thesis by A1,A3,HENMODEL:def 1;
end;
hence contradiction by GOEDELCP:24;
end;
hence thesis;
end;
begin :: Upward Transfer of Consistency and Satisfiability
theorem Th19:
for p ex Al1 being countable QC-alphabet st p is Element of CQC-WFF(Al1)
& Al is Al1-expanding
proof
defpred P[Element of CQC-WFF(Al)] means ex Al1 being countable QC-alphabet
st $1 is Element of CQC-WFF(Al1) & Al is Al1-expanding;
A1: P[VERUM(Al)]
proof
set Al1 = [:NAT, NAT:];
reconsider Al1 as countable QC-alphabet by QC_LANG1:def 1,CARD_4:7;
NAT c= QC-symbols(Al) & Al = [:NAT,QC-symbols(Al):] by QC_LANG1:3,5;
then Al1 c= Al by ZFMISC_1:95;
then reconsider Al as Al1-expanding QC-alphabet by Def1;
VERUM(Al1) = VERUM(Al);
hence thesis;
end;
A2: for k,P,l holds P[P!l]
proof
let k,P,l;
bound_QC-variables(Al) c= QC-variables(Al) &
QC-variables(Al) c= [:NAT, QC-symbols(Al):] by QC_LANG1:4;
then bound_QC-variables(Al) c= [:NAT, QC-symbols(Al):];
then consider A,B being set such that
A3: A is finite & A c= NAT & B is finite & B c= QC-symbols(Al) &
rng l c= [:A,B:] by FINSET_1:13,XBOOLE_1:1;
[:A,B:] c= [:NAT,B:] by A3,ZFMISC_1:95;
then
A4: rng l c= [:NAT,B:] by A3;
set Al1 = [:NAT, NAT:] \/ [:NAT, {P`2}:] \/ [:NAT,B:];
[:NAT, NAT:] is countable & [:NAT, {P`2}:] is countable by CARD_4:7;
then
A5: [:NAT, NAT:] \/ [:NAT, {P`2}:] is countable & [:NAT,B:] is countable
by A3,CARD_2:85,CARD_4:7;
A6: Al1 = [:NAT, NAT \/ {P`2}:] \/ [:NAT,B:] by ZFMISC_1:97
.= [:NAT, NAT \/ {P`2} \/ B:] by ZFMISC_1:97;
NAT c= NAT \/ {P`2} & NAT \/ {P`2} c= NAT \/ {P`2} \/ B by XBOOLE_1:7;
then reconsider Al1 as countable QC-alphabet
by A5,A6,QC_LANG1:def 1,CARD_2:85,XBOOLE_1:1;
P in [:NAT,QC-symbols(Al):] by TARSKI:def 3,QC_LANG1:6;
then consider a,b being object such that
A7: a in NAT & b in QC-symbols(Al) & P = [a,b] by ZFMISC_1:def 2;
P`2 in QC-symbols(Al) by A7;
then {P`2} c= QC-symbols(Al) & NAT c= NAT & NAT c= QC-symbols(Al)
by QC_LANG1:3,ZFMISC_1:31;
then [:NAT,{P`2}:] c= [:NAT,QC-symbols(Al):] &
[:NAT,NAT:] c= [:NAT, QC-symbols(Al):] by ZFMISC_1:95;
then [:NAT,NAT:] \/ [:NAT,{P`2}:] c= [:NAT,QC-symbols(Al):]
& [:NAT,B:] c= [:NAT,QC-symbols(Al):] by A3,ZFMISC_1:95, XBOOLE_1:8;
then Al1 c= [:NAT,QC-symbols(Al):] by XBOOLE_1:8;
then Al1 c= Al by QC_LANG1:5;
then reconsider Al as Al1-expanding QC-alphabet by Def1;
[:NAT, NAT \/ {P`2} \/ B:] = [:NAT, QC-symbols(Al1):] by A6,QC_LANG1:5;
then
A8: QC-symbols(Al1) = NAT \/ {P`2} \/ B by ZFMISC_1:110;
set P2 = [a,b];
b = P`2 by A7;
then b in {P`2} by TARSKI:def 1;
then b in NAT \/ {P`2} by XBOOLE_0:def 3;
then reconsider b as QC-symbol of Al1 by A8,XBOOLE_0:def 3;
reconsider a as Element of NAT by A7;
A9: P`1 = 7 + the_arity_of P & P`1 = a by A7,QC_LANG1:def 8;
then 7 <= a by NAT_1:11;
then [a,b] in {[n,x] where x is QC-symbol of Al1 : 7 <= n};
then reconsider P2 as QC-pred_symbol of Al1;
P2`1 = 7 + k by A9,QC_LANG1:11;
then the_arity_of P2 = k by QC_LANG1:def 8;
then P2 in {Q where Q is QC-pred_symbol of Al1: the_arity_of Q = k};
then reconsider P2 as QC-pred_symbol of k,Al1;
set l2 = l;
for s being object st s in rng l2 holds s in bound_QC-variables(Al1)
proof
let s be object such that
A10: s in rng l2;
consider s1,s2 being object such that
A11: s1 in {4} & s2 in QC-symbols(Al) & s = [s1,s2] by A10,ZFMISC_1:def 2;
B c= QC-symbols(Al1) by A8,XBOOLE_1:7;
then
A12: [:NAT,B:] c= [:NAT,QC-symbols(Al1):] by ZFMISC_1:95;
s in [:NAT,B:] by A4,A10;
then consider s3,s4 being object such that
A13: s3 in NAT & s4 in QC-symbols(Al1) & s = [s3,s4] by A12,ZFMISC_1:def 2;
s = [s1,s4] by A11,A13,XTUPLE_0:1;
hence thesis by A11,A13,ZFMISC_1:def 2;
end;
then
A14: rng l2 c= bound_QC-variables(Al1);
reconsider l2 as CQC-variable_list of k,Al1
by A14,FINSEQ_1:def 4,XBOOLE_1:1;
P2!l2 = Al-Cast(P2!l2) .= Al-Cast(P2)!Al-Cast(l2) by Th8 .= P!l by A7;
then P!l is Element of CQC-WFF(Al1) & Al is Al1-expanding;
hence thesis;
end;
A15: for r st P[r] holds P['not' r]
proof
let r such that
A16: P[r];
consider Al1 being countable QC-alphabet such that
A17: r is Element of CQC-WFF(Al1) & Al is Al1-expanding by A16;
reconsider Al as Al1-expanding QC-alphabet by A17;
consider r2 being Element of CQC-WFF(Al1) such that
A18: r = r2 by A17;
'not' r2 = 'not' r by A18;
hence thesis by A17;
end;
A19: for r,s st P[r] & P[s] holds P[r '&' s]
proof
let r,s such that
A20: P[r] & P[s];
consider Al1, Al2 being countable QC-alphabet such that
A21: r is Element of CQC-WFF(Al1) & s is Element of CQC-WFF(Al2) &
Al is Al1-expanding & Al is Al2-expanding by A20;
set Al3 = Al1 \/ Al2;
Al1 = [:NAT,QC-symbols(Al1):] & Al2 =[:NAT,QC-symbols(Al2):] by QC_LANG1:5;
then
A22: Al3 = [:NAT, QC-symbols(Al1) \/ QC-symbols(Al2):] by ZFMISC_1:97;
NAT c= QC-symbols(Al1) \/ QC-symbols(Al2) by XBOOLE_1:10,QC_LANG1:3;
then reconsider Al3 as QC-alphabet by A22,QC_LANG1:def 1;
reconsider Al3 as countable Al1-expanding Al2-expanding QC-alphabet
by Def1,CARD_2:85,XBOOLE_1:7;
consider r2 being Element of CQC-WFF(Al1), s2 being Element of CQC-WFF(Al2)
such that
A23: r2 = r & s2 = s by A21;
reconsider r2 as Element of CQC-WFF(Al3) by Th7;
reconsider s2 as Element of CQC-WFF(Al3) by Th7;
Al1 c= Al & Al2 c= Al by A21;
then reconsider Al as Al3-expanding QC-alphabet by Def1,XBOOLE_1:8;
r2 '&' s2 = r '&' s by A23;
then r '&' s is Element of CQC-WFF(Al3) & Al is Al3-expanding;
hence thesis;
end;
for x,r st P[r] holds P[All(x,r)]
proof
let x,r such that
A24: P[r];
consider Al1 being countable QC-alphabet such that
A25: r is Element of CQC-WFF(Al1) & Al is Al1-expanding by A24;
consider s1,s2 being object such that
A26: s1 in {4} & s2 in QC-symbols(Al) & x = [s1,s2] by ZFMISC_1:def 2;
set Al2 = [:NAT, QC-symbols(Al1) \/ {s2}:];
A27: Al1 = [:NAT, QC-symbols(Al1):] & QC-symbols(Al1) c= QC-symbols(Al1)\/{s2}
& NAT c= QC-symbols(Al1) by QC_LANG1:3,5, XBOOLE_1:7;
then Al1 c= Al2 & NAT c= QC-symbols(Al1)\/{s2} by ZFMISC_1:95;
then reconsider Al2 as Al1-expanding QC-alphabet by Def1,QC_LANG1:def 1;
A28: Al2 = [:NAT, QC-symbols(Al1):] \/ [:NAT, {s2}:]
& [:NAT, QC-symbols(Al1):] c= Al by A25,A27,ZFMISC_1:97;
[:NAT, QC-symbols(Al1):] is countable & [:NAT, {s2}:] is countable
by QC_LANG1:5,CARD_4:7;
then reconsider Al2 as countable Al1-expanding QC-alphabet
by A28,CARD_2:85;
{s2} c= QC-symbols(Al) by A26,ZFMISC_1:31;
then [:NAT, {s2}:] c= [:NAT,QC-symbols(Al):] & Al = [:NAT,QC-symbols(Al):]
by QC_LANG1:5,ZFMISC_1:96;
then reconsider Al as Al2-expanding QC-alphabet by Def1,A28,XBOOLE_1:8;
consider r2 being Element of CQC-WFF(Al1) such that
A29: r = r2 by A25;
reconsider r2 as Element of CQC-WFF(Al2) by Th7;
A30: x = [4,s2] by A26,TARSKI:def 1;
Al2 = [:NAT,QC-symbols(Al2):] by QC_LANG1:5;
then QC-symbols(Al2) = QC-symbols(Al1) \/ {s2} & s2 in {s2}
by TARSKI:def 1,ZFMISC_1:110;
then s2 in QC-symbols(Al2) by XBOOLE_0:def 3;
then x is bound_QC-variable of Al2 by A30,ZFMISC_1:105;
then consider x2 being bound_QC-variable of Al2 such that
A31: x = x2;
All(x2,r2) = All(x,r) by A29,A31;
then All(x,r) is Element of CQC-WFF(Al2) & Al is Al2-expanding;
hence thesis;
end;
then
A32: for r,s,x,k,l,P holds P[VERUM(Al)] & P[P!l] & (P[r] implies P['not' r]) &
(P[r] & P[s] implies P[r '&' s]) & (P[r] implies P[All(x,r)])
by A1,A2,A15,A19;
for p holds P[p] from CQC_LANG:sch 1(A32);
hence thesis;
end;
theorem Th20:
for PHI being finite Subset of CQC-WFF(Al) ex Al1 being countable QC-alphabet
st PHI is finite Subset of CQC-WFF(Al1) & Al is Al1-expanding
proof
let PHI be finite Subset of CQC-WFF(Al);
defpred P[set] means $1 is finite Subset of CQC-WFF(Al) implies
ex Al1 being countable QC-alphabet st $1 is finite Subset of CQC-WFF(Al1) &
Al is Al1-expanding;
A1: PHI is finite;
A2: P[{}]
proof
set Al1 = [:NAT,NAT:];
reconsider Al1 as countable QC-alphabet by QC_LANG1:def 1,CARD_4:7;
Al = [:NAT,QC-symbols(Al):] & NAT c= QC-symbols(Al) by QC_LANG1:3,5;
then Al is Al1-expanding & {} is finite Subset of CQC-WFF(Al1) by
XBOOLE_1:2, ZFMISC_1:96;
hence thesis;
end;
A3: for x,B being set st x in PHI & B c= PHI & P[B] holds P[B\/{x}]
proof
let x,B be set such that
A4: x in PHI & B c= PHI & P[B];
reconsider x as Element of CQC-WFF(Al) by A4;
reconsider B as finite Subset of CQC-WFF(Al) by A4,XBOOLE_1:1;
consider Al1 being countable QC-alphabet such that
A5: x is Element of CQC-WFF(Al1) & Al is Al1-expanding by Th19;
consider Al2 being countable QC-alphabet such that
A6: B is finite Subset of CQC-WFF(Al2) & Al is Al2-expanding by A4;
set Al3 = Al1 \/ Al2;
Al1 = [:NAT,QC-symbols(Al1):] & Al2 =[:NAT,QC-symbols(Al2):] by QC_LANG1:5;
then
A7: Al3 = [:NAT, QC-symbols(Al1) \/ QC-symbols(Al2):] by ZFMISC_1:97;
NAT c= QC-symbols(Al1) \/ QC-symbols(Al2) by QC_LANG1:3,XBOOLE_1:10;
then reconsider Al3 as QC-alphabet by A7,QC_LANG1:def 1;
reconsider Al3 as countable Al1-expanding Al2-expanding QC-alphabet
by Def1,CARD_2:85,XBOOLE_1:7;
consider x2 being Element of CQC-WFF(Al1) such that
A8: x = x2 by A5;
for s being object st s in B holds s in CQC-WFF(Al3)
proof
let s be object such that
A9: s in B;
consider s2 being Element of CQC-WFF(Al2) such that
A10: s = s2 by A6,A9;
s2 is Element of CQC-WFF(Al3) by Th7;
hence s in CQC-WFF(Al3) by A10;
end;
then x2 is Element of CQC-WFF(Al3) & B c= CQC-WFF(Al3) by Th7;
then {x2} c= CQC-WFF(Al3) & B c= CQC-WFF(Al3) by ZFMISC_1:31;
then
A11: B \/ {x} c= CQC-WFF(Al3) by A8,XBOOLE_1:8;
Al1 c= Al & Al2 c= Al by A5,A6;
then Al is Al3-expanding QC-alphabet by Def1,XBOOLE_1:8;
hence thesis by A11;
end;
P[PHI] from FINSET_1:sch 2(A1,A2,A3);
hence thesis;
end;
registration
let Al;
let PHI be finite Subset of CQC-WFF(Al);
cluster still_not-bound_in PHI -> finite;
coherence
proof
deffunc snb(Element of CQC-WFF(Al)) = still_not-bound_in $1;
A1: for x being set st x in {snb(p) : p in PHI} holds x is finite
proof
let x be set such that
A2: x in {(still_not-bound_in p) : p in PHI};
ex p st x = still_not-bound_in p & p in PHI by A2;
hence x is finite by CQC_SIM1:19;
end;
A3: PHI is finite;
{snb(p) : p in PHI} is finite from FRAENKEL:sch 21(A3);
then union {snb(p) : p in PHI} is finite by A1,FINSET_1:7;
hence still_not-bound_in PHI is finite by GOEDELCP:def 8;
end;
end;
theorem Th21:
for THETA being Subset of CQC-WFF(Al2) st PHI = THETA holds
for A,J,v st J,v |= PHI
ex A2 being non empty set, J2 being interpretation of Al2,A2,
v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA
proof
let THETA be Subset of CQC-WFF(Al2) such that
A1: PHI = THETA;
let A,J,v such that
A2: J,v |= PHI;
set J2 = (QC-pred_symbols(Al2) --> empty_rel(A)) +* J;
A3: dom J = QC-pred_symbols(Al) & dom (QC-pred_symbols(Al2) --> empty_rel(A)) =
QC-pred_symbols(Al2) by FUNCT_2:def 1;
then dom J2 = QC-pred_symbols(Al) \/ QC-pred_symbols(Al2) by FUNCT_4:def 1;
then
A4: dom J2 = QC-pred_symbols(Al2) by Th3,XBOOLE_1:12;
J in Funcs(QC-pred_symbols(Al),relations_on A) by FUNCT_2:8;
then rng J c= relations_on A by FUNCT_2:92;
then (rng(QC-pred_symbols(Al2) --> empty_rel(A))) \/
(rng J) c= relations_on A & rng J2 c=(rng(QC-pred_symbols(Al2) -->
empty_rel(A)))\/(rng J) by FUNCT_4:17,XBOOLE_1:8;
then reconsider J2 as Function of QC-pred_symbols(Al2),relations_on A
by A4,FUNCT_2:2,XBOOLE_1:1;
A5: J = J2|QC-pred_symbols(Al) by A3,FUNCT_4:23;
for P2 being Element of QC-pred_symbols(Al2), r being Element of relations_on
A st J2.P2 = r holds r = empty_rel(A) or the_arity_of P2 = the_arity_of r
proof
let P2 be Element of QC-pred_symbols(Al2), r be Element of relations_on A
such that
A6: J2.P2 = r;
per cases;
suppose P2 in QC-pred_symbols(Al);
then consider P being QC-pred_symbol of Al such that
A7: P = P2;
A8: J.P = r by A3,A6,A7,FUNCT_4:13;
7 + the_arity_of P2 = P`1 by A7,QC_LANG1:def 8 .= 7 + the_arity_of P
by QC_LANG1:def 8;
hence thesis by A8,VALUAT_1:def 5;
end;
suppose not P2 in QC-pred_symbols(Al);
then not P2 in dom J by FUNCT_2:def 1;
then J2.P2 = (QC-pred_symbols(Al2) --> empty_rel(A)).P2 by FUNCT_4:11
.= empty_rel(A);
hence thesis by A6;
end;
end;
then reconsider J2 as interpretation of Al2,A by VALUAT_1:def 5;
set a = the Element of A;
set v2 = (bound_QC-variables(Al2) --> a) +* v;
v in Valuations_in(Al,A);
then v in Funcs(bound_QC-variables(Al),A) by VALUAT_1:def 1;
then
A9: dom v = bound_QC-variables(Al) & dom (bound_QC-variables(Al2) --> a) =
bound_QC-variables(Al2) by FUNCT_2:92;
then dom v2=bound_QC-variables(Al)\/bound_QC-variables(Al2) by FUNCT_4:def 1;
then
A10: dom v2 = bound_QC-variables(Al2) by Th4,XBOOLE_1:12;
v in Valuations_in(Al,A);
then v in Funcs(bound_QC-variables(Al),A) by VALUAT_1:def 1;
then rng v c= A by FUNCT_2:92;
then (rng (bound_QC-variables(Al2) --> a)) \/ (rng v) c= A &
rng v2 c= (rng (bound_QC-variables(Al2) --> a)) \/ (rng v)
by FUNCT_4:17, XBOOLE_1:8;
then reconsider v2 as Function of bound_QC-variables(Al2),A
by A10,FUNCT_2:2,XBOOLE_1:1;
A11: v = v2|bound_QC-variables(Al) by A9,FUNCT_4:23;
v2 in Funcs(bound_QC-variables(Al2),A) by FUNCT_2:8;
then reconsider v2 as Element of Valuations_in(Al2,A) by VALUAT_1:def 1;
for p2 being Element of CQC-WFF(Al2) st p2 in THETA holds J2,v2 |= p2
proof
let p2 be Element of CQC-WFF(Al2) such that
A12: p2 in THETA;
consider p such that
A13: p = p2 & p in PHI by A1,A12;
J,v |= p by A2,A13,CALCUL_1:def 11;
then J2,v2 |= Al2-Cast(p) by A5,A11,Th9;
hence thesis by A13;
end;
hence thesis by CALCUL_1:def 11;
end;
theorem Th22:
for CHI being Subset of CQC-WFF(Al) st CHI c= PHI holds CHI is Consistent
proof
let CHI be Subset of CQC-WFF(Al) such that
A1: CHI c= PHI;
assume CHI is Inconsistent;
then ex f being FinSequence of CQC-WFF(Al) st rng f c= CHI &
|- f^<*'not' VERUM(Al)*> by HENMODEL:def 1, GOEDELCP:24;
then PHI |- ('not' VERUM(Al)) by A1,HENMODEL:def 1,XBOOLE_1:1;
hence contradiction by GOEDELCP:24;
end;
theorem
PHI is Al2-Consistent
proof
let PSI be Subset of CQC-WFF(Al2) such that
A1: PHI = PSI;
for CHI being Subset of CQC-WFF(Al2) st CHI c= PSI & CHI is finite
holds CHI is Consistent
proof
let CHI be Subset of CQC-WFF(Al2) such that
A2: CHI c= PSI & CHI is finite;
reconsider CHI as finite Subset of CQC-WFF(Al) by A1,A2,XBOOLE_1:1;
consider Al1 being countable QC-alphabet such that
A3: CHI is finite Subset of CQC-WFF(Al1) & Al is Al1-expanding by Th20;
reconsider Al as Al1-expanding QC-alphabet by A3;
reconsider CHI as finite Subset of CQC-WFF(Al);
reconsider PHI as Consistent Subset of CQC-WFF(Al);
reconsider CHI as Consistent Subset of CQC-WFF(Al) by A1,A2,Th22;
CHI is Al1-Consistent by Th18;
then reconsider CHI as Consistent Subset of CQC-WFF(Al1) by A3;
still_not-bound_in CHI is finite;
then consider CZ being Consistent Subset of CQC-WFF(Al1), JH being
Henkin_interpretation of CZ such that
A4: JH,valH(Al1) |= CHI by GOEDELCP:34;
Al1 c= Al & Al c= Al2 by Def1;
then reconsider Al2 as Al1-expanding QC-alphabet by Def1,XBOOLE_1:1;
consider CHI2 being Subset of CQC-WFF(Al2) such that
A5: CHI = CHI2;
ex A being non empty set, J2 being interpretation of Al2,A, v2
being Element of Valuations_in(Al2,A) st J2,v2 |= CHI2 by A4,A5,Th21;
hence thesis by A5,HENMODEL:12;
end;
hence thesis by HENMODEL:7;
end;