:: 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 :: (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, 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;