:: CQC_THE3 semantic presentation

theorem Th1: :: CQC_THE3:1

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

proof end;

theorem Th2: :: CQC_THE3:2

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

proof end;

theorem Th3: :: CQC_THE3:3

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

proof end;

theorem Th4: :: CQC_THE3:4

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

proof end;

definition

let c₁, c₂ be Element of CQC-WFF ;
pred c₁ |- c₂ means :Def1: :: CQC_THE3:def 1
{a₁} |- a₂;

end;

:: deftheorem Def1 defines |- CQC_THE3:def 1 :

theorem Th5: :: CQC_THE3:5

for b₁ being Element of CQC-WFF holds b₁ |- b₁

proof end;

theorem Th6: :: CQC_THE3:6

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

proof end;

definition

let c₁, c₂ be Subset of CQC-WFF ;
pred c₁ |- c₂ means :Def2: :: CQC_THE3:def 2
for b₁ being Element of CQC-WFF st b₁ in a₂ holds
a₁ |- b₁;

end;

:: deftheorem Def2 defines |- CQC_THE3:def 2 :

theorem Th7: :: CQC_THE3:7

for b₁, b₂ being Subset of CQC-WFF holds
( b₁ |- b₂ iff b₂ c= Cn b₁ )

proof end;

theorem Th8: :: CQC_THE3:8

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

proof end;

theorem Th9: :: CQC_THE3:9

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

proof end;

theorem Th10: :: CQC_THE3:10

for b₁ being Element of CQC-WFF
for b₂ being Subset of CQC-WFF holds
( b₂ |- {b₁} iff b₂ |- b₁ )

proof end;

theorem Th11: :: CQC_THE3:11

for b₁, b₂ being Element of CQC-WFF holds
( {b₁} |- {b₂} iff b₁ |- b₂ )

proof end;

theorem Th12: :: CQC_THE3:12

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

proof end;

theorem Th13: :: CQC_THE3:13

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

proof end;

theorem Th14: :: CQC_THE3:14

{} CQC-WFF |- TAUT by Th13;

definition

let c₁ be Subset of CQC-WFF ;
pred |- c₁ means :Def3: :: CQC_THE3:def 3
for b₁ being Element of CQC-WFF st b₁ in a₁ holds
|- b₁;

end;

:: deftheorem Def3 defines |- CQC_THE3:def 3 :

theorem Th15: :: CQC_THE3:15

for b₁ being Subset of CQC-WFF holds
( |- b₁ iff {} CQC-WFF |- b₁ )

proof end;

theorem Th16: :: CQC_THE3:16

|- TAUT by Th14, Th15;

theorem Th17: :: CQC_THE3:17

for b₁ being Subset of CQC-WFF holds
( |- b₁ iff b₁ c= TAUT )

proof end;

definition

let c₁, c₂ be Subset of CQC-WFF ;
pred c₁ |-| c₂ means :Def4: :: CQC_THE3:def 4
for b₁ being Element of CQC-WFF holds
( a₁ |- b₁ iff a₂ |- b₁ );
reflexivity ;
symmetry ;

end;

:: deftheorem Def4 defines |-| CQC_THE3:def 4 :

theorem Th18: :: CQC_THE3:18

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

proof end;

theorem Th19: :: CQC_THE3:19

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

proof end;

theorem Th20: :: CQC_THE3:20

for b₁, b₂ being Subset of CQC-WFF holds
( b₁ |-| b₂ iff Cn b₁ = Cn b₂ )

proof end;

Lemma21: for b₁, b₂ being Subset of CQC-WFF holds b₁ \/ b₂ c= (Cn b₁) \/ (Cn b₂)

proof end;

theorem Th21: :: CQC_THE3:21

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

proof end;

theorem Th22: :: CQC_THE3:22

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

proof end;

theorem Th23: :: CQC_THE3:23

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

proof end;

theorem Th24: :: CQC_THE3:24

