:: GOEDELCP semantic presentation

definition

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

end;

:: deftheorem Def1 defines negation_faithful GOEDELCP:def 1 :

definition

let c₁ be Subset of CQC-WFF ;
attr a₁ is with_examples means :Def2: :: GOEDELCP:def 2
for b₁ being bound_QC-variable
for b₂ being Element of CQC-WFF ex b₃ being bound_QC-variable st a₁ |- ('not' (Ex b₁,b₂)) 'or' (b₂ . b₁,b₃);

end;

:: deftheorem Def2 defines with_examples GOEDELCP:def 2 :

theorem Th1: :: GOEDELCP:1

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

theorem Th2: :: GOEDELCP:2

for b₁, b₂ being Element of CQC-WFF
for b₃ being FinSequence of CQC-WFF st |- b₃ ^ <*(('not' b₁) 'or' b₂)*> & |- b₃ ^ <*b₁*> holds
|- b₃ ^ <*b₂*>

proof end;

theorem Th3: :: GOEDELCP:3

for b₁ being Subset of CQC-WFF
for b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st b₁ is with_examples holds
( b₁ |- Ex b₃,b₂ iff ex b₄ being bound_QC-variable st b₁ |- b₂ . b₃,b₄ )

proof end;

theorem Th4: :: GOEDELCP:4

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

theorem Th5: :: GOEDELCP:5

for b₁, b₂ being Element of CQC-WFF
for b₃ being FinSequence of CQC-WFF st |- b₃ ^ <*b₁*> & |- b₃ ^ <*b₂*> holds
|- b₃ ^ <*(b₁ '&' b₂)*>

proof end;

theorem Th6: :: GOEDELCP:6

for b₁ being Subset of CQC-WFF
for b₂, b₃ being Element of CQC-WFF holds
( ( b₁ |- b₂ & b₁ |- b₃ ) iff b₁ |- b₂ '&' b₃ )

proof end;

theorem Th7: :: GOEDELCP:7

for b₁, b₂ being Element of CQC-WFF
for b₃ being Consistent Subset of CQC-WFF
for b₄ being Henkin_interpretation of b₃ st ( b₃ is negation_faithful & b₃ is with_examples implies ( b₄, valH |= b₁ iff b₃ |- b₁ ) ) & ( b₃ is negation_faithful & b₃ is with_examples implies ( b₄, valH |= b₂ iff b₃ |- b₂ ) ) & b₃ is negation_faithful & b₃ is with_examples holds
( b₄, valH |= b₁ '&' b₂ iff b₃ |- b₁ '&' b₂ ) by Th6, VALUAT_1:29;

theorem Th8: :: GOEDELCP:8

for b₁ being Consistent Subset of CQC-WFF
for b₂ being Henkin_interpretation of b₁
for b₃ being Element of CQC-WFF st QuantNbr b₃ <= 0 & b₁ is negation_faithful & b₁ is with_examples holds
( b₂, valH |= b₃ iff b₁ |- b₃ )

proof end;

theorem Th9: :: GOEDELCP:9

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable
for b₃ being non empty set
for b₄ being interpretation of b₃
for b₅ being Element of Valuations_in b₃ holds
( b₄,b₅ |= Ex b₂,b₁ iff ex b₆ being Element of b₃ st b₄,b₅ . (b₂ | b₆) |= b₁ )

proof end;

theorem Th10: :: GOEDELCP:10

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable
for b₃ being Consistent Subset of CQC-WFF
for b₄ being Henkin_interpretation of b₃ holds
( b₄, valH |= Ex b₂,b₁ iff ex b₅ being bound_QC-variable st b₄, valH |= b₁ . b₂,b₅ )

proof end;

theorem Th11: :: GOEDELCP:11

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable
for b₃ being non empty set
for b₄ being interpretation of b₃
for b₅ being Element of Valuations_in b₃ holds
( b₄,b₅ |= 'not' (Ex b₂,('not' b₁)) iff b₄,b₅ |= All b₂,b₁ )

proof end;

