GOEDELCP: G{\"o}del's Completeness Theorem

:: G{\"o}del's Completeness Theorem
:: by Patrick Braselmann and Peter Koepke
::
:: Received September 25, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users

registration

cluster countable for QC-alphabet ;

proof end;

end;

definition

let Al be QC-alphabet ;
let X be Subset of (CQC-WFF Al);

attr X is negation_faithful means :Def1: :: GOEDELCP:def 1
for p being Element of CQC-WFF Al holds
( X |- p or X |- 'not' p );

end;

:: deftheorem Def1 defines negation_faithful GOEDELCP:def 1 :

definition

let Al be QC-alphabet ;
let X be Subset of (CQC-WFF Al);

attr X is with_examples means :: GOEDELCP:def 2
for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al ex y being bound_QC-variable of Al st X |- ('not' (Ex (x,p))) 'or' (p . (x,y));

end;

:: deftheorem defines with_examples GOEDELCP:def 2 :

theorem :: GOEDELCP:1

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for CX being Consistent Subset of (CQC-WFF Al) st CX is negation_faithful holds
( CX |- p iff not CX |- 'not' p ) by HENMODEL:def 2;

theorem Th2: :: GOEDELCP:2

for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st |- f ^ <*(('not' p) 'or' q)*> & |- f ^ <*p*> holds
|- f ^ <*q*>

proof end;

theorem Th3: :: GOEDELCP:3

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al st X is with_examples holds
( X |- Ex (x,p) iff ex y being bound_QC-variable of Al st X |- p . (x,y) )

proof end;

theorem :: GOEDELCP:4

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX st ( CX is negation_faithful & CX is with_examples implies ( JH, valH Al |= p iff CX |- p ) ) & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= 'not' p iff CX |- 'not' p ) by HENMODEL:def 2, VALUAT_1:17;

theorem Th5: :: GOEDELCP:5

for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for f1 being FinSequence of CQC-WFF Al st |- f1 ^ <*p*> & |- f1 ^ <*q*> holds
|- f1 ^ <*(p '&' q)*>

proof end;

theorem Th6: :: GOEDELCP:6

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p, q being Element of CQC-WFF Al holds
( ( X |- p & X |- q ) iff X |- p '&' q )

proof end;

theorem :: GOEDELCP:7

for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX st ( 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 ) ) & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p '&' q iff CX |- p '&' q ) by Th6, VALUAT_1:18;

theorem Th8: :: GOEDELCP:8

for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX
for p being Element of CQC-WFF Al st QuantNbr p <= 0 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )

proof end;

theorem Th9: :: GOEDELCP:9

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of 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 |= Ex (x,p) iff ex a being Element of A st J,v . (x | a) |= p )

proof end;

theorem Th10: :: GOEDELCP:10

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX holds
( JH, valH Al |= Ex (x,p) iff ex y being bound_QC-variable of Al st JH, valH Al |= p . (x,y) )

proof end;

theorem Th11: :: GOEDELCP:11

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of 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 |= 'not' (Ex (x,('not' p))) iff J,v |= All (x,p) )

proof end;

theorem Th12: :: GOEDELCP:12

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds
( X |- 'not' (Ex (x,('not' p))) iff X |- All (x,p) )

proof end;

theorem :: GOEDELCP:13

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds QuantNbr (Ex (x,p)) = (QuantNbr p) + 1

proof end;

theorem Th14: :: GOEDELCP:14

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x, y being bound_QC-variable of Al holds QuantNbr p = QuantNbr (p . (x,y))

proof end;

theorem Th15: :: GOEDELCP:15

for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX
for p being Element of CQC-WFF Al st QuantNbr p = 1 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )

proof end;

theorem Th16: :: GOEDELCP:16

for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX
for n being Nat st ( for p being Element of CQC-WFF Al st QuantNbr p <= n & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p ) ) holds
for p being Element of CQC-WFF Al st QuantNbr p <= n + 1 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )

proof end;

:: Ebb et al, Chapter V, Henkin's Theorem 1.10

theorem Th17: :: GOEDELCP:17

for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX
for p being Element of CQC-WFF Al st CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )

proof end;

:: Variables

theorem Th18: :: GOEDELCP:18

for Al being QC-alphabet st Al is countable holds
QC-WFF Al is countable

proof end;

definition

let Al be QC-alphabet ;

func ExCl Al -> Subset of (CQC-WFF Al) means :Def3: :: GOEDELCP:def 3
for a being set holds
( a in it iff ex x being bound_QC-variable of Al ex p being Element of CQC-WFF Al st a = Ex (x,p) );

proof end;

proof end;

end;

:: deftheorem Def3 defines ExCl GOEDELCP:def 3 :

theorem Th19: :: GOEDELCP:19

for Al being QC-alphabet st Al is countable holds
CQC-WFF Al is countable

proof end;

theorem Th20: :: GOEDELCP:20

for Al being QC-alphabet st Al is countable holds
( not ExCl Al is empty & ExCl Al is countable )

proof end;

Lm1: for A being non empty set st A is countable holds
ex f being Function st
( dom f = NAT & A = rng f )

proof end;

definition

let Al be QC-alphabet ;
let p be Element of QC-WFF Al;
assume A1: p is existential ;

func Ex-bound_in p -> bound_QC-variable of Al means :Def4: :: GOEDELCP:def 4
ex q being Element of QC-WFF Al st p = Ex (it,q);

