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-2021 Association of Mizar Users

definition

let Al be QC-alphabet ;
let T be Subset of (CQC-WFF Al);

attr T is being_a_theory means :: CQC_THE1:def 1
( VERUM Al in T & ( for p, q, r being Element of CQC-WFF Al
for s being QC-formula of Al
for x, y being bound_QC-variable of Al 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 Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T implies s . y in T ) ) ) );

end;

:: deftheorem defines being_a_theory CQC_THE1:def 1 :

theorem :: CQC_THE1:1

canceled;

theorem :: CQC_THE1:2

canceled;

theorem :: CQC_THE1:3

canceled;

theorem :: CQC_THE1:4

canceled;

::$CT 4

theorem :: CQC_THE1:5

for Al being QC-alphabet
for T, S being Subset of (CQC-WFF Al) st T is being_a_theory & S is being_a_theory holds
T /\ S is being_a_theory

proof end;

:: --------- The consequence operation

definition

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

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

proof end;

proof end;

end;

:: deftheorem Def2 defines Cn CQC_THE1:def 2 :

theorem Th2: :: CQC_THE1:6

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al) holds VERUM Al in Cn X

proof end;

theorem Th3: :: CQC_THE1:7

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

proof end;

theorem Th4: :: CQC_THE1:8

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

proof end;

theorem Th5: :: CQC_THE1:9

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

proof end;

theorem Th6: :: CQC_THE1:10

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

proof end;

theorem Th7: :: CQC_THE1:11

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

proof end;

theorem Th8: :: CQC_THE1:12

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

proof end;

theorem Th9: :: CQC_THE1:13

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al 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 Th10: :: CQC_THE1:14

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

proof end;

theorem Th11: :: CQC_THE1:15

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al) holds Cn X is being_a_theory by Th2, Th3, Th4, Th5, Th6, Th7, Th8, Th9, Th10;

theorem Th12: :: CQC_THE1:16

for Al being QC-alphabet
for T, X being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds
Cn X c= T by Def2;

theorem Th13: :: CQC_THE1:17

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al) holds X c= Cn X

proof end;

theorem Th14: :: CQC_THE1:18

for Al being QC-alphabet
for X, Y being Subset of (CQC-WFF Al) st X c= Y holds
Cn X c= Cn Y

proof end;

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

proof end;

theorem :: CQC_THE1:19

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al) holds Cn (Cn X) = Cn X by Lm1, Th13;

theorem Th16: :: CQC_THE1:20

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

proof end;

:: ---------- The notion of proof

definition

func Proof_Step_Kinds -> set equals :: CQC_THE1:def 3
{ k where k is Nat : k <= 9 } ;

end;

:: deftheorem defines Proof_Step_Kinds CQC_THE1:def 3 :

theorem Th17: :: CQC_THE1:21

0 in Proof_Step_Kinds & ... & 9 in Proof_Step_Kinds ;

registration

cluster Proof_Step_Kinds -> non empty ;

coherence by Th17;

end;

theorem :: CQC_THE1:22

Proof_Step_Kinds is finite

proof end;

theorem Th19: :: CQC_THE1:23

for Al being QC-alphabet
for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]
for n being Nat st 1 <= n & n <= len f holds
not not (f . n) `2 = 0 & ... & not (f . n) `2 = 9

proof end;

definition

let Al be QC-alphabet ;
let PR be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:];
let n be Nat;
let X be Subset of (CQC-WFF Al);

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 Al if (PR . n) `2 = 1
ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p if (PR . n) `2 = 2
ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) if (PR . n) `2 = 3
ex p, q, r being Element of CQC-WFF Al 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 Al st (PR . n) `1 = (p '&' q) => (q '&' p) if (PR . n) `2 = 5
ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p if (PR . n) `2 = 6
ex i, j being Nat ex p, q being Element of CQC-WFF Al 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 Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al 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 Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st
( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) if (PR . n) `2 = 9
;

end;

:: deftheorem Def4 defines is_a_correct_step_wrt CQC_THE1:def 4 :

definition

let Al be QC-alphabet ;
let X be Subset of (CQC-WFF Al);
let f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:];

pred f is_a_proof_wrt X means :: CQC_THE1:def 5
( f <> {} & ( for n being Nat st 1 <= n & n <= len f holds
f,n is_a_correct_step_wrt X ) );

end;

:: deftheorem defines is_a_proof_wrt CQC_THE1:def 5 :

theorem :: CQC_THE1:24

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X holds
rng f <> {} by RELAT_1:41;

theorem Th21: :: CQC_THE1:25

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

proof end;

theorem :: CQC_THE1:26

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X holds
not not (f . 1) `2 = 0 & ... & not (f . 1) `2 = 6

proof end;

theorem Th23: :: CQC_THE1:27

for Al being QC-alphabet
for n being Nat
for X being Subset of (CQC-WFF Al)
for f, g being FinSequence of [:(CQC-WFF Al),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 Th24: :: CQC_THE1:28

for Al being QC-alphabet
for n being Nat
for X being Subset of (CQC-WFF Al)
for f, g being FinSequence of [:(CQC-WFF Al),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 Th25: :: CQC_THE1:29

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for f, g being FinSequence of [:(CQC-WFF Al),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:30

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

proof end;

theorem Th27: :: CQC_THE1:31

for Al being QC-alphabet
for l being Nat
for X being Subset of (CQC-WFF Al)
for f being FinSequence of [:(CQC-WFF Al),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 Al be QC-alphabet ;
let f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:];
assume A1: f <> {} ;

func Effect f -> Element of CQC-WFF Al equals :Def6: :: CQC_THE1:def 6
(f . (len f)) `1 ;

