:: The G\"odel Completeness Theorem for Uncountable Languages
:: 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,
ARYTM_3, RELAT_1, CARD_1, XXREAL_0, TARSKI, ZF_MODEL, REALSET1, ARYTM_1,
CARD_3, ZFMISC_1, FINSET_1, MCART_1, NAT_1, ORDINAL1, GOEDELCP, MARGREL1,
FUNCT_2, QC_TRANS, GOEDCPUC;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XXREAL_0, CARD_1,
CARD_3, FINSEQ_1, RELAT_1, QC_LANG1, QC_LANG2, ORDINAL1, NUMBERS,
CQC_THE1, CQC_LANG, FUNCT_1, FINSET_1, VALUAT_1, RELSET_1, FUNCT_2,
NAT_1, CQC_SIM1, DOMAIN_1, MCART_1, SUBSTUT1, SUBLEMMA, SUBSTUT2,
CALCUL_1, HENMODEL, GOEDELCP, MARGREL1, QC_LANG3, FUNCT_4, FUNCOP_1,
COHSP_1, QC_TRANS, XTUPLE_0;
constructors SETFAM_1, DOMAIN_1, XXREAL_0, NAT_1, NAT_D, FINSEQ_2, QC_LANG1,
CQC_THE1, CQC_SIM1, SUBSTUT2, CALCUL_1, HENMODEL, CARD_3, RELSET_1,
CARD_1, WELLORD2, GOEDELCP, VALUAT_1, MARGREL1, CQC_LANG, QC_LANG3,
FUNCT_4, FUNCOP_1, COHSP_1, QC_TRANS;
registrations SUBSET_1, RELAT_1, ORDINAL1, XREAL_0, FINSEQ_1, FINSET_1,
XBOOLE_0, QC_LANG1, CQC_LANG, QC_TRANS, XTUPLE_0, NAT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
equalities TARSKI;
expansions TARSKI;
theorems TARSKI, FUNCT_1, XBOOLE_0, XBOOLE_1, QC_LANG1, ZFMISC_1, QC_LANG2,
HENMODEL, CALCUL_1, SUBLEMMA, NAT_1, FINSEQ_1, VALUAT_1, FUNCT_2,
XXREAL_0, ORDINAL1, CARD_1, GOEDELCP, ORDERS_1, COHSP_1, QC_TRANS,
XTUPLE_0;
schemes NAT_1, FUNCT_1, CQC_LANG, FINSET_1;
begin :: Formula-Constant Extension
reserve Al for QC-alphabet,
PHI for Consistent Subset of CQC-WFF(Al),
PSI for 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 Element of NAT,
l for CQC-variable_list of k,Al,
P for QC-pred_symbol of k,Al,
x,y for bound_QC-variable of Al,
z for QC-symbol of Al,
Al2 for Al-expanding QC-alphabet;
definition
let Al;
let PHI be Subset of CQC-WFF(Al);
attr PHI is satisfiable means :Def1:
ex A,J,v st J,v |= PHI;
end;
reserve 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:
ex s being set st for p,x holds not [s,[x,p]] in QC-symbols(Al)
proof
assume
A1: for s being set holds ex p,x st [s,[x,p]] in QC-symbols(Al);
for s being set holds s in union union QC-symbols(Al)
proof
let s be set;
consider p,x such that
A2: [s,[x,p]] in QC-symbols(Al) by A1;
A3: {s} in {{s,[x,p]},{s}} by TARSKI:def 2;
A4: s in {s} by TARSKI:def 1;
{{s,[x,p]},{s}} c= union QC-symbols(Al) by A2,ZFMISC_1:74;
then {s} c= union union QC-symbols(Al) by A3,ZFMISC_1:74;
hence thesis by A4;
end;
then union union QC-symbols(Al) in union union QC-symbols(Al) &
for X being set holds not X in X;
hence contradiction;
end;
definition
let Al;
mode free_symbol of Al -> set means :Def2:
for p,x holds not [it,[x,p]] in QC-symbols(Al);
existence by Th1;
end;
definition
let Al;
func FCEx(Al) -> Al-expanding QC-alphabet equals
[:NAT, QC-symbols(Al) \/
the set of all [the free_symbol of Al,[x,p]] :];
coherence
proof
set Al2 = [:NAT, QC-symbols(Al) \/
the set of all [the free_symbol of Al,[x,p]] :];
set X = QC-symbols(Al)\/
the set of all [the free_symbol of Al,[x,p]] ;
Al2 is non empty set & NAT c= X & Al2 = [: NAT, X :]
by QC_LANG1:3,XBOOLE_1:10;
then reconsider Al2 as QC-alphabet by QC_LANG1:def 1;
[: NAT, QC-symbols(Al) :] c= [:NAT, QC-symbols(Al):] \/
[: NAT, the set of all [the free_symbol of Al,[x,p]] :]
by XBOOLE_1:7;
then [: NAT, QC-symbols(Al) :] c= [:NAT, X :] by ZFMISC_1:97;
then Al c= Al2 by QC_LANG1:5;
hence thesis by QC_TRANS:def 1;
end;
end;
definition
let Al,p,x;
func Example_of(p,x) -> bound_QC-variable of FCEx(Al) equals
[4,[the free_symbol of Al,[x,p]]];
coherence
proof
set Al2 = FCEx(Al);
[: NAT, QC-symbols(Al2) :] = [:NAT, QC-symbols(Al) \/
the set of all [the free_symbol of Al,[y,q]] :] by QC_LANG1:5;
then
A1: QC-symbols(Al2) = QC-symbols(Al) \/
the set of all [the free_symbol of Al,[y,q]] by ZFMISC_1:110;
[the free_symbol of Al,[x,p]] in
the set of all [the free_symbol of Al,[y,q]] ;
then
A2: [the free_symbol of Al,[x,p]] in QC-symbols(Al2) by A1, XBOOLE_0:def 3;
4 in {4} by TARSKI:def 1;
then [4, [the free_symbol of Al,[x,p]]] in [:{4},QC-symbols(Al2):]
by A2,ZFMISC_1:87;
hence thesis by QC_LANG1:def 4;
end;
end;
definition
let Al,p,x;
func Example_Formula_of(p,x) -> Element of CQC-WFF(FCEx(Al))
equals
('not' Ex((FCEx(Al))-Cast(x),(FCEx(Al))-Cast(p))) 'or'
(((FCEx(Al))-Cast(p)).((FCEx(Al))-Cast(x),Example_of(p,x)));
coherence;
end;
definition
let Al;
func Example_Formulae_of(Al) -> Subset of CQC-WFF(FCEx(Al)) equals
the set of all Example_Formula_of(p,x) ;
coherence
proof
for z being object st z in the set of all Example_Formula_of(p,x)
holds z in CQC-WFF(FCEx(Al))
proof
let z be object such that
A1: z in the set of all Example_Formula_of(p,x) ;
ex p,x st z = Example_Formula_of(p,x) by A1;
hence thesis;
end;
hence thesis by TARSKI:def 3;
end;
end;
theorem Th2:
for k being Element of NAT st k > 0 ex F being k-element FinSequence st
(for n being Nat st n <= k & 1 <= n holds F.n is QC-alphabet) &
F.1 = Al &
for n being Nat st n < k & 1 <= n holds
ex Al2 being QC-alphabet st F.n = Al2 & F.(n+1) = FCEx(Al2)
proof
defpred A[Nat] means $1 > 0 implies
ex F being $1-element FinSequence st
( for n being Nat st n <= $1 & 1 <= n holds F.n is QC-alphabet ) &
F.1 = Al & ( for n being Nat st n < $1 & 1 <= n holds
ex Al2 being QC-alphabet st F.n = Al2 & F.(n+1) = FCEx(Al2));
A1: for k being Nat st A[k] holds A[k+1]
proof
let k be Nat;
assume
A2: A[k];
per cases;
suppose
A3: k = 0;
A4: <*Al*> is 1-element FinSequence & <*Al*>.1 = Al;
A5: for n being Nat st
n < 1 & 1 <= n holds ex Al2 being QC-alphabet
st <*Al*>.n = Al2 & <*Al*>.(n+1) = FCEx(Al2);
for n being Nat st n<=1 & 1<=n holds <*Al*>.n is QC-alphabet
by A4,XXREAL_0:1;
hence thesis by A3,A4,A5;
end;
suppose
A6: k <> 0;
then consider F being k-element FinSequence such that
A7: ( for n being Nat st n <= k & 1 <= n holds F.n is QC-alphabet ) &
( F.1 = Al ) & ( for n being Nat st n < k & 1 <= n holds ex Al2 being
QC-alphabet st F.n = Al2 & F.(n+1) = FCEx(Al2)) by A2;
set K = F.k;
K is QC-alphabet
proof
per cases;
suppose k = 1;
hence thesis by A7;
end;
suppose
A8: k <> 1;
consider j being Nat such that
A9: k = j+1 by NAT_1:6, A6;
j <> 0 by A8,A9;
then j >= 1 & j < k by A9,NAT_1:25,19;
then ex Al2 being QC-alphabet st F.j = Al2 & F.(k) = FCEx(Al2)
by A7,A9;
hence thesis;
end;
end;
then reconsider K as QC-alphabet;
set K2 = <*FCEx(K)*>;
set F2 = F^K2;
reconsider F2 as (k+1)-element FinSequence;
A10: 1 <= k & len F = k by A6,NAT_1:25,CARD_1:def 7;
A11: for n being Nat st n < k & 1 <= n holds
ex Al2 being QC-alphabet st F2.n = Al2 & F2.(n+1) = FCEx(Al2)
proof
let n be Nat such that
A12: n < k & 1 <= n;
consider Al2 being QC-alphabet such that
A13: F.n = Al2 & F.(n+1) = FCEx(Al2) by A7,A12;
1 <= n+1 & n+1 <= k & k = len F by A12,NAT_1:13,CARD_1:def 7;
then F2.n = F.n & F2.(n+1) = F.(n+1) by A12,FINSEQ_1:64;
hence thesis by A13;
end;
A14: K is QC-alphabet & F2.k = K by A10,FINSEQ_1:64;
A15: for n being Nat st n < k+1 & 1 <= n holds
ex Al2 being QC-alphabet st F2.n = Al2 & F2.(n+1) = FCEx(Al2)
proof
let n be Nat such that
A16: n < k+1 & 1 <= n;
per cases;
suppose n <> k;
hence thesis by A11,A16,NAT_1:22;
end;
suppose n = k;
hence thesis by A10,A14,FINSEQ_1:42;
end;
end;
A17: for n being Nat st n <= k+1 & 1 <= n holds F2.n is QC-alphabet
proof
let n be Nat such that
A18: n <= k+1 & 1 <= n;
per cases;
suppose n <> k+1;
then n <= k by A18,NAT_1:8;
then F2.n = F.n & F.n is QC-alphabet by A7,A10,A18,FINSEQ_1:64;
hence thesis;
end;
suppose n = k +1;
hence thesis by A10,FINSEQ_1:42;
end;
end;
F2.1 = Al by A7,A10,FINSEQ_1:64;
hence thesis by A15,A17;
end;
end;
A19: A[0];
for n being Nat holds A[n] from NAT_1:sch 2(A19,A1);
hence thesis;
end;
definition
let Al;
let k be Nat;
mode FCEx-Sequence of Al,k -> (k+1)-element FinSequence means :Def7:
( for n being Nat st n <= (k+1) & 1 <= n holds it.n is QC-alphabet ) &
it.1 = Al &
( for n being Nat st n < (k+1) & 1 <= n holds
ex Al2 being QC-alphabet st it.n = Al2 & it.(n+1) = FCEx(Al2) );
existence by Th2;
end;
theorem Th3:
for k being Nat for S being FCEx-Sequence of Al,k holds
S.(k+1) is QC-alphabet
proof
let k be Nat;
let S be FCEx-Sequence of Al,k;
0 < 0 + (k + 1);
then 1 <= k + 1 & k + 1 <= k + 1 by NAT_1:19;
hence thesis by Def7;
end;
theorem Th4:
for k being Nat for S being FCEx-Sequence of Al,k holds
S.(k+1) is Al-expanding QC-alphabet
proof
let k be Nat;
let S be FCEx-Sequence of Al,k;
set Al2 = S.(k+1);
reconsider Al2 as QC-alphabet by Th3;
Al c= Al2
proof
let x be object;
assume
A1: x in Al;
defpred A[Nat] means $1 < k+1 implies x in S.($1+1);
A2: A[0] by A1,Def7;
A3: for l being Nat st A[l] holds A[l+1]
proof
let l be Nat;
assume
A4: A[l];
assume
A5: l+1 < k+1;
A6: for n being Nat st n+1 < (k+1) & 1 <= n+1 holds
ex Al2 being QC-alphabet st S.(n+1) = Al2 & S.(n+2) = FCEx(Al2)
proof
let n be Nat such that
A7: n + 1 < k + 1 & 1 <= n+1;
set m = n +1;
ex Al2 being QC-alphabet st S.(m) = Al2 & S.(m+1) = FCEx(Al2)
by Def7,A7;
hence thesis;
end;
0 < 0 + (l + 1);
then consider Al2 being QC-alphabet such that
A8: S.(l+1) = Al2 & S.(l+2) = FCEx(Al2) by A5,A6,NAT_1:19;
S.(l+1) c= S.(l+2) by A8,QC_TRANS:def 1;
hence thesis by A4,A5,NAT_1:16,XXREAL_0:2;
end;
for n being Nat holds A[n] from NAT_1:sch 2(A2,A3);
then k < k+1 implies x in S.(k+1);
hence thesis by NAT_1:13;
end;
hence thesis by QC_TRANS:def 1;
end;
definition
let Al;
let k be Nat;
func k-th_FCEx(Al) -> Al-expanding QC-alphabet equals
(the FCEx-Sequence of Al,k).(k+1);
coherence by Th4;
end;
definition
let Al,PHI;
mode EF-Sequence of Al,PHI -> Function means :Def9:
dom it = NAT & it.0 = PHI & for n being Nat holds
it.(n+1) = it.n \/ Example_Formulae_of(n-th_FCEx(Al));
existence
proof
deffunc F1() = PHI;
deffunc F2(Nat,set) = $2 \/ Example_Formulae_of($1-th_FCEx(Al));
ex f being Function st dom f = NAT & f.0 = F1() &
for n being Nat holds f.(n+1) = F2(n,f.n)
from NAT_1:sch 11;
hence thesis;
end;
end;
theorem Th5:
for k being Nat holds
FCEx(k-th_FCEx(Al)) = (k+1)-th_FCEx(Al)
proof
let k be Nat;
k+1+1 <= k+1+1 & 0 < 0 + (k + 1);
then k+1 < k+2 & 1 <= k+1 by NAT_1:19;
then consider Al2 being QC-alphabet such that
A1: (the FCEx-Sequence of Al,k+1).(k+1) = Al2 &
(the FCEx-Sequence of Al,k+1).(k+2) = FCEx(Al2) by Def7;
set X = (the FCEx-Sequence of Al,k+1).(k+1);
X = k-th_FCEx(Al)
proof
defpred A[Nat] means 0 < $1 & $1 <= k+1 implies
(the FCEx-Sequence of Al,k).$1 = (the FCEx-Sequence of Al,k+1).$1;
A2: A[0];
A3: for n being Nat st A[n] holds A[n+1]
proof
let n be Nat;
assume
A4: A[n];
per cases;
suppose
A5: (n+1) <= k+1;
per cases;
suppose
A6: n=0;
(the FCEx-Sequence of Al,k).1 = Al by Def7
.= (the FCEx-Sequence of Al,k+1).1 by Def7;
hence A[n+1] by A6;
end;
suppose
A7: n <> 0;
A8: 0 < 0 + n & n <= n+1 by A7,NAT_1:11;
0 < 0 + n by A7;
then
A9: 1 <= n by NAT_1:19;
A10: n < k+1 by A5,NAT_1:13;
then n < k+1+1 by NAT_1:13;
then
consider Al3 being QC-alphabet such that
A11: (the FCEx-Sequence of Al,k+1).n = Al3 &
(the FCEx-Sequence of Al,k+1).(n+1) = FCEx(Al3) by A9,Def7;
consider Al4 being QC-alphabet such that
A12: (the FCEx-Sequence of Al,k).n = Al4 &
(the FCEx-Sequence of Al,k).(n+1) = FCEx(Al4) by A9,A10,Def7;
thus A[n+1] by A4,A8,A11,A12,XXREAL_0:2;
end;
end;
suppose not n+1 <= k+1;
hence A[n+1];
end;
end;
for n being Nat holds A[n] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
hence thesis by A1;
end;
theorem Th6:
for k,n st n <= k holds n-th_FCEx(Al) c= k-th_FCEx(Al)
proof
let k;
defpred P[Nat] means $1 <= k implies ex j st j = k-$1 &
j-th_FCEx(Al) c= k-th_FCEx(Al);
A1: P[0];
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
A3: P[n];
per cases;
suppose
A4: n+1 <= k;
then consider j such that
A5: j = k-n & j-th_FCEx(Al) c= k-th_FCEx(Al) by A3,NAT_1:13;
set j2=k-(n+1);
reconsider j2 as Element of NAT by A4,NAT_1:21;
FCEx(j2-th_FCEx(Al)) = j-th_FCEx(Al) by A5,Th5;
then j2-th_FCEx(Al) c= j-th_FCEx(Al) by QC_TRANS:def 1;
hence thesis by A5,XBOOLE_1:1;
end;
suppose not n+1 <= k;
hence thesis;
end;
end;
A6: for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
let n such that
A7: n <= k;
set n2 = k - n;
reconsider n2 as Element of NAT by A7,NAT_1:21;
k = n + n2;
then consider n3 being Element of NAT such that
A8: n3 = k-n2 & n3-th_FCEx(Al) c= k-th_FCEx(Al) by A6,NAT_1:11;
thus thesis by A8;
end;
definition
let Al,PHI; let k be Nat;
func k-th_EF(Al,PHI) -> Subset of CQC-WFF(k-th_FCEx(Al)) equals
(the EF-Sequence of Al,PHI).k;
coherence
proof
defpred P[Nat] means (the EF-Sequence of Al,PHI).$1
is Subset of CQC-WFF($1-th_FCEx(Al));
A1: P[0]
proof
0-th_FCEx(Al) = Al by Def7;
hence thesis by Def9;
end;
A2: for n being Nat holds P[n] implies P[n+1]
proof
let n be Nat;
assume
A3: P[n];
set E = (the EF-Sequence of Al,PHI).(n+1);
set S = (the EF-Sequence of Al,PHI).n;
A4: Example_Formulae_of(n-th_FCEx(Al)) is Subset of
CQC-WFF(FCEx(n-th_FCEx(Al))) & FCEx(n-th_FCEx(Al)) = (n+1)-th_FCEx(Al)
by Th5;
S c= CQC-WFF(FCEx(n-th_FCEx(Al)))
proof
let p be object;
assume
A5: p in S;
reconsider p as Element of CQC-WFF(n-th_FCEx(Al)) by A3,A5;
p is Element of CQC-WFF(FCEx(n-th_FCEx(Al))) by QC_TRANS:7;
hence thesis;
end;
then S \/ Example_Formulae_of(n-th_FCEx(Al))c= CQC-WFF((n+1)-th_FCEx(Al))
by A4,XBOOLE_1:8;
hence thesis by Def9;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
end;
theorem Th7:
for r,s,x holds Al2-Cast(r 'or' s) = Al2-Cast(r) 'or' Al2-Cast(s) &
Al2-Cast(Ex(x,r)) = Ex(Al2-Cast(x),Al2-Cast(r))
proof
let r,s,x;
A1: Al2-Cast('not' r) = 'not' Al2-Cast(r) &
Al2-Cast('not' s) = 'not' Al2-Cast(s) by QC_TRANS:8;
thus Al2-Cast(r 'or' s)
= Al2-Cast('not' ('not' r '&' 'not' s)) by QC_LANG2:def 3
.= 'not' Al2-Cast('not' r '&' 'not' s) by QC_TRANS:8
.= 'not' ('not' Al2-Cast(r) '&' 'not' Al2-Cast(s)) by A1,QC_TRANS:8
.= Al2-Cast(r) 'or' Al2-Cast(s) by QC_LANG2:def 3;
thus Al2-Cast(Ex(x,r)) = Al2-Cast('not' All(x,'not' r)) by QC_LANG2:def 5
.= 'not' Al2-Cast(All(x,'not' r)) by QC_TRANS:8
.= 'not' All(Al2-Cast(x),Al2-Cast('not' r)) by QC_TRANS:8
.= 'not' All(Al2-Cast(x),'not' Al2-Cast(r)) by QC_TRANS:8
.= Ex(Al2-Cast(x),Al2-Cast(r)) by QC_LANG2:def 5;
end;
theorem Th8:
for p,q,A,J,v holds (J,v |= p or J,v |= q) iff J,v |= p 'or' q
proof
let p,q,A,J,v;
thus (J,v |= p or J,v |= q) implies J,v |= p 'or' q
proof
assume J,v |= p or J,v |= q;
then not J,v |= 'not' p or not J,v |= 'not' q by VALUAT_1:17;
then not J,v |= 'not' p '&' 'not' q by VALUAT_1:18;
then J,v |= 'not' ('not' p '&' 'not' q) by VALUAT_1:17;
hence thesis by QC_LANG2:def 3;
end;
thus J,v |= p 'or' q implies (J,v |= p or J,v |= q)
proof
assume J,v |= p 'or' q;
then J,v |= 'not' ('not' p '&' 'not' q) by QC_LANG2:def 3;
then not J,v |= 'not' p or not J,v |= 'not' q by VALUAT_1:17,18;
hence J,v |= p or J,v |= q by VALUAT_1:17;
end;
end;
:: Ebbinghaus Lemma 5.3.4
theorem Th9:
PHI \/ Example_Formulae_of(Al) is Consistent Subset of CQC-WFF(FCEx(Al))
proof
reconsider Al2 = FCEx(Al) as Al-expanding QC-alphabet;
for s being object st s in CQC-WFF(Al) holds s in CQC-WFF(Al2)
proof
let s be object;
assume s in CQC-WFF(Al);
then reconsider s as Element of CQC-WFF(Al);
s is Element of CQC-WFF(Al2) by QC_TRANS:7;
hence thesis;
end;
then
A1: CQC-WFF(Al) c= CQC-WFF(Al2);
then PHI c= CQC-WFF(Al2) & Example_Formulae_of(Al) c= CQC-WFF(Al2);
then reconsider B = PHI \/ Example_Formulae_of(Al) as Subset of CQC-WFF(Al2)
by XBOOLE_1:8;
B is Consistent
proof
assume B is Inconsistent;
then consider CHI2 being Subset of CQC-WFF(Al2) such that
A2: CHI2 c= B & CHI2 is finite & CHI2 is Inconsistent by HENMODEL:7;
reconsider CHI2 as finite Subset of CQC-WFF(Al2) by A2;
consider Al1 being countable QC-alphabet such that
A3: CHI2 is finite Subset of CQC-WFF(Al1) & Al2 is Al1-expanding
by QC_TRANS:20;
reconsider Al2 as Al1-expanding QC-alphabet by A3;
consider CHI1 being Subset of CQC-WFF(Al1) such that
A4: CHI1 = CHI2 by A3;
reconsider CHI1 as finite Subset of CQC-WFF(Al1) by A4;
set PHI1 = CHI1 /\ PHI;
PHI1 c= CHI1 & CHI1 c= CQC-WFF(Al1) by XBOOLE_1:18;
then reconsider PHI1 as Subset of CQC-WFF(Al1) by XBOOLE_1:1;
reconsider Al2 as Al-expanding QC-alphabet;
PHI is Subset of CQC-WFF(Al2) by A1,XBOOLE_1:1;
then consider PHIp being Subset of CQC-WFF(Al2) such that
A5: PHIp = PHI;
set PHI2 = CHI2 /\ PHIp;
reconsider PHI2 as Subset of CQC-WFF(Al2);
PHI1 is Consistent
proof
reconsider Al2 as Al1-expanding QC-alphabet;
PHI is Al2-Consistent by QC_TRANS:23;
then PHIp is Consistent & PHI2 c= PHIp by A5,QC_TRANS:def 2,XBOOLE_1:18;
then PHI2 is Consistent & PHI2 = PHI1 by A4,A5,QC_TRANS:22;
then PHI2 is Al1-Consistent by QC_TRANS:18;
hence PHI1 is Consistent by A4,A5,QC_TRANS:def 2;
end;
then reconsider PHI1 as Consistent Subset of CQC-WFF(Al1);
still_not-bound_in PHI1 is finite;
then consider CZ being Consistent Subset of CQC-WFF(Al1), JH being
Henkin_interpretation of CZ such that
A6: JH,valH(Al1) |= PHI1 by GOEDELCP:34;
consider A2 being non empty set, J2 being interpretation of Al2,A2,
v2 being Element of Valuations_in (Al2,A2) such that
A7: J2,v2 |= PHI2 by A4,A5,A6,QC_TRANS:21;
set Ex2 = CHI2 /\ Example_Formulae_of(Al);
reconsider Ex2 as Subset of CQC-WFF(Al2);
A8: CHI2 = CHI2 /\ (PHIp \/ Example_Formulae_of(Al)) by A2,A5,XBOOLE_1:28
.= PHI2 \/ Ex2 by XBOOLE_1:23;
ex A being non empty set, J being interpretation of Al2,A, v being Element
of Valuations_in(Al2,A) st J,v |= PHI2 \/ Ex2
proof
defpred P[set] means ex A being non empty set, J being interpretation of
Al2,A, v being Element of Valuations_in(Al2,A), Ex3 being Subset of
CQC-WFF(Al2) st Ex3 = $1 & J,v |= PHI2 \/ Ex3;
A9: Ex2 is finite;
J2,v2 |= PHI2 \/ {}CQC-WFF(Al2) by A7; then
A10: P[{}];
A11: for b,B being set st b in Ex2 & B c= Ex2 & P[B] holds P[B \/ {b}]
proof
let b,B be set such that
A12: b in Ex2 & B c= Ex2 & P[B];
reconsider B as Subset of CQC-WFF(Al2) by A12;
consider A being non empty set, J being interpretation of Al2,A, v
being Element of Valuations_in(Al2,A) such that
A13: J,v |= PHI2 \/ B by A12;
Ex2 c= Example_Formulae_of(Al) by XBOOLE_1:18;
then b in Example_Formulae_of(Al) by A12;
then consider p,x such that
A14: b = Example_Formula_of(p,x);
set fc = Example_of(p,x);
set x2 = Al2-Cast(x);
set p2 = Al2-Cast(p);
reconsider fc,x2 as bound_QC-variable of Al2;
reconsider p2 as Element of CQC-WFF(Al2);
reconsider b as Element of CQC-WFF(Al2) by A14;
A15: J,v |= b implies thesis
proof
assume
A16: J,v |= b;
for q2 being Element of CQC-WFF(Al2) st q2 in PHI2 \/ (B \/ {b})
holds J,v |= q2
proof
let q2 be Element of CQC-WFF(Al2);
assume q2 in PHI2 \/ (B \/ {b});
then q2 in (PHI2 \/ B) \/ {b} by XBOOLE_1:4;
then
A17: q2 in (PHI2 \/ B) or q2 in {b} by XBOOLE_0:def 3;
per cases;
suppose q2 in (PHI2 \/ B);
hence thesis by A13,CALCUL_1:def 11;
end;
suppose not q2 in (PHI2 \/ B);
hence thesis by A16,A17,TARSKI:def 1;
end;
end;
hence thesis by CALCUL_1:def 11;
end;
per cases;
suppose not J,v |= Ex(x2,p2);
then J,v |= 'not' Ex(x2,p2) by VALUAT_1:17;
hence thesis by A14,A15,Th8;
end;
suppose J,v |= Ex(x2,p2);
then consider a being Element of A such that
A18: J,v.(x2|a) |= p2 by GOEDELCP:9;
reconsider vp = v.(fc|a) as Element of Valuations_in(Al2,A);
A19: for p2 being Element of CQC-WFF(Al2) st p2 is Element of CQC-WFF(Al)
holds v|(still_not-bound_in p2) = vp|(still_not-bound_in p2)
proof
let p2 be Element of CQC-WFF(Al2);
assume p2 is Element of CQC-WFF(Al);
then consider pp being Element of CQC-WFF(Al) such that
A20: pp = p2;
not [the free_symbol of Al,[x,p]] in QC-symbols(Al) by Def2;
then not [4,[the free_symbol of Al,[x,p]]] in
[:{4},QC-symbols(Al):] by ZFMISC_1:87;
then not fc in bound_QC-variables(Al) by QC_LANG1:def 4;
then not fc in still_not-bound_in pp;
then not fc in still_not-bound_in Al2-Cast(pp) by QC_TRANS:12;
then not fc in still_not-bound_in p2 by A20,QC_TRANS:def 3;
hence v|(still_not-bound_in p2) = vp|(still_not-bound_in p2)
by CALCUL_1:26;
end;
p2 = p by QC_TRANS:def 3;
then v|(still_not-bound_in p2) = vp|(still_not-bound_in p2) by A19;
then v.(x2|a)|(still_not-bound_in p2) =
vp.(x2|a)|(still_not-bound_in p2) by SUBLEMMA:64;
then J,vp.(x2|a) |= p2 & vp.fc = a by A18,SUBLEMMA:49,68;
then
A21: J,vp |= p2.(x2,fc) by CALCUL_1:24;
for q2 being Element of CQC-WFF(Al2) st q2 in PHI2 \/ (B \/ {b})
holds J,vp |= q2
proof
let q2 be Element of CQC-WFF(Al2);
assume q2 in PHI2 \/ (B \/ {b});
then q2 in (PHI2 \/ B) \/ {b} by XBOOLE_1:4;
then
A22: q2 in (PHI2 \/ B) or q2 in {b} by XBOOLE_0:def 3;
per cases;
suppose
A23: q2 in PHI2;
then
A24: q2 in PHI2 \/ B by XBOOLE_0:def 3;
PHI2 c= PHI & PHI c= CQC-WFF(Al) by A5,XBOOLE_1:18;
then PHI2 c= CQC-WFF(Al);
then v|(still_not-bound_in q2) = vp|(still_not-bound_in q2)
& J,v |= q2 by A13,A19,A23,A24,CALCUL_1:def 11;
hence J,vp |= q2 by SUBLEMMA:68;
end;
suppose
A25: q2 in B;
B c= Example_Formulae_of(Al) by A12,XBOOLE_1:18;
then q2 in Example_Formulae_of(Al) by A25;
then consider r,y such that
A26: q2 = Example_Formula_of(r,y);
set fcr = Example_of(r,y);
set y2 = Al2-Cast(y);
set r2 = Al2-Cast(r);
reconsider fcr,y2 as bound_QC-variable of Al2;
reconsider r2 as Element of CQC-WFF(Al2);
per cases;
suppose fcr = fc;
then [the free_symbol of Al,[x,p]] =
[the free_symbol of Al,[y,r]] by XTUPLE_0:1;
then [x,p] = [y,r] by XTUPLE_0:1;
then r = p & x = y by XTUPLE_0:1;
hence thesis by A21,A26,Th8;
end;
suppose
A27: not fcr = fc;
A28: q2 in PHI2 \/ B by A25,XBOOLE_0:def 3;
per cases;
suppose
A29: J,v |= 'not' Ex(y2,r2);
set fml = 'not' Ex(y2,r2);
'not' Ex(y,r) = Al2-Cast('not' Ex(y,r)) by QC_TRANS:def 3
.= 'not' Al2-Cast(Ex(y,r)) by QC_TRANS:8
.= fml by Th7;
then v|(still_not-bound_in fml) =
vp|(still_not-bound_in fml) & J,v |= fml by A19,A29;
then J,vp |= fml by SUBLEMMA:68;
hence J,vp |= q2 by A26,Th8;
end;
suppose not J,v |= 'not' Ex(y2,r2);
then J,v |= r2.(y2,fcr) by A13,A26,A28,Th8,CALCUL_1:def 11;
then consider a2 being Element of A such that
A30: v.fcr = a2 & J,v.(y2|a2) |= r2 by CALCUL_1:24;
A31: vp.fcr = a2 by A27,A30,SUBLEMMA:48;
not [the free_symbol of Al,[x,p]] in QC-symbols(Al)
by Def2;
then not [4,[the free_symbol of Al,[x,p]]] in
[:{4},QC-symbols(Al):] by ZFMISC_1:87;
then not fc in bound_QC-variables(Al) by QC_LANG1:def 4;
then not fc in still_not-bound_in r;
then not fc in still_not-bound_in r2 by QC_TRANS:12;
then v.(fc|a)|still_not-bound_in r2 =
v|still_not-bound_in r2 by CALCUL_1:26;
then vp.(y2|a2)|still_not-bound_in r2 =
v.(y2|a2)|still_not-bound_in r2 by SUBLEMMA:64;
then J,vp.(y2|a2) |= r2 by A30,SUBLEMMA:68;
then J,vp |= r2.(y2,fcr) by A31,CALCUL_1:24;
hence thesis by A26,Th8;
end;
end;
end;
suppose not q2 in PHI2 & not q2 in B;
then q2 = b by A22,TARSKI:def 1,XBOOLE_0:def 3;
hence thesis by A14,A21,Th8;
end;
end;
hence thesis by CALCUL_1:def 11;
end;
end;
P[Ex2] from FINSET_1:sch 2(A9,A10,A11);
hence thesis;
end;
hence contradiction by A2,A8,HENMODEL:12;
end;
hence thesis;
end;
begin :: The Completeness Theorem
:: Ebbinghaus Lemma 5.3.1
theorem Th10:
ex Al2 being Al-expanding QC-alphabet,
PSI being Consistent Subset of CQC-WFF(Al2)
st PHI c= PSI & PSI is with_examples
proof
deffunc S(Nat) = $1-th_FCEx(Al);
deffunc PSI(Nat) = $1-th_EF(Al,PHI);
set Al2 = union the set of all S(n) ;
set PSI = union the set of all PSI(n) ;
A1: PHI c= PSI
proof
PHI = PSI(0) by Def9;
then PHI in the set of all PSI(n) ;
hence PHI c= PSI by ZFMISC_1:74;
end;
A2: Al c= Al2 & for n holds S(n) c= Al2
proof
Al = S(0) by Def7;
then Al in the set of all S(n) ;
hence Al c= Al2 by ZFMISC_1:74;
let n;
S(n) in the set of all S(k) ;
hence S(n) c= Al2 by ZFMISC_1:74;
end;
reconsider Al2 as non empty set by A2;
set Al2sym = union the set of all QC-symbols(S(n)) ;
NAT c= Al2sym & Al2 = [:NAT,Al2sym:]
proof
for s being object st s in Al2 holds s in [:NAT,Al2sym:]
proof
let s be object such that
A3: s in Al2;
consider P being set such that
A4: s in P & P in the set of all S(n) by A3,TARSKI:def 4;
consider n being Element of NAT such that
A5: P = S(n) by A4;
A6: for y being set st y in QC-symbols(S(n)) holds y in Al2sym
proof
let y be set such that
A7: y in QC-symbols(S(n));
QC-symbols(S(n)) in the set of all QC-symbols(S(k)) ;
hence y in Al2sym by A7,TARSKI:def 4;
end;
s in [:NAT,QC-symbols(S(n)):] by A5,A4,QC_LANG1:5;
then ex k , y being object st k in NAT & y in QC-symbols(S(n)) &
s = [k,y] by ZFMISC_1:def 2;
then ex k being set,y being set st k in NAT &y in Al2sym & s=[k,y] by A6;
hence thesis by ZFMISC_1:87;
end;
then
A8: Al2 c= [:NAT,Al2sym:];
QC-symbols(Al) = QC-symbols(S(0)) by Def7;
then QC-symbols(Al) in the set of all QC-symbols(S(n)) ;
then NAT c= QC-symbols(Al) & QC-symbols(Al) c= Al2sym
by QC_LANG1:3,ZFMISC_1:74;
hence NAT c= Al2sym;
for x being object st x in [:NAT,Al2sym:] holds x in Al2
proof
let x be object such that
A9: x in [:NAT,Al2sym:];
consider m,y being object such that
A10: m in NAT & y in Al2sym & x = [m,y] by A9,ZFMISC_1:def 2;
consider P being set such that
A11: y in P & P in the set of all QC-symbols(S(n)) by A10,TARSKI:def 4;
consider n being Element of NAT such that
A12: P = QC-symbols(S(n)) by A11;
[m,y] in [:NAT,QC-symbols(S(n)):] by A10,A11,A12,ZFMISC_1:87;
then
A13: [m,y] in S(n) by QC_LANG1:5;
S(n) c= Al2 by A2;
hence thesis by A10,A13;
end;
then [:NAT, Al2sym:] c= Al2;
hence Al2 = [:NAT, Al2sym:] by A8,XBOOLE_0:def 10;
end;
then reconsider Al2 as QC-alphabet by QC_LANG1:def 1;
reconsider Al2 as Al-expanding QC-alphabet by A2,QC_TRANS:def 1;
for p being object st p in PSI holds p in CQC-WFF(Al2)
proof
let p be object such that
A14: p in PSI;
consider P being set such that
A15: p in P & P in the set of all PSI(n) by A14,TARSKI:def 4;
consider n being Element of NAT such that
A16: P = PSI(n) by A15;
Al2 is S(n)-expanding QC-alphabet by A2,QC_TRANS:def 1;
then p is Element of CQC-WFF(Al2) by QC_TRANS:7,A15,A16;
hence thesis;
end;
then reconsider PSI as Subset of CQC-WFF(Al2) by TARSKI:def 3;
PSI is Consistent
proof
defpred C[Nat] means PSI($1) is Consistent & PSI($1) is Al2-Consistent;
A17: C[0]
proof
A18: PSI(0) = PHI by Def9;
PHI is Al2-Consistent by QC_TRANS:23;
then S(0) = Al & for S being Subset of CQC-WFF(Al2) st PSI(0) = S holds
S is Consistent by A18,Def7,QC_TRANS:def 2;
hence thesis by A18,QC_TRANS:def 2;
end;
A19: for n being Nat holds C[n] implies C[n+1]
proof
let n be Nat;
A20: FCEx(S(n)) = S(n+1) by Th5;
reconsider Al2 as S(n+1)-expanding QC-alphabet by A2,QC_TRANS:def 1;
assume C[n];
then reconsider PSIn = PSI(n) as Consistent Subset of CQC-WFF(S(n));
PSI(n+1) = PSIn \/ Example_Formulae_of(S(n)) by Def9;
then reconsider PSIn1 = PSI(n+1) as Consistent Subset of CQC-WFF(S(n+1))
by A20,Th9;
PSIn1 is Al2-Consistent by QC_TRANS:23;
hence thesis;
end;
A21: for n being Nat holds C[n] from NAT_1:sch 2(A17,A19);
A22: for n holds PSI(n) c= PSI
proof
let n;
let p be object such that
A23: p in PSI(n);
PSI(n) in the set of all PSI(k);
hence p in PSI by A23,TARSKI:def 4;
end;
A24: for n holds PSI(n) in bool CQC-WFF(Al2)
proof
let n;
PSI(n) c= PSI & PSI c= CQC-WFF(Al2) by A22;
then PSI(n) c= CQC-WFF(Al2);
hence thesis;
end;
consider f being Function such that
A25: dom f = NAT & for n holds f.n = PSI(n) from FUNCT_1:sch 4;
for y being object st y in rng f holds y in bool CQC-WFF(Al2)
proof
let y be object such that
A26: y in rng f;
consider x being object such that
A27: x in dom f & y = f.x by A26,FUNCT_1:def 3;
reconsider x as Element of NAT by A25,A27;
f.x = PSI(x) by A25;
hence thesis by A24,A27;
end;
then reconsider f as sequence of bool CQC-WFF(Al2)
by A25,FUNCT_2:2,TARSKI:def 3;
set PSIp = union rng f;
f in Funcs(NAT,bool CQC-WFF(Al2)) by FUNCT_2:8;
then union rng f c= union (bool CQC-WFF(Al2)) by ZFMISC_1:77,FUNCT_2:92;
then reconsider PSIp as Subset of CQC-WFF(Al2) by ZFMISC_1:81;
for n,m being Nat
st m in dom f & n in dom f & n < m holds f.n is Consistent &
f.n c= f.m
proof
let nn,mm be Nat such that
A28: mm in dom f & nn in dom f & nn < mm;
reconsider n = nn, m= mm as Element of NAT by ORDINAL1:def 12;
f.n is Subset of CQC-WFF(Al2) & f.n = PSI(n) & PSI(n) is Al2-Consistent
by A21,A25;
hence f.nn is Consistent by QC_TRANS:def 2;
defpred S[Nat] means
$1 <= m implies ex k st k=m-$1 & PSI(k) c= PSI(m);
A29: S[0];
A30: for k being Nat holds S[k] implies S[k+1]
proof
let k be Nat;
assume
A31: S[k];
set j1 = m-k;
set j2 = m-(k+1);
per cases;
suppose
A32: k+1 <= m;
then k <= m by NAT_1:13;
then reconsider j1,j2 as Element of NAT by A32,NAT_1:21;
PSI(j2+1) = (the EF-Sequence of Al,PHI).(j2)
\/ Example_Formulae_of(j2-th_FCEx(Al)) by Def9;
then PSI(j2) c= PSI(j1) & PSI(j1) c= PSI(m)
by A31,A32,NAT_1:13,XBOOLE_1:7;
hence thesis by XBOOLE_1:1;
end;
suppose not k+1<=m;
hence thesis;
end;
end;
A33: for k being Nat holds S[k] from NAT_1:sch 2(A29,A30);
set k = m-n;
reconsider k as Element of NAT by A28,NAT_1:21;
S[k] & k <= k+n by A33,NAT_1:11;
then PSI(n) c= PSI(m) & f.n = PSI(n) & f.m = PSI(m) by A25;
hence f.nn c= f.mm;
end;
then reconsider PSIp as Consistent Subset of CQC-WFF(Al2) by HENMODEL:11;
for y being object st y in the set of all PSI(n)
ex x being object st x in dom f & y = f.x
proof
let P be object such that
A34: P in the set of all PSI(n) ;
consider n such that
A35: P = PSI(n) by A34;
n in dom f & f.n = P by A25,A35;
hence thesis;
end;
then
A36: the set of all PSI(n) c= rng f by FUNCT_1:9;
for y being object st y in rng f holds y in the set of all PSI(n)
proof
let y be object such that
A37: y in rng f;
consider x being object such that
A38: x in dom f & y = f.x by A37,FUNCT_1:def 3;
reconsider x as Element of NAT by A25,A38;
f.x = PSI(x) by A25;
hence thesis by A38;
end;
then rng f c= the set of all PSI(n) ;
then PSIp = PSI by A36,XBOOLE_0:def 10;
hence thesis;
end;
then reconsider PSI as Consistent Subset of CQC-WFF(Al2);
set S = the set of all S(n) ;
S(0) in S;
then reconsider S as non empty set;
A39: for a,b being set st a in S & b in S holds ex c being set st
a \/ b c= c & c in S
proof
let a,b be set such that
A40: a in S & b in S;
consider i such that
A41: a = S(i) by A40;
consider j such that
A42: b = S(j) by A40;
per cases;
suppose j <= i;
then S(j) c= S(i) by Th6;
hence thesis by A40,A41,A42,XBOOLE_1:8;
end;
suppose not j <= i;
then S(i) c= S(j) by Th6;
hence thesis by A40,A41,A42,XBOOLE_1:8;
end;
end;
A43: for p being Element of CQC-WFF(Al2) holds ex n st
p is Element of CQC-WFF(S(n))
proof
defpred P[Element of CQC-WFF(Al2)] means ex n st $1 is Element of
CQC-WFF(S(n));
A44: P[VERUM(Al2)]
proof
reconsider Al2 as (S(0))-expanding QC-alphabet by A2,QC_TRANS:def 1;
VERUM(S(0)) in CQC-WFF(S(0));
then Al2-Cast(VERUM(S(0))) in CQC-WFF(S(0)) by QC_TRANS:def 3;
then VERUM(Al2) in CQC-WFF(S(0)) by QC_TRANS:8;
hence thesis;
end;
A45: for k being Nat
for P being QC-pred_symbol of k,Al2, l being CQC-variable_list
of k,Al2 holds P[P!l]
proof
let k be Nat;
let P be QC-pred_symbol of k,Al2, l be CQC-variable_list of k,Al2;
ex n st rng l c= bound_QC-variables(S(n)) & P is QC-pred_symbol of k,S(n)
proof
A46: rng l c= bound_QC-variables(Al2) & {P} c= QC-pred_symbols(Al2)
by ZFMISC_1:31;
bound_QC-variables(Al2) c= QC-variables(Al2)
& QC-variables(Al2) c= [:NAT,QC-symbols(Al2):] by QC_LANG1:4;
then
A47: bound_QC-variables(Al2) c= [:NAT,QC-symbols(Al2):] &
QC-pred_symbols(Al2) c= [:NAT,QC-symbols(Al2):]
by QC_LANG1:6;
then rng l c= [:NAT,QC-symbols(Al2):] & {P} c= [:NAT,QC-symbols(Al2):]
by A46;
then rng l c= Al2 & {P} c= Al2 by QC_LANG1:5;
then rng l \/ {P} c= union S & rng l \/ {P} is finite by XBOOLE_1:8;
then consider a being set such that
A48: a in S & rng l \/ {P} c= a by A39,COHSP_1:6,13;
consider n such that
A49: a = S(n) by A48;
take n;
A50: rng l c= rng l \/ {P} & {P} c= rng l \/ {P} by XBOOLE_1:7;
for s being object st s in rng l holds s in bound_QC-variables(S(n))
proof
let s be object such that
A51: s in rng l;
s in bound_QC-variables(Al2) by A51;
then s in [:{4}, QC-symbols(Al2):] by QC_LANG1:def 4;
then consider s1,s2 being object such that
A52: s1 in {4} & s2 in QC-symbols(Al2) & s = [s1,s2] by ZFMISC_1:def 2;
rng l c= S(n) & {P} c= S(n) by A48,A49,A50;
then s in S(n) by A51;
then s in [:NAT,QC-symbols(S(n)):] by QC_LANG1:5;
then consider s3,s4 being object such that
A53: s3 in NAT & s4 in QC-symbols(S(n)) & s = [s3,s4] by ZFMISC_1:def 2;
s = [s1,s4] by A52,A53,XTUPLE_0:1;
then s in [:{4},QC-symbols(S(n)):] by A52,A53,ZFMISC_1:def 2;
hence thesis by QC_LANG1:def 4;
end;
hence rng l c= bound_QC-variables(S(n));
thus P is QC-pred_symbol of k,S(n)
proof
P in [:NAT,QC-symbols(Al2):] by A47;
then consider p1,p2 being object such that
A54: p1 in NAT & p2 in QC-symbols(Al2) & P = [p1,p2] by ZFMISC_1:def 2;
rng l c= S(n) & P in S(n) by A48,A49,A50,ZFMISC_1:31;
then P in [:NAT,QC-symbols(S(n)):] by QC_LANG1:5;
then reconsider p2 as QC-symbol of S(n) by A54,ZFMISC_1:87;
A55: P`1 =(the_arity_of P)+7 by QC_LANG1:def 8 .= k + 7 by QC_LANG1:11;
reconsider p1 as Element of NAT by A54;
P`1=7 + the_arity_of P & P`1=p1 by A54,QC_LANG1:def 8;
then 7 <= p1 by NAT_1:11;
then [p1,p2] in
{[m,x] where m is Nat, x is QC-symbol of S(n):
7 <= m};
then reconsider P as QC-pred_symbol of S(n) by A54,QC_LANG1:def 7;
the_arity_of P = k by A55,QC_LANG1:def 8;
then P in {Q where Q is QC-pred_symbol of S(n): the_arity_of Q=k};
hence thesis by QC_LANG1:def 9;
end;
end;
then consider n such that
A56: rng l c= bound_QC-variables(S(n)) & P is QC-pred_symbol of k,S(n);
l is CQC-variable_list of k,S(n) by A56,FINSEQ_1:def 4,XBOOLE_1:1;
then consider l2 being CQC-variable_list of k,S(n), P2 being
QC-pred_symbol of k,S(n) such that
A57: l2 = l & P = P2 by A56;
reconsider Al2 as (S(n))-expanding QC-alphabet by A2,QC_TRANS:def 1;
A58: Al2-Cast(P2) = P & Al2-Cast(l2) = l by A57,QC_TRANS:def 5,def 6;
P2!l2 = Al2-Cast(P2!l2) by QC_TRANS:def 3 .= P!l by A58,QC_TRANS:8;
hence thesis;
end;
A59: for r being Element of CQC-WFF(Al2) st P[r] holds P['not' r]
proof
let r be Element of CQC-WFF(Al2);
assume P[r];
then consider n such that
A60: r is Element of CQC-WFF(S(n));
consider r2 being Element of CQC-WFF(S(n)) such that
A61: r = r2 by A60;
reconsider Al2 as (S(n))-expanding QC-alphabet by A2,QC_TRANS:def 1;
'not' r2 = Al2-Cast('not' r2) by QC_TRANS:def 3
.= 'not' Al2-Cast(r2) by QC_TRANS:8 .= 'not' r by A61,QC_TRANS:def 3;
hence thesis;
end;
A62: for r,s being Element of CQC-WFF(Al2) st P[r] & P[s] holds P[r '&' s]
proof
let r,s be Element of CQC-WFF(Al2);
assume P[r] & P[s];
then consider n,m such that
A63: r is Element of CQC-WFF(S(n)) & s is Element of CQC-WFF(S(m));
per cases;
suppose n <= m;
then reconsider Sm=S(m) as S(n)-expanding QC-alphabet
by Th6,QC_TRANS:def 1;
r is Element of CQC-WFF(Sm) by A63,QC_TRANS:7;
then consider r2,s2 being Element of CQC-WFF(Sm) such that
A64: r2 = r & s2 = s by A63;
reconsider Al2 as Sm-expanding QC-alphabet by A2,QC_TRANS:def 1;
A65: r = Al2-Cast(r2) & s = Al2-Cast(s2) by A64,QC_TRANS:def 3;
r2 '&' s2 = Al2-Cast(r2 '&' s2) by QC_TRANS:def 3
.= r '&' s by A65,QC_TRANS:8;
hence thesis;
end;
suppose not n <= m;
then reconsider Sn=S(n) as S(m)-expanding QC-alphabet
by Th6,QC_TRANS:def 1;
s is Element of CQC-WFF(Sn) by A63,QC_TRANS:7;
then consider r2,s2 being Element of CQC-WFF(Sn) such that
A66: r2 = r & s2 = s by A63;
reconsider Al2 as Sn-expanding QC-alphabet by A2,QC_TRANS:def 1;
A67: r = Al2-Cast(r2) & s = Al2-Cast(s2) by A66,QC_TRANS:def 3;
r2 '&' s2 = Al2-Cast(r2 '&' s2) by QC_TRANS:def 3
.= r '&' s by A67,QC_TRANS:8;
hence thesis;
end;
end;
for x being bound_QC-variable of Al2, r being Element of CQC-WFF(Al2) st
P[r] holds P[All(x,r)]
proof
let x be bound_QC-variable of Al2, r be Element of CQC-WFF(Al2);
x in QC-variables(Al2) & QC-variables(Al2) c= [:NAT,QC-symbols(Al2):]
by QC_LANG1:4;
then x in [:NAT,QC-symbols(Al2):] & Al2 = [:NAT,QC-symbols(Al2):]
by QC_LANG1:5;
then {x} c= union S & {x} is finite by ZFMISC_1:31;
then consider a being set such that
A68: a in S & {x} c= a by A39,COHSP_1:6,13;
consider n such that
A69: a = S(n) by A68;
assume P[r];
then consider m such that
A70: r is Element of CQC-WFF(S(m));
x in bound_QC-variables(Al2);
then x in [:{4},QC-symbols(Al2):] by QC_LANG1:def 4;
then consider x1,x2 being object such that
A71: x1 in {4} & x2 in QC-symbols(Al2) & x = [x1,x2] by ZFMISC_1:def 2;
A72: x in S(n) by A68,A69,ZFMISC_1:31;
per cases;
suppose
A73: n <= m;
then reconsider Sm=S(m) as S(n)-expanding QC-alphabet
by Th6,QC_TRANS:def 1;
S(n) c= S(m) by A73,Th6;
then x in S(m) by A72;
then x in [:NAT, QC-symbols(S(m)):] by QC_LANG1:5;
then consider x3,x4 being object such that
A74: x3 in NAT & x4 in QC-symbols(S(m)) & x = [x3,x4] by ZFMISC_1:def 2;
x = [x1,x4] by A71,A74,XTUPLE_0:1;
then x in [:{4},QC-symbols(Sm):] by A71,A74,ZFMISC_1:def 2;
then x is bound_QC-variable of Sm by QC_LANG1:def 4;
then consider x2 being bound_QC-variable of Sm, r2 being Element of
CQC-WFF(Sm) such that
A75: x2 = x & r2 = r by A70;
reconsider Al2 as Sm-expanding QC-alphabet by A2,QC_TRANS:def 1;
A76: r = Al2-Cast(r2) & x = Al2-Cast(x2) by A75,QC_TRANS:def 3,def 4;
All(x2,r2) = Al2-Cast(All(x2,r2)) by QC_TRANS:def 3
.= All(x,r) by A76,QC_TRANS:8;
hence thesis;
end;
suppose not n <= m;
then reconsider Sn=S(n) as S(m)-expanding QC-alphabet
by Th6,QC_TRANS:def 1;
x in [:NAT,QC-symbols(Sn):] by A72,QC_LANG1:5;
then consider x3,x4 being object such that
A77: x3 in NAT & x4 in QC-symbols(Sn) & x = [x3,x4] by ZFMISC_1:def 2;
x = [x1,x4] by A71,A77,XTUPLE_0:1;
then x in [:{4},QC-symbols(Sn):] by A71,A77,ZFMISC_1:def 2;
then x is bound_QC-variable of Sn & r is Element of CQC-WFF(Sn)
by A70,QC_TRANS:7,QC_LANG1:def 4;
then consider x2 being bound_QC-variable of Sn, r2 being Element of
CQC-WFF(Sn) such that
A78: x2 = x & r2 = r;
reconsider Al2 as Sn-expanding QC-alphabet by A2,QC_TRANS:def 1;
A79: r = Al2-Cast(r2) & x = Al2-Cast(x2) by A78,QC_TRANS:def 3,def 4;
All(x2,r2) = Al2-Cast(All(x2,r2)) by QC_TRANS:def 3
.= All(x,r) by A79,QC_TRANS:8;
hence thesis;
end;
end;
then
A80: for r,s being Element of CQC-WFF(Al2), x being bound_QC-variable of
Al2, k being Nat, l being CQC-variable_list of k,Al2,
P being QC-pred_symbol of k,Al2 holds P[VERUM(Al2)] & 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 A44,A45,A59,A62;
for p being Element of CQC-WFF(Al2) holds P[p] from CQC_LANG:sch 1(A80);
hence thesis;
end;
PSI is with_examples
proof
for x being bound_QC-variable of Al2, p being Element of CQC-WFF(Al2) holds
ex y be bound_QC-variable of Al2 st PSI |- ('not' Ex(x,p) 'or' (p.(x,y)))
proof
let x be bound_QC-variable of Al2, p be Element of CQC-WFF(Al2);
ex n st (x is bound_QC-variable of S(n) & p is Element of CQC-WFF(S(n)))
proof
consider m such that
A81: p is Element of CQC-WFF(S(m)) by A43;
x in QC-variables(Al2) & QC-variables(Al2) c= [:NAT,QC-symbols(Al2):]
by QC_LANG1:4;
then x in [:NAT,QC-symbols(Al2):] & Al2 = [:NAT,QC-symbols(Al2):]
by QC_LANG1:5;
then {x} c= union S & {x} is finite by ZFMISC_1:31;
then consider a being set such that
A82: a in S & {x} c= a by A39,COHSP_1:6,13;
consider n such that
A83: a = S(n) by A82;
x in bound_QC-variables(Al2);
then x in [:{4},QC-symbols(Al2):] by QC_LANG1:def 4;
then consider x1,x2 being object such that
A84: x1 in {4} & x2 in QC-symbols(Al2) & x = [x1,x2] by ZFMISC_1:def 2;
A85: x in S(n) by A82,A83,ZFMISC_1:31;
per cases;
suppose
A86: n <= m;
then reconsider Sm = S(m) as S(n)-expanding QC-alphabet by
Th6,QC_TRANS:def 1;
S(n) c= S(m) by A86,Th6;
then x in S(m) by A85;
then x in [:NAT, QC-symbols(S(m)):] by QC_LANG1:5;
then consider x3,x4 being object such that
A87: x3 in NAT & x4 in QC-symbols(S(m)) & x = [x3,x4] by ZFMISC_1:def 2;
x = [x1,x4] by A84,A87,XTUPLE_0:1;
then x in [:{4},QC-symbols(Sm):] by A84,A87,ZFMISC_1:def 2;
then x is bound_QC-variable of Sm by QC_LANG1:def 4;
hence thesis by A81;
end;
suppose not n <= m;
then reconsider Sn = S(n) as S(m)-expanding QC-alphabet by
Th6,QC_TRANS:def 1;
x in [:NAT, QC-symbols(S(n)):] by A85,QC_LANG1:5;
then consider x3,x4 being object such that
A88: x3 in NAT & x4 in QC-symbols(S(n)) & x = [x3,x4] by ZFMISC_1:def 2;
x = [x1,x4] by A84,A88,XTUPLE_0:1;
then x in [:{4},QC-symbols(Sn):] by A84,A88,ZFMISC_1:def 2;
then x is bound_QC-variable of Sn & p is Element of CQC-WFF(Sn)
by A81,QC_TRANS:7,QC_LANG1:def 4;
hence thesis;
end;
end;
then consider n such that
A89: x is bound_QC-variable of S(n) & p is Element of CQC-WFF(S(n));
A90: FCEx(S(n)) = S(n+1) by Th5;
A91: PSI(n+1) = PSI(n) \/ Example_Formulae_of(S(n)) by Def9;
consider x2 being bound_QC-variable of S(n), p2 being Element of
CQC-WFF(S(n)) such that
A92: x2 = x & p2 = p by A89;
Example_Formula_of(p2,x2) in Example_Formulae_of(S(n));
then
A93: Example_Formula_of(p2,x2) in PSI(n+1) by A91,XBOOLE_0:def 3;
S(n) c= S(n+1) by Th6,NAT_1:11;
then reconsider Sn1 = S(n+1) as S(n)-expanding QC-alphabet
by QC_TRANS:def 1;
set y2 = Example_of(p2,x2);
reconsider y2 as bound_QC-variable of Sn1 by Th5;
reconsider Al2 as Sn1-expanding QC-alphabet by A2,QC_TRANS:def 1;
y2 is bound_QC-variable of Al2 by TARSKI:def 3, QC_TRANS:4;
then consider y being bound_QC-variable of Al2 such that
A94: y = y2;
A95: Sn1-Cast(p2) = p & Sn1-Cast(x2) = x by A92,QC_TRANS:def 3,def 4;
then
A96: Al2-Cast(Sn1-Cast(p2)) = p & Al2-Cast(Sn1-Cast(x2)) = x
by QC_TRANS:def 3,def 4;
A97: Al2-Cast(Ex(Sn1-Cast(x2),Sn1-Cast(p2))) = Ex(x,p) by A96,Th7;
reconsider p as Element of CQC-WFF(Al2);
reconsider x as bound_QC-variable of Al2;
A98: (Sn1-Cast(p2)).(Sn1-Cast(x2),y2) = p.(x,y) by A94,A95,QC_TRANS:17;
A99: Example_Formula_of(p2,x2)
= Al2-Cast(('not' Ex(Sn1-Cast(x2), Sn1-Cast(p2))) 'or'
((Sn1-Cast(p2)).(Sn1-Cast(x2),y2))) by A90,QC_TRANS:def 3
.= Al2-Cast('not' Ex(Sn1-Cast(x2), Sn1-Cast(p2))) 'or'
Al2-Cast((Sn1-Cast(p2)).(Sn1-Cast(x2),y2)) by Th7
.= 'not' Al2-Cast(Ex(Sn1-Cast(x2), Sn1-Cast(p2))) 'or'
Al2-Cast((Sn1-Cast(p2)).(Sn1-Cast(x2),y2)) by QC_TRANS:8
.= 'not' Ex(x,p) 'or' p.(x,y) by A97,A98,QC_TRANS:def 3;
set example = 'not' Ex(x,p) 'or' p.(x,y);
reconsider example as Element of CQC-WFF(Al2);
reconsider PSI as Consistent Subset of CQC-WFF(Al2);
PSI(n+1) in the set of all PSI(m) ;
then PSI(n+1) c= PSI by ZFMISC_1:74;
hence thesis by A93,A99,GOEDELCP:21;
end;
hence thesis by GOEDELCP:def 2;
end;
hence thesis by A1;
end;
theorem Th11:
PHI \/ {p} is Consistent or PHI \/ {'not' p} is Consistent
proof
assume not PHI \/ {p} is Consistent & not PHI \/ {'not' p} is Consistent;
then PHI |- 'not' p & PHI |- p by HENMODEL:9,10;
hence contradiction by HENMODEL:def 2;
end;
:: Ebbinghaus Lemma 5.3.2
theorem Th12:
for PSI being Consistent Subset of CQC-WFF(Al)
ex THETA being Consistent Subset of CQC-WFF(Al)
st THETA is negation_faithful & PSI c= THETA
proof
let PSI be Consistent Subset of CQC-WFF(Al);
set U = { PHI : PSI c= PHI };
A1: PSI in U;
( for Z being set st Z c= U & Z is c=-linear holds ex Y being set st
( Y in U & ( for X being set st X in Z holds X c= Y ) ) )
proof
let Z be set such that
A2: Z c= U & Z is c=-linear;
per cases;
suppose
A3: Z is empty;
PSI in U & for X being set st X in Z holds X c= PSI by A3;
hence thesis;
end;
suppose
A4: Z is non empty;
set Y = union Z;
A5: PSI c= Y
proof
let z be object such that
A6: z in PSI;
consider X being object such that
A7: X in Z by A4, XBOOLE_0:7;
X in U by A2,A7;
then ex R being Consistent Subset of CQC-WFF(Al) st X = R & PSI c= R;
hence z in Y by A6,A7,TARSKI:def 4;
end;
A8: Y is Consistent Subset of CQC-WFF(Al)
proof
for X being set st X in Z holds X c= CQC-WFF(Al)
proof
let X be set such that
A9: X in Z;
X in U by A2,A9;
then ex R being Consistent Subset of CQC-WFF(Al) st X = R & PSI c= R;
hence X c= CQC-WFF(Al);
end;
then reconsider Y as Subset of CQC-WFF(Al) by ZFMISC_1:76;
Y is Consistent
proof
assume Y is Inconsistent;
then consider X being Subset of CQC-WFF(Al) such that
A10: X c= Y & X is finite & X is Inconsistent by HENMODEL:7;
ex Rs being finite Subset of Z st for x being set st x in X holds
ex R being set st R in Rs & x in R
proof
defpred R[set] means ex Rs being finite Subset of Z
st for x being set st x in $1 holds
ex R being set st R in Rs & x in R;
A11: R[ {} ]
proof
consider Rs being object such that
A12: Rs in Z by A4, XBOOLE_0:7;
set Rss = {Rs};
reconsider Rss as finite Subset of Z by A12,ZFMISC_1:31;
for x being set st x in {} ex R being set st R in Rss & x in R;
hence thesis;
end;
A13: for x,B being set st x in X & B c= X & R[B] holds R[B \/ {x}]
proof
let x,B being set such that
A14: x in X & B c= X & R[B];
consider Rs being finite Subset of Z such that
A15: for b being set st b in B holds ex R being set st
R in Rs & b in R by A14;
consider S being set such that
A16: (x in S & S in Z) by A10,A14,TARSKI:def 4;
set Rss = Rs \/ {S};
Rs c= Z & {S} c= Z by A16, ZFMISC_1:31;
then
A17: Rss c= Z by XBOOLE_1:8;
for y being set st y in B \/ {x} holds ex R being set
st R in Rss & y in R
proof
let y be set such that
A18: y in B \/ {x};
per cases by A18,XBOOLE_0:def 3;
suppose y in {x};
then
A19: y = x by TARSKI:def 1;
S in {S} by TARSKI:def 1;
then S in Rss by XBOOLE_0:def 3;
hence thesis by A16,A19;
end;
suppose y in B;
then consider R being set such that
A20: R in Rs & y in R by A15;
R in Rss by A20, XBOOLE_0:def 3;
hence thesis by A20;
end;
end;
hence thesis by A17;
end;
A21: X is finite by A10;
R[X] from FINSET_1:sch 2(A21,A11,A13);
hence thesis;
end;
then consider Rs being finite Subset of Z such that
A22: for x being set st x in X holds ex R being set st R in Rs & x in R;
defpred F[set] means $1 is non empty implies union $1 in $1;
A23: Rs is finite;
A24: F[{}];
A25: for x,B being set st x in Rs & B c= Rs & F[B] holds F[B \/ {x}]
proof
let x,B be set such that
A26: x in Rs & B c= Rs & F[B];
per cases;
suppose
A27: B is empty;
A28: union (B \/ {x}) = x by A27,ZFMISC_1:25;
thus thesis by A27,A28,TARSKI:def 1;
end;
suppose
A29: B is non empty;
per cases by A2,A26,A29,ORDINAL1:def 8,XBOOLE_0:def 9;
suppose
A30: x c= union B;
union (B \/ {x}) = union B \/ union {x} by ZFMISC_1:78
.= union B \/ x by ZFMISC_1:25
.= union B by A30,XBOOLE_1:12;
hence thesis by A26,A29,XBOOLE_0:def 3;
end;
suppose
A31: union B c= x;
A32: x in {x} by TARSKI:def 1;
union (B \/ {x}) = union B \/ union {x} by ZFMISC_1:78
.= union B \/ x by ZFMISC_1:25
.= x by A31, XBOOLE_1:12;
hence thesis by A32,XBOOLE_0:def 3;
end;
end;
end;
A33: F[Rs] from FINSET_1:sch 2(A23,A24,A25);
X is non empty
proof
assume
A34: X is empty;
X |- 'not' VERUM(Al) by A10,HENMODEL:6;
then X \/ {VERUM(Al)} is Inconsistent &
X \/ {VERUM(Al)} = {VERUM(Al)} by A34,HENMODEL:10;
hence contradiction by HENMODEL:13;
end;
then consider x being object such that
A35: x in X by XBOOLE_0:def 1;
ex R being set st R in Rs & x in R by A22,A35;
then union Rs in Z by A33;
then union Rs in U by A2;
then consider uRs being Consistent Subset of CQC-WFF(Al) such that
A36: union Rs = uRs & PSI c= uRs;
for x being object st x in X holds x in uRs
proof
let x be object such that
A37: x in X;
ex R being set st R in Rs & x in R by A22,A37;
hence thesis by A36,TARSKI:def 4;
end;
then
A38: X c= uRs;
consider f being FinSequence of CQC-WFF(Al) such that
A39: rng f c= X & |- f^<*'not' VERUM(Al)*>
by A10,HENMODEL:def 1, GOEDELCP:24;
rng f c= uRs by A38,A39;
hence contradiction by A39,HENMODEL:def 1,GOEDELCP:24;
end;
hence thesis;
end;
Y in U & for X being set st X in Z holds X c= Y by A5,A8,ZFMISC_1:74;
hence thesis;
end;
end;
then consider THETA being set such that
A40: (THETA in U & (for Z being set st Z in U & Z <> THETA holds
not THETA c= Z )) by A1,ORDERS_1:65; ::Zorns Lemma
A41: ex PHI st PHI = THETA & PSI c= PHI by A40;
then reconsider THETA as Consistent Subset of CQC-WFF(Al);
A42: for p holds (p in THETA or 'not' p in THETA)
proof
let p;
per cases by Th11;
suppose
A43: THETA \/ {p} is Consistent;
assume
A44: not p in THETA;
p in {p} by TARSKI:def 1;
then
A45: p in THETA \/ {p} & not p in THETA by XBOOLE_0:def 3, A44;
PSI c= THETA \/ {p} by A41,XBOOLE_1:10;
then THETA \/ {p} in U by A43;
hence thesis by A40,A45,XBOOLE_1:10;
end;
suppose
A46: THETA \/ {'not' p} is Consistent;
'not' p in THETA
proof
assume
A47: not ('not' p in THETA);
'not' p in {'not' p} by TARSKI:def 1;
then
A48: 'not' p in THETA \/ {'not' p} & not 'not' p in THETA
by XBOOLE_0:def 3, A47;
PSI c= THETA \/ {'not' p} by A41,XBOOLE_1:10;
then THETA \/ {'not' p} in U by A46;
hence thesis by A40,A48,XBOOLE_1:10;
end;
hence thesis;
end;
end;
for p holds THETA |- p or THETA |- 'not' p
proof
let p;
p in THETA or 'not' p in THETA by A42;
hence thesis by GOEDELCP:21;
end;
then THETA is negation_faithful by GOEDELCP:def 1;
hence thesis by A41;
end;
theorem Th13:
for THETA being Consistent Subset of CQC-WFF(Al)
st PHI c= THETA & PHI is with_examples holds THETA is with_examples
proof
let THETA be Consistent Subset of CQC-WFF(Al) such that
A1: PHI c= THETA & PHI is with_examples;
now
let x be bound_QC-variable of Al, p be Element of CQC-WFF(Al);
consider y being bound_QC-variable of Al such that
A2: PHI |- ('not' Ex(x,p) 'or' (p.(x,y))) by A1,GOEDELCP:def 2;
consider f being FinSequence of CQC-WFF(Al) such that
A3: rng f c= PHI & |- f^<*('not' Ex(x,p) 'or' (p.(x,y)))*>
by A2, HENMODEL:def 1;
take y;
thus THETA |- ('not' Ex(x,p) 'or' (p.(x,y)))
by A1,A3,HENMODEL:def 1,XBOOLE_1:1;
end;
hence thesis by GOEDELCP:def 2;
end;
:: Ebbinghaus Corollary 5.3.3
:: Model Existence Theorem
registration
let Al;
cluster Consistent -> satisfiable for Subset of CQC-WFF(Al);
coherence
proof
let PHI be Subset of CQC-WFF(Al);
assume
A1: PHI is Consistent;
then consider Al2 being Al-expanding QC-alphabet,
PSI being Consistent Subset of CQC-WFF(Al2) such that
A2: PHI c= PSI & PSI is with_examples by Th10;
consider THETA being Consistent Subset of CQC-WFF(Al2) such that
A3: THETA is negation_faithful & PSI c= THETA by Th12;
set JH =the Henkin_interpretation of THETA;
now
let p be Element of CQC-WFF(Al2);
A4: THETA is with_examples by Th13, A3, A2;
assume p in THETA;
then THETA |- p by GOEDELCP:21;
hence JH,valH(Al2) |= p by GOEDELCP:17,A3,A4;
end;
then JH,valH(Al2) |= THETA by CALCUL_1:def 11;
then ex A,J,v st J,v |= PHI by A1,A2,A3,QC_TRANS:10,XBOOLE_1:1;
hence thesis;
end;
end;
:: Completeness Theorem
theorem
PSI |= p implies PSI |- p
proof
set CHI = PSI \/ {'not' p};
assume A1: PSI |= p;
assume not PSI |- p;
then CHI is Consistent by HENMODEL:9;
then ex A,J,v st J,v |= CHI by Def1;
hence contradiction by GOEDELCP:37,A1;
end;