for b₁, b₂ being Subset of CQC-WFF holds b₁ \/ b₂ |-| (Cn b₁) \/ (Cn b₂)

proof end;

theorem Th25: :: CQC_THE3:25

for b₁, b₂, b₃ being Subset of CQC-WFF st b₁ |-| b₂ holds
b₁ \/ b₃ |-| b₂ \/ b₃

proof end;

theorem Th26: :: CQC_THE3:26

for b₁, b₂, b₃, b₄ being Subset of CQC-WFF st b₁ |-| b₂ & b₁ \/ b₃ |- b₄ holds
b₂ \/ b₃ |- b₄

proof end;

theorem Th27: :: CQC_THE3:27

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

proof end;

definition

let c₁, c₂ be Element of CQC-WFF ;
pred c₁ |-| c₂ means :Def5: :: CQC_THE3:def 5
( a₁ |- a₂ & a₂ |- a₁ );
reflexivity by Th5;
symmetry ;

end;

:: deftheorem Def5 defines |-| CQC_THE3:def 5 :

theorem Th28: :: CQC_THE3:28

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

proof end;

theorem Th29: :: CQC_THE3:29

for b₁, b₂ being Element of CQC-WFF holds
( b₁ |-| b₂ iff {b₁} |-| {b₂} )

proof end;

theorem Th30: :: CQC_THE3:30

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

proof end;

theorem Th31: :: CQC_THE3:31

for b₁, b₂ being Element of CQC-WFF holds {b₁,b₂} |-| {(b₁ '&' b₂)}

proof end;

theorem Th32: :: CQC_THE3:32

for b₁, b₂ being Element of CQC-WFF holds b₁ '&' b₂ |-| b₂ '&' b₁

proof end;

Lemma31: for b₁, b₂ being Element of CQC-WFF
for b₃ being Subset of CQC-WFF st b₃ |- b₁ & b₃ |- b₂ holds
b₃ |- b₁ '&' b₂

proof end;

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

proof end;

theorem Th33: :: CQC_THE3:33

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

Lemma33: for b₁, b₂, b₃, b₄ being Element of CQC-WFF st b₁ |-| b₂ & b₃ |-| b₄ holds
b₁ '&' b₃ |- b₂ '&' b₄

proof end;

theorem Th34: :: CQC_THE3:34

for b₁, b₂, b₃, b₄ being Element of CQC-WFF st b₁ |-| b₂ & b₃ |-| b₄ holds
b₁ '&' b₃ |-| b₂ '&' b₄

proof end;

theorem Th35: :: CQC_THE3:35

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

proof end;

theorem Th36: :: CQC_THE3:36

for b₁ being Element of CQC-WFF
for b₂ being bound_QC-variable holds All b₂,b₁ |-| b₁

proof end;

theorem Th37: :: CQC_THE3:37

for b₁, b₂ being Element of CQC-WFF
for b₃, b₄ being bound_QC-variable st b₁ |-| b₂ holds
All b₃,b₁ |-| All b₄,b₂

proof end;

definition

let c₁, c₂ be Element of CQC-WFF ;
pred c₁ is_an_universal_closure_of c₂ means :Def6: :: CQC_THE3:def 6
( a₁ is closed & ex b₁ being Nat st
( 1 <= b₁ & ex b₂ being FinSequence st
( len b₂ = b₁ & b₂ . 1 = a₂ & b₂ . b₁ = a₁ & ( for b₃ being Nat st 1 <= b₃ & b₃ < b₁ holds
ex b₄ being bound_QC-variableex b₅ being Element of CQC-WFF st
( b₅ = b₂ . b₃ & b₂ . (b₃ + 1) = All b₄,b₅ ) ) ) ) );

end;

:: deftheorem Def6 defines is_an_universal_closure_of CQC_THE3:def 6 :

theorem Th38: :: CQC_THE3:38