theorem Th12: :: GOEDELCP:12

for b₁ being Subset of CQC-WFF
for b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable holds
( b₁ |- 'not' (Ex b₃,('not' b₂)) iff b₁ |- All b₃,b₂ )

proof end;

theorem Th13: :: GOEDELCP:13

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable holds QuantNbr (Ex b₂,b₁) = (QuantNbr b₁) + 1

proof end;

theorem Th14: :: GOEDELCP:14

for b₁ being Element of CQC-WFF
for b₂, b₃ being bound_QC-variable holds QuantNbr b₁ = QuantNbr (b₁ . b₂,b₃)

proof end;

theorem Th15: :: GOEDELCP:15

for b₁ being Consistent Subset of CQC-WFF
for b₂ being Henkin_interpretation of b₁
for b₃ being Element of CQC-WFF st QuantNbr b₃ = 1 & b₁ is negation_faithful & b₁ is with_examples holds
( b₂, valH |= b₃ iff b₁ |- b₃ )

proof end;

theorem Th16: :: GOEDELCP:16

for b₁ being Consistent Subset of CQC-WFF
for b₂ being Henkin_interpretation of b₁
for b₃ being Nat st ( for b₄ being Element of CQC-WFF st QuantNbr b₄ <= b₃ & b₁ is negation_faithful & b₁ is with_examples holds
( b₂, valH |= b₄ iff b₁ |- b₄ ) ) holds
for b₄ being Element of CQC-WFF st QuantNbr b₄ <= b₃ + 1 & b₁ is negation_faithful & b₁ is with_examples holds
( b₂, valH |= b₄ iff b₁ |- b₄ )

proof end;

theorem Th17: :: GOEDELCP:17

for b₁ being Consistent Subset of CQC-WFF
for b₂ being Henkin_interpretation of b₁
for b₃ being Element of CQC-WFF st b₁ is negation_faithful & b₁ is with_examples holds
( b₂, valH |= b₃ iff b₁ |- b₃ )

proof end;

theorem Th18: :: GOEDELCP:18

QC-WFF is countable

proof end;

definition

