Errata to the submitted article
Ralph Matthes
Non-Strictly Positive Fixed-Points for Classical Natural Deduction
(31 pages, 2 July 2003)
Insignificant typos and omissions:
throughout: apparently -> evidently (added on September 2)
p.6 proof, l.6: rules -> rule
l.-9: F by can -> F can
p.8 def mult. elim.: e[*:=E] will be written as e[E] in the sequel
p.9 remark 7: F^+ should not be confounded with system F^+ (p.21)
p.10 l.4 before remark 9: the side hypotheses ->
the side hypotheses in the last three rules
remark 9: the subscript to SN should be an asterisk *
p.14 constructions l.3: can be more elegantly by ->
can more elegantly be
p.16 (2) replace "=>" by a dot
p.22 proof lemma 29 l.4: Then U -> Then "intersection over U"
p.27 l.3 v_0 -> v_1, same in third line from below in that proof
Mathematical mistake (with correction):
p.27 l.1 E[t] in SN implies E_n[t] in SN:
This requires in general e[t] in SN => t in SN.
Its truth is not an immediate consequence of the derived rule
for SN in the center of p.25, but can be proven from it by
course-of-value induction on SN. (Course of value is needed
in case E=* in the fourth rule of SN.)
FINIS