existence by A1, QC_LANG2:def 13;
uniqueness by QC_LANG2:13;

end;

:: deftheorem Def4 defines Ex-bound_in GOEDELCP:def 4 :

definition

let Al be QC-alphabet ;
let p be Element of CQC-WFF Al;
assume A1: p is existential ;

func Ex-the_scope_of p -> Element of CQC-WFF Al means :Def5: :: GOEDELCP:def 5
ex x being bound_QC-variable of Al st p = Ex (x,it);

proof end;

uniqueness by QC_LANG2:13;

end;

:: deftheorem Def5 defines Ex-the_scope_of GOEDELCP:def 5 :

definition

let Al be QC-alphabet ;
let F be sequence of (CQC-WFF Al);
let a be Nat;

func bound_in (F,a) -> bound_QC-variable of Al means :Def6: :: GOEDELCP:def 6
for p being Element of CQC-WFF Al st p = F . a holds
it = Ex-bound_in p;

proof end;

proof end;

end;

:: deftheorem Def6 defines bound_in GOEDELCP:def 6 :

definition

let Al be QC-alphabet ;
let F be sequence of (CQC-WFF Al);
let a be Nat;

func the_scope_of (F,a) -> Element of CQC-WFF Al means :Def7: :: GOEDELCP:def 7
for p being Element of CQC-WFF Al st p = F . a holds
it = Ex-the_scope_of p;

proof end;

proof end;

end;

:: deftheorem Def7 defines the_scope_of GOEDELCP:def 7 :

definition

let Al be QC-alphabet ;
let X be Subset of (CQC-WFF Al);

func still_not-bound_in X -> Subset of (bound_QC-variables Al) equals :: GOEDELCP:def 8
union { (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X } ;

proof end;

end;

:: deftheorem defines still_not-bound_in GOEDELCP:def 8 :

theorem Th21: :: GOEDELCP:21

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al st p in X holds
X |- p

proof end;

theorem Th22: :: GOEDELCP:22

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds
( Ex-bound_in (Ex (x,p)) = x & Ex-the_scope_of (Ex (x,p)) = p )

proof end;

theorem Th23: :: GOEDELCP:23

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al) holds X |- VERUM Al

proof end;

theorem Th24: :: GOEDELCP:24

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al) holds
( X |- 'not' (VERUM Al) iff X is Inconsistent ) by Th23, HENMODEL:6, HENMODEL:def 2;

theorem Th25: :: GOEDELCP:25

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for f, g being FinSequence of CQC-WFF Al st 0 < len f & |- f ^ <*p*> holds
|- (((Ant f) ^ g) ^ <*(Suc f)*>) ^ <*p*>

proof end;

theorem Th26: :: GOEDELCP:26

for Al being QC-alphabet
for p being Element of CQC-WFF Al holds still_not-bound_in {p} = still_not-bound_in p

proof end;

theorem Th27: :: GOEDELCP:27

for Al being QC-alphabet
for X, Y being Subset of (CQC-WFF Al) holds still_not-bound_in (X \/ Y) = (still_not-bound_in X) \/ (still_not-bound_in Y)

proof end;

theorem Th28: :: GOEDELCP:28

for Al being QC-alphabet
for A being Subset of (bound_QC-variables Al) st A is finite holds
ex x being bound_QC-variable of Al st not x in A

proof end;

theorem Th29: :: GOEDELCP:29

for Al being QC-alphabet
for X, Y being Subset of (CQC-WFF Al) st X c= Y holds
still_not-bound_in X c= still_not-bound_in Y

proof end;

theorem Th30: :: GOEDELCP:30

for Al being QC-alphabet
for f being FinSequence of CQC-WFF Al holds still_not-bound_in (rng f) = still_not-bound_in f

proof end;

:: Ebb et al, Chapter V, Lemma 2.1

theorem Th31: :: GOEDELCP:31

for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al) st Al is countable & still_not-bound_in CX is finite holds
ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY & CY is with_examples )

proof end;

theorem Th32: :: GOEDELCP:32

for Al being QC-alphabet
for X, Y being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al st X |- p & X c= Y holds
Y |- p

proof end;

:: Ebb et al, Chapter V, Lemma 2.2

theorem Th33: :: GOEDELCP:33

for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al) st Al is countable & CX is with_examples holds
ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY & CY is negation_faithful & CY is with_examples )

proof end;

theorem Th34: :: GOEDELCP:34

for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al) st Al is countable & still_not-bound_in CX is finite holds
ex CZ being Consistent Subset of (CQC-WFF Al) ex JH1 being Henkin_interpretation of CZ st JH1, valH Al |= CX

proof end;

:: Ebb et al, Chapter V, Completeness Theorem 4.1

theorem Th35: :: GOEDELCP:35

for Al being QC-alphabet
for X, Y being Subset 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) st J,v |= X & Y c= X holds
J,v |= Y

proof end;

theorem Th36: :: GOEDELCP:36

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al st still_not-bound_in X is finite holds
still_not-bound_in (X \/ {p}) is finite

proof end;

theorem Th37: :: GOEDELCP:37

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p 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) st X |= p holds
not J,v |= X \/ {('not' p)}

proof end;

::

WP:

Goedel Completeness Theorem

theorem :: GOEDELCP:38

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al st Al is countable & still_not-bound_in X is finite & X |= p holds
X |- p

proof end;