:: G{\"o}del's Completeness Theorem
:: by Patrick Braselmann and Peter Koepke
::
:: Received September 25, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

registration
cluster countable for QC-alphabet ;
existence
 ex b1 being QC-alphabet st b1 is countable
proofend;
end;

definition
let Al be QC-alphabet ;
let X be Subset of (CQC-WFF Al);
attrX is negation_faithful  means :Def1: :: GOEDELCP:def 1
 for p being Element of CQC-WFF Al holds
( X |- p or X |- 'not' p );
end;

:: deftheorem Def1 defines negation_faithful GOEDELCP:def_1_:_
 for Al being QC-alphabet
for X being Subset of (CQC-WFF Al) holds
( X is negation_faithful iff for p being Element of CQC-WFF Al holds
( X |- p or X |- 'not' p ) );

definition
let Al be QC-alphabet ;
let X be Subset of (CQC-WFF Al);
attrX is with_examples  means :Def2: :: GOEDELCP:def 2
 for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al ex y being bound_QC-variable of Al st X |- ('not' (Ex (x,p))) 'or' (p . (x,y));
end;

:: deftheorem Def2 defines with_examples GOEDELCP:def_2_:_
 for Al being QC-alphabet
for X being Subset of (CQC-WFF Al) holds
( X is with_examples iff for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al ex y being bound_QC-variable of Al st X |- ('not' (Ex (x,p))) 'or' (p . (x,y)) );

theorem :: GOEDELCP:1
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for CX being Consistent Subset of (CQC-WFF Al) st CX is negation_faithful holds
( CX |- p iff not CX |- 'not' p ) by Def1, HENMODEL:def_2;

theorem Th2: :: GOEDELCP:2
for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st |- f ^ <*(('not' p) 'or' q)*> &amp; |- f ^ <*p*> holds
|- f ^ <*q*>
proofend;

theorem Th3: :: GOEDELCP:3
for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al st X is with_examples holds
( X |- Ex (x,p) iff ex y being bound_QC-variable of Al st X |- p . (x,y) )
proofend;

theorem :: GOEDELCP:4
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX st ( CX is negation_faithful &amp; CX is with_examples implies ( JH, valH Al |= p iff CX |- p ) ) &amp; CX is negation_faithful &amp; CX is with_examples holds
( JH, valH Al |= 'not' p iff CX |- 'not' p ) by Def1, HENMODEL:def_2, VALUAT_1:17;

theorem Th5: :: GOEDELCP:5
for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for f1 being FinSequence of CQC-WFF Al st |- f1 ^ <*p*> &amp; |- f1 ^ <*q*> holds
|- f1 ^ <*(p '&amp;' q)*>
proofend;

theorem Th6: :: GOEDELCP:6
for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p, q being Element of CQC-WFF Al holds
( ( X |- p &amp; X |- q ) iff X |- p '&amp;' q )
proofend;

theorem :: GOEDELCP:7
for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX st ( CX is negation_faithful &amp; CX is with_examples implies ( JH, valH Al |= p iff CX |- p ) ) &amp; ( CX is negation_faithful &amp; CX is with_examples implies ( JH, valH Al |= q iff CX |- q ) ) &amp; CX is negation_faithful &amp; CX is with_examples holds
( JH, valH Al |= p '&amp;' q iff CX |- p '&amp;' q ) by Th6, VALUAT_1:18;

theorem Th8: :: GOEDELCP:8
for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX
for p being Element of CQC-WFF Al st QuantNbr p <= 0 &amp; CX is negation_faithful &amp; CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
proofend;

theorem Th9: :: GOEDELCP:9
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds
( J,v |= Ex (x,p) iff ex a being Element of A st J,v . (x | a) |= p )
proofend;

theorem Th10: :: GOEDELCP:10
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX holds
( JH, valH Al |= Ex (x,p) iff ex y being bound_QC-variable of Al st JH, valH Al |= p . (x,y) )
proofend;

theorem Th11: :: GOEDELCP:11
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds
( J,v |= 'not' (Ex (x,('not' p))) iff J,v |= All (x,p) )
proofend;

theorem Th12: :: GOEDELCP:12
for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds
( X |- 'not' (Ex (x,('not' p))) iff X |- All (x,p) )
proofend;

theorem :: GOEDELCP:13
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds QuantNbr (Ex (x,p)) = (QuantNbr p) + 1
proofend;

theorem Th14: :: GOEDELCP:14
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x, y being bound_QC-variable of Al holds QuantNbr p = QuantNbr (p . (x,y))
proofend;

theorem Th15: :: GOEDELCP:15
for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX
for p being Element of CQC-WFF Al st QuantNbr p = 1 &amp; CX is negation_faithful &amp; CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
proofend;

theorem Th16: :: GOEDELCP:16
for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX
for n being Element of NAT st ( for p being Element of CQC-WFF Al st QuantNbr p <= n &amp; CX is negation_faithful &amp; CX is with_examples holds
( JH, valH Al |= p iff CX |- p ) ) holds
for p being Element of CQC-WFF Al st QuantNbr p <= n + 1 &amp; CX is negation_faithful &amp; CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
proofend;

:: Ebb et al, Chapter V, Henkin's Theorem 1.10
theorem Th17: :: GOEDELCP:17
for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX
for p being Element of CQC-WFF Al st CX is negation_faithful &amp; CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
proofend;

begin

:: Variables
theorem Th18: :: GOEDELCP:18
for Al being QC-alphabet st Al is countable holds
QC-WFF Al is countable
proofend;

definition
let Al be QC-alphabet ;
func ExCl Al ->  Subset of (CQC-WFF Al) means :Def3: :: GOEDELCP:def 3
 for a being set holds
( a in it iff ex x being bound_QC-variable of Al ex p being Element of CQC-WFF Al st a = Ex (x,p) );
existence
 ex b1 being Subset of (CQC-WFF Al) st
for a being set holds
( a in b1 iff ex x being bound_QC-variable of Al ex p being Element of CQC-WFF Al st a = Ex (x,p) )
proofend;
uniqueness
 for b1, b2 being Subset of (CQC-WFF Al) st ( for a being set holds
( a in b1 iff ex x being bound_QC-variable of Al ex p being Element of CQC-WFF Al st a = Ex (x,p) ) ) &amp; ( for a being set holds
( a in b2 iff ex x being bound_QC-variable of Al ex p being Element of CQC-WFF Al st a = Ex (x,p) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines ExCl GOEDELCP:def_3_:_
 for Al being QC-alphabet
for b2 being Subset of (CQC-WFF Al) holds
( b2 = ExCl Al iff for a being set holds
( a in b2 iff ex x being bound_QC-variable of Al ex p being Element of CQC-WFF Al st a = Ex (x,p) ) );

theorem Th19: :: GOEDELCP:19
for Al being QC-alphabet st Al is countable holds
CQC-WFF Al is countable
proofend;

theorem Th20: :: GOEDELCP:20
for Al being QC-alphabet st Al is countable holds
( not ExCl Al is empty &amp; ExCl Al is countable )
proofend;

Lm1:  for A being non empty set st A is countable holds
ex f being Function st
( dom f = NAT &amp; A = rng f )
proofend;

definition
let Al be QC-alphabet ;
let p be Element of QC-WFF Al;
assume A1: p is existential ;
func Ex-bound_in p ->  bound_QC-variable of Al means :Def4: :: GOEDELCP:def 4
 ex q being Element of QC-WFF Al st p = Ex (it,q);
existence
 ex b1 being bound_QC-variable of Al ex q being Element of QC-WFF Al st p = Ex (b1,q) by A1, QC_LANG2:def_13;
uniqueness
 for b1, b2 being bound_QC-variable of Al st ex q being Element of QC-WFF Al st p = Ex (b1,q) &amp; ex q being Element of QC-WFF Al st p = Ex (b2,q) holds
b1 = b2 by QC_LANG2:13;
end;

:: deftheorem Def4 defines Ex-bound_in GOEDELCP:def_4_:_
 for Al being QC-alphabet
for p being Element of QC-WFF Al st p is existential holds
for b3 being bound_QC-variable of Al holds
( b3 = Ex-bound_in p iff ex q being Element of QC-WFF Al st p = Ex (b3,q) );

definition
let Al be QC-alphabet ;
let p be Element of CQC-WFF Al;
assume B1: p is existential ;
func Ex-the_scope_of p ->  Element of CQC-WFF Al means :Def5: :: GOEDELCP:def 5
 ex x being bound_QC-variable of Al st p = Ex (x,it);
existence
 ex b1 being Element of CQC-WFF Al ex x being bound_QC-variable of Al st p = Ex (x,b1)
proofend;
uniqueness
 for b1, b2 being Element of CQC-WFF Al st ex x being bound_QC-variable of Al st p = Ex (x,b1) &amp; ex x being bound_QC-variable of Al st p = Ex (x,b2) holds
b1 = b2 by QC_LANG2:13;
end;

:: deftheorem Def5 defines Ex-the_scope_of GOEDELCP:def_5_:_
 for Al being QC-alphabet
for p being Element of CQC-WFF Al st p is existential holds
for b3 being Element of CQC-WFF Al holds
( b3 = Ex-the_scope_of p iff ex x being bound_QC-variable of Al st p = Ex (x,b3) );

definition
let Al be QC-alphabet ;
let F be Function of NAT,(CQC-WFF Al);
let a be Element of NAT ;
func bound_in (F,a) ->  bound_QC-variable of Al means :Def6: :: GOEDELCP:def 6
 for p being Element of CQC-WFF Al st p = F . a holds
it = Ex-bound_in p;
existence
 ex b1 being bound_QC-variable of Al st
for p being Element of CQC-WFF Al st p = F . a holds
b1 = Ex-bound_in p
proofend;
uniqueness
 for b1, b2 being bound_QC-variable of Al st ( for p being Element of CQC-WFF Al st p = F . a holds
b1 = Ex-bound_in p ) &amp; ( for p being Element of CQC-WFF Al st p = F . a holds
b2 = Ex-bound_in p ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines bound_in GOEDELCP:def_6_:_
 for Al being QC-alphabet
for F being Function of NAT,(CQC-WFF Al)
for a being Element of NAT
for b4 being bound_QC-variable of Al holds
( b4 = bound_in (F,a) iff for p being Element of CQC-WFF Al st p = F . a holds
b4 = Ex-bound_in p );

definition
let Al be QC-alphabet ;
let F be Function of NAT,(CQC-WFF Al);
let a be Element of NAT ;
func the_scope_of (F,a) ->  Element of CQC-WFF Al means :Def7: :: GOEDELCP:def 7
 for p being Element of CQC-WFF Al st p = F . a holds
it = Ex-the_scope_of p;
existence
 ex b1 being Element of CQC-WFF Al st
for p being Element of CQC-WFF Al st p = F . a holds
b1 = Ex-the_scope_of p
proofend;
uniqueness
 for b1, b2 being Element of CQC-WFF Al st ( for p being Element of CQC-WFF Al st p = F . a holds
b1 = Ex-the_scope_of p ) &amp; ( for p being Element of CQC-WFF Al st p = F . a holds
b2 = Ex-the_scope_of p ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines the_scope_of GOEDELCP:def_7_:_
 for Al being QC-alphabet
for F being Function of NAT,(CQC-WFF Al)
for a being Element of NAT
for b4 being Element of CQC-WFF Al holds
( b4 = the_scope_of (F,a) iff for p being Element of CQC-WFF Al st p = F . a holds
b4 = Ex-the_scope_of p );

definition
let Al be QC-alphabet ;
let X be Subset of (CQC-WFF Al);
func still_not-bound_in X ->  Subset of (bound_QC-variables Al) equals :: GOEDELCP:def 8
 union  {  (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X  }  ;
coherence
 union  {  (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X  }  is Subset of (bound_QC-variables Al)
proofend;
end;

:: deftheorem  defines still_not-bound_in GOEDELCP:def_8_:_
 for Al being QC-alphabet
for X being Subset of (CQC-WFF Al) holds still_not-bound_in X = union  {  (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X  }  ;

theorem Th21: :: GOEDELCP:21
for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al st p in X holds
X |- p
proofend;

theorem Th22: :: GOEDELCP:22
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds
( Ex-bound_in (Ex (x,p)) = x &amp; Ex-the_scope_of (Ex (x,p)) = p )
proofend;

theorem Th23: :: GOEDELCP:23
for Al being QC-alphabet
for X being Subset of (CQC-WFF Al) holds X |- VERUM Al
proofend;

theorem Th24: :: GOEDELCP:24
for Al being QC-alphabet
for X being Subset of (CQC-WFF Al) holds
( X |- 'not' (VERUM Al) iff X is Inconsistent )
proofend;

theorem Th25: :: GOEDELCP:25
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for f, g being FinSequence of CQC-WFF Al st 0 < len f &amp; |- f ^ <*p*> holds
|- (((Ant f) ^ g) ^ <*(Suc f)*>) ^ <*p*>
proofend;

theorem Th26: :: GOEDELCP:26
for Al being QC-alphabet
for p being Element of CQC-WFF Al holds still_not-bound_in {p} = still_not-bound_in p
proofend;

theorem Th27: :: GOEDELCP:27
for Al being QC-alphabet
for X, Y being Subset of (CQC-WFF Al) holds still_not-bound_in (X \/ Y) = (still_not-bound_in X) \/ (still_not-bound_in Y)
proofend;

theorem Th28: :: GOEDELCP:28
for Al being QC-alphabet
for A being Subset of (bound_QC-variables Al) st A is finite holds
ex x being bound_QC-variable of Al st not x in A
proofend;

theorem Th29: :: GOEDELCP:29
for Al being QC-alphabet
for X, Y being Subset of (CQC-WFF Al) st X c= Y holds
still_not-bound_in X c= still_not-bound_in Y
proofend;

theorem Th30: :: GOEDELCP:30
for Al being QC-alphabet
for f being FinSequence of CQC-WFF Al holds still_not-bound_in (rng f) = still_not-bound_in f
proofend;

:: Ebb et al, Chapter V, Lemma 2.1
theorem Th31: :: GOEDELCP:31
for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al) st Al is countable &amp; still_not-bound_in CX is finite holds
ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY &amp; CY is with_examples )
proofend;

theorem Th32: :: GOEDELCP:32
for Al being QC-alphabet
for X, Y being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al st X |- p &amp; X c= Y holds
Y |- p
proofend;

:: Ebb et al, Chapter V, Lemma 2.2
theorem Th33: :: GOEDELCP:33
for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al) st Al is countable &amp; CX is with_examples holds
ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY &amp; CY is negation_faithful &amp; CY is with_examples )
proofend;

theorem Th34: :: GOEDELCP:34
for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al) st Al is countable &amp; still_not-bound_in CX is finite holds
ex CZ being Consistent Subset of (CQC-WFF Al) ex JH1 being Henkin_interpretation of CZ st JH1, valH Al |= CX
proofend;

begin

:: Ebb et al, Chapter V, Completeness Theorem 4.1
theorem Th35: :: GOEDELCP:35
for Al being QC-alphabet
for X, Y being Subset of (CQC-WFF Al)
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st J,v |= X &amp; Y c= X holds
J,v |= Y
proofend;

theorem Th36: :: GOEDELCP:36
for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al st still_not-bound_in X is finite holds
still_not-bound_in (X \/ {p}) is finite
proofend;

theorem Th37: :: GOEDELCP:37
for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st X |= p holds
not J,v |= X \/ {('not' p)}
proofend;

:: [WP: ] Goedel_Completeness_Theorem
theorem :: GOEDELCP:38
for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al st Al is countable &amp; still_not-bound_in X is finite &amp; X |= p holds
X |- p
proofend;