func ExCl -> Subset of CQC-WFF means :Def3: :: GOEDELCP:def 3
for b₁ being set holds
( b₁ in a₁ iff ex b₂ being bound_QC-variableex b₃ being Element of CQC-WFF st b₁ = Ex b₂,b₃ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines ExCl GOEDELCP:def 3 :

theorem Th19: :: GOEDELCP:19

CQC-WFF is countable by Th18, CARD_4:46;

theorem Th20: :: GOEDELCP:20

( not ExCl is empty & ExCl is countable )

proof end;

Lemma23: for b₁ being non empty set st b₁ is countable holds
ex b₂ being Function st
( dom b₂ = NAT & b₁ = rng b₂ )

proof end;

definition

let c₁ be Element of QC-WFF ;
assume E24: c₁ is existential ;
func Ex-bound_in c₁ -> bound_QC-variable means :Def4: :: GOEDELCP:def 4
ex b₁ being Element of QC-WFF st a₁ = Ex a₂,b₁;
existence by E24, QC_LANG2:def 13;
uniqueness by QC_LANG2:19;

end;

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

definition

let c₁ be Element of CQC-WFF ;
assume E25: c₁ is existential ;
func Ex-the_scope_of c₁ -> Element of CQC-WFF means :Def5: :: GOEDELCP:def 5
ex b₁ being bound_QC-variable st a₁ = Ex b₁,a₂;
existence

proof end;

uniqueness by QC_LANG2:19;

end;

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

definition

let c₁ be Function of NAT , CQC-WFF ;
let c₂ be Nat;
func bound_in c₁,c₂ -> bound_QC-variable means :Def6: :: GOEDELCP:def 6
for b₁ being Element of CQC-WFF st b₁ = a₁ . a₂ holds
a₃ = Ex-bound_in b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines bound_in GOEDELCP:def 6 :

definition

let c₁ be Function of NAT , CQC-WFF ;
let c₂ be Nat;
func the_scope_of c₁,c₂ -> Element of CQC-WFF means :Def7: :: GOEDELCP:def 7
for b₁ being Element of CQC-WFF st b₁ = a₁ . a₂ holds
a₃ = Ex-the_scope_of b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines the_scope_of GOEDELCP:def 7 :

definition

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

proof end;

end;

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

theorem Th21: :: GOEDELCP:21

for b₁ being Subset of CQC-WFF
for b₂ being Element of CQC-WFF st b₂ in b₁ holds
b₁ |- b₂

proof end;

theorem Th22: :: GOEDELCP:22

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable holds
( Ex-bound_in (Ex b₂,b₁) = b₂ & Ex-the_scope_of (Ex b₂,b₁) = b₁ )

proof end;

theorem Th23: :: GOEDELCP:23

for b₁ being Subset of CQC-WFF holds b₁ |- VERUM

proof end;

theorem Th24: :: GOEDELCP:24

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

proof end;

theorem Th25: :: GOEDELCP:25

for b₁ being Element of CQC-WFF
for b₂, b₃ being FinSequence of CQC-WFF st 0 < len b₂ & |- b₂ ^ <*b₁*> holds
|- (((Ant b₂) ^ b₃) ^ <*(Suc b₂)*>) ^ <*b₁*>

proof end;

theorem Th26: :: GOEDELCP:26

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

proof end;

theorem Th27: :: GOEDELCP:27

for b₁, b₂ being Subset of CQC-WFF holds still_not-bound_in (b₁ \/ b₂) = (still_not-bound_in b₁) \/ (still_not-bound_in b₂)

proof end;

theorem Th28: :: GOEDELCP:28

for b₁ being Subset of bound_QC-variables st b₁ is finite holds
ex b₂ being bound_QC-variable st not b₂ in b₁

proof end;

theorem Th29: :: GOEDELCP:29

for b₁, b₂ being Subset of CQC-WFF st b₁ c= b₂ holds
still_not-bound_in b₁ c= still_not-bound_in b₂

proof end;

theorem Th30: :: GOEDELCP:30

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

proof end;

theorem Th31: :: GOEDELCP:31

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

proof end;

theorem Th32: :: GOEDELCP:32

for b₁, b₂ being Subset of CQC-WFF
for b₃ being Element of CQC-WFF st b₁ |- b₃ & b₁ c= b₂ holds
b₂ |- b₃

proof end;

theorem Th33: :: GOEDELCP:33

for b₁ being Consistent Subset of CQC-WFF st b₁ is with_examples holds
ex b₂ being Consistent Subset of CQC-WFF st
( b₁ c= b₂ & b₂ is negation_faithful & b₂ is with_examples )

proof end;

theorem Th34: :: GOEDELCP:34

for b₁ being Consistent Subset of CQC-WFF st still_not-bound_in b₁ is finite holds
ex b₂ being Consistent Subset of CQC-WFF ex b₃ being Henkin_interpretation of b₂ st b₃, valH |= b₁

proof end;

theorem Th35: :: GOEDELCP:35

for b₁, b₂ being Subset of CQC-WFF
for b₃ being non empty set
for b₄ being interpretation of b₃
for b₅ being Element of Valuations_in b₃ st b₄,b₅ |= b₁ & b₂ c= b₁ holds
b₄,b₅ |= b₂

proof end;

theorem Th36: :: GOEDELCP:36

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

proof end;

theorem Th37: :: GOEDELCP:37

for b₁ being Subset of CQC-WFF
for b₂ being Element of CQC-WFF
for b₃ being non empty set
for b₄ being interpretation of b₃
for b₅ being Element of Valuations_in b₃ st b₁ |= b₂ holds
not b₄,b₅ |= b₁ \/ {('not' b₂)}

proof end;

theorem Th38: :: GOEDELCP:38

for b₁ being Subset of CQC-WFF
for b₂ being Element of CQC-WFF st still_not-bound_in b₁ is finite & b₁ |= b₂ holds
b₁ |- b₂

proof end;