:: A First-Order Predicate Calculus. Axiomatics, the Consequence Operation and a Concept of Proof
:: by Agata Darmochwa{\l}
::
:: 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
( (() => p) => p in T & 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 :
for Al being QC-alphabet
for T being Subset of (CQC-WFF Al) holds
( T is being_a_theory iff ( 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
( (() => p) => p in T & 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 ) ) ) ) );

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 );
existence
ex b1 being Subset of (CQC-WFF Al) st
for t being Element of CQC-WFF Al holds
( t in b1 iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds
t in T )
proof end;
uniqueness
for b1, b2 being Subset of (CQC-WFF Al) st ( for t being Element of CQC-WFF Al holds
( t in b1 iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds
t in T ) ) & ( for t being Element of CQC-WFF Al holds
( t in b2 iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds
t in T ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Cn CQC_THE1:def 2 :
for Al being QC-alphabet
for X, b3 being Subset of (CQC-WFF Al) holds
( b3 = Cn X iff for t being Element of CQC-WFF Al holds
( t in b3 iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds
t in T ) );

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 (() => 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 => (() => 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 ;

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 } ;
coherence
{ k where k is Nat : k <= 9 } is set
;
end;

:: deftheorem defines Proof_Step_Kinds CQC_THE1:def 3 :
Proof_Step_Kinds = { k where k is Nat : k <= 9 } ;

theorem Th17: :: CQC_THE1:21
0 in Proof_Step_Kinds & ... & 9 in Proof_Step_Kinds ;

registration
coherence by Th17;
end;

theorem :: CQC_THE1:22
proof end;

theorem Th19: :: CQC_THE1:23
for Al being QC-alphabet
for f being FinSequence of
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 ;
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 = (() => p) => p if (PR . n) 2 = 2
ex p, q being Element of CQC-WFF Al st (PR . n) 1 = 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
;
consistency
( ( (PR . n) 2 = 0 & (PR . n) 2 = 1 implies ( (PR . n) 1 in X iff (PR . n) 1 = VERUM Al ) ) & ( (PR . n) 2 = 0 & (PR . n) 2 = 2 implies ( (PR . n) 1 in X iff ex p being Element of CQC-WFF Al st (PR . n) 1 = (() => p) => p ) ) & ( (PR . n) 2 = 0 & (PR . n) 2 = 3 implies ( (PR . n) 1 in X iff ex p, q being Element of CQC-WFF Al st (PR . n) 1 = p => (() => q) ) ) & ( (PR . n) 2 = 0 & (PR . n) 2 = 4 implies ( (PR . n) 1 in X iff ex p, q, r being Element of CQC-WFF Al st (PR . n) 1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & ( (PR . n) 2 = 0 & (PR . n) 2 = 5 implies ( (PR . n) 1 in X iff ex p, q being Element of CQC-WFF Al st (PR . n) 1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) 2 = 0 & (PR . n) 2 = 6 implies ( (PR . n) 1 in X iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) 1 = (All (x,p)) => p ) ) & ( (PR . n) 2 = 0 & (PR . n) 2 = 7 implies ( (PR . n) 1 in X iff 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 ) ) ) & ( (PR . n) 2 = 0 & (PR . n) 2 = 8 implies ( (PR . n) 1 in X iff 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)) ) ) ) & ( (PR . n) 2 = 0 & (PR . n) 2 = 9 implies ( (PR . n) 1 in X iff 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 ) ) ) & ( (PR . n) 2 = 1 & (PR . n) 2 = 2 implies ( (PR . n) 1 = VERUM Al iff ex p being Element of CQC-WFF Al st (PR . n) 1 = (() => p) => p ) ) & ( (PR . n) 2 = 1 & (PR . n) 2 = 3 implies ( (PR . n) 1 = VERUM Al iff ex p, q being Element of CQC-WFF Al st (PR . n) 1 = p => (() => q) ) ) & ( (PR . n) 2 = 1 & (PR . n) 2 = 4 implies ( (PR . n) 1 = VERUM Al iff ex p, q, r being Element of CQC-WFF Al st (PR . n) 1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & ( (PR . n) 2 = 1 & (PR . n) 2 = 5 implies ( (PR . n) 1 = VERUM Al iff ex p, q being Element of CQC-WFF Al st (PR . n) 1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) 2 = 1 & (PR . n) 2 = 6 implies ( (PR . n) 1 = VERUM Al iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) 1 = (All (x,p)) => p ) ) & ( (PR . n) 2 = 1 & (PR . n) 2 = 7 implies ( (PR . n) 1 = VERUM Al iff 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 ) ) ) & ( (PR . n) 2 = 1 & (PR . n) 2 = 8 implies ( (PR . n) 1 = VERUM Al iff 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)) ) ) ) & ( (PR . n) 2 = 1 & (PR . n) 2 = 9 implies ( (PR . n) 1 = VERUM Al iff 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 ) ) ) & ( (PR . n) 2 = 2 & (PR . n) 2 = 3 implies ( ex p being Element of CQC-WFF Al st (PR . n) 1 = (() => p) => p iff ex p, q being Element of CQC-WFF Al st (PR . n) 1 = p => (() => q) ) ) & ( (PR . n) 2 = 2 & (PR . n) 2 = 4 implies ( ex p being Element of CQC-WFF Al st (PR . n) 1 = (() => p) => p iff ex p, q, r being Element of CQC-WFF Al st (PR . n) 1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & ( (PR . n) 2 = 2 & (PR . n) 2 = 5 implies ( ex p being Element of CQC-WFF Al st (PR . n) 1 = (() => p) => p iff ex p, q being Element of CQC-WFF Al st (PR . n) 1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) 2 = 2 & (PR . n) 2 = 6 implies ( ex p being Element of CQC-WFF Al st (PR . n) 1 = (() => p) => p iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) 1 = (All (x,p)) => p ) ) & ( (PR . n) 2 = 2 & (PR . n) 2 = 7 implies ( ex p being Element of CQC-WFF Al st (PR . n) 1 = (() => p) => p iff 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 ) ) ) & ( (PR . n) 2 = 2 & (PR . n) 2 = 8 implies ( ex p being Element of CQC-WFF Al st (PR . n) 1 = (() => p) => p iff 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)) ) ) ) & ( (PR . n) 2 = 2 & (PR . n) 2 = 9 implies ( ex p being Element of CQC-WFF Al st (PR . n) 1 = (() => p) => p iff 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 ) ) ) & ( (PR . n) 2 = 3 & (PR . n) 2 = 4 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) 1 = p => (() => q) iff ex p, q, r being Element of CQC-WFF Al st (PR . n) 1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & ( (PR . n) 2 = 3 & (PR . n) 2 = 5 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) 1 = p => (() => q) iff ex p, q being Element of CQC-WFF Al st (PR . n) 1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) 2 = 3 & (PR . n) 2 = 6 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) 1 = p => (() => q) iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) 1 = (All (x,p)) => p ) ) & ( (PR . n) 2 = 3 & (PR . n) 2 = 7 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) 1 = p => (() => q) iff 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 ) ) ) & ( (PR . n) 2 = 3 & (PR . n) 2 = 8 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) 1 = p => (() => q) iff 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)) ) ) ) & ( (PR . n) 2 = 3 & (PR . n) 2 = 9 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) 1 = p => (() => q) iff 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 ) ) ) & ( (PR . n) 2 = 4 & (PR . n) 2 = 5 implies ( ex p, q, r being Element of CQC-WFF Al st (PR . n) 1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex p, q being Element of CQC-WFF Al st (PR . n) 1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) 2 = 4 & (PR . n) 2 = 6 implies ( ex p, q, r being Element of CQC-WFF Al st (PR . n) 1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) 1 = (All (x,p)) => p ) ) & ( (PR . n) 2 = 4 & (PR . n) 2 = 7 implies ( ex p, q, r being Element of CQC-WFF Al st (PR . n) 1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff 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 ) ) ) & ( (PR . n) 2 = 4 & (PR . n) 2 = 8 implies ( ex p, q, r being Element of CQC-WFF Al st (PR . n) 1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff 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)) ) ) ) & ( (PR . n) 2 = 4 & (PR . n) 2 = 9 implies ( ex p, q, r being Element of CQC-WFF Al st (PR . n) 1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff 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 ) ) ) & ( (PR . n) 2 = 5 & (PR . n) 2 = 6 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) 1 = (p '&' q) => (q '&' p) iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) 1 = (All (x,p)) => p ) ) & ( (PR . n) 2 = 5 & (PR . n) 2 = 7 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) 1 = (p '&' q) => (q '&' p) iff 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 ) ) ) & ( (PR . n) 2 = 5 & (PR . n) 2 = 8 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) 1 = (p '&' q) => (q '&' p) iff 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)) ) ) ) & ( (PR . n) 2 = 5 & (PR . n) 2 = 9 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) 1 = (p '&' q) => (q '&' p) iff 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 ) ) ) & ( (PR . n) 2 = 6 & (PR . n) 2 = 7 implies ( ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) 1 = (All (x,p)) => p iff 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 ) ) ) & ( (PR . n) 2 = 6 & (PR . n) 2 = 8 implies ( ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) 1 = (All (x,p)) => p iff 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)) ) ) ) & ( (PR . n) 2 = 6 & (PR . n) 2 = 9 implies ( ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) 1 = (All (x,p)) => p iff 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 ) ) ) & ( (PR . n) 2 = 7 & (PR . n) 2 = 8 implies ( 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 ) iff 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)) ) ) ) & ( (PR . n) 2 = 7 & (PR . n) 2 = 9 implies ( 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 ) iff 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 ) ) ) & ( (PR . n) 2 = 8 & (PR . n) 2 = 9 implies ( 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)) ) iff 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 ) ) ) )
;
end;

