:: GOEDELCP semantic presentation

begin

registration
cluster countable for ( ( ) ( ) QC-alphabet ) ;
end;

definition
let Al be ( ( ) ( ) QC-alphabet ) ;
let X be ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
attr X is negation_faithful means :: GOEDELCP:def 1
 for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds
( X : ( ( ) ( ) Element of QC-pred_symbols Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) or X : ( ( ) ( ) Element of QC-pred_symbols Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ) |- 'not' p : ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) );
end;

definition
let Al be ( ( ) ( ) QC-alphabet ) ;
let X be ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
attr X is with_examples means :: GOEDELCP:def 2
 for x being ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) )
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ex y being ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st X : ( ( ) ( ) Element of QC-pred_symbols Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ) |- ('not' (Ex (x : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,p : ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) 'or' (p : ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . (x : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,y : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
end;

theorem :: GOEDELCP:1
for Al being ( ( ) ( ) QC-alphabet )
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for CX being ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) st CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is negation_faithful holds
( CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) iff not CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) |- 'not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: GOEDELCP:2
for Al being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st |- f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ^ <*(('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) 'or' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) *> : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite V45(1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) & |- f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ^ <*p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) *> : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite V45(1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds
|- f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ^ <*q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) *> : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite V45(1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: GOEDELCP:3
for Al being ( ( ) ( ) QC-alphabet )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for x being ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is with_examples holds
( X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |- Ex (x : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) iff ex y being ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . (x : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,y : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: GOEDELCP:4
for Al being ( ( ) ( ) QC-alphabet )
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for CX being ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) )
for JH being ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Henkin_interpretation of CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) ) st ( CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is negation_faithful & CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is with_examples implies ( JH : ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Henkin_interpretation of b3 : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) ) , valH Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (b1 : ( ( ) ( ) QC-alphabet ) ,(HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) )) ) |= p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) iff CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) & CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is negation_faithful & CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is with_examples holds
( JH : ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Henkin_interpretation of b3 : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) ) , valH Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (b1 : ( ( ) ( ) QC-alphabet ) ,(HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) )) ) |= 'not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) iff CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) |- 'not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: GOEDELCP:5
for Al being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for f1 being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st |- f1 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ^ <*p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) *> : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite V45(1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) & |- f1 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ^ <*q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) *> : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite V45(1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds
|- f1 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ^ <*(p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) '&' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) *> : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite V45(1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: GOEDELCP:6
for Al being ( ( ) ( ) QC-alphabet )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for p, q being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds
( ( X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) & X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |- q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) iff X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) '&' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: GOEDELCP:7
for Al being ( ( ) ( ) QC-alphabet )
for p, q being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for CX being ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) )
for JH being ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Henkin_interpretation of CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) ) st ( CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is negation_faithful & CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is with_examples implies ( JH : ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Henkin_interpretation of b4 : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) ) , valH Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (b1 : ( ( ) ( ) QC-alphabet ) ,(HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) )) ) |= p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) iff CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) & ( CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is negation_faithful & CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is with_examples implies ( JH : ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Henkin_interpretation of b4 : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) ) , valH Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (b1 : ( ( ) ( ) QC-alphabet ) ,(HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) )) ) |= q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) iff CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) |- q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) & CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is negation_faithful & CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is with_examples holds
( JH : ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Henkin_interpretation of b4 : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) ) , valH Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (b1 : ( ( ) ( ) QC-alphabet ) ,(HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) )) ) |= p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) '&' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) iff CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) '&' q : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: GOEDELCP:8
for Al being ( ( ) ( ) QC-alphabet )
for CX being ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) )
for JH being ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Henkin_interpretation of CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) )
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st QuantNbr p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) <= 0 : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) & CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is negation_faithful & CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is with_examples holds
( JH : ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Henkin_interpretation of b2 : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) ) , valH Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (b1 : ( ( ) ( ) QC-alphabet ) ,(HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) )) ) |= p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) iff CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: GOEDELCP:9
for Al being ( ( ) ( ) QC-alphabet )
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for x being ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) )
for A being ( ( non empty ) ( non empty ) set )
for J being ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354(b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354(b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) interpretation of Al : ( ( ) ( ) QC-alphabet ) ,A : ( ( non empty ) ( non empty ) set ) )
for v being ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined b4 : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (Al : ( ( ) ( ) QC-alphabet ) ,A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) )) ) holds
( J : ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354(b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354(b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) interpretation of b1 : ( ( ) ( ) QC-alphabet ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ,v : ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined b4 : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (b1 : ( ( ) ( ) QC-alphabet ) ,b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) )) ) |= Ex (x : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) iff ex a being ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) st J : ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354(b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354(b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) interpretation of b1 : ( ( ) ( ) QC-alphabet ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ,v : ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined b4 : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (b1 : ( ( ) ( ) QC-alphabet ) ,b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) )) ) . (x : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) | a : ( ( ) ( ) Element of b4 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined b4 : ( ( non empty ) ( non empty ) set ) -valued Function-like finite countable ) Element of bool [:(bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined b4 : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (b1 : ( ( ) ( ) QC-alphabet ) ,b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) )) ) |= p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: GOEDELCP:10
for Al being ( ( ) ( ) QC-alphabet )
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for x being ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) )
for CX being ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) )
for JH being ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Henkin_interpretation of CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) ) holds
( JH : ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Henkin_interpretation of b4 : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) ) , valH Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (b1 : ( ( ) ( ) QC-alphabet ) ,(HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) )) ) |= Ex (x : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) iff ex y being ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st JH : ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Henkin_interpretation of b4 : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) ) , valH Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (b1 : ( ( ) ( ) QC-alphabet ) ,(HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) )) ) |= p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . (x : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,y : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: GOEDELCP:11
for Al being ( ( ) ( ) QC-alphabet )
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for x being ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) )
for A being ( ( non empty ) ( non empty ) set )
for J being ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354(b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354(b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) interpretation of Al : ( ( ) ( ) QC-alphabet ) ,A : ( ( non empty ) ( non empty ) set ) )
for v being ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined b4 : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (Al : ( ( ) ( ) QC-alphabet ) ,A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) )) ) holds
( J : ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354(b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354(b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) interpretation of b1 : ( ( ) ( ) QC-alphabet ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ,v : ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined b4 : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (b1 : ( ( ) ( ) QC-alphabet ) ,b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) )) ) |= 'not' (Ex (x : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) iff J : ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354(b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354(b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) interpretation of b1 : ( ( ) ( ) QC-alphabet ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ,v : ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined b4 : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (b1 : ( ( ) ( ) QC-alphabet ) ,b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) )) ) |= All (x : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: GOEDELCP:12
for Al being ( ( ) ( ) QC-alphabet )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for x being ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds
( X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |- 'not' (Ex (x : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) iff X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |- All (x : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: GOEDELCP:13
for Al being ( ( ) ( ) QC-alphabet )
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for x being ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds QuantNbr (Ex (x : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) = (QuantNbr p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: GOEDELCP:14
for Al being ( ( ) ( ) QC-alphabet )
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for x, y being ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds QuantNbr p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) = QuantNbr (p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . (x : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,y : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: GOEDELCP:15
for Al being ( ( ) ( ) QC-alphabet )
for CX being ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) )
for JH being ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Henkin_interpretation of CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) )
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st QuantNbr p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) = 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) & CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is negation_faithful & CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is with_examples holds
( JH : ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Henkin_interpretation of b2 : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) ) , valH Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (b1 : ( ( ) ( ) QC-alphabet ) ,(HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) )) ) |= p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) iff CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: GOEDELCP:16
for Al being ( ( ) ( ) QC-alphabet )
for CX being ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) )
for JH being ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Henkin_interpretation of CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) )
for n being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st ( for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st QuantNbr p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) <= n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) & CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is negation_faithful & CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is with_examples holds
( JH : ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Henkin_interpretation of b2 : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) ) , valH Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (b1 : ( ( ) ( ) QC-alphabet ) ,(HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) )) ) |= p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) iff CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) holds
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st QuantNbr p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) <= n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) & CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is negation_faithful & CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is with_examples holds
( JH : ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Henkin_interpretation of b2 : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) ) , valH Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (b1 : ( ( ) ( ) QC-alphabet ) ,(HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) )) ) |= p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) iff CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: GOEDELCP:17
for Al being ( ( ) ( ) QC-alphabet )
for CX being ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) )
for JH being ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Henkin_interpretation of CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) )
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is negation_faithful & CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is with_examples holds
( JH : ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Henkin_interpretation of b2 : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) ) , valH Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (b1 : ( ( ) ( ) QC-alphabet ) ,(HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) )) ) |= p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) iff CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

