begin
theorem
canceled;
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
:: deftheorem defines FALSUM QC_LANG2:def 1 :
:: deftheorem defines => QC_LANG2:def 2 :
:: deftheorem defines 'or' QC_LANG2:def 3 :
:: deftheorem defines <=> QC_LANG2:def 4 :
:: deftheorem defines Ex QC_LANG2:def 5 :
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 :
:: deftheorem defines Ex QC_LANG2:def 7 :
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 :
:: deftheorem defines Ex QC_LANG2:def 9 :
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 :
:: deftheorem Def11 defines conditional QC_LANG2:def 11 :
:: deftheorem defines biconditional QC_LANG2:def 12 :
:: deftheorem Def13 defines existential QC_LANG2:def 13 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem defines the_left_disjunct_of QC_LANG2:def 14 :
:: deftheorem defines the_right_disjunct_of QC_LANG2:def 15 :
:: deftheorem defines the_antecedent_of QC_LANG2:def 16 :
:: deftheorem QC_LANG2:def 17 :
canceled;
:: deftheorem defines the_left_side_of QC_LANG2:def 18 :
:: deftheorem defines the_right_side_of QC_LANG2:def 19 :
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 :
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 :
:: deftheorem Def22 defines is_proper_subformula_of QC_LANG2:def 22 :
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 :
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