:: by Patrick Braselmann and Peter Koepke

::

:: Received September 25, 2004

:: Copyright (c) 2004-2017 Association of Mizar Users

definition

let Al be QC-alphabet ;

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

end;
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 );

for p being Element of CQC-WFF Al holds

( X |- p or X |- 'not' p );

:: deftheorem Def1 defines negation_faithful GOEDELCP:def 1 :

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al) holds

( X is negation_faithful iff for p being Element of CQC-WFF Al holds

( X |- p or X |- 'not' p ) );

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al) holds

( X is negation_faithful iff for p being Element of CQC-WFF Al holds

( X |- p or X |- 'not' p ) );

definition

let Al be QC-alphabet ;

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

end;
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));

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));

:: deftheorem defines with_examples GOEDELCP:def 2 :

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al) holds

( X is with_examples iff 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)) );

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al) holds

( X is with_examples iff 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)) );

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;

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*>

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) )

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;

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)*>

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 )

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;

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 )

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 )

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) )

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) )

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) )

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

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))

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 )

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 )

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 )

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

definition

let Al be QC-alphabet ;

ex b_{1} being Subset of (CQC-WFF Al) st

for a being set holds

( a in b_{1} iff ex x being bound_QC-variable of Al ex p being Element of CQC-WFF Al st a = Ex (x,p) )

for b_{1}, b_{2} being Subset of (CQC-WFF Al) st ( for a being set holds

( a in b_{1} iff ex x being bound_QC-variable of Al ex p being Element of CQC-WFF Al st a = Ex (x,p) ) ) & ( for a being set holds

( a in b_{2} iff ex x being bound_QC-variable of Al ex p being Element of CQC-WFF Al st a = Ex (x,p) ) ) holds

b_{1} = b_{2}

end;
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) );

existence 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) );

ex b

for a being set holds

( a in b

proof end;

uniqueness for b

( a in b

( a in b

b

proof end;

:: deftheorem Def3 defines ExCl GOEDELCP:def 3 :

for Al being QC-alphabet

for b_{2} being Subset of (CQC-WFF Al) holds

( b_{2} = ExCl Al iff for a being set holds

( a in b_{2} iff ex x being bound_QC-variable of Al ex p being Element of CQC-WFF Al st a = Ex (x,p) ) );

for Al being QC-alphabet

for b

( b

( a in b

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 ;

ex b_{1} being bound_QC-variable of Al ex q being Element of QC-WFF Al st p = Ex (b_{1},q)
by A1, QC_LANG2:def 13;

uniqueness

for b_{1}, b_{2} being bound_QC-variable of Al st ex q being Element of QC-WFF Al st p = Ex (b_{1},q) & ex q being Element of QC-WFF Al st p = Ex (b_{2},q) holds

b_{1} = b_{2}
by QC_LANG2:13;

end;
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 ex q being Element of QC-WFF Al st p = Ex (it,q);

ex b

uniqueness

for b

b

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

for Al being QC-alphabet

for p being Element of QC-WFF Al st p is existential holds

for b_{3} being bound_QC-variable of Al holds

( b_{3} = Ex-bound_in p iff ex q being Element of QC-WFF Al st p = Ex (b_{3},q) );

for Al being QC-alphabet

for p being Element of QC-WFF Al st p is existential holds

for b

( b

definition

let Al be QC-alphabet ;

let p be Element of CQC-WFF Al;

assume A1: p is existential ;

ex b_{1} being Element of CQC-WFF Al ex x being bound_QC-variable of Al st p = Ex (x,b_{1})

for b_{1}, b_{2} being Element of CQC-WFF Al st ex x being bound_QC-variable of Al st p = Ex (x,b_{1}) & ex x being bound_QC-variable of Al st p = Ex (x,b_{2}) holds

b_{1} = b_{2}
by QC_LANG2:13;

end;
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);

existence ex x being bound_QC-variable of Al st p = Ex (x,it);

ex b

proof end;

uniqueness for b

b

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

for Al being QC-alphabet

for p being Element of CQC-WFF Al st p is existential holds

for b_{3} being Element of CQC-WFF Al holds

( b_{3} = Ex-the_scope_of p iff ex x being bound_QC-variable of Al st p = Ex (x,b_{3}) );

for Al being QC-alphabet

for p being Element of CQC-WFF Al st p is existential holds

for b

( b

definition

let Al be QC-alphabet ;

let F be sequence of (CQC-WFF Al);

let a be Nat;

ex b_{1} being bound_QC-variable of Al st

for p being Element of CQC-WFF Al st p = F . a holds

b_{1} = Ex-bound_in p

for b_{1}, b_{2} being bound_QC-variable of Al st ( for p being Element of CQC-WFF Al st p = F . a holds

b_{1} = Ex-bound_in p ) & ( for p being Element of CQC-WFF Al st p = F . a holds

b_{2} = Ex-bound_in p ) holds

b_{1} = b_{2}

end;
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;

existence for p being Element of CQC-WFF Al st p = F . a holds

it = Ex-bound_in p;

ex b

for p being Element of CQC-WFF Al st p = F . a holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def6 defines bound_in GOEDELCP:def 6 :

for Al being QC-alphabet

for F being sequence of (CQC-WFF Al)

for a being Nat

for b_{4} being bound_QC-variable of Al holds

( b_{4} = bound_in (F,a) iff for p being Element of CQC-WFF Al st p = F . a holds

b_{4} = Ex-bound_in p );

for Al being QC-alphabet

for F being sequence of (CQC-WFF Al)

for a being Nat

for b

( b

b

definition

let Al be QC-alphabet ;

let F be sequence of (CQC-WFF Al);

let a be Nat;

ex b_{1} being Element of CQC-WFF Al st

for p being Element of CQC-WFF Al st p = F . a holds

b_{1} = Ex-the_scope_of p

for b_{1}, b_{2} being Element of CQC-WFF Al st ( for p being Element of CQC-WFF Al st p = F . a holds

b_{1} = Ex-the_scope_of p ) & ( for p being Element of CQC-WFF Al st p = F . a holds

b_{2} = Ex-the_scope_of p ) holds

b_{1} = b_{2}

end;
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;

existence for p being Element of CQC-WFF Al st p = F . a holds

it = Ex-the_scope_of p;

ex b

for p being Element of CQC-WFF Al st p = F . a holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def7 defines the_scope_of GOEDELCP:def 7 :

for Al being QC-alphabet

for F being sequence of (CQC-WFF Al)

for a being Nat

for b_{4} being Element of CQC-WFF Al holds

( b_{4} = the_scope_of (F,a) iff for p being Element of CQC-WFF Al st p = F . a holds

b_{4} = Ex-the_scope_of p );

for Al being QC-alphabet

for F being sequence of (CQC-WFF Al)

for a being Nat

for b

( b

b

definition

let Al be QC-alphabet ;

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

union { (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X } is Subset of (bound_QC-variables Al)

end;
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 } ;

coherence union { (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X } ;

union { (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X } is Subset of (bound_QC-variables Al)

proof end;

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

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al) holds still_not-bound_in X = union { (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X } ;

for Al being QC-alphabet

for X being Subset of (CQC-WFF Al) holds still_not-bound_in X = union { (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X } ;

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

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 )

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 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;

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*>

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

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)

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

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

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

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 )

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

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 )

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

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

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

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)}

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;

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

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;