:: The G\"odel Completeness Theorem for Uncountable Languages
:: by Julian J. Schl\"oder and Peter Koepke
::
:: Received May 7, 2012
:: Copyright (c) 2012-2021 Association of Mizar Users


definition
let Al be QC-alphabet ;
let PHI be Subset of (CQC-WFF Al);
attr PHI is satisfiable means :Def1: :: GOEDCPUC:def 1
 ex A being non empty set ex J being interpretation of Al,A ex v being Element of Valuations_in (Al,A) st J,v |= PHI;
end;

:: deftheorem Def1 defines satisfiable GOEDCPUC:def 1 :
for Al being QC-alphabet
for PHI being Subset of (CQC-WFF Al) holds
( PHI is satisfiable iff ex A being non empty set ex J being interpretation of Al,A ex v being Element of Valuations_in (Al,A) st J,v |= PHI );

theorem Th1: :: GOEDCPUC:1
for Al being QC-alphabet ex s being set st
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds not [s,[x,p]] in QC-symbols Al
proof end;

definition
let Al be QC-alphabet ;
mode free_symbol of Al -> set means :Def2: :: GOEDCPUC:def 2
 for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds not [it,[x,p]] in QC-symbols Al;
existence
ex b1 being set st
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds not [b1,[x,p]] in QC-symbols Al by Th1;
end;

:: deftheorem Def2 defines free_symbol GOEDCPUC:def 2 :
for Al being QC-alphabet
for b2 being set holds
( b2 is free_symbol of Al iff for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds not [b2,[x,p]] in QC-symbols Al );

