:: 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 b₁ being set st
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds not [b₁,[x,p]] in QC-symbols Al by Th1;

end;

:: deftheorem Def2 defines free_symbol GOEDCPUC:def 2 :
for Al being QC-alphabet
for b₂ being set holds
( b₂ is free_symbol of Al iff for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds not [b₂,[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 b₂ -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 b₁ being k + 1 -element FinSequence st
( ( for n being Nat st n <= k + 1 & 1 <= n holds
b₁ . n is QC-alphabet ) & b₁ . 1 = Al & ( for n being Nat st n < k + 1 & 1 <= n holds
ex Al2 being QC-alphabet st
( b₁ . n = Al2 & b₁ . (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 b₃ being b₂ + 1 -element FinSequence holds
( b₃ is FCEx-Sequence of Al,k iff ( ( for n being Nat st n <= k + 1 & 1 <= n holds
b₃ . n is QC-alphabet ) & b₃ . 1 = Al & ( for n being Nat st n < k + 1 & 1 <= n holds
ex Al2 being QC-alphabet st
( b₃ . n = Al2 & b₃ . (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 b₁ -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 b₁ being Function st
( dom b₁ = NAT & b₁ . 0 = PHI & ( for n being Nat holds b₁ . (n + 1) = (b₁ . 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 b₃ being Function holds
( b₃ is EF-Sequence of Al,PHI iff ( dom b₃ = NAT & b₃ . 0 = PHI & ( for n being Nat holds b₃ . (n + 1) = (b₃ . 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 b₁ -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 b₁ -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 b₁ being Subset of (CQC-WFF Al) st b₁ is Consistent holds
b₁ 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;