:: G{\"o}del's Completeness Theorem
:: by Patrick Braselmann and Peter Koepke
::
:: Received September 25, 2004
:: Copyright (c) 2004-2017 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, CQC_LANG, QC_LANG1, XBOOLE_0, VALUAT_1,
FINSEQ_1, HENMODEL, CQC_THE1, XBOOLEAN, BVFUNC_2, FUNCT_1, ORDINAL4,
CALCUL_1, ARYTM_3, RELAT_1, CARD_1, XXREAL_0, TARSKI, ZF_MODEL, CQC_SIM1,
REALSET1, SUBSTUT1, SUBSTUT2, ZF_LANG, ARYTM_1, CARD_3, ZFMISC_1,
FINSET_1, MCART_1, GOEDELCP, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XXREAL_0, ORDINAL1,
CARD_1, CARD_3, FINSEQ_1, FUNCT_1, NAT_1, QC_LANG1, QC_LANG2, QC_LANG3,
NUMBERS, CQC_LANG, RELAT_1, FINSET_1, VALUAT_1, RELSET_1, FUNCT_2,
CQC_SIM1, DOMAIN_1, XTUPLE_0, XFAMILY, MCART_1, SUBSTUT1, SUBLEMMA,
SUBSTUT2, CALCUL_1, HENMODEL;
constructors SETFAM_1, DOMAIN_1, XXREAL_0, NAT_1, NAT_D, FINSEQ_2, QC_LANG3,
CQC_SIM1, SUBSTUT2, CALCUL_1, HENMODEL, CARD_3, RELSET_1, XTUPLE_0,
XFAMILY;
registrations SUBSET_1, RELAT_1, ORDINAL1, XXREAL_0, XREAL_0, CQC_LANG,
HENMODEL, FINSEQ_1, FINSET_1, CARD_3, RELSET_1, XTUPLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: Henkin`s Theorem
registration
cluster countable for QC-alphabet;
end;
reserve Al for QC-alphabet;
reserve b,c,d for set,
X,Y for Subset of CQC-WFF(Al),
i,j,k,m,n for Nat,
p,p1,q,r,s,s1 for Element of CQC-WFF(Al),
x,x1,x2,y,y1 for bound_QC-variable of Al,
A for non empty set,
J for interpretation of Al, A,
v for Element of Valuations_in(Al,A),
f1,f2 for FinSequence of CQC-WFF(Al),
CX,CY,CZ for Consistent Subset of CQC-WFF(Al),
JH for Henkin_interpretation of CX,
a for Element of A,
t,u for QC-symbol of Al;
definition
let Al,X;
attr X is negation_faithful means
:: GOEDELCP:def 1
X |- p or X |- 'not' p;
end;
definition
let Al,X;
attr X is with_examples means
:: GOEDELCP:def 2
for x,p holds ex y st X |- ('not' Ex(x,p)) 'or' (p.(x,y));
end;
theorem :: GOEDELCP:1
CX is negation_faithful implies (CX |- p iff not CX |- 'not' p);
theorem :: GOEDELCP:2
for f being FinSequence of CQC-WFF(Al) holds
|- f^<*'not' p 'or' q*> & |- f^<*p*> implies |- f^<*q*>;
theorem :: GOEDELCP:3
X is with_examples implies (X |- Ex(x,p) iff ex y st X |- p.(x,y));
theorem :: GOEDELCP:4
(CX is negation_faithful & CX is with_examples implies
(JH,valH(Al) |= p iff CX |- p)) implies
(CX is negation_faithful & CX is with_examples implies
(JH,valH(Al) |= 'not' p iff CX |- 'not' p));
theorem :: GOEDELCP:5
|- f1^<*p*> & |- f1^<*q*> implies |- f1^<*p '&' q*>;
theorem :: GOEDELCP:6
X |- p & X |- q iff X |- p '&' q;
theorem :: GOEDELCP:7
(CX is negation_faithful & CX is with_examples implies
(JH,valH(Al) |= p iff CX |- p)) &
(CX is negation_faithful & CX is with_examples implies
(JH,valH(Al) |= q iff CX |- q)) implies
(CX is negation_faithful & CX is with_examples
implies (JH,valH(Al) |= p '&' q iff CX |- p '&' q));
theorem :: GOEDELCP:8
for p st QuantNbr(p) <= 0 holds
CX is negation_faithful & CX is with_examples implies
(JH,valH(Al) |= p iff CX |- p);
theorem :: GOEDELCP:9
J,v |= Ex(x,p) iff ex a st J,v.(x|a) |= p;
theorem :: GOEDELCP:10
JH,valH(Al) |= Ex(x,p) iff ex y st JH,valH(Al) |= p.(x,y);
theorem :: GOEDELCP:11
J,v |= 'not' Ex(x,'not' p) iff J,v |= All(x,p);
theorem :: GOEDELCP:12
X |- 'not' Ex(x,'not' p) iff X |- All(x,p);
theorem :: GOEDELCP:13
QuantNbr(Ex(x,p)) = QuantNbr(p)+1;
theorem :: GOEDELCP:14
QuantNbr(p) = QuantNbr(p.(x,y));
reserve L for PATH of q,p,
F1,F3 for QC-formula of Al,
a for set;
theorem :: GOEDELCP:15
for p st QuantNbr(p) = 1 holds (CX is negation_faithful & CX is with_examples
implies (JH,valH(Al) |= p iff CX |- p));
theorem :: GOEDELCP:16
for n st for p st QuantNbr(p) <= n holds
(CX is negation_faithful & CX is with_examples
implies (JH,valH(Al) |= p iff CX |- p)) holds
for p st QuantNbr(p) <= n+1 holds
(CX is negation_faithful & CX is with_examples
implies (JH,valH(Al) |= p iff CX |- p));
:: Ebb et al, Chapter V, Henkin's Theorem 1.10
theorem :: GOEDELCP:17
for p holds (CX is negation_faithful & CX is with_examples
implies (JH,valH(Al) |= p iff CX |- p));
begin :: Satisfiability of Consistent Sets of Formulas with Finitely Many Free
:: Variables
theorem :: GOEDELCP:18
Al is countable implies
QC-WFF(Al) is countable;
definition
let Al;
func ExCl(Al) -> Subset of CQC-WFF(Al) means
:: GOEDELCP:def 3
a in it iff ex x,p st a = Ex(x,p);
end;
theorem :: GOEDELCP:19
Al is countable implies
CQC-WFF(Al) is countable;
theorem :: GOEDELCP:20
Al is countable implies
ExCl(Al) is non empty & ExCl(Al) is countable;
definition
let Al;
let p be Element of QC-WFF(Al) such that
p is existential;
func Ex-bound_in p -> bound_QC-variable of Al means
:: GOEDELCP:def 4
ex q being Element of QC-WFF(Al) st p = Ex(it,q);
end;
definition
let Al;
let p be Element of CQC-WFF(Al) such that
p is existential;
func Ex-the_scope_of p -> Element of CQC-WFF(Al) means
:: GOEDELCP:def 5
ex x st p = Ex(x,it);
end;
definition
let Al;
let F be sequence of CQC-WFF(Al),a be Nat;
func bound_in(F,a) -> bound_QC-variable of Al means
:: GOEDELCP:def 6
p = F.a implies it = Ex-bound_in p;
end;
definition
let Al;
let F be sequence of CQC-WFF(Al),a be Nat;
func the_scope_of(F,a) -> Element of CQC-WFF(Al) means
:: GOEDELCP:def 7
p = F.a implies it = Ex-the_scope_of p;
end;
definition
let Al,X;
func still_not-bound_in X -> Subset of bound_QC-variables(Al) equals
:: GOEDELCP:def 8
union {still_not-bound_in p : p in X};
end;
theorem :: GOEDELCP:21
p in X implies X |- p;
theorem :: GOEDELCP:22
Ex-bound_in Ex(x,p) = x & Ex-the_scope_of Ex(x,p) = p;
theorem :: GOEDELCP:23
X |- VERUM(Al);
theorem :: GOEDELCP:24
X |- 'not' VERUM(Al) iff X is Inconsistent;
reserve C,D for Element of [:CQC-WFF(Al),bool bound_QC-variables(Al):];
reserve K,L for Subset of bound_QC-variables(Al);
theorem :: GOEDELCP:25
for f,g being FinSequence of CQC-WFF(Al) st 0 < len f & |- f^<*p*> holds
|- Ant(f)^g^<*Suc(f)*>^<*p*>;
theorem :: GOEDELCP:26
still_not-bound_in {p} = still_not-bound_in p;
theorem :: GOEDELCP:27
still_not-bound_in (X \/ Y) = still_not-bound_in X \/ still_not-bound_in Y;
theorem :: GOEDELCP:28
for A being Subset of bound_QC-variables(Al) st A is finite holds
ex x st not x in A;
theorem :: GOEDELCP:29
X c= Y implies still_not-bound_in X c= still_not-bound_in Y;
theorem :: GOEDELCP:30
for f being FinSequence of CQC-WFF(Al) holds
still_not-bound_in rng f = still_not-bound_in f;
:: Ebb et al, Chapter V, Lemma 2.1
theorem :: GOEDELCP:31
( Al is countable &
still_not-bound_in CX is finite ) implies
ex CY st CX c= CY & CY is with_examples;
theorem :: GOEDELCP:32
X |- p & X c= Y implies Y |- p;
reserve C,D for Subset of CQC-WFF(Al);
:: Ebb et al, Chapter V, Lemma 2.2
theorem :: GOEDELCP:33
( Al is countable &
CX is with_examples ) implies ( ex CY st CX c= CY &
CY is negation_faithful & CY is with_examples );
reserve JH1 for Henkin_interpretation of CZ,
J for interpretation of Al, A,
v for Element of Valuations_in(Al,A);
theorem :: GOEDELCP:34
(Al is countable & still_not-bound_in CX is finite)
implies ex CZ,JH1 st JH1,valH(Al) |= CX;
begin :: Goedel's Completeness Theorem,
:: Ebb et al, Chapter V, Completeness Theorem 4.1
theorem :: GOEDELCP:35
J,v |= X & Y c= X implies J,v |= Y;
theorem :: GOEDELCP:36
still_not-bound_in X is finite implies
still_not-bound_in (X \/ {p}) is finite;
theorem :: GOEDELCP:37
X |= p implies not J,v |= X \/ {'not' p};
::$N Goedel Completeness Theorem
theorem :: GOEDELCP:38
( Al is countable &
still_not-bound_in X is finite & X |= p ) implies X |- p;