for b₁, b₂ being Element of CQC-WFF st b₁ is_an_universal_closure_of b₂ holds
b₁ |-| b₂

proof end;

theorem Th39: :: CQC_THE3:39

for b₁, b₂ being Element of CQC-WFF st |- b₁ => b₂ holds
b₁ |- b₂

proof end;

theorem Th40: :: CQC_THE3:40

for b₁, b₂ being Element of CQC-WFF
for b₃ being Subset of CQC-WFF st b₃ |- b₁ => b₂ holds
b₃ \/ {b₁} |- b₂

proof end;

theorem Th41: :: CQC_THE3:41

for b₁, b₂ being Element of CQC-WFF st b₁ is closed & b₁ |- b₂ holds
|- b₁ => b₂

proof end;

theorem Th42: :: CQC_THE3:42

for b₁, b₂, b₃ being Element of CQC-WFF
for b₄ being Subset of CQC-WFF st b₁ is_an_universal_closure_of b₂ holds
( b₄ \/ {b₂} |- b₃ iff b₄ |- b₁ => b₃ )

proof end;

theorem Th43: :: CQC_THE3:43

for b₁, b₂ being Element of CQC-WFF st b₁ is closed & b₁ |- b₂ holds
'not' b₂ |- 'not' b₁

proof end;

theorem Th44: :: CQC_THE3:44

for b₁, b₂ being Element of CQC-WFF
for b₃ being Subset of CQC-WFF st b₁ is closed & b₃ \/ {b₁} |- b₂ holds
b₃ \/ {('not' b₂)} |- 'not' b₁

proof end;

theorem Th45: :: CQC_THE3:45

for b₁, b₂ being Element of CQC-WFF st b₁ is closed & 'not' b₁ |- 'not' b₂ holds
b₂ |- b₁

proof end;

theorem Th46: :: CQC_THE3:46

for b₁, b₂ being Element of CQC-WFF
for b₃ being Subset of CQC-WFF st b₁ is closed & b₃ \/ {('not' b₁)} |- 'not' b₂ holds
b₃ \/ {b₂} |- b₁

proof end;

theorem Th47: :: CQC_THE3:47

for b₁, b₂ being Element of CQC-WFF st b₁ is closed & b₂ is closed holds
( b₁ |- b₂ iff 'not' b₂ |- 'not' b₁ ) by Th43, Th45;

theorem Th48: :: CQC_THE3:48

for b₁, b₂, b₃, b₄ being Element of CQC-WFF st b₁ is_an_universal_closure_of b₂ & b₃ is_an_universal_closure_of b₄ holds
( b₂ |- b₄ iff 'not' b₃ |- 'not' b₁ )

proof end;

theorem Th49: :: CQC_THE3:49

for b₁, b₂, b₃, b₄ being Element of CQC-WFF st b₁ is_an_universal_closure_of b₂ & b₃ is_an_universal_closure_of b₄ holds
( b₂ |-| b₄ iff 'not' b₁ |-| 'not' b₃ )

proof end;

definition

let c₁, c₂ be Element of CQC-WFF ;
pred c₁ <==> c₂ means :Def7: :: CQC_THE3:def 7
|- a₁ <=> a₂;
reflexivity

proof end;

symmetry

proof end;

end;

:: deftheorem Def7 defines <==> CQC_THE3:def 7 :

theorem Th50: :: CQC_THE3:50

for b₁, b₂ being Element of CQC-WFF holds
( b₁ <==> b₂ iff ( |- b₁ => b₂ & |- b₂ => b₁ ) )

proof end;

theorem Th51: :: CQC_THE3:51

for b₁, b₂, b₃ being Element of CQC-WFF st b₁ <==> b₂ & b₂ <==> b₃ holds
b₁ <==> b₃

proof end;

theorem Th52: :: CQC_THE3:52

for b₁, b₂ being Element of CQC-WFF st b₁ <==> b₂ holds
b₁ |-| b₂

proof end;