proof end;

end;

:: deftheorem Def6 defines Effect CQC_THE1:def 6 :

theorem Th28: :: CQC_THE1:32

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

proof end;

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

proof end;

theorem Th29: :: CQC_THE1:33

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

Lm10: for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for X being Subset of (CQC-WFF Al) st p => q in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),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 Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = G ) }

proof end;

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

proof end;

theorem Th30: :: CQC_THE1:34

for Al being QC-alphabet
for Y, X being Subset of (CQC-WFF Al) st Y = { p where p is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = p ) } holds
Y is being_a_theory by Lm3, Lm4, Lm5, Lm6, Lm7, Lm8, Lm9, Lm10, Lm11;

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

proof end;

theorem Th31: :: CQC_THE1:35

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

proof end;

theorem Th32: :: CQC_THE1:36

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

proof end;

theorem :: CQC_THE1:37

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

proof end;

:: --------- TAUT(Al) - the set of all tautologies

definition

let Al be QC-alphabet ;

func TAUT Al -> Subset of (CQC-WFF Al) equals :: CQC_THE1:def 7
Cn ({} (CQC-WFF Al));

end;

:: deftheorem defines TAUT CQC_THE1:def 7 :

theorem Th34: :: CQC_THE1:38

for Al being QC-alphabet
for T being Subset of (CQC-WFF Al) st T is being_a_theory holds
TAUT Al c= T

proof end;

theorem :: CQC_THE1:39

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al) holds TAUT Al c= Cn X by Th11, Th34;

theorem :: CQC_THE1:40

for Al being QC-alphabet holds TAUT Al is being_a_theory by Th11;

theorem Th37: :: CQC_THE1:41

for Al being QC-alphabet holds VERUM Al in TAUT Al

proof end;

theorem :: CQC_THE1:42

for Al being QC-alphabet
for p being Element of CQC-WFF Al holds (('not' p) => p) => p in TAUT Al

proof end;

theorem :: CQC_THE1:43

for Al being QC-alphabet
for p, q being Element of CQC-WFF Al holds p => (('not' p) => q) in TAUT Al

proof end;

theorem :: CQC_THE1:44

for Al being QC-alphabet
for p, q, r being Element of CQC-WFF Al holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in TAUT Al

proof end;

theorem :: CQC_THE1:45

for Al being QC-alphabet
for p, q being Element of CQC-WFF Al holds (p '&' q) => (q '&' p) in TAUT Al

proof end;

theorem :: CQC_THE1:46

for Al being QC-alphabet
for p, q being Element of CQC-WFF Al st p in TAUT Al & p => q in TAUT Al holds
q in TAUT Al

proof end;

theorem :: CQC_THE1:47

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

theorem :: CQC_THE1:48

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

theorem :: CQC_THE1:49

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

:: --------- Relation of consequence of a set of formulas

definition

let Al be QC-alphabet ;
let X be Subset of (CQC-WFF Al);
let s be QC-formula of Al;

pred X |- s means :Def8: :: CQC_THE1:def 8
s in Cn X;

end;

:: deftheorem Def8 defines |- CQC_THE1:def 8 :

theorem :: CQC_THE1:50

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al) holds X |- VERUM Al by Th2;

theorem :: CQC_THE1:51

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al holds X |- (('not' p) => p) => p by Th3;

theorem :: CQC_THE1:52

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p, q being Element of CQC-WFF Al holds X |- p => (('not' p) => q) by Th4;

theorem :: CQC_THE1:53

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p, q, r being Element of CQC-WFF Al holds X |- (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by Th5;

theorem :: CQC_THE1:54

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p, q being Element of CQC-WFF Al holds X |- (p '&' q) => (q '&' p) by Th6;

theorem :: CQC_THE1:55

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p, q being Element of CQC-WFF Al st X |- p & X |- p => q holds
X |- q by Th7;

theorem :: CQC_THE1:56

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds X |- (All (x,p)) => p by Th8;

theorem :: CQC_THE1:57

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

theorem :: CQC_THE1:58

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for s being QC-formula of Al
for x, y being bound_QC-variable of Al st s . y in CQC-WFF Al & not x in still_not-bound_in s & X |- s . x holds
X |- s . y by Th10;

definition

let Al be QC-alphabet ;
let s be QC-formula of Al;

attr s is valid means :: CQC_THE1:def 9
{} (CQC-WFF Al) |- s;

end;

:: deftheorem defines valid CQC_THE1:def 9 :

definition

let Al be QC-alphabet ;
let s be QC-formula of Al;

redefine attr s is valid means :: CQC_THE1:def 10
s in TAUT Al;

compatibility by Def8;

end;

:: deftheorem defines valid CQC_THE1:def 10 :

theorem :: CQC_THE1:59

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al st p is valid holds
X |- p

proof end;

theorem :: CQC_THE1:60

for Al being QC-alphabet holds VERUM Al is valid by Th37;

theorem :: CQC_THE1:61

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

proof end;

theorem :: CQC_THE1:62

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

proof end;

theorem :: CQC_THE1:63

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

proof end;

theorem :: CQC_THE1:64

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

proof end;

theorem :: CQC_THE1:65

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

proof end;

theorem :: CQC_THE1:66

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds (All (x,p)) => p is valid by Th8;

theorem :: CQC_THE1:67

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

theorem :: CQC_THE1:68

for Al being QC-alphabet
for s being QC-formula of Al
for x, y being bound_QC-variable of Al st s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x is valid holds
s . y is valid by Th10;