begin
theorem
canceled;
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
:: deftheorem defines FALSUM QC_LANG2:def 1 :
FALSUM = 'not' VERUM;
:: deftheorem defines => QC_LANG2:def 2 :
for p, q being Element of QC-WFF holds p => q = 'not' (p '&' ('not' q));
:: deftheorem defines 'or' QC_LANG2:def 3 :
for p, q being Element of QC-WFF holds p 'or' q = 'not' (('not' p) '&' ('not' q));
:: deftheorem defines <=> QC_LANG2:def 4 :
for p, q being Element of QC-WFF holds p <=> q = (p => q) '&' (q => p);
:: deftheorem defines Ex QC_LANG2:def 5 :
for x being bound_QC-variable
for p being Element of QC-WFF holds Ex (x,p) = 'not' (All (x,('not' p)));
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
canceled;
theorem
theorem Th17:
theorem
theorem Th19:
definition
let x,
y be
bound_QC-variable;
let p be
Element of
QC-WFF ;
func All (
x,
y,
p)
-> QC-formula equals
All (
x,
(All (y,p)));
correctness
coherence
All (x,(All (y,p))) is QC-formula;
;
func Ex (
x,
y,
p)
-> QC-formula equals
Ex (
x,
(Ex (y,p)));
correctness
coherence
Ex (x,(Ex (y,p))) is QC-formula;
;
end;
:: deftheorem defines All QC_LANG2:def 6 :
for x, y being bound_QC-variable
for p being Element of QC-WFF holds All (x,y,p) = All (x,(All (y,p)));
:: deftheorem defines Ex QC_LANG2:def 7 :
for x, y being bound_QC-variable
for p being Element of QC-WFF holds Ex (x,y,p) = Ex (x,(Ex (y,p)));
theorem
theorem Th21:
theorem
theorem Th23:
theorem
theorem
definition
let x,
y,
z be
bound_QC-variable;
let p be
Element of
QC-WFF ;
func All (
x,
y,
z,
p)
-> QC-formula equals
All (
x,
(All (y,z,p)));
correctness
coherence
All (x,(All (y,z,p))) is QC-formula;
;
func Ex (
x,
y,
z,
p)
-> QC-formula equals
Ex (
x,
(Ex (y,z,p)));
correctness
coherence
Ex (x,(Ex (y,z,p))) is QC-formula;
;
end;
:: deftheorem defines All QC_LANG2:def 8 :
for x, y, z being bound_QC-variable
for p being Element of QC-WFF holds All (x,y,z,p) = All (x,(All (y,z,p)));
:: deftheorem defines Ex QC_LANG2:def 9 :
for x, y, z being bound_QC-variable
for p being Element of QC-WFF holds Ex (x,y,z,p) = Ex (x,(Ex (y,z,p)));
theorem
for
x,
y,
z being
bound_QC-variable for
p being
Element of
QC-WFF holds
(
All (
x,
y,
z,
p)
= All (
x,
(All (y,z,p))) &
Ex (
x,
y,
z,
p)
= Ex (
x,
(Ex (y,z,p))) ) ;
theorem
for
p1,
p2 being
Element of
QC-WFF for
x1,
x2,
y1,
y2,
z1,
z2 being
bound_QC-variable st
All (
x1,
y1,
z1,
p1)
= All (
x2,
y2,
z2,
p2) holds
(
x1 = x2 &
y1 = y2 &
z1 = z2 &
p1 = p2 )
theorem
theorem
for
x,
y,
z being
bound_QC-variable for
p,
q being
Element of
QC-WFF for
t,
s being
bound_QC-variable st
All (
x,
y,
z,
p)
= All (
t,
s,
q) holds
(
x = t &
y = s &
All (
z,
p)
= q )
theorem
for
p1,
p2 being
Element of
QC-WFF for
x1,
x2,
y1,
y2,
z1,
z2 being
bound_QC-variable st
Ex (
x1,
y1,
z1,
p1)
= Ex (
x2,
y2,
z2,
p2) holds
(
x1 = x2 &
y1 = y2 &
z1 = z2 &
p1 = p2 )
theorem
theorem
for
x,
y,
z being
bound_QC-variable for
p,
q being
Element of
QC-WFF for
t,
s being
bound_QC-variable st
Ex (
x,
y,
z,
p)
= Ex (
t,
s,
q) holds
(
x = t &
y = s &
Ex (
z,
p)
= q )
theorem
for
x,
y,
z being
bound_QC-variable for
p being
Element of
QC-WFF holds
(
All (
x,
y,
z,
p) is
universal &
bound_in (All (x,y,z,p)) = x &
the_scope_of (All (x,y,z,p)) = All (
y,
z,
p) )
by Th8, QC_LANG1:def 20;
:: deftheorem defines disjunctive QC_LANG2:def 10 :
for H being Element of QC-WFF holds
( H is disjunctive iff ex p, q being Element of QC-WFF st H = p 'or' q );
:: deftheorem Def11 defines conditional QC_LANG2:def 11 :
for H being Element of QC-WFF holds
( H is conditional iff ex p, q being Element of QC-WFF st H = p => q );
:: deftheorem defines biconditional QC_LANG2:def 12 :
for H being Element of QC-WFF holds
( H is biconditional iff ex p, q being Element of QC-WFF st H = p <=> q );
:: deftheorem Def13 defines existential QC_LANG2:def 13 :
for H being Element of QC-WFF holds
( H is existential iff ex x being bound_QC-variable ex p being Element of QC-WFF st H = Ex (x,p) );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem defines the_left_disjunct_of QC_LANG2:def 14 :
for H being Element of QC-WFF holds the_left_disjunct_of H = the_argument_of (the_left_argument_of (the_argument_of H));
:: deftheorem defines the_right_disjunct_of QC_LANG2:def 15 :
for H being Element of QC-WFF holds the_right_disjunct_of H = the_argument_of (the_right_argument_of (the_argument_of H));
:: deftheorem defines the_antecedent_of QC_LANG2:def 16 :
for H being Element of QC-WFF holds the_antecedent_of H = the_left_argument_of (the_argument_of H);
:: deftheorem QC_LANG2:def 17 :
canceled;
:: deftheorem defines the_left_side_of QC_LANG2:def 18 :
for H being Element of QC-WFF holds the_left_side_of H = the_antecedent_of (the_left_argument_of H);
:: deftheorem defines the_right_side_of QC_LANG2:def 19 :
for H being Element of QC-WFF holds the_right_side_of H = the_consequent_of (the_left_argument_of H);
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th45:
theorem Th46:
theorem Th47:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem Def20 defines is_immediate_constituent_of QC_LANG2:def 20 :
for G, H being Element of QC-WFF holds
( G is_immediate_constituent_of H iff ( H = 'not' G or ex F being Element of QC-WFF st
( H = G '&' F or H = F '&' G ) or ex x being bound_QC-variable st H = All (x,G) ) );
theorem
canceled;
theorem Th58:
theorem Th59:
theorem Th60:
theorem
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
:: deftheorem Def21 defines is_subformula_of QC_LANG2:def 21 :
for G, H being Element of QC-WFF holds
( G is_subformula_of H iff ex n being Element of NAT ex L being FinSequence st
( 1 <= n & len L = n & L . 1 = G & L . n = H & ( for k being Element of NAT st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) ) );
:: deftheorem Def22 defines is_proper_subformula_of QC_LANG2:def 22 :
for H, F being Element of QC-WFF holds
( H is_proper_subformula_of F iff ( H is_subformula_of F & H <> F ) );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th71:
theorem Th72:
theorem Th73:
theorem Th74:
theorem Th75:
theorem Th76:
theorem Th77:
theorem Th78:
theorem Th79:
theorem
theorem Th81:
theorem Th82:
theorem Th83:
theorem
theorem Th85:
theorem Th86:
theorem
theorem
theorem Th89:
theorem
theorem Th91:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th99:
theorem Th100:
theorem Th101:
:: deftheorem Def23 defines Subformulae QC_LANG2:def 23 :
for H being Element of QC-WFF
for b2 being set holds
( b2 = Subformulae H iff for a being set holds
( a in b2 iff ex F being Element of QC-WFF st
( F = a & F is_subformula_of H ) ) );
theorem
canceled;
theorem Th103:
theorem Th104:
theorem
theorem
canceled;
theorem Th107:
theorem Th108:
theorem
theorem Th110:
theorem Th111:
theorem Th112:
theorem Th113:
theorem
theorem
theorem
theorem
theorem
theorem
theorem