CQC_THE1: A First-Order Predicate Calculus. Axiomatics, the Consequence Operation and a Concept of Proof

:: A First-Order Predicate Calculus. Axiomatics, the Consequence Operation and a Concept of Proof
:: by Agata Darmochwa{\l}
::
:: Received May 25, 1990
:: Copyright (c) 1990-2011 Association of Mizar Users

begin

theorem :: CQC_THE1:1

canceled;

theorem :: CQC_THE1:2

canceled;

theorem :: CQC_THE1:3

canceled;

theorem :: CQC_THE1:4

canceled;

theorem :: CQC_THE1:5

canceled;

theorem :: CQC_THE1:6

canceled;

theorem :: CQC_THE1:7

canceled;

theorem :: CQC_THE1:8

canceled;

theorem :: CQC_THE1:9

canceled;

theorem :: CQC_THE1:10

canceled;

theorem Th11: :: CQC_THE1:11

for n being Element of NAT holds { k where k is Element of NAT : k <= n + 1 } = { i where i is Element of NAT : i <= n } \/ {(n + 1)}

proof end;

theorem Th12: :: CQC_THE1:12

for n being Element of NAT holds { k where k is Element of NAT : k <= n } is finite

proof end;

theorem :: CQC_THE1:13

for X, Y, Z being set st X is finite & X c= [:Y,Z:] holds
ex A, B being set st
( A is finite & A c= Y & B is finite & B c= Z & X c= [:A,B:] ) by FINSET_1:32;

theorem :: CQC_THE1:14

for X, Z, Y being set st X is finite & Z is finite & X c= [:Y,Z:] holds
ex A being set st
( A is finite & A c= Y & X c= [:A,Z:] ) by FINSET_1:33;

definition

let T be Subset of CQC-WFF;
attr T is being_a_theory means :Def1: :: CQC_THE1:def 1
( VERUM in T & ( for p, q, r being Element of CQC-WFF
for s being QC-formula
for x, y being bound_QC-variable holds
( (('not' p) => p) => p in T & p => (('not' p) => q) in T & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T & (p '&' q) => (q '&' p) in T & ( p in T & p => q in T implies q in T ) & (All (x,p)) => p in T & ( p => q in T & not x in still_not-bound_in p implies p => (All (x,q)) in T ) & ( s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in T implies s . y in T ) ) ) );

end;

:: deftheorem Def1 defines being_a_theory CQC_THE1:def 1 :

theorem :: CQC_THE1:15

canceled;

theorem :: CQC_THE1:16

canceled;

theorem :: CQC_THE1:17

canceled;

theorem :: CQC_THE1:18

canceled;

theorem :: CQC_THE1:19

canceled;

theorem :: CQC_THE1:20

canceled;

theorem :: CQC_THE1:21

canceled;

theorem :: CQC_THE1:22

canceled;

theorem :: CQC_THE1:23

canceled;

theorem :: CQC_THE1:24

canceled;

theorem :: CQC_THE1:25

for T, S being Subset of CQC-WFF st T is being_a_theory & S is being_a_theory holds
T /\ S is being_a_theory

proof end;

definition

let X be Subset of CQC-WFF;
func Cn X -> Subset of CQC-WFF means :Def2: :: CQC_THE1:def 2
for t being Element of CQC-WFF holds
( t in it iff for T being Subset of CQC-WFF st T is being_a_theory & X c= T holds
t in T );
existence

proof end;

proof end;

end;

:: deftheorem Def2 defines Cn CQC_THE1:def 2 :

theorem :: CQC_THE1:26

canceled;

theorem Th27: :: CQC_THE1:27

for X being Subset of CQC-WFF holds VERUM in Cn X

proof end;

theorem Th28: :: CQC_THE1:28

for X being Subset of CQC-WFF
for p being Element of CQC-WFF holds (('not' p) => p) => p in Cn X

proof end;

theorem Th29: :: CQC_THE1:29

for X being Subset of CQC-WFF
for p, q being Element of CQC-WFF holds p => (('not' p) => q) in Cn X

proof end;

theorem Th30: :: CQC_THE1:30

for X being Subset of CQC-WFF
for p, q, r being Element of CQC-WFF holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Cn X