Lemma46: for b₁, b₂ being Element of CQC-WFF st b₁ <==> b₂ holds
'not' b₁ <==> 'not' b₂

proof end;

Lemma47: for b₁, b₂ being Element of CQC-WFF st 'not' b₁ <==> 'not' b₂ holds
b₁ <==> b₂

proof end;

theorem Th53: :: CQC_THE3:53

for b₁, b₂ being Element of CQC-WFF holds
( b₁ <==> b₂ iff 'not' b₁ <==> 'not' b₂ ) by Lemma46, Lemma47;

theorem Th54: :: CQC_THE3:54

for b₁, b₂, b₃, b₄ being Element of CQC-WFF st b₁ <==> b₂ & b₃ <==> b₄ holds
b₁ '&' b₃ <==> b₂ '&' b₄

proof end;

theorem Th55: :: CQC_THE3:55

for b₁, b₂, b₃, b₄ being Element of CQC-WFF st b₁ <==> b₂ & b₃ <==> b₄ holds
b₁ => b₃ <==> b₂ => b₄

proof end;

theorem Th56: :: CQC_THE3:56

for b₁, b₂, b₃, b₄ being Element of CQC-WFF st b₁ <==> b₂ & b₃ <==> b₄ holds
b₁ 'or' b₃ <==> b₂ 'or' b₄

proof end;

theorem Th57: :: CQC_THE3:57

for b₁, b₂, b₃, b₄ being Element of CQC-WFF st b₁ <==> b₂ & b₃ <==> b₄ holds
b₁ <=> b₃ <==> b₂ <=> b₄

proof end;

theorem Th58: :: CQC_THE3:58

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st b₁ <==> b₂ holds
All b₃,b₁ <==> All b₃,b₂

proof end;

theorem Th59: :: CQC_THE3:59

for b₁, b₂ being Element of CQC-WFF
for b₃ being bound_QC-variable st b₁ <==> b₂ holds
Ex b₃,b₁ <==> Ex b₃,b₂

proof end;

theorem Th60: :: CQC_THE3:60

canceled;

theorem Th61: :: CQC_THE3:61

for b₁ being Nat
for b₂ being QC-variable_list of b₁
for b₃ being free_QC-variable
for b₄ being bound_QC-variable holds still_not-bound_in b₂ c= still_not-bound_in (Subst b₂,(b₃ .--> b₄))

proof end;

theorem Th62: :: CQC_THE3:62

for b₁ being Nat
for b₂ being QC-variable_list of b₁
for b₃ being free_QC-variable
for b₄ being bound_QC-variable holds still_not-bound_in (Subst b₂,(b₃ .--> b₄)) c= (still_not-bound_in b₂) \/ {b₄}

proof end;

theorem Th63: :: CQC_THE3:63

for b₁ being bound_QC-variable
for b₂ being QC-formula holds still_not-bound_in b₂ c= still_not-bound_in (b₂ . b₁)

proof end;

theorem Th64: :: CQC_THE3:64

for b₁ being bound_QC-variable
for b₂ being QC-formula holds still_not-bound_in (b₂ . b₁) c= (still_not-bound_in b₂) \/ {b₁}

proof end;

theorem Th65: :: CQC_THE3:65

for b₁ being Element of CQC-WFF
for b₂ being QC-formula
for b₃, b₄ being bound_QC-variable st b₁ = b₂ . b₃ & b₃ <> b₄ & not b₄ in still_not-bound_in b₂ holds
not b₄ in still_not-bound_in b₁

proof end;

theorem Th66: :: CQC_THE3:66

for b₁, b₂ being Element of CQC-WFF
for b₃ being QC-formula
for b₄, b₅ being bound_QC-variable st b₁ = b₃ . b₄ & b₂ = b₃ . b₅ & not b₄ in still_not-bound_in b₃ & not b₅ in still_not-bound_in b₃ holds
All b₄,b₁ <==> All b₅,b₂

proof end;