:: The G\"odel Completeness Theorem for Uncountable Languages
:: by Julian J. Schl\"oder and Peter Koepke
::
:: Received May 7, 2012
:: Copyright (c) 2012 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, NAT_1,
CARD_1, CARD_3, FINSEQ_1, RELAT_1, QC_LANG1, QC_LANG2, NUMBERS, CQC_THE1,
CQC_LANG, FUNCT_1, FINSET_1, VALUAT_1, RELSET_1, FUNCT_2, CQC_SIM1,
DOMAIN_1, MCART_1, SUBSTUT1, SUBLEMMA, SUBSTUT2, CALCUL_1, HENMODEL,
ORDINAL1, 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, FUNCT_1, ORDINAL1, XXREAL_0, XREAL_0,
HENMODEL, FINSEQ_1, FINSET_1, CARD_3, XBOOLE_0, QC_LANG1, CQC_LANG,
MARGREL1, VALUAT_1, CARD_1, GOEDELCP, FUNCT_4, FUNCOP_1, QC_TRANS,
XTUPLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0, GOEDELCP;
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 free_symbol of Al,[x,p]] : not contradiction} :];
coherence
proof
set Al2 = [:NAT, QC-symbols(Al) \/
{ [the free_symbol of Al,[x,p]] : not contradiction} :];
set X = QC-symbols(Al)\/
{ [the free_symbol of Al,[x,p]] : not contradiction};
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 free_symbol of Al,[x,p]] : not contradiction} :]
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 free_symbol of Al,[y,q]] : not contradiction} :] by QC_LANG1:5;
then
A1: QC-symbols(Al2) = QC-symbols(Al) \/
{ [the free_symbol of Al,[y,q]] : not contradiction} by ZFMISC_1:110;
[the free_symbol of Al,[x,p]] in
{ [the free_symbol of Al,[y,q]] : not contradiction };
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
{ Example_Formula_of(p,x) : not contradiction };
coherence
proof
for z being set st z in { Example_Formula_of(p,x) : not contradiction }
holds z in CQC-WFF(FCEx(Al))
proof
let z be set such that
A1: z in { Example_Formula_of(p,x) : not contradiction };
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 by FINSEQ_1:40;
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,NAT_1:2;
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;
A15: K is QC-alphabet & F2.k = K by A10,FINSEQ_1:64;
A16: 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
A17: n < k+1 & 1 <= n;
per cases;
suppose n <> k;
hence thesis by A11,A17,NAT_1:22;
end;
suppose n = k;
hence thesis by A10,A15,FINSEQ_1:42;
end;
end;
A18: for n being Nat st n <= k+1 & 1 <= n holds F2.n is QC-alphabet
proof
let n be Nat such that
A19: n <= k+1 & 1 <= n;
per cases;
suppose n <> k+1;
then n <= k by A19,NAT_1:8;
then F2.n = F.n & F.n is QC-alphabet by A7,A10,A19,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 A16,A18;
end;
end;
A20: A[0];
for n being Nat holds A[n] from NAT_1:sch 2(A20,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 NAT_1:5,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) by NAT_1:5;
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 set;
assume
A2: x in Al;
defpred A[Nat] means $1 < k+1 implies x in S.($1+1);
A3: A[0] by A2,Def7;
A4: for l being Nat st A[l] holds A[l+1]
proof
let l be Nat;
assume
A5: A[l];
assume
A6: l+1 < k+1;
A8: 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
A9: 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,A9;
hence thesis;
end;
0 < 0 + (l + 1) by NAT_1:5;
then consider Al2 being QC-alphabet such that
A10: S.(l+1) = Al2 & S.(l+2) = FCEx(Al2) by A6,A8,NAT_1:19;
S.(l+1) c= S.(l+2) by A10,QC_TRANS:def 1;
hence thesis by A5,A6,NAT_1:16,XXREAL_0:2;
end;
for n being Nat holds A[n] from NAT_1:sch 2(A3,A4);
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) by NAT_1:5;
then k+1 < k+2 & 1 <= k+1 by NAT_1:19;
then consider Al2 being QC-alphabet such that
A2: (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;
A4: A[0];
A5: for n being Nat st A[n] holds A[n+1]
proof
let n be Nat;
assume
A6: A[n];
per cases;
suppose
A7: (n+1) <= k+1;
per cases;
suppose
A8: 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 A8;
end;
suppose
A9: n <> 0;
A10: 0 < 0 + n & n <= n+1 by A9,NAT_1:11;
0 < 0 + n by A9,NAT_1:2;
then
A12: 1 <= n by NAT_1:19;
A13: n < k+1 by A7,NAT_1:13;
then n < k+1+1 by NAT_1:13;
then
consider Al3 being QC-alphabet such that
A15: (the FCEx-Sequence of Al,k+1).n = Al3 &
(the FCEx-Sequence of Al,k+1).(n+1) = FCEx(Al3) by A12,Def7;
consider Al4 being QC-alphabet such that
A16: (the FCEx-Sequence of Al,k).n = Al4 &
(the FCEx-Sequence of Al,k).(n+1) = FCEx(Al4) by A12,A13,Def7;
thus A[n+1] by A6,A10,A15,A16,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(A4,A5);
hence thesis by NAT_1:5;
end;
hence thesis by A2;
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;
A3: for n being Nat holds P[n] implies P[n+1]
proof
let n be Nat;
assume
A4: P[n];
set E = (the EF-Sequence of Al,PHI).(n+1);
set S = (the EF-Sequence of Al,PHI).n;
A5: 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 set;
assume
A6: p in S;
reconsider p as Element of CQC-WFF(n-th_FCEx(Al)) by A4,A6;
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 A5,XBOOLE_1:8;
hence thesis by Def9;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A1,A3);
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 set st s in CQC-WFF(Al) holds s in CQC-WFF(Al2)
proof
let s be set;
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) by TARSKI:def 3;
then PHI c= CQC-WFF(Al2) & Example_Formulae_of(Al) c= CQC-WFF(Al2)
by XBOOLE_1:1;
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
A7: 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 A7,QC_TRANS:def 2,XBOOLE_1:18;
then PHI2 is Consistent & PHI2 = PHI1 by A4,A7,QC_TRANS:22;
then PHI2 is Al1-Consistent by QC_TRANS:18;
hence PHI1 is Consistent by A4,A7,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
A9: 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
A10: J2,v2 |= PHI2 by A4,A7,A9,QC_TRANS:21;
set Ex2 = CHI2 /\ Example_Formulae_of(Al);
reconsider Ex2 as Subset of CQC-WFF(Al2);
A11: CHI2 = CHI2 /\ (PHIp \/ Example_Formulae_of(Al)) by A2,A7,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;
A12: Ex2 is finite;
J2,v2 |= PHI2 \/ {}CQC-WFF(Al2) by A10; then
A13: P[{}];
A14: 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
A15: b in Ex2 & B c= Ex2 & P[B];
reconsider B as Subset of CQC-WFF(Al2) by A15;
consider A being non empty set, J being interpretation of Al2,A, v
being Element of Valuations_in(Al2,A) such that
A16: J,v |= PHI2 \/ B by A15;
Ex2 c= Example_Formulae_of(Al) by XBOOLE_1:18;
then b in Example_Formulae_of(Al) by A15;
then consider p,x such that
A17: 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 A17;
A20: J,v |= b implies thesis
proof
assume
A21: 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
A22: q2 in (PHI2 \/ B) or q2 in {b} by XBOOLE_0:def 3;
per cases;
suppose q2 in (PHI2 \/ B);
hence thesis by A16,CALCUL_1:def 11;
end;
suppose not q2 in (PHI2 \/ B);
hence thesis by A21,A22,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 A17,A20,Th8;
end;
suppose J,v |= Ex(x2,p2);
then consider a being Element of A such that
A23: J,v.(x2|a) |= p2 by GOEDELCP:9;
reconsider vp = v.(fc|a) as Element of Valuations_in(Al2,A);
A24: 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
A25: 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 A25,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 A24;
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 A23,SUBLEMMA:49,68;
then
A27: 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
A28: q2 in (PHI2 \/ B) or q2 in {b} by XBOOLE_0:def 3;
per cases;
suppose
A29: q2 in PHI2;
then
A30: q2 in PHI2 \/ B by XBOOLE_0:def 3;
PHI2 c= PHI & PHI c= CQC-WFF(Al) by A7,XBOOLE_1:18;
then PHI2 c= CQC-WFF(Al) by XBOOLE_1:1;
then v|(still_not-bound_in q2) = vp|(still_not-bound_in q2)
& J,v |= q2 by A16,A24,A29,A30,CALCUL_1:def 11;
hence J,vp |= q2 by SUBLEMMA:68;
end;
suppose
A31: q2 in B;
B c= Example_Formulae_of(Al) by A15,XBOOLE_1:18;
then q2 in Example_Formulae_of(Al) by A31;
then consider r,y such that
A32: 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 A27,A32,Th8;
end;
suppose
A35: not fcr = fc;
A36: q2 in PHI2 \/ B by A31,XBOOLE_0:def 3;
per cases;
suppose
A37: 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 A24,A37;
then J,vp |= fml by SUBLEMMA:68;
hence J,vp |= q2 by A32,Th8;
end;
suppose not J,v |= 'not' Ex(y2,r2);
then J,v |= r2.(y2,fcr) by A16,A32,A36,Th8,CALCUL_1:def 11;
then consider a2 being Element of A such that
A38: v.fcr = a2 & J,v.(y2|a2) |= r2 by CALCUL_1:24;
A39: vp.fcr = a2 by A35,A38,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 A38,SUBLEMMA:68;
then J,vp |= r2.(y2,fcr) by A39,CALCUL_1:24;
hence thesis by A32,Th8;
end;
end;
end;
suppose not q2 in PHI2 & not q2 in B;
then q2 = b by A28,TARSKI:def 1,XBOOLE_0:def 3;
hence thesis by A17,A27,Th8;
end;
end;
hence thesis by CALCUL_1:def 11;
end;
end;
P[Ex2] from FINSET_1:sch 2(A12,A13,A14);
hence thesis;
end;
hence contradiction by A2,A11,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 {S(n) : not contradiction};
set PSI = union {PSI(n) : not contradiction};
A1: PHI c= PSI
proof
PHI = PSI(0) by Def9;
then PHI in {PSI(n) : not contradiction};
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 {S(n) : not contradiction};
hence Al c= Al2 by ZFMISC_1:74;
let n;
S(n) in {S(k) : not contradiction};
hence S(n) c= Al2 by ZFMISC_1:74;
end;
reconsider Al2 as non empty set by A2;
set Al2sym = union {QC-symbols(S(n)) : not contradiction};
NAT c= Al2sym & Al2 = [:NAT,Al2sym:]
proof
for s being set st s in Al2 holds s in [:NAT,Al2sym:]
proof
let s be set such that
A4: s in Al2;
consider P being set such that
A5: s in P & P in {S(n) : not contradiction} by A4,TARSKI:def 4;
consider n being Element of NAT such that
A6: P = S(n) by A5;
A7: for y being set st y in QC-symbols(S(n)) holds y in Al2sym
proof
let y be set such that
A8: y in QC-symbols(S(n));
QC-symbols(S(n)) in {QC-symbols(S(k)) : not contradiction};
hence y in Al2sym by A8,TARSKI:def 4;
end;
s in [:NAT,QC-symbols(S(n)):] by A6,A5,QC_LANG1:5;
then ex k being set, y being set 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 A7;
hence thesis by ZFMISC_1:87;
end;
then
A9: Al2 c= [:NAT,Al2sym:] by TARSKI:def 3;
QC-symbols(Al) = QC-symbols(S(0)) by Def7;
then QC-symbols(Al) in {QC-symbols(S(n)) : not contradiction};
then NAT c= QC-symbols(Al) & QC-symbols(Al) c= Al2sym
by QC_LANG1:3,ZFMISC_1:74;
hence NAT c= Al2sym by XBOOLE_1:1;
for x being set st x in [:NAT,Al2sym:] holds x in Al2
proof
let x be set such that
A10: x in [:NAT,Al2sym:];
consider m,y being set such that
A11: m in NAT & y in Al2sym & x = [m,y] by A10,ZFMISC_1:def 2;
consider P being set such that
A12: y in P & P in {QC-symbols(S(n)) : not contradiction} by A11,TARSKI:def 4;
consider n being Element of NAT such that
A13: P = QC-symbols(S(n)) by A12;
[m,y] in [:NAT,QC-symbols(S(n)):] by A11,A12,A13,ZFMISC_1:87;
then
A14: [m,y] in S(n) by QC_LANG1:5;
S(n) c= Al2 by A2;
hence thesis by A11,A14;
end;
then [:NAT, Al2sym:] c= Al2 by TARSKI:def 3;
hence Al2 = [:NAT, Al2sym:] by A9,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 set st p in PSI holds p in CQC-WFF(Al2)
proof
let p be set such that
A15: p in PSI;
consider P being set such that
A16: p in P & P in {PSI(n) : not contradiction} by A15,TARSKI:def 4;
consider n being Element of NAT such that
A17: P = PSI(n) by A16;
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,A16,A17;
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;
A19: C[0]
proof
A20: 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 A20,Def7,QC_TRANS:def 2;
hence PSI(0) is Consistent & PSI(0) is Al2-Consistent by QC_TRANS:def 2;
end;
A21: for n being Nat holds C[n] implies C[n+1]
proof
let n be Nat;
A22: 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 A22,Th9;
PSIn1 is Al2-Consistent by QC_TRANS:23;
hence thesis;
end;
A23: for n being Nat holds C[n] from NAT_1:sch 2(A19,A21);
A24: for n holds PSI(n) c= PSI
proof
let n;
let p be set such that
A25: p in PSI(n);
PSI(n) in {PSI(k):not contradiction};
hence p in PSI by A25,TARSKI:def 4;
end;
A26: for n holds PSI(n) in bool CQC-WFF(Al2)
proof
let n;
PSI(n) c= PSI & PSI c= CQC-WFF(Al2) by A24;
then PSI(n) c= CQC-WFF(Al2) by XBOOLE_1:1;
hence thesis;
end;
consider f being Function such that
A27: dom f = NAT & for n holds f.n = PSI(n) from FUNCT_1:sch 4;
for y being set st y in rng f holds y in bool CQC-WFF(Al2)
proof
let y be set such that
A28: y in rng f;
consider x being set such that
A29: x in dom f & y = f.x by A28,FUNCT_1:def 3;
reconsider x as Element of NAT by A27,A29;
f.x = PSI(x) by A27;
hence thesis by A26,A29;
end;
then reconsider f as Function of NAT,bool CQC-WFF(Al2)
by A27,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 st m in dom f & n in dom f & n < m holds f.n is Consistent &
f.n c= f.m
proof
let n,m such that
A30: m in dom f & n in dom f & n < m;
f.n is Subset of CQC-WFF(Al2) & f.n = PSI(n) & PSI(n) is Al2-Consistent
by A23,A27;
hence f.n 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);
A31: S[0];
A32: for k being Nat holds S[k] implies S[k+1]
proof
let k be Nat;
assume
A33: S[k];
set j1 = m-k;
set j2 = m-(k+1);
per cases;
suppose
A34: k+1 <= m;
then k <= m by NAT_1:13;
then reconsider j1,j2 as Element of NAT by A34,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 A33,A34,NAT_1:13,XBOOLE_1:7;
hence thesis by XBOOLE_1:1;
end;
suppose not k+1<=m;
hence thesis;
end;
end;
A37: for k being Nat holds S[k] from NAT_1:sch 2(A31,A32);
set k = m-n;
reconsider k as Element of NAT by A30,NAT_1:21;
S[k] & k <= k+n by A37,NAT_1:11;
then PSI(n) c= PSI(m) & f.n = PSI(n) & f.m = PSI(m) by A27;
hence f.n c= f.m;
end;
then reconsider PSIp as Consistent Subset of CQC-WFF(Al2) by HENMODEL:11;
for y being set st y in {PSI(n): not contradiction} holds ex x being set
st (x in dom f & y = f.x)
proof
let P be set such that
A38: P in {PSI(n) : not contradiction};
consider n such that
A39: P = PSI(n) by A38;
n in dom f & f.n = P by A27,A39;
hence thesis;
end;
then
A40: {PSI(n) : not contradiction} c= rng f by FUNCT_1:9;
for y being set st y in rng f holds y in {PSI(n) : not contradiction}
proof
let y be set such that
A41: y in rng f;
consider x being set such that
A42: x in dom f & y = f.x by A41,FUNCT_1:def 3;
reconsider x as Element of NAT by A27,A42;
f.x = PSI(x) by A27;
hence thesis by A42;
end;
then rng f c= {PSI(n) : not contradiction} by TARSKI:def 3;
then PSIp = PSI by A40,XBOOLE_0:def 10;
hence thesis;
end;
then reconsider PSI as Consistent Subset of CQC-WFF(Al2);
set S = {S(n) : not contradiction};
S(0) in S;
then reconsider S as non empty set;
A46: 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
A43: a in S & b in S;
consider i such that
A44: a = S(i) by A43;
consider j such that
A45: b = S(j) by A43;
per cases;
suppose j <= i;
then S(j) c= S(i) by Th6;
hence thesis by A43,A44,A45,XBOOLE_1:8;
end;
suppose not j <= i;
then S(i) c= S(j) by Th6;
hence thesis by A43,A44,A45,XBOOLE_1:8;
end;
end;
A47: 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));
A48: 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;
A49: for k for P being QC-pred_symbol of k,Al2, l being CQC-variable_list
of k,Al2 holds P[P!l]
proof
let k;
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
A50: 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
A51: bound_QC-variables(Al2) c= [:NAT,QC-symbols(Al2):] &
QC-pred_symbols(Al2) c= [:NAT,QC-symbols(Al2):]
by QC_LANG1:6,XBOOLE_1:1;
then rng l c= [:NAT,QC-symbols(Al2):] & {P} c= [:NAT,QC-symbols(Al2):]
by A50,XBOOLE_1:1;
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
A52: a in S & rng l \/ {P} c= a by A46,COHSP_1:6,13;
consider n such that
A53: a = S(n) by A52;
take n;
A54: rng l c= rng l \/ {P} & {P} c= rng l \/ {P} by XBOOLE_1:7;
for s being set st s in rng l holds s in bound_QC-variables(S(n))
proof
let s be set such that
A55: s in rng l;
s in bound_QC-variables(Al2) by A55;
then s in [:{4}, QC-symbols(Al2):] by QC_LANG1:def 4;
then consider s1,s2 being set such that
A56: 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 A52,A53,A54,XBOOLE_1:1;
then s in S(n) by A55;
then s in [:NAT,QC-symbols(S(n)):] by QC_LANG1:5;
then consider s3,s4 being set such that
A57: s3 in NAT & s4 in QC-symbols(S(n)) & s = [s3,s4] by ZFMISC_1:def 2;
s = [s1,s4] by A56,A57,XTUPLE_0:1;
then s in [:{4},QC-symbols(S(n)):] by A56,A57,ZFMISC_1:def 2;
hence thesis by QC_LANG1:def 4;
end;
hence rng l c= bound_QC-variables(S(n)) by TARSKI:def 3;
thus P is QC-pred_symbol of k,S(n)
proof
P in [:NAT,QC-symbols(Al2):] by A50,A51,ZFMISC_1:31,XBOOLE_1:1;
then consider p1,p2 being set such that
A58: 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 A52,A53,A54,ZFMISC_1:31,XBOOLE_1:1;
then P in [:NAT,QC-symbols(S(n)):] by QC_LANG1:5;
then reconsider p2 as QC-symbol of S(n) by A58,ZFMISC_1:87;
A59: 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 A58;
P`1=7 + the_arity_of P & P`1=p1 by A58,QC_LANG1:def 8,XTUPLE_0:def 2;
then 7 <= p1 by NAT_1:11;
then [p1,p2] in {[m,x] where x is QC-symbol of S(n): 7 <= m};
then reconsider P as QC-pred_symbol of S(n) by A58,QC_LANG1:def 7;
the_arity_of P = k by A59,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
A60: 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 A60,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
A61: l2 = l & P = P2 by A60;
reconsider Al2 as (S(n))-expanding QC-alphabet by A2,QC_TRANS:def 1;
A62: Al2-Cast(P2) = P & Al2-Cast(l2) = l by A61,QC_TRANS:def 5,def 6;
P2!l2 = Al2-Cast(P2!l2) by QC_TRANS:def 3 .= P!l by A62,QC_TRANS:8;
hence thesis;
end;
A63: 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
A64: r is Element of CQC-WFF(S(n));
consider r2 being Element of CQC-WFF(S(n)) such that
A65: r = r2 by A64;
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 A65,QC_TRANS:def 3;
hence thesis;
end;
A66: 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
A67: 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 A67,QC_TRANS:7;
then consider r2,s2 being Element of CQC-WFF(Sm) such that
A68: r2 = r & s2 = s by A67;
reconsider Al2 as Sm-expanding QC-alphabet by A2,QC_TRANS:def 1;
A69: r = Al2-Cast(r2) & s = Al2-Cast(s2) by A68,QC_TRANS:def 3;
r2 '&' s2 = Al2-Cast(r2 '&' s2) by QC_TRANS:def 3
.= r '&' s by A69,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 A67,QC_TRANS:7;
then consider r2,s2 being Element of CQC-WFF(Sn) such that
A70: r2 = r & s2 = s by A67;
reconsider Al2 as Sn-expanding QC-alphabet by A2,QC_TRANS:def 1;
A71: r = Al2-Cast(r2) & s = Al2-Cast(s2) by A70,QC_TRANS:def 3;
r2 '&' s2 = Al2-Cast(r2 '&' s2) by QC_TRANS:def 3
.= r '&' s by A71,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
A72: a in S & {x} c= a by A46,COHSP_1:6,13;
consider n such that
A73: a = S(n) by A72;
assume P[r];
then consider m such that
A74: 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 set such that
A75: x1 in {4} & x2 in QC-symbols(Al2) & x = [x1,x2] by ZFMISC_1:def 2;
A76: x in S(n) by A72,A73,ZFMISC_1:31;
per cases;
suppose
A77: 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 A77,Th6;
then x in S(m) by A76;
then x in [:NAT, QC-symbols(S(m)):] by QC_LANG1:5;
then consider x3,x4 being set such that
A78: x3 in NAT & x4 in QC-symbols(S(m)) & x = [x3,x4] by ZFMISC_1:def 2;
x = [x1,x4] by A75,A78,XTUPLE_0:1;
then x in [:{4},QC-symbols(Sm):] by A75,A78,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
A79: x2 = x & r2 = r by A74;
reconsider Al2 as Sm-expanding QC-alphabet by A2,QC_TRANS:def 1;
A80: r = Al2-Cast(r2) & x = Al2-Cast(x2) by A79,QC_TRANS:def 3,def 4;
All(x2,r2) = Al2-Cast(All(x2,r2)) by QC_TRANS:def 3
.= All(x,r) by A80,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 A76,QC_LANG1:5;
then consider x3,x4 being set such that
A81: x3 in NAT & x4 in QC-symbols(Sn) & x = [x3,x4] by ZFMISC_1:def 2;
x = [x1,x4] by A75,A81,XTUPLE_0:1;
then x in [:{4},QC-symbols(Sn):] by A75,A81,ZFMISC_1:def 2;
then x is bound_QC-variable of Sn & r is Element of CQC-WFF(Sn)
by A74,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
A82: x2 = x & r2 = r;
reconsider Al2 as Sn-expanding QC-alphabet by A2,QC_TRANS:def 1;
A83: r = Al2-Cast(r2) & x = Al2-Cast(x2) by A82,QC_TRANS:def 3,def 4;
All(x2,r2) = Al2-Cast(All(x2,r2)) by QC_TRANS:def 3
.= All(x,r) by A83,QC_TRANS:8;
hence thesis;
end;
end;
then
A84: for r,s being Element of CQC-WFF(Al2), x being bound_QC-variable of
Al2, k being Element of 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 A48,A49,A63,A66;
for p being Element of CQC-WFF(Al2) holds P[p] from CQC_LANG:sch 1(A84);
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
A85: p is Element of CQC-WFF(S(m)) by A47;
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
A86: a in S & {x} c= a by A46,COHSP_1:6,13;
consider n such that
A87: a = S(n) by A86;
x in bound_QC-variables(Al2);
then x in [:{4},QC-symbols(Al2):] by QC_LANG1:def 4;
then consider x1,x2 being set such that
A88: x1 in {4} & x2 in QC-symbols(Al2) & x = [x1,x2] by ZFMISC_1:def 2;
A89: x in S(n) by A86,A87,ZFMISC_1:31;
per cases;
suppose
A90: 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 A90,Th6;
then x in S(m) by A89;
then x in [:NAT, QC-symbols(S(m)):] by QC_LANG1:5;
then consider x3,x4 being set such that
A91: x3 in NAT & x4 in QC-symbols(S(m)) & x = [x3,x4] by ZFMISC_1:def 2;
x = [x1,x4] by A88,A91,XTUPLE_0:1;
then x in [:{4},QC-symbols(Sm):] by A88,A91,ZFMISC_1:def 2;
then x is bound_QC-variable of Sm by QC_LANG1:def 4;
hence thesis by A85;
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 A89,QC_LANG1:5;
then consider x3,x4 being set such that
A92: x3 in NAT & x4 in QC-symbols(S(n)) & x = [x3,x4] by ZFMISC_1:def 2;
x = [x1,x4] by A88,A92,XTUPLE_0:1;
then x in [:{4},QC-symbols(Sn):] by A88,A92,ZFMISC_1:def 2;
then x is bound_QC-variable of Sn & p is Element of CQC-WFF(Sn)
by A85,QC_TRANS:7,QC_LANG1:def 4;
hence thesis;
end;
end;
then consider n such that
A93: x is bound_QC-variable of S(n) & p is Element of CQC-WFF(S(n));
A94: FCEx(S(n)) = S(n+1) by Th5;
A95: 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
A96: x2 = x & p2 = p by A93;
Example_Formula_of(p2,x2) in Example_Formulae_of(S(n));
then
A97: Example_Formula_of(p2,x2) in PSI(n+1) by A95,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
A98: y = y2;
A99: Sn1-Cast(p2) = p & Sn1-Cast(x2) = x by A96,QC_TRANS:def 3,def 4;
then
A100: Al2-Cast(Sn1-Cast(p2)) = p & Al2-Cast(Sn1-Cast(x2)) = x
by QC_TRANS:def 3,def 4;
A101: Al2-Cast(Ex(Sn1-Cast(x2),Sn1-Cast(p2))) = Ex(x,p) by A100,Th7;
reconsider p as Element of CQC-WFF(Al2);
reconsider x as bound_QC-variable of Al2;
A102: (Sn1-Cast(p2)).(Sn1-Cast(x2),y2) = p.(x,y) by A98,A99,QC_TRANS:17;
A103: Example_Formula_of(p2,x2)
= Al2-Cast(('not' Ex(Sn1-Cast(x2), Sn1-Cast(p2))) 'or'
((Sn1-Cast(p2)).(Sn1-Cast(x2),y2))) by A94,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 A101,A102,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 {PSI(m) : not contradiction};
then PSI(n+1) c= PSI by ZFMISC_1:74;
hence thesis by A97,A103,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;
A7: PSI c= Y
proof
let z be set such that
A5: z in PSI;
consider X being set such that
A6: X in Z by A4, XBOOLE_0:7;
X in U by A2,A6;
then ex R being Consistent Subset of CQC-WFF(Al) st X = R & PSI c= R;
hence z in Y by A5,A6,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;
A13: R[ {} ]
proof
consider Rs being set such that
A14: Rs in Z by A4, XBOOLE_0:7;
set Rss = {Rs};
reconsider Rss as finite Subset of Z by A14,ZFMISC_1:31;
for x being set st x in {} ex R being set st R in Rss & x in R;
hence thesis;
end;
A15: 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
A16: x in X & B c= X & R[B];
consider Rs being finite Subset of Z such that
A17: for b being set st b in B holds ex R being set st
R in Rs & b in R by A16;
consider S being set such that
A18: (x in S & S in Z) by A10,A16,TARSKI:def 4;
set Rss = Rs \/ {S};
Rs c= Z & {S} c= Z by A18, ZFMISC_1:31;
then
A19: 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
A20: y in B \/ {x};
per cases by A20,XBOOLE_0:def 3;
suppose y in {x};
then
A22: 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 A18,A22;
end;
suppose y in B;
then consider R being set such that
A23: R in Rs & y in R by A17;
R in Rss by A23, XBOOLE_0:def 3;
hence thesis by A23;
end;
end;
hence thesis by A19;
end;
A24: X is finite by A10;
R[X] from FINSET_1:sch 2(A24,A13,A15);
hence thesis;
end;
then consider Rs being finite Subset of Z such that
A25: 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;
A30: Rs is finite;
A31: F[{}];
A32: 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
A33: x in Rs & B c= Rs & F[B];
per cases;
suppose
A34: B is empty;
A35: union (B \/ {x}) = x by A34,ZFMISC_1:25;
thus thesis by A34,A35,TARSKI:def 1;
end;
suppose
A36: B is non empty;
per cases by A2,A33,A36,ORDINAL1:def 8,XBOOLE_0:def 9;
suppose
A38: 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 A38,XBOOLE_1:12;
hence thesis by A33,A36,XBOOLE_0:def 3;
end;
suppose
A39: union B c= x;
A40: 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 A39, XBOOLE_1:12;
hence thesis by A40,XBOOLE_0:def 3;
end;
end;
end;
A41: F[Rs] from FINSET_1:sch 2(A30,A31,A32);
X is non empty
proof
assume
A42: X is empty;
X |- 'not' VERUM(Al) by A10,HENMODEL:6;
then X \/ {VERUM(Al)} is Inconsistent &
X \/ {VERUM(Al)} = {VERUM(Al)} by A42,HENMODEL:10;
hence contradiction by HENMODEL:13;
end;
then consider x being set such that
A43: x in X by XBOOLE_0:def 1;
ex R being set st R in Rs & x in R by A25,A43;
then union Rs in Z by A41;
then union Rs in U by A2;
then consider uRs being Consistent Subset of CQC-WFF(Al) such that
A44: union Rs = uRs & PSI c= uRs;
for x being set st x in X holds x in uRs
proof
let x be set such that
A45: x in X;
ex R being set st R in Rs & x in R by A25,A45;
hence thesis by A44,TARSKI:def 4;
end;
then
A46: X c= uRs by TARSKI:def 3;
consider f being FinSequence of CQC-WFF(Al) such that
A47: rng f c= X & |- f^<*'not' VERUM(Al)*>
by A10,HENMODEL:def 1, GOEDELCP:24;
rng f c= uRs by A46,A47,XBOOLE_1:1;
hence contradiction by A47,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 A7,A8,ZFMISC_1:74;
hence thesis;
end;
end;
then consider THETA being set such that
A48: (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
A49: ex PHI st PHI = THETA & PSI c= PHI by A48;
then reconsider THETA as Consistent Subset of CQC-WFF(Al);
A50: for p holds (p in THETA or 'not' p in THETA)
proof
let p;
per cases by Th11;
suppose
A51: THETA \/ {p} is Consistent;
assume
A52: not p in THETA;
p in {p} by TARSKI:def 1;
then
A54: p in THETA \/ {p} & not p in THETA by XBOOLE_0:def 3, A52;
PSI c= THETA \/ {p} by A49,XBOOLE_1:10;
then THETA \/ {p} in U by A51;
hence thesis by A48,A54,XBOOLE_1:10;
end;
suppose
A55: THETA \/ {'not' p} is Consistent;
'not' p in THETA
proof
assume
A56: not ('not' p in THETA);
'not' p in {'not' p} by TARSKI:def 1;
then
A58: 'not' p in THETA \/ {'not' p} & not 'not' p in THETA
by XBOOLE_0:def 3, A56;
PSI c= THETA \/ {'not' p} by A49,XBOOLE_1:10;
then THETA \/ {'not' p} in U by A55;
hence thesis by A48,A58,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 A50;
hence thesis by GOEDELCP:21;
end;
then THETA is negation_faithful by GOEDELCP:def 1;
hence thesis by A49;
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
A4: PHI |- ('not' Ex(x,p) 'or' (p.(x,y))) by A1,GOEDELCP:def 2;
consider f being FinSequence of CQC-WFF(Al) such that
A5: rng f c= PHI & |- f^<*('not' Ex(x,p) 'or' (p.(x,y)))*>
by A4, HENMODEL:def 1;
take y;
thus THETA |- ('not' Ex(x,p) 'or' (p.(x,y)))
by A1,A5,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
A0: PHI is Consistent;
then consider Al2 being Al-expanding QC-alphabet,
PSI being Consistent Subset of CQC-WFF(Al2) such that
A1: PHI c= PSI & PSI is with_examples by Th10;
consider THETA being Consistent Subset of CQC-WFF(Al2) such that
A2: 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);
A3: THETA is with_examples by Th13, A2, A1;
assume p in THETA;
then THETA |- p by GOEDELCP:21;
hence JH,valH(Al2) |= p by GOEDELCP:17,A2,A3;
end;
then JH,valH(Al2) |= THETA by CALCUL_1:def 11;
then ex A,J,v st J,v |= PHI by A0,A1,A2,QC_TRANS:10,XBOOLE_1:1;
hence thesis by Def1;
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;