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-2011 Association of Mizar Users

begin

definition

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

end;

:: deftheorem Def1 defines negation_faithful GOEDELCP:def 1 :

definition

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

end;

:: deftheorem Def2 defines with_examples GOEDELCP:def 2 :

theorem :: GOEDELCP:1

for p being Element of CQC-WFF
for CX being Consistent Subset of CQC-WFF st CX is negation_faithful holds
( CX |- p iff not CX |- 'not' p ) by Def1, HENMODEL:def 3;

theorem Th2: :: GOEDELCP:2

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

proof end;

theorem Th3: :: GOEDELCP:3

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

proof end;

theorem :: GOEDELCP:4

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

theorem Th5: :: GOEDELCP:5

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

proof end;

theorem Th6: :: GOEDELCP:6

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

proof end;

theorem :: GOEDELCP:7

for p, q being Element of CQC-WFF
for CX being Consistent Subset of CQC-WFF
for JH being Henkin_interpretation of CX st ( CX is negation_faithful & CX is with_examples implies ( JH, valH |= p iff CX |- p ) ) & ( CX is negation_faithful & CX is with_examples implies ( JH, valH |= q iff CX |- q ) ) & CX is negation_faithful & CX is with_examples holds
( JH, valH |= p '&' q iff CX |- p '&' q ) by Th6, VALUAT_1:29;

theorem Th8: :: GOEDELCP:8

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

proof end;

theorem Th9: :: GOEDELCP:9

for p being Element of CQC-WFF
for x being bound_QC-variable
for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in 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 p being Element of CQC-WFF
for x being bound_QC-variable
for CX being Consistent Subset of CQC-WFF
for JH being Henkin_interpretation of CX holds
( JH, valH |= Ex (x,p) iff ex y being bound_QC-variable st JH, valH |= p . (x,y) )

proof end;

theorem Th11: :: GOEDELCP:11

for p being Element of CQC-WFF
for x being bound_QC-variable
for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A holds
( J,v |= 'not' (Ex (x,('not' p))) iff J,v |= All (x,p) )

proof end;

theorem Th12: :: GOEDELCP:12

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

proof end;

theorem :: GOEDELCP:13

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

proof end;

theorem Th14: :: GOEDELCP:14

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

proof end;

theorem Th15: :: GOEDELCP:15

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

proof end;

theorem Th16: :: GOEDELCP:16

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

proof end;

theorem Th17: :: GOEDELCP:17

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

proof end;

begin

theorem Th18: :: GOEDELCP:18

QC-WFF is countable

proof end;

definition

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

proof end;

proof end;

end;

:: deftheorem Def3 defines ExCl GOEDELCP:def 3 :

theorem Th19: :: GOEDELCP:19

CQC-WFF is countable by Th18;

theorem Th20: :: GOEDELCP:20

( not ExCl is empty & ExCl 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 p be Element of QC-WFF ;
assume A1: p is existential ;
func Ex-bound_in p -> bound_QC-variable means :Def4: :: GOEDELCP:def 4
ex q being Element of QC-WFF st p = Ex (it,q);
existence by A1, QC_LANG2:def 13;
uniqueness by QC_LANG2:19;

end;

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

definition

let p be Element of CQC-WFF ;
assume A1: p is existential ;
func Ex-the_scope_of p -> Element of CQC-WFF means :Def5: :: GOEDELCP:def 5
ex x being bound_QC-variable st p = Ex (x,it);
existence

proof end;

uniqueness by QC_LANG2:19;

end;

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

definition

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

proof end;

proof end;

end;

:: deftheorem Def6 defines bound_in GOEDELCP:def 6 :

definition

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

proof end;

proof end;

end;

:: deftheorem Def7 defines the_scope_of GOEDELCP:def 7 :

definition

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

proof end;

end;

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

theorem Th21: :: GOEDELCP:21

for X being Subset of CQC-WFF
for p being Element of CQC-WFF st p in X holds
X |- p

proof end;

theorem Th22: :: GOEDELCP:22

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

proof end;

theorem Th23: :: GOEDELCP:23

for X being Subset of CQC-WFF holds X |- VERUM

proof end;

theorem Th24: :: GOEDELCP:24

for X being Subset of CQC-WFF holds
( X |- 'not' VERUM iff not X is Consistent )

proof end;

theorem Th25: :: GOEDELCP:25

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

proof end;

theorem Th26: :: GOEDELCP:26

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

proof end;

theorem Th27: :: GOEDELCP:27

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

proof end;

theorem Th28: :: GOEDELCP:28

for A being Subset of bound_QC-variables st A is finite holds
ex x being bound_QC-variable st not x in A

proof end;

theorem Th29: :: GOEDELCP:29

for X, Y being Subset of CQC-WFF st X c= Y holds
still_not-bound_in X c= still_not-bound_in Y

proof end;

theorem Th30: :: GOEDELCP:30

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

proof end;

theorem Th31: :: GOEDELCP:31

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

proof end;

theorem Th32: :: GOEDELCP:32

for X, Y being Subset of CQC-WFF
for p being Element of CQC-WFF st X |- p & X c= Y holds
Y |- p

proof end;

theorem Th33: :: GOEDELCP:33

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

proof end;

theorem Th34: :: GOEDELCP:34

for CX being Consistent Subset of CQC-WFF st still_not-bound_in CX is finite holds
ex CZ being Consistent Subset of CQC-WFF ex JH1 being Henkin_interpretation of CZ st JH1, valH |= CX

proof end;

begin

theorem Th35: :: GOEDELCP:35

for X, Y being Subset of CQC-WFF
for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A st J,v |= X & Y c= X holds
J,v |= Y

proof end;

theorem Th36: :: GOEDELCP:36

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

proof end;

theorem Th37: :: GOEDELCP:37

for X being Subset of CQC-WFF
for p being Element of CQC-WFF
for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A st X |= p holds
not J,v |= X \/ {('not' p)}

proof end;

theorem :: GOEDELCP:38

for X being Subset of CQC-WFF
for p being Element of CQC-WFF st still_not-bound_in X is finite & X |= p holds
X |- p

proof end;