:: The G\"odel Completeness Theorem for Uncountable Languages
:: by Julian J. Schl\"oder and Peter Koepke
::
:: Received May 7, 2012
:: Copyright (c) 2012-2018 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-symbo