definition
let Al be QC-alphabet ;
func FCEx Al -> Al -expanding QC-alphabet equals :: GOEDCPUC:def 3
[:NAT,((QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ):];
coherence
[:NAT,((QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ):] is Al -expanding QC-alphabet
proof end;
end;

:: deftheorem defines FCEx GOEDCPUC:def 3 :
for Al being QC-alphabet holds FCEx Al = [:NAT,((QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ):];

definition
let Al be QC-alphabet ;
let p be Element of CQC-WFF Al;
let x be bound_QC-variable of Al;
func Example_of (p,x) -> bound_QC-variable of (FCEx Al) equals :: GOEDCPUC:def 4
[4,[ the free_symbol of Al,[x,p]]];
coherence
[4,[ the free_symbol of Al,[x,p]]] is bound_QC-variable of (FCEx Al)
proof end;
end;

:: deftheorem defines Example_of GOEDCPUC:def 4 :
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds Example_of (p,x) = [4,[ the free_symbol of Al,[x,p]]];

definition
let Al be QC-alphabet ;
let p be Element of CQC-WFF Al;
let x be bound_QC-variable of Al;
func Example_Formula_of (p,x) -> Element of CQC-WFF (FCEx Al) equals :: GOEDCPUC:def 5
('not' (Ex (((FCEx Al) -Cast x),((FCEx Al) -Cast p)))) 'or' (((FCEx Al) -Cast p) . (((FCEx Al) -Cast x),(Example_of (p,x))));
coherence
('not' (Ex (((FCEx Al) -Cast x),((FCEx Al) -Cast p)))) 'or' (((FCEx Al) -Cast p) . (((FCEx Al) -Cast x),(Example_of (p,x)))) is Element of CQC-WFF (FCEx Al) ;
end;

:: deftheorem defines Example_Formula_of GOEDCPUC:def 5 :
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds Example_Formula_of (p,x) = ('not' (Ex (((FCEx Al) -Cast x),((FCEx Al) -Cast p)))) 'or' (((FCEx Al) -Cast p) . (((FCEx Al) -Cast x),(Example_of (p,x))));

definition
let Al be QC-alphabet ;
func Example_Formulae_of Al -> Subset of (CQC-WFF (FCEx Al)) equals :: GOEDCPUC:def 6
 { (Example_Formula_of (p,x)) where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ;
coherence
{ (Example_Formula_of (p,x)) where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } is Subset of (CQC-WFF (FCEx Al))
proof end;
end;

:: deftheorem defines Example_Formulae_of GOEDCPUC:def 6 :
for Al being QC-alphabet holds Example_Formulae_of Al = { (Example_Formula_of (p,x)) where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ;

theorem Th2: :: GOEDCPUC:2
for Al being QC-alphabet
for k being Element of NAT st k > 0 holds
ex F being b2 -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 end;

definition
let Al be QC-alphabet ;
let k be Nat;
mode FCEx-Sequence of Al,k -> k + 1 -element FinSequence means :Def7: :: GOEDCPUC:def 7
( ( 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
ex b1 being k + 1 -element FinSequence st
( ( for n being Nat st n <= k + 1 & 1 <= n holds
b1 . n is QC-alphabet ) & b1 . 1 = Al & ( for n being Nat st n < k + 1 & 1 <= n holds
ex Al2 being QC-alphabet st
( b1 . n = Al2 & b1 . (n + 1) = FCEx Al2 ) ) ) by Th2;
end;

:: deftheorem Def7 defines FCEx-Sequence GOEDCPUC:def 7 :
for Al being QC-alphabet
for k being Nat
for b3 being b2 + 1 -element FinSequence holds
( b3 is FCEx-Sequence of Al,k iff ( ( for n being Nat st n <= k + 1 & 1 <= n holds
b3 . n is QC-alphabet ) & b3 . 1 = Al & ( for n being Nat st n < k + 1 & 1 <= n holds
ex Al2 being QC-alphabet st
( b3 . n = Al2 & b3 . (n + 1) = FCEx Al2 ) ) ) );

theorem Th3: :: GOEDCPUC:3
for Al being QC-alphabet
for k being Nat
for S being FCEx-Sequence of Al,k holds S . (k + 1) is QC-alphabet
proof end;

theorem Th4: :: GOEDCPUC:4
for Al being QC-alphabet
for k being Nat
for S being FCEx-Sequence of Al,k holds S . (k + 1) is b1 -expanding QC-alphabet
proof end;

definition
let Al be QC-alphabet ;
let k be Nat;
func k -th_FCEx Al -> Al -expanding QC-alphabet equals :: GOEDCPUC:def 8
 the FCEx-Sequence of Al,k . (k + 1);
coherence
the FCEx-Sequence of Al,k . (k + 1) is Al -expanding QC-alphabet by Th4;
end;

:: deftheorem defines -th_FCEx GOEDCPUC:def 8 :
for Al being QC-alphabet
for k being Nat holds k -th_FCEx Al = the FCEx-Sequence of Al,k . (k + 1);

definition
let Al be QC-alphabet ;
let PHI be Consistent Subset of (CQC-WFF Al);
mode EF-Sequence of Al,PHI -> Function means :Def9: :: GOEDCPUC:def 9
( dom it = NAT & it . 0 = PHI & ( for n being Nat holds it . (n + 1) = (it . n) \/ (Example_Formulae_of (n -th_FCEx Al)) ) );
existence
ex b1 being Function st
( dom b1 = NAT & b1 . 0 = PHI & ( for n being Nat holds b1 . (n + 1) = (b1 . n) \/ (Example_Formulae_of (n -th_FCEx Al)) ) )
proof end;
end;

:: deftheorem Def9 defines EF-Sequence GOEDCPUC:def 9 :
for Al being QC-alphabet
for PHI being Consistent Subset of (CQC-WFF Al)
for b3 being Function holds
( b3 is EF-Sequence of Al,PHI iff ( dom b3 = NAT & b3 . 0 = PHI & ( for n being Nat holds b3 . (n + 1) = (b3 . n) \/ (Example_Formulae_of (n -th_FCEx Al)) ) ) );

theorem Th5: :: GOEDCPUC:5
for Al being QC-alphabet
for k being Nat holds FCEx (k -th_FCEx Al) = (k + 1) -th_FCEx Al
proof end;

theorem Th6: :: GOEDCPUC:6
for Al being QC-alphabet
for k, n being Element of NAT st n <= k holds
n -th_FCEx Al c= k -th_FCEx Al
proof end;

definition
let Al be QC-alphabet ;
let PHI be Consistent Subset of (CQC-WFF Al);
let k be Nat;
func k -th_EF (Al,PHI) -> Subset of (CQC-WFF (k -th_FCEx Al)) equals :: GOEDCPUC:def 10
 the EF-Sequence of Al,PHI . k;
coherence
the EF-Sequence of Al,PHI . k is Subset of (CQC-WFF (k -th_FCEx Al))
proof end;
end;

:: deftheorem defines -th_EF GOEDCPUC:def 10 :
for Al being QC-alphabet
for PHI being Consistent Subset of (CQC-WFF Al)
for k being Nat holds k -th_EF (Al,PHI) = the EF-Sequence of Al,PHI . k;

theorem Th7: :: GOEDCPUC:7
for Al being QC-alphabet
for Al2 being b1 -expanding QC-alphabet
for r, s being Element of CQC-WFF Al
for x being bound_QC-variable of Al 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 end;

theorem Th8: :: GOEDCPUC:8
for Al being QC-alphabet
for p, q 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) holds
( ( J,v |= p or J,v |= q ) iff J,v |= p 'or' q )
proof end;

:: Ebbinghaus Lemma 5.3.4
theorem Th9: :: GOEDCPUC:9
for Al being QC-alphabet
for PHI being Consistent Subset of (CQC-WFF Al) holds PHI \/ (Example_Formulae_of Al) is Consistent Subset of (CQC-WFF (FCEx Al))
proof end;

:: Ebbinghaus Lemma 5.3.1
theorem Th10: :: GOEDCPUC:10
for Al being QC-alphabet
for PHI being Consistent Subset of (CQC-WFF Al) ex Al2 being b1 -expanding QC-alphabet ex PSI being Consistent Subset of (CQC-WFF Al2) st
( PHI c= PSI & PSI is with_examples )
proof end;

theorem Th11: :: GOEDCPUC:11
for Al being QC-alphabet
for PHI being Consistent Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al holds
( PHI \/ {p} is Consistent or PHI \/ {('not' p)} is Consistent )
proof end;

:: Ebbinghaus Lemma 5.3.2
theorem Th12: :: GOEDCPUC:12
for Al being QC-alphabet
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 end;

theorem Th13: :: GOEDCPUC:13
for Al being QC-alphabet
for PHI, THETA being Consistent Subset of (CQC-WFF Al) st PHI c= THETA & PHI is with_examples holds
THETA is with_examples
proof end;

:: Ebbinghaus Corollary 5.3.3
:: Model Existence Theorem
registration
let Al be QC-alphabet ;
cluster Consistent -> satisfiable for Element of bool (CQC-WFF Al);
coherence
for b1 being Subset of (CQC-WFF Al) st b1 is Consistent holds
b1 is satisfiable
proof end;
end;

:: Completeness Theorem
theorem :: GOEDCPUC:14
for Al being QC-alphabet
for PSI being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al st PSI |= p holds
PSI |- p
proof end;