:: deftheorem Def4 defines is_a_correct_step_wrt CQC_THE1:def 4 :
for Al being QC-alphabet
for PR being FinSequence of
for n being Nat
for X being Subset of (CQC-WFF Al) holds
( ( (PR . n) 2 = 0 implies ( PR,n is_a_correct_step_wrt X iff (PR . n) 1 in X ) ) & ( (PR . n) 2 = 1 implies ( PR,n is_a_correct_step_wrt X iff (PR . n) 1 = VERUM Al ) ) & ( (PR . n) 2 = 2 implies ( PR,n is_a_correct_step_wrt X iff ex p being Element of CQC-WFF Al st (PR . n) 1 = (() => p) => p ) ) & ( (PR . n) 2 = 3 implies ( PR,n is_a_correct_step_wrt X iff ex p, q being Element of CQC-WFF Al st (PR . n) 1 = p => (() => q) ) ) & ( (PR . n) 2 = 4 implies ( PR,n is_a_correct_step_wrt X iff ex p, q, r being Element of CQC-WFF Al st (PR . n) 1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & ( (PR . n) 2 = 5 implies ( PR,n is_a_correct_step_wrt X iff ex p, q being Element of CQC-WFF Al st (PR . n) 1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) 2 = 6 implies ( PR,n is_a_correct_step_wrt X iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) 1 = (All (x,p)) => p ) ) & ( (PR . n) 2 = 7 implies ( PR,n is_a_correct_step_wrt X iff 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 ) ) ) & ( (PR . n) 2 = 8 implies ( PR,n is_a_correct_step_wrt X iff 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)) ) ) ) & ( (PR . n) 2 = 9 implies ( PR,n is_a_correct_step_wrt X iff 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 ) ) ) );

