:: The G\"odel Completeness Theorem for Uncountable Languages
:: by Julian J. Schl\"oder and Peter Koepke
::
:: Received May 7, 2012
:: Copyright (c) 2012-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, QC_LANG1, CQC_LANG, XBOOLE_0, VALUAT_1,
FINSEQ_1, HENMODEL, CQC_THE1, XBOOLEAN, BVFUNC_2, FUNCT_1, ORDINAL4,
ARYTM_3, RELAT_1, CARD_1, XXREAL_0, TARSKI, ZF_MODEL, REALSET1, ARYTM_1,
CARD_3, ZFMISC_1, FINSET_1, MCART_1, NAT_1, ORDINAL1, GOEDELCP, MARGREL1,
FUNCT_2, QC_TRANS, GOEDCPUC;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XXREAL_0, CARD_1,
CARD_3, FINSEQ_1, RELAT_1, QC_LANG1, QC_LANG2, ORDINAL1, NUMBERS,
CQC_THE1, CQC_LANG, FUNCT_1, FINSET_1, VALUAT_1, RELSET_1, FUNCT_2,
NAT_1, CQC_SIM1, DOMAIN_1, MCART_1, SUBSTUT1, SUBLEMMA, SUBSTUT2,
CALCUL_1, HENMODEL, GOEDELCP, MARGREL1, QC_LANG3, FUNCT_4, FUNCOP_1,
COHSP_1, QC_TRANS, XTUPLE_0;
constructors SETFAM_1, DOMAIN_1, XXREAL_0, NAT_1, NAT_D, FINSEQ_2, QC_LANG1,
CQC_THE1, CQC_SIM1, SUBSTUT2, CALCUL_1, HENMODEL, CARD_3, RELSET_1,
CARD_1, WELLORD2, GOEDELCP, VALUAT_1, MARGREL1, CQC_LANG, QC_LANG3,
FUNCT_4, FUNCOP_1, COHSP_1, QC_TRANS;
registrations SUBSET_1, RELAT_1, ORDINAL1, XXREAL_0, XREAL_0, FINSEQ_1,
FINSET_1, XBOOLE_0, QC_LANG1, CQC_LANG, QC_TRANS, XTUPLE_0, NAT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: Formula-Constant Extension
reserve Al for QC-alphabet,
PHI for Consistent Subset of CQC-WFF(Al),
PSI for Subset of CQC-WFF(Al),
p,q,r,s for Element of CQC-WFF(Al),
A for non empty set,
J for interpretation of Al,A,
v for Element of Valuations_in(Al,A),
m,n,i,j,k for Element of NAT,
l for CQC-variable_list of k,Al,
P for QC-pred_symbol of k,Al,
x,y for bound_QC-variable of Al,
z for QC-symbol of Al,
Al2 for Al-expanding QC-alphabet;
definition
let Al;
let PHI be Subset of CQC-WFF(Al);
attr PHI is satisfiable means
:: GOEDCPUC:def 1
ex A,J,v st J,v |= PHI;
end;
reserve J2 for interpretation of Al2,A,
Jp for interpretation of Al,A,
v2 for Element of Valuations_in(Al2,A),
vp for Element of Valuations_in(Al,A);
theorem :: GOEDCPUC:1
ex s being set st for p,x holds not [s,[x,p]] in QC-symbols(Al);
definition
let Al;
mode free_symbol of Al -> set means
:: GOEDCPUC:def 2
for p,x holds not [it,[x,p]] in QC-symbols(Al);
end;
definition
let Al;
func FCEx(Al) -> Al-expanding QC-alphabet equals
:: GOEDCPUC:def 3
[:NAT, QC-symbols(Al) \/
the set of all [the free_symbol of Al,[x,p]] :];
end;
definition
let Al,p,x;
func Example_of(p,x) -> bound_QC-variable of FCEx(Al) equals
:: GOEDCPUC:def 4
[4,[the free_symbol of Al,[x,p]]];
end;
definition
let Al,p,x;
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)));
end;
definition
let Al;
func Example_Formulae_of(Al) -> Subset of CQC-WFF(FCEx(Al)) equals
:: GOEDCPUC:def 6
the set of all Example_Formula_of(p,x) ;
end;
theorem :: GOEDCPUC:2
for k being Element of NAT st k > 0 ex F being k-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);
definition
let Al;
let k be Nat;
mode FCEx-Sequence of Al,k -> (k+1)-element FinSequence means
:: 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) );
end;
theorem :: GOEDCPUC:3
for k being Nat for S being FCEx-Sequence of Al,k holds
S.(k+1) is QC-alphabet;
theorem :: GOEDCPUC:4
for k being Nat for S being FCEx-Sequence of Al,k holds
S.(k+1) is Al-expanding QC-alphabet;
definition
let Al;
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);
end;
definition
let Al,PHI;
mode EF-Sequence of Al,PHI -> Function means
:: 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));
end;
theorem :: GOEDCPUC:5
for k being Nat holds
FCEx(k-th_FCEx(Al)) = (k+1)-th_FCEx(Al);
theorem :: GOEDCPUC:6
for k,n st n <= k holds n-th_FCEx(Al) c= k-th_FCEx(Al);
definition
let Al,PHI; 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;
end;
theorem :: GOEDCPUC:7
for r,s,x 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));
theorem :: GOEDCPUC:8
for p,q,A,J,v holds (J,v |= p or J,v |= q) iff J,v |= p 'or' q;
:: Ebbinghaus Lemma 5.3.4
theorem :: GOEDCPUC:9
PHI \/ Example_Formulae_of(Al) is Consistent Subset of CQC-WFF(FCEx(Al));
begin :: The Completeness Theorem
:: Ebbinghaus Lemma 5.3.1
theorem :: GOEDCPUC:10
ex Al2 being Al-expanding QC-alphabet,
PSI being Consistent Subset of CQC-WFF(Al2)
st PHI c= PSI & PSI is with_examples;
theorem :: GOEDCPUC:11
PHI \/ {p} is Consistent or PHI \/ {'not' p} is Consistent;
:: Ebbinghaus Lemma 5.3.2
theorem :: GOEDCPUC:12
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;
theorem :: GOEDCPUC:13
for THETA being Consistent Subset of CQC-WFF(Al)
st PHI c= THETA & PHI is with_examples holds THETA is with_examples;
:: Ebbinghaus Corollary 5.3.3
:: Model Existence Theorem
registration
let Al;
cluster Consistent -> satisfiable for Subset of CQC-WFF(Al);
end;
:: Completeness Theorem
theorem :: GOEDCPUC:14
PSI |= p implies PSI |- p;