John Staples
-------------------------------------8<---------------------------
The papers (all sole-authored by Solomon Feferman) are:
1. Finitary inductively presented logics, in Logic Colloquium
'88, eds Bonotto, Valentini and Zanardo, pp. 191-220, Elsevier,
1989.
2. Logics for Termination and Correctness of Functional Programs,
II. Logics of Strength PRA. Manuscript. Text of a lecture for
the conference Leeds Proof Theory '90, V. Leeds, August 1990
(to appear?).
3. What Rests on What? The Proof-Theoretic Analysis of Mathematics,
Proceedings of the 15th international Wittgenstein Symposium,
August 1992 (to appear?).
4. Why a little bit goes a long way: Logical foundations of
scientifically applicable mathematics, Proceedings of the
Philosophy of Science Association meeting, Chicago, Oct. 1992
(to appear?).
Paper 1 is the most relevant to QED, and the most comprehensive. It
defines and analyses the finitary inductively presented (fip) theory FSO.
For example, FSO is shown to universal for fip logics, and a conservative
extension of primitive recursive arithmetic. It is formulated as a theory
of functions on, and classes of, `pure tree expressions' (i.e. objects
built from atomic objects called urelements by an ordered pairing operation).
Conceptually and pedagogically, FSO aims to be a theoretical framework for
the formalisation of meta-mathematics. The general approach is intended to
be useful in practice for computer implementation of logics. (The preceding
two sentences paraphrase part of Feferman's abstract; note they do not
state that FSO is immediately suitable for practical use.) Another paraphrase
from the introduction: the use of some FSO-like notion seems to Feferman
essential for stepping as naturally and directly as possible from a
humanly understandable presentation of a logic, to a computer-ready
presentation.
Paper 2, being part II of a longer work, is short on motivation, but the
title does a fair job of indicating that it is not so squarely focussed
on QED issues. The technical content is related to the content of the
other papers however.
Papers 3 and 4 are targetted at philosophers of science and mathematics,
and so have lots of motivation, discussion, references and insights, but
less technical content. The technical context is related to papers 1 and
2, but a wider range of formalisms is considered. The QED relevance of
these papers is reduced by the fact that they focus on using restricted
proof techniques directly in mathematics, rather than focussing on
metatheory. Their main point is that a large part of applicable
mathematics *can* be done under various proof restrictions. Before
that becomes relevant to QED however, one needs to ask: do people *want*
to do mathematics under these restrictions, particularly if that would
be more work, less natural or even just less familiar? Here are two
relevant sentences from the final paragraph of 3, in which the restricted
forms of mathematics considered are described as `non-platonist'. My
addition in brackets, [...].
`The uninformed common view - that adopting one of the non-platonistic
positions means pretty much giving up mathematics as we know it - needs
to be drastically corrected, and that [view] should also no longer serve
as the last-ditch stand of set-theoretical realism. On the other hand,
would-be non-platonists must recognise the now clearly marked sacrifices
required by such a commitment and should have well thought-out reasons
for making them.'
To that I would add that the sacrifices recognised in these papers of
Feferman's are mainly loss of provability in principle of certain results.
There is little or no consideration of how convenient the restricted proofs
are in practice compared to conventional proofs, or whether there is any
loss of uniformity of proof (e.g. whether a single scheme of theorems still
has a corresponding single, schematic proof).
Some bottom lines
1. Feferman does a highly professional job. For example, at first
I deplored his use in paper 1 of `pure tree expression' as a
basic semantic concept, since it seemed an annoying minor
departure from the standard notion of list. However, it seemed
to work like a Swiss watch! - at least for his purposes.
2. FSO is the main issue arising out of these papers, and I'd like
to comment separately on its semantics and syntax.
3. FSO semantics.
I can't criticise the general idea, since we've been thinking
along similar lines!-using lists. Pure tree expressions would
be OK by me. The main thing is to agree on something workable,
and both approaches are.
4. FSO syntax (including proof rules).
For a QED metatheory we certainly want to satisfy Feferman's
`natural and direct' criteria. The FSO vocabulary is in that
ball-park and I'd be happy for QED to give it a shot. (By that
I mean, it looks good enough to be a basis for QED 1.
Eventually there will be QED 2, QED 3 etc. to allow incorporation
of new insights.)
The FSO proof rules - particularly the limitation to primitive
recursion - are a concern, because they threaten to make meta
theory proofs longer, and perhaps harder and less uniform. I
suggest that QED maintain a degree of flexibility on this, as
follows. Fix the semantics, but have more than one strength of
theory: e.g. FSO as the `weak but pure' version, and anything
provable in ZFC about pure expression trees as the `strong but
mathematically respectable' version. The strong version can
support any form of reasoning about the semantic basis of QED.
The FSO version can be concerned with e.g. proof strength. More
importantly for me, it also defines a vocabulary small and simple
enough to have easy implementations. A metatheory is supposed
to simplify implementations, by allowing various things to be data
that would otherwise be coded. However it doesn't help with
simplification if the metatheory is hard to implement!
Am I betraying platonist tendencies? My excuse is that I'm a
utilitarian - I like mathematics to work as easily as possible.
In our work we've not yet put out metatheory proof rules - we've
regarded metatheory vocabulary and semantics as higher priorities,
given limited funding. We have grander aspirations however, and
QED certainly should.
John Staples