begin

theorem :: GOEDELCP:18
for Al being ( ( ) ( ) QC-alphabet ) st Al : ( ( ) ( ) QC-alphabet ) is countable holds
QC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) is countable ;

definition
let Al be ( ( ) ( ) QC-alphabet ) ;
func ExCl Al -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) means :: GOEDELCP:def 3
 for a being ( ( ) ( ) set ) holds
( a : ( ( ) ( ) set ) in it : ( ( ) ( ) Element of QC-pred_symbols Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ) iff ex x being ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ex p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st a : ( ( ) ( ) set ) = Ex (x : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,p : ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) );
end;

theorem :: GOEDELCP:19
for Al being ( ( ) ( ) QC-alphabet ) st Al : ( ( ) ( ) QC-alphabet ) is countable holds
CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is countable ;

theorem :: GOEDELCP:20
for Al being ( ( ) ( ) QC-alphabet ) st Al : ( ( ) ( ) QC-alphabet ) is countable holds
( not ExCl Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is empty & ExCl Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is countable ) ;

definition
let Al be ( ( ) ( ) QC-alphabet ) ;
let p be ( ( ) ( ) Element of QC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) ) ;
assume p : ( ( ) ( ) Element of QC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) ) is existential ;
func Ex-bound_in p -> ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) means :: GOEDELCP:def 4
 ex q being ( ( ) ( ) Element of QC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of QC-pred_symbols Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ) = Ex (it : ( ( bound_QC-variables Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -valued V45(K224(Al : ( ( ) ( ) QC-alphabet ) ,p : ( ( ) ( ) Element of QC-pred_symbols Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bound_QC-variables Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite V45(K224(Al : ( ( ) ( ) QC-alphabet ) ,p : ( ( ) ( ) Element of QC-pred_symbols Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like countable ) FinSequence of QC-variables Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of QC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of QC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) ) ;
end;

definition
let Al be ( ( ) ( ) QC-alphabet ) ;
let p be ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
assume p : ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) is existential ;
func Ex-the_scope_of p -> ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) means :: GOEDELCP:def 5
 ex x being ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st p : ( ( ) ( ) Element of QC-pred_symbols Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ) = Ex (x : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,it : ( ( bound_QC-variables Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -valued V45(K224(Al : ( ( ) ( ) QC-alphabet ) ,p : ( ( ) ( ) Element of QC-pred_symbols Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bound_QC-variables Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite V45(K224(Al : ( ( ) ( ) QC-alphabet ) ,p : ( ( ) ( ) Element of QC-pred_symbols Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like countable ) FinSequence of QC-variables Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
end;

definition
let Al be ( ( ) ( ) QC-alphabet ) ;
let F be ( ( Function-like V32( NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V32( NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Function of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
let a be ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;
func bound_in (F,a) -> ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) means :: GOEDELCP:def 6
 for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st p : ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) = F : ( ( ) ( ) Element of QC-pred_symbols Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ) . a : ( ( bound_QC-variables Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -valued V45(K224(Al : ( ( ) ( ) QC-alphabet ) ,F : ( ( ) ( ) Element of QC-pred_symbols Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bound_QC-variables Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite V45(K224(Al : ( ( ) ( ) QC-alphabet ) ,F : ( ( ) ( ) Element of QC-pred_symbols Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like countable ) FinSequence of QC-variables Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds
it : ( ( ) ( ) Element of vSUB Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ) = Ex-bound_in p : ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;
end;

definition
let Al be ( ( ) ( ) QC-alphabet ) ;
let F be ( ( Function-like V32( NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V32( NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Function of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
let a be ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;
func the_scope_of (F,a) -> ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) means :: GOEDELCP:def 7
 for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st p : ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) = F : ( ( ) ( ) Element of QC-pred_symbols Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ) . a : ( ( bound_QC-variables Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -valued V45(K224(Al : ( ( ) ( ) QC-alphabet ) ,F : ( ( ) ( ) Element of QC-pred_symbols Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bound_QC-variables Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite V45(K224(Al : ( ( ) ( ) QC-alphabet ) ,F : ( ( ) ( ) Element of QC-pred_symbols Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like countable ) FinSequence of QC-variables Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds
it : ( ( ) ( ) Element of vSUB Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ) = Ex-the_scope_of p : ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
end;

definition
let Al be ( ( ) ( ) QC-alphabet ) ;
let X be ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
func still_not-bound_in X -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) equals :: GOEDELCP:def 8
 union { (still_not-bound_in p : ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool (bound_QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) where p is ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : p : ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF Al : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) in X : ( ( ) ( ) Element of QC-pred_symbols Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ) } : ( ( ) ( ) set ) ;
end;

theorem :: GOEDELCP:21
for Al being ( ( ) ( ) QC-alphabet )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) in X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: GOEDELCP:22
for Al being ( ( ) ( ) QC-alphabet )
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for x being ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds
( Ex-bound_in (Ex (x : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) = x : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) & Ex-the_scope_of (Ex (x : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ,p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) = p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: GOEDELCP:23
for Al being ( ( ) ( ) QC-alphabet )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |- VERUM Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: GOEDELCP:24
for Al being ( ( ) ( ) QC-alphabet )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
( X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |- 'not' (VERUM Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) iff X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is Inconsistent ) ;

theorem :: GOEDELCP:25
for Al being ( ( ) ( ) QC-alphabet )
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for f, g being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st 0 : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) < len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) & |- f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ^ <*p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) *> : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite V45(1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds
|- (((Ant f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ^ g : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ^ <*(Suc f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) *> : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite V45(1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ^ <*p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) *> : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite V45(1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V30() V35() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: GOEDELCP:26
for Al being ( ( ) ( ) QC-alphabet )
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds still_not-bound_in {p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( finite countable ) Element of bool (CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = still_not-bound_in p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool (bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: GOEDELCP:27
for Al being ( ( ) ( ) QC-alphabet )
for X, Y being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds still_not-bound_in (X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \/ Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool (CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = (still_not-bound_in X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \/ (still_not-bound_in Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool (bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: GOEDELCP:28
for Al being ( ( ) ( ) QC-alphabet )
for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is finite holds
ex x being ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables Al : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st not x : ( ( ) ( ) bound_QC-variable of ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) in A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: GOEDELCP:29
for Al being ( ( ) ( ) QC-alphabet )
for X, Y being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
still_not-bound_in X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= still_not-bound_in Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: GOEDELCP:30
for Al being ( ( ) ( ) QC-alphabet )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds still_not-bound_in (rng f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( finite countable ) Element of bool (CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = still_not-bound_in f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite countable denumerable ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like countable ) FinSequence of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool (bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: GOEDELCP:31
for Al being ( ( ) ( ) QC-alphabet )
for CX being ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) st Al : ( ( ) ( ) QC-alphabet ) is countable & still_not-bound_in CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is finite holds
ex CY being ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) st
( CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) c= CY : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) & CY : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is with_examples ) ;

theorem :: GOEDELCP:32
for Al being ( ( ) ( ) QC-alphabet )
for X, Y being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) & X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: GOEDELCP:33
for Al being ( ( ) ( ) QC-alphabet )
for CX being ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) st Al : ( ( ) ( ) QC-alphabet ) is countable & CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is with_examples holds
ex CY being ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) st
( CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) c= CY : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) & CY : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is negation_faithful & CY : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) is with_examples ) ;

theorem :: GOEDELCP:34
for Al being ( ( ) ( ) QC-alphabet )
for CX being ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) st Al : ( ( ) ( ) QC-alphabet ) is countable & still_not-bound_in CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is finite holds
ex CZ being ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) ex JH1 being ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Henkin_interpretation of CZ : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) ) st JH1 : ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354((HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Henkin_interpretation of b3 : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) ) , valH Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (b1 : ( ( ) ( ) QC-alphabet ) ,(HCar b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , HCar b1 : ( ( ) ( ) QC-alphabet ) : ( ( non empty ) ( non empty ) set ) )) ) |= CX : ( ( Consistent ) ( Consistent ) Subset of ( ( ) ( non empty ) set ) ) ;

begin

theorem :: GOEDELCP:35
for Al being ( ( ) ( ) QC-alphabet )
for X, Y being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for A being ( ( non empty ) ( non empty ) set )
for J being ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354(b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354(b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) interpretation of Al : ( ( ) ( ) QC-alphabet ) ,A : ( ( non empty ) ( non empty ) set ) )
for v being ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined b4 : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (Al : ( ( ) ( ) QC-alphabet ) ,A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) )) ) st J : ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354(b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354(b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) interpretation of b1 : ( ( ) ( ) QC-alphabet ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ,v : ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined b4 : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (b1 : ( ( ) ( ) QC-alphabet ) ,b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) )) ) |= X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
J : ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354(b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354(b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) interpretation of b1 : ( ( ) ( ) QC-alphabet ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ,v : ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined b4 : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (b1 : ( ( ) ( ) QC-alphabet ) ,b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) )) ) |= Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: GOEDELCP:36
for Al being ( ( ) ( ) QC-alphabet )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st still_not-bound_in X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is finite holds
still_not-bound_in (X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \/ {p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( finite countable ) Element of bool (CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool (CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is finite ;

theorem :: GOEDELCP:37
for Al being ( ( ) ( ) QC-alphabet )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for A being ( ( non empty ) ( non empty ) set )
for J being ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354(b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354(b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) interpretation of Al : ( ( ) ( ) QC-alphabet ) ,A : ( ( non empty ) ( non empty ) set ) )
for v being ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined b4 : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (Al : ( ( ) ( ) QC-alphabet ) ,A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) )) ) st X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |= p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds
not J : ( ( ) ( Relation-like QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) -defined K354(b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like V32( QC-pred_symbols b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) set ) ,K354(b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) interpretation of b1 : ( ( ) ( ) QC-alphabet ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ,v : ( ( ) ( Relation-like bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined b4 : ( ( non empty ) ( non empty ) set ) -valued Function-like V32( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ) Element of Valuations_in (b1 : ( ( ) ( ) QC-alphabet ) ,b4 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) M5( bound_QC-variables b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( ) Element of bool (QC-variables b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) )) ) |= X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \/ {('not' p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( finite countable ) Element of bool (CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool (CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: GOEDELCP:38
for Al being ( ( ) ( ) QC-alphabet )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for p being ( ( ) ( ) Element of CQC-WFF Al : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st Al : ( ( ) ( ) QC-alphabet ) is countable & still_not-bound_in X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is finite & X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |= p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds
X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) |- p : ( ( ) ( ) Element of CQC-WFF b1 : ( ( ) ( ) QC-alphabet ) : ( ( ) ( non empty ) Element of bool (QC-WFF b1 : ( ( ) ( ) QC-alphabet ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;