proof end;

theorem Th31: :: CQC_THE1:31

for X being Subset of CQC-WFF
for p, q being Element of CQC-WFF holds (p '&' q) => (q '&' p) in Cn X

proof end;

theorem Th32: :: CQC_THE1:32

for X being Subset of CQC-WFF
for p, q being Element of CQC-WFF st p in Cn X & p => q in Cn X holds
q in Cn X

proof end;

theorem Th33: :: CQC_THE1:33

for X being Subset of CQC-WFF
for p being Element of CQC-WFF
for x being bound_QC-variable holds (All (x,p)) => p in Cn X

proof end;

theorem Th34: :: CQC_THE1:34

for X being Subset of CQC-WFF
for p, q being Element of CQC-WFF
for x being bound_QC-variable st p => q in Cn X & not x in still_not-bound_in p holds
p => (All (x,q)) in Cn X

proof end;

theorem Th35: :: CQC_THE1:35

for X being Subset of CQC-WFF
for s being QC-formula
for x, y being bound_QC-variable st s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in Cn X holds
s . y in Cn X

proof end;

theorem Th36: :: CQC_THE1:36

for X being Subset of CQC-WFF holds Cn X is being_a_theory

proof end;

theorem Th37: :: CQC_THE1:37

for T, X being Subset of CQC-WFF st T is being_a_theory & X c= T holds
Cn X c= T

proof end;

theorem Th38: :: CQC_THE1:38

for X being Subset of CQC-WFF holds X c= Cn X

proof end;

theorem Th39: :: CQC_THE1:39

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

proof end;

Lm1: for X being Subset of CQC-WFF holds Cn (Cn X) c= Cn X

proof end;

theorem :: CQC_THE1:40

for X being Subset of CQC-WFF holds Cn (Cn X) = Cn X

proof end;

theorem Th41: :: CQC_THE1:41

for T being Subset of CQC-WFF holds
( T is being_a_theory iff Cn T = T )

proof end;

definition

func Proof_Step_Kinds -> set equals :: CQC_THE1:def 3
{ k where k is Element of NAT : k <= 9 } ;
coherence ;

end;

:: deftheorem defines Proof_Step_Kinds CQC_THE1:def 3 :

registration

cluster Proof_Step_Kinds -> non empty ;
coherence

proof end;

end;

theorem :: CQC_THE1:42

canceled;

theorem Th43: :: CQC_THE1:43

( 0 in Proof_Step_Kinds & 1 in Proof_Step_Kinds & 2 in Proof_Step_Kinds & 3 in Proof_Step_Kinds & 4 in Proof_Step_Kinds & 5 in Proof_Step_Kinds & 6 in Proof_Step_Kinds & 7 in Proof_Step_Kinds & 8 in Proof_Step_Kinds & 9 in Proof_Step_Kinds ) ;

theorem :: CQC_THE1:44

Proof_Step_Kinds is finite by Th12;

theorem Th45: :: CQC_THE1:45

for f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:]
for n being Nat st 1 <= n & n <= len f & not (f . n) `2 = 0 & not (f . n) `2 = 1 & not (f . n) `2 = 2 & not (f . n) `2 = 3 & not (f . n) `2 = 4 & not (f . n) `2 = 5 & not (f . n) `2 = 6 & not (f . n) `2 = 7 & not (f . n) `2 = 8 holds
(f . n) `2 = 9

proof end;

definition

let PR be FinSequence of [:CQC-WFF,Proof_Step_Kinds:];
let n be Nat;
let X be Subset of CQC-WFF;
pred PR,n is_a_correct_step_wrt X means :Def4: :: CQC_THE1:def 4
(PR . n) `1 in X if (PR . n) `2 = 0
(PR . n) `1 = VERUM if (PR . n) `2 = 1
ex p being Element of CQC-WFF st (PR . n) `1 = (('not' p) => p) => p if (PR . n) `2 = 2
ex p, q being Element of CQC-WFF st (PR . n) `1 = p => (('not' p) => q) if (PR . n) `2 = 3
ex p, q, r being Element of CQC-WFF st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) if (PR . n) `2 = 4
ex p, q being Element of CQC-WFF st (PR . n) `1 = (p '&' q) => (q '&' p) if (PR . n) `2 = 5
ex p being Element of CQC-WFF ex x being bound_QC-variable st (PR . n) `1 = (All (x,p)) => p if (PR . n) `2 = 6
ex i, j being Element of NAT ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) if (PR . n) `2 = 7
ex i being Element of NAT ex p, q being Element of CQC-WFF ex x being bound_QC-variable st
( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) if (PR . n) `2 = 8
ex i being Element of NAT ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) if (PR . n) `2 = 9
;
consistency ;