definition
let Al be QC-alphabet ;
let X be Subset of (CQC-WFF Al);
let f be FinSequence of ;
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 :
for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for f being FinSequence of holds
( f is_a_proof_wrt X iff ( f <> {} & ( for n being Nat st 1 <= n & n <= len f holds
f,n is_a_correct_step_wrt X ) ) );

theorem :: CQC_THE1:24
for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for f being FinSequence of 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 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 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 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 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 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 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 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 ;
assume A1: f <> {} ;
func Effect f -> Element of CQC-WFF Al equals :Def6: :: CQC_THE1:def 6
(f . (len f)) 1 ;
coherence
(f . (len f)) 1 is Element of CQC-WFF Al
proof end;
end;

:: deftheorem Def6 defines Effect CQC_THE1:def 6 :
for Al being QC-alphabet
for f being FinSequence of st f <> {} holds
Effect f = (f . (len f)) 1 ;

theorem Th28: :: CQC_THE1:32
for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for f being FinSequence of 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 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 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 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 (() => p) => p in { F where F is Element of CQC-WFF Al : ex f being FinSequence of 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 => (() => q) in { F where F is Element of CQC-WFF Al : ex f being FinSequence of 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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));
correctness
coherence
Cn ({} (CQC-WFF Al)) is Subset of (CQC-WFF Al)
;
;
end;

:: deftheorem defines TAUT CQC_THE1:def 7 :
for Al being QC-alphabet holds TAUT Al = Cn ({} (CQC-WFF Al));

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 ;

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 (() => 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 => (() => 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 :
for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for s being QC-formula of Al holds
( X |- s iff s in Cn X );

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 |- (() => 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 => (() => 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 :
for Al being QC-alphabet
for s being QC-formula of Al holds
( s is valid iff {} (CQC-WFF Al) |- s );

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
( s is valid iff s in TAUT Al )
by Def8;
end;

:: deftheorem defines valid CQC_THE1:def 10 :
for Al being QC-alphabet
for s being QC-formula of Al holds
( s is valid iff s in TAUT Al );

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 (() => 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 => (() => 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;