:: 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 Association of Mizar Users
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
theorem Th12: :: CQC_THE1:12
deffunc H1( set ) -> set = $1 `1 ;
theorem :: CQC_THE1:13
theorem :: CQC_THE1:14
:: 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
:: deftheorem Def2 defines Cn CQC_THE1:def 2 :
theorem :: CQC_THE1:26
canceled;
theorem Th27: :: CQC_THE1:27
theorem Th28: :: CQC_THE1:28
theorem Th29: :: CQC_THE1:29
theorem Th30: :: CQC_THE1:30
theorem Th31: :: CQC_THE1:31
theorem Th32: :: CQC_THE1:32
theorem Th33: :: CQC_THE1:33
theorem Th34: :: CQC_THE1:34
theorem Th35: :: CQC_THE1:35
theorem Th36: :: CQC_THE1:36
theorem Th37: :: CQC_THE1:37
theorem Th38: :: CQC_THE1:38
theorem Th39: :: CQC_THE1:39
Lm1:
for X being Subset of CQC-WFF holds Cn (Cn X) c= Cn X
theorem :: CQC_THE1:40
theorem Th41: :: CQC_THE1:41
:: deftheorem defines Proof_Step_Kinds CQC_THE1:def 3 :
theorem :: CQC_THE1:42
canceled;
theorem Th43: :: CQC_THE1:43
theorem :: CQC_THE1:44
theorem Th45: :: CQC_THE1:45
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
( ( (PR . n) `2 = 0 & (PR . n) `2 = 1 implies ( (PR . n) `1 in X iff (PR . n) `1 = VERUM ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 2 implies ( (PR . n) `1 in X iff ex p being Element of CQC-WFF st (PR . n) `1 = (('not' p) => 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 st (PR . n) `1 = p => (('not' 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 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 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 ex x being bound_QC-variable 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 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 ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 8 implies ( (PR . n) `1 in X iff 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) ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 9 implies ( (PR . n) `1 in X iff 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 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 2 implies ( (PR . n) `1 = VERUM iff ex p being Element of CQC-WFF st (PR . n) `1 = (('not' p) => p) => p ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 3 implies ( (PR . n) `1 = VERUM iff ex p, q being Element of CQC-WFF st (PR . n) `1 = p => (('not' p) => q) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 4 implies ( (PR . n) `1 = VERUM iff ex p, q, r being Element of CQC-WFF 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 iff ex p, q being Element of CQC-WFF st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 6 implies ( (PR . n) `1 = VERUM iff ex p being Element of CQC-WFF ex x being bound_QC-variable st (PR . n) `1 = (All x,p) => p ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 7 implies ( (PR . n) `1 = VERUM iff 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 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 8 implies ( (PR . n) `1 = VERUM iff 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) ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 9 implies ( (PR . n) `1 = VERUM iff 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 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 3 implies ( ex p being Element of CQC-WFF st (PR . n) `1 = (('not' p) => p) => p iff ex p, q being Element of CQC-WFF st (PR . n) `1 = p => (('not' p) => q) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 4 implies ( ex p being Element of CQC-WFF st (PR . n) `1 = (('not' p) => p) => p iff ex p, q, r being Element of CQC-WFF 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 st (PR . n) `1 = (('not' p) => p) => p iff ex p, q being Element of CQC-WFF st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 6 implies ( ex p being Element of CQC-WFF st (PR . n) `1 = (('not' p) => p) => p iff ex p being Element of CQC-WFF ex x being bound_QC-variable st (PR . n) `1 = (All x,p) => p ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 7 implies ( ex p being Element of CQC-WFF st (PR . n) `1 = (('not' p) => p) => p iff 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 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 8 implies ( ex p being Element of CQC-WFF st (PR . n) `1 = (('not' p) => p) => p iff 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) ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 9 implies ( ex p being Element of CQC-WFF st (PR . n) `1 = (('not' p) => p) => p iff 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 ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 4 implies ( ex p, q being Element of CQC-WFF st (PR . n) `1 = p => (('not' p) => q) iff ex p, q, r being Element of CQC-WFF 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 st (PR . n) `1 = p => (('not' p) => q) iff ex p, q being Element of CQC-WFF 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 st (PR . n) `1 = p => (('not' p) => q) iff ex p being Element of CQC-WFF ex x being bound_QC-variable 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 st (PR . n) `1 = p => (('not' p) => q) iff 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 ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 8 implies ( ex p, q being Element of CQC-WFF st (PR . n) `1 = p => (('not' p) => q) iff 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) ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 9 implies ( ex p, q being Element of CQC-WFF st (PR . n) `1 = p => (('not' p) => q) iff 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 ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 5 implies ( ex p, q, r being Element of CQC-WFF st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex p, q being Element of CQC-WFF 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 st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex p being Element of CQC-WFF ex x being bound_QC-variable 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 st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff 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 ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 8 implies ( ex p, q, r being Element of CQC-WFF st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff 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) ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 9 implies ( ex p, q, r being Element of CQC-WFF st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff 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 ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 6 implies ( ex p, q being Element of CQC-WFF st (PR . n) `1 = (p '&' q) => (q '&' p) iff ex p being Element of CQC-WFF ex x being bound_QC-variable 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 st (PR . n) `1 = (p '&' q) => (q '&' p) iff 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 ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 8 implies ( ex p, q being Element of CQC-WFF st (PR . n) `1 = (p '&' q) => (q '&' p) iff 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) ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 9 implies ( ex p, q being Element of CQC-WFF st (PR . n) `1 = (p '&' q) => (q '&' p) iff 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 ) ) ) & ( (PR . n) `2 = 6 & (PR . n) `2 = 7 implies ( ex p being Element of CQC-WFF ex x being bound_QC-variable st (PR . n) `1 = (All x,p) => p iff 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 ) ) ) & ( (PR . n) `2 = 6 & (PR . n) `2 = 8 implies ( ex p being Element of CQC-WFF ex x being bound_QC-variable st (PR . n) `1 = (All x,p) => p iff 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) ) ) ) & ( (PR . n) `2 = 6 & (PR . n) `2 = 9 implies ( ex p being Element of CQC-WFF ex x being bound_QC-variable st (PR . n) `1 = (All x,p) => p iff 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 ) ) ) & ( (PR . n) `2 = 7 & (PR . n) `2 = 8 implies ( 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 ) iff 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) ) ) ) & ( (PR . n) `2 = 7 & (PR . n) `2 = 9 implies ( 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 ) iff 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 ) ) ) & ( (PR . n) `2 = 8 & (PR . n) `2 = 9 implies ( 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) ) iff 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 ) ) ) )
;
end;
:: deftheorem Def4 defines is_a_correct_step_wrt CQC_THE1:def 4 :
for
PR being
FinSequence of
[:CQC-WFF ,Proof_Step_Kinds :] for
n being
Nat for
X being
Subset of
CQC-WFF 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 ) ) & (
(PR . n) `2 = 2 implies (
PR,
n is_a_correct_step_wrt X iff ex
p being
Element of
CQC-WFF st
(PR . n) `1 = (('not' p) => p) => p ) ) & (
(PR . n) `2 = 3 implies (
PR,
n is_a_correct_step_wrt X iff ex
p,
q being
Element of
CQC-WFF st
(PR . n) `1 = p => (('not' 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 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 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 ex
x being
bound_QC-variable 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
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 ) ) ) & (
(PR . n) `2 = 8 implies (
PR,
n is_a_correct_step_wrt X iff 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) ) ) ) & (
(PR . n) `2 = 9 implies (
PR,
n is_a_correct_step_wrt X iff 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 ) ) ) );
:: 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
theorem Th58: :: CQC_THE1:58
theorem :: CQC_THE1:59
theorem Th60: :: CQC_THE1:60
theorem Th61: :: CQC_THE1:61
theorem Th62: :: CQC_THE1:62
theorem :: CQC_THE1:63
theorem Th64: :: CQC_THE1:64
:: deftheorem Def6 defines Effect CQC_THE1:def 6 :
theorem :: CQC_THE1:65
canceled;
theorem Th66: :: CQC_THE1:66
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
theorem Th67: :: CQC_THE1:67
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 ) }
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 ) }
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 ) }
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 ) }
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 ) }
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 ) }
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 ) }
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 ) }
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 ) }
theorem Th68: :: CQC_THE1:68
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
theorem Th69: :: CQC_THE1:69
theorem Th70: :: CQC_THE1:70
theorem :: CQC_THE1:71
:: deftheorem CQC_THE1:def 7 :
canceled;
:: deftheorem defines TAUT CQC_THE1:def 8 :
theorem :: CQC_THE1:72
canceled;
theorem :: CQC_THE1:73
canceled;
theorem Th74: :: CQC_THE1:74
theorem Th75: :: CQC_THE1:75
theorem Th76: :: CQC_THE1:76
theorem Th77: :: CQC_THE1:77
theorem :: CQC_THE1:78
theorem :: CQC_THE1:79
theorem :: CQC_THE1:80
theorem :: CQC_THE1:81
theorem :: CQC_THE1:82
theorem :: CQC_THE1:83
theorem :: CQC_THE1:84
theorem :: CQC_THE1:85
:: deftheorem Def9 defines |- CQC_THE1:def 9 :
theorem :: CQC_THE1:86
canceled;
theorem :: CQC_THE1:87
theorem :: CQC_THE1:88
theorem :: CQC_THE1:89
theorem :: CQC_THE1:90
theorem :: CQC_THE1:91
theorem :: CQC_THE1:92
theorem :: CQC_THE1:93
theorem :: CQC_THE1:94
theorem :: CQC_THE1:95
:: deftheorem Def10 defines valid CQC_THE1:def 10 :
Lm13:
for s being QC-formula holds
( s is valid iff s in TAUT )
:: deftheorem defines valid CQC_THE1:def 11 :
theorem :: CQC_THE1:96
canceled;
theorem :: CQC_THE1:97
canceled;
theorem :: CQC_THE1:98
theorem :: CQC_THE1:99
theorem :: CQC_THE1:100
theorem :: CQC_THE1:101
theorem :: CQC_THE1:102
theorem :: CQC_THE1:103
theorem :: CQC_THE1:104
theorem :: CQC_THE1:105
theorem :: CQC_THE1:106
theorem :: CQC_THE1:107