end;

:: deftheorem Def4 defines is_a_correct_step_wrt CQC_THE1:def 4 :

definition

let X be Subset of CQC-WFF;
let f be FinSequence of [:CQC-WFF,Proof_Step_Kinds:];
pred f is_a_proof_wrt X means :Def5: :: CQC_THE1:def 5
( f <> {} & ( for n being Element of NAT st 1 <= n & n <= len f holds
f,n is_a_correct_step_wrt X ) );

end;

:: deftheorem Def5 defines is_a_proof_wrt CQC_THE1:def 5 :

theorem :: CQC_THE1:46

canceled;

theorem :: CQC_THE1:47

canceled;

theorem :: CQC_THE1:48

canceled;

theorem :: CQC_THE1:49

canceled;

theorem :: CQC_THE1:50

canceled;

theorem :: CQC_THE1:51

canceled;

theorem :: CQC_THE1:52

canceled;

theorem :: CQC_THE1:53

canceled;

theorem :: CQC_THE1:54

canceled;

theorem :: CQC_THE1:55

canceled;

theorem :: CQC_THE1:56

canceled;

theorem :: CQC_THE1:57

for X being Subset of CQC-WFF
for f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st f is_a_proof_wrt X holds
rng f <> {}

proof end;

theorem Th58: :: CQC_THE1:58

for X being Subset of CQC-WFF
for f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st f is_a_proof_wrt X holds
1 <= len f

proof end;

theorem :: CQC_THE1:59

