From owner-qed Mon Jul 4 19:48:06 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id TAA25176 for qed-out; Mon, 4 Jul 1994 19:45:47 -0500 Received: from uqcspe.cs.uq.oz.au (uqcspe.cs.uq.oz.au [130.102.192.8]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id TAA25170 for ; Mon, 4 Jul 1994 19:45:33 -0500 Received: from everest.cs.uq.oz.au by uqcspe.cs.uq.oz.au id ; Tue, 5 Jul 94 10:44:34 +1000 Received: by everest (5.0/SMI-SVR4) id AA23905; Tue, 5 Jul 1994 10:44:31 --1000 Date: Tue, 5 Jul 1994 10:44:30 +1000 (EST) From: John Staples Reply-To: John Staples Subject: Feferman's FSO, etc. To: qed@mcs.anl.gov Cc: rhys@meteor.brisnet.org.au, staples@cs.uq.oz.au Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; CHARSET=US-ASCII Content-Length: 6709 Sender: owner-qed@mcs.anl.gov Precedence: bulk Bob Boyer kindly put me in touch (deliberately vague) with the following papers of Feferman on FSO and related systems. Below I've reviewed them briefly, from the point of view of expressing an opinion on QED relevance. If any QED-er would like me to do for you what Bob did for me (deliberately vague again), then please let me know within the next week. 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