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

registration
existence
ex b1 being QC-alphabet st b1 is countable
proof end;
end;

definition
let Al be QC-alphabet ;
let X be Subset of (CQC-WFF Al);
attr X 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);
attr X is with_examples means :: 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 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 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 ^ <*(() 'or' q)*> & |- f ^ <*p*> holds
|- f ^ <*q*>
proof end;

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) )
proof end;

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 & CX is with_examples implies ( JH, valH Al |= p iff CX |- p ) ) & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= 'not' p iff CX |- 'not' p ) by ;

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*> & |- f1 ^ <*q*> holds
|- f1 ^ <*(p '&' q)*>
proof end;

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 & X |- q ) iff X |- p '&' q )
proof end;

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 & CX is with_examples implies ( JH, valH Al |= p iff CX |- p ) ) & ( CX is negation_faithful & CX is with_examples implies ( JH, valH Al |= q iff CX |- q ) ) & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p '&' q iff CX |- p '&' q ) by ;

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 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
proof end;

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 )
proof end;

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) )
proof end;

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,())) iff J,v |= All (x,p) )
proof end;

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,())) iff X |- All (x,p) )
proof end;

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)) = () + 1
proof end;

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))
proof end;

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 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
proof end;

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 Nat st ( for p being Element of CQC-WFF Al st QuantNbr p <= n & CX is negation_faithful & 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 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
proof end;

:: 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 & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
proof end;

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

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) )
proof end;
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) ) ) & ( 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
proof end;
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
proof end;

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

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

proof end;

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 ;
uniqueness
for b1, b2 being bound_QC-variable of Al st ex q being Element of QC-WFF Al st p = Ex (b1,q) & 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 A1: 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)
proof end;
uniqueness
for b1, b2 being Element of CQC-WFF Al st ex x being bound_QC-variable of Al st p = Ex (x,b1) & 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 sequence of (CQC-WFF Al);
let a be 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
proof end;
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 ) & ( for p being Element of CQC-WFF Al st p = F . a holds
b2 = Ex-bound_in p ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines bound_in GOEDELCP:def 6 :
for Al being QC-alphabet
for F being sequence of (CQC-WFF Al)
for a being 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 sequence of (CQC-WFF Al);
let a be 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
proof end;
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 ) & ( for p being Element of CQC-WFF Al st p = F . a holds
b2 = Ex-the_scope_of p ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines the_scope_of GOEDELCP:def 7 :
for Al being QC-alphabet
for F being sequence of (CQC-WFF Al)
for a being 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 () equals :: GOEDELCP:def 8
union { where p is Element of CQC-WFF Al : p in X } ;
coherence
union { where p is Element of CQC-WFF Al : p in X } is Subset of ()
proof end;
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 { 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
proof end;

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 & Ex-the_scope_of (Ex (x,p)) = p )
proof end;

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

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 ) by ;

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 & |- f ^ <*p*> holds
|- (((Ant f) ^ g) ^ <*(Suc f)*>) ^ <*p*>
proof end;

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
proof end;

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) = \/
proof end;

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

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
proof end;

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
proof end;

:: 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 & still_not-bound_in CX is finite holds
ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY & CY is with_examples )
proof end;

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 & X c= Y holds
Y |- p
proof end;

:: 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 & CX is with_examples holds
ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY & CY is negation_faithful & CY is with_examples )
proof end;

theorem Th34: :: GOEDELCP:34
for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al) st Al is countable & 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
proof end;

:: 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 & Y c= X holds
J,v |= Y
proof end;

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
proof end;

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 \/ {()}
proof end;

:: 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 & still_not-bound_in X is finite & X |= p holds
X |- p
proof end;