for X being Subset of CQC-WFF
for f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] holds
( not f is_a_proof_wrt X or (f . 1) `2 = 0 or (f . 1) `2 = 1 or (f . 1) `2 = 2 or (f . 1) `2 = 3 or (f . 1) `2 = 4 or (f . 1) `2 = 5 or (f . 1) `2 = 6 )

proof end;

theorem Th60: :: CQC_THE1:60

for n being Element of NAT
for X being Subset of CQC-WFF
for f, g being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st 1 <= n & n <= len f holds
( f,n is_a_correct_step_wrt X iff f ^ g,n is_a_correct_step_wrt X )

proof end;

theorem Th61: :: CQC_THE1:61

for n being Element of NAT
for X being Subset of CQC-WFF
for g, f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st 1 <= n & n <= len g & g,n is_a_correct_step_wrt X holds
f ^ g,n + (len f) is_a_correct_step_wrt X

proof end;

theorem Th62: :: CQC_THE1:62

for X being Subset of CQC-WFF
for f, g being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st f is_a_proof_wrt X & g is_a_proof_wrt X holds
f ^ g is_a_proof_wrt X

proof end;

theorem :: CQC_THE1:63

for X, Y being Subset of CQC-WFF
for f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st f is_a_proof_wrt X & X c= Y holds
f is_a_proof_wrt Y

proof end;

theorem Th64: :: CQC_THE1:64

for l being Element of NAT
for X being Subset of CQC-WFF
for f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st f is_a_proof_wrt X & 1 <= l & l <= len f holds
(f . l) `1 in Cn X

proof end;

definition

let f be FinSequence of [:CQC-WFF,Proof_Step_Kinds:];
assume A1: f <> {} ;
func Effect f -> Element of CQC-WFF equals :Def6: :: CQC_THE1:def 6
(f . (len f)) `1 ;
coherence

proof end;

end;

:: deftheorem Def6 defines Effect CQC_THE1:def 6 :

theorem :: CQC_THE1:65

canceled;

theorem Th66: :: CQC_THE1:66

for X being Subset of CQC-WFF
for f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st f is_a_proof_wrt X holds
Effect f in Cn X

proof end;

Lm2: for X being Subset of CQC-WFF holds { p where p is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = p ) } c= CQC-WFF

proof end;

theorem Th67: :: CQC_THE1:67

for X being Subset of CQC-WFF holds X c= { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = F ) }

proof end;

Lm3: for X being Subset of CQC-WFF holds VERUM in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = F ) }

proof end;

Lm4: for p being Element of CQC-WFF
for X being Subset of CQC-WFF holds (('not' p) => p) => p in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = F ) }

proof end;

Lm5: for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF holds p => (('not' p) => q) in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = F ) }

proof end;

Lm6: for p, q, r being Element of CQC-WFF
for X being Subset of CQC-WFF holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = F ) }

proof end;

Lm7: for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF holds (p '&' q) => (q '&' p) in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = F ) }

proof end;

Lm8: for p, q being Element of CQC-WFF
for X being Subset of CQC-WFF st p in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = F ) } & p => q in { G where G is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = G ) } holds
q in { H where H is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = H ) }

proof end;

Lm9: for p being Element of CQC-WFF
for x being bound_QC-variable
for X being Subset of CQC-WFF holds (All (x,p)) => p in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = F ) }

proof end;

Lm10: for p, q being Element of CQC-WFF
for x being bound_QC-variable
for X being Subset of CQC-WFF st p => q in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = F ) } & not x in still_not-bound_in p holds
p => (All (x,q)) in { G where G is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = G ) }

proof end;

Lm11: for s being QC-formula
for x, y being bound_QC-variable
for X being Subset of CQC-WFF st s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = F ) } holds
s . y in { G where G is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = G ) }

proof end;

theorem Th68: :: CQC_THE1:68

for Y, X being Subset of CQC-WFF st Y = { p where p is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = p ) } holds
Y is being_a_theory

proof end;

Lm12: for X being Subset of CQC-WFF holds { p where p is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = p ) } c= Cn X

proof end;

theorem Th69: :: CQC_THE1:69

for X being Subset of CQC-WFF holds { p where p is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = p ) } = Cn X

proof end;

theorem Th70: :: CQC_THE1:70

for X being Subset of CQC-WFF
for p being Element of CQC-WFF holds
( p in Cn X iff ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = p ) )

proof end;

theorem :: CQC_THE1:71

for X being Subset of CQC-WFF
for p being Element of CQC-WFF st p in Cn X holds
ex Y being Subset of CQC-WFF st
( Y c= X & Y is finite & p in Cn Y )

proof end;

definition

canceled;
func TAUT -> Subset of CQC-WFF equals :: CQC_THE1:def 8
Cn ({} CQC-WFF);
correctness ;

end;

:: deftheorem CQC_THE1:def 7 :

:: deftheorem defines TAUT CQC_THE1:def 8 :

theorem :: CQC_THE1:72

canceled;

theorem :: CQC_THE1:73

canceled;

theorem Th74: :: CQC_THE1:74

for T being Subset of CQC-WFF st T is being_a_theory holds
TAUT c= T

proof end;

theorem :: CQC_THE1:75

for X being Subset of CQC-WFF holds TAUT c= Cn X by Th36, Th74;

theorem Th76: :: CQC_THE1:76

TAUT is being_a_theory by Th36;

theorem Th77: :: CQC_THE1:77

VERUM in TAUT by Def1, Th76;

theorem :: CQC_THE1:78

for p being Element of CQC-WFF holds (('not' p) => p) => p in TAUT by Def1, Th76;

theorem :: CQC_THE1:79

for p, q being Element of CQC-WFF holds p => (('not' p) => q) in TAUT by Def1, Th76;

theorem :: CQC_THE1:80

for p, q, r being Element of CQC-WFF holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in TAUT by Def1, Th76;

theorem :: CQC_THE1:81

for p, q being Element of CQC-WFF holds (p '&' q) => (q '&' p) in TAUT by Def1, Th76;

theorem :: CQC_THE1:82

for p, q being Element of CQC-WFF st p in TAUT & p => q in TAUT holds
q in TAUT by Def1, Th76;

theorem :: CQC_THE1:83

for p being Element of CQC-WFF
for x being bound_QC-variable holds (All (x,p)) => p in TAUT by Th33;

theorem :: CQC_THE1:84

for p, q being Element of CQC-WFF
for x being bound_QC-variable st p => q in TAUT & not x in still_not-bound_in p holds
p => (All (x,q)) in TAUT by Th34;

theorem :: CQC_THE1:85

for s being QC-formula
for x, y being bound_QC-variable st s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in TAUT holds
s . y in TAUT by Th35;

definition

let X be Subset of CQC-WFF;
let s be QC-formula;
pred X |- s means :Def9: :: CQC_THE1:def 9
s in Cn X;

end;

:: deftheorem Def9 defines |- CQC_THE1:def 9 :

theorem :: CQC_THE1:86

canceled;

theorem :: CQC_THE1:87

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

proof end;

theorem :: CQC_THE1:88

for X being Subset of CQC-WFF
for p being Element of CQC-WFF holds X |- (('not' p) => p) => p

proof end;

theorem :: CQC_THE1:89

for X being Subset of CQC-WFF
for p, q being Element of CQC-WFF holds X |- p => (('not' p) => q)

proof end;

theorem :: CQC_THE1:90

for X being Subset of CQC-WFF
for p, q, r being Element of CQC-WFF holds X |- (p => q) => (('not' (q '&' r)) => ('not' (p '&' r)))

proof end;

theorem :: CQC_THE1:91

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

proof end;

theorem :: CQC_THE1:92

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

proof end;

theorem :: CQC_THE1:93

for X being Subset of CQC-WFF
for p being Element of CQC-WFF
for x being bound_QC-variable holds X |- (All (x,p)) => p

proof end;

theorem :: CQC_THE1:94

for X being Subset of CQC-WFF
for p, q being Element of CQC-WFF
for x being bound_QC-variable st X |- p => q & not x in still_not-bound_in p holds
X |- p => (All (x,q))

proof end;

theorem :: CQC_THE1:95

for X being Subset of CQC-WFF
for s being QC-formula
for y, x being bound_QC-variable st s . y in CQC-WFF & not x in still_not-bound_in s & X |- s . x holds
X |- s . y

proof end;

definition

let s be QC-formula;
attr s is valid means :Def10: :: CQC_THE1:def 10
{} CQC-WFF |- s;

end;

:: deftheorem Def10 defines valid CQC_THE1:def 10 :

Lm13: for s being QC-formula holds
( s is valid iff s in TAUT )

proof end;

definition

let s be QC-formula;
redefine attr s is valid means :: CQC_THE1:def 11
s in TAUT ;
compatibility by Lm13;

end;

:: deftheorem defines valid CQC_THE1:def 11 :

theorem :: CQC_THE1:96

canceled;

theorem :: CQC_THE1:97

canceled;

theorem :: CQC_THE1:98

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

proof end;

theorem :: CQC_THE1:99

VERUM is valid by Lm13, Th77;

theorem :: CQC_THE1:100

for p being Element of CQC-WFF holds (('not' p) => p) => p is valid

proof end;

theorem :: CQC_THE1:101

for p, q being Element of CQC-WFF holds p => (('not' p) => q) is valid

proof end;

theorem :: CQC_THE1:102

for p, q, r being Element of CQC-WFF holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) is valid

proof end;

theorem :: CQC_THE1:103

for p, q being Element of CQC-WFF holds (p '&' q) => (q '&' p) is valid

proof end;

theorem :: CQC_THE1:104

for p, q being Element of CQC-WFF st p is valid & p => q is valid holds
q is valid

proof end;

theorem :: CQC_THE1:105

for p being Element of CQC-WFF
for x being bound_QC-variable holds (All (x,p)) => p is valid

proof end;

theorem :: CQC_THE1:106

for p, q being Element of CQC-WFF
for x being bound_QC-variable st p => q is valid & not x in still_not-bound_in p holds
p => (All (x,q)) is valid

proof end;

theorem :: CQC_THE1:107

for s being QC-formula
for y, x being bound_QC-variable st s . y in CQC-WFF & not x in still_not-bound_in s & s . x is valid holds
s . y is valid

proof end;