On Thu, Aug 28, 2014 at 8:42 PM, Solomon Feferman wrote:

I provide one answer to these questions via a formal system W (‘W’ in honor of Hermann Weyl) that has variables ranging over a universe of individuals containing numbers, sets, functions, functionals, etc., and closed under pairing, together with variables ranging over classes of individuals. (Sets are those classes that have characteristic functions.) While thus conceptually rich, W is proof-theoretically weak. The main metatheorem, due to joint work with Gerhard Jäger, is that W is a conservative extension of Peano Arithmetic, PA. Nevertheless, a considerable part of modern analysis can be developed in W. In W we have the class (not a set) R of real numbers, the class of arbitrary functions from R to R, the class of functionals on such to R, and so on. I showed in detail in extensive unpublished notes from around 1980 how to develop all of 19th c. classical analysis and much of 20th c. functional analysis up to the spectral theorem for bounded self-adjoint operators.

I developed some alternative conservative extensions of PA and HA called ALPO and B. The former, “analysis with the limited principle of omniscience”, was based on classical logic low down, and constructive logic higher up, and the latter for “Bishop” which was based on constructive logic. If I recall, both systems accommodated extensionality, which demanded additional subtleties in the conservation proofs. Both of these systems, if I recall, had substantially simpler axioms, and of course, there is the obvious issue of how important an advantage it is to have extensionality and to have simple axiomatizations.

The real issue you want to deal with is the formalization of the *actual* mathematics. There is a “new” framework to, at least potentially, deal with formalizations of *actual* mathematics without prejudging the matter with a particular style of formalization. This is the so called SRM = Strict Reverse Mathematics program. I put “new” in quotes because my writings about this PREDATE my discovery and formulation of the Reverse Mathematics program. SRM at the time was highly premature. I’m just now trying to get SRM off the ground properly.

The basic idea is this. Suppose you want to show that a body of mathematics is “a conservative extension of PA”. Closely related formulations are that the body of mathematics is “interpretable in PA” or “interpretable in ” … You take the body of mathematics itself as a system of mathematical statements including required definitions, and treat that as an actual formal system. This is quite different than the usual procedures for formalizing actual mathematics in a formal system, where one has, to various extents, restate the mathematics using coding and various and sundry adjustments. SRM could well be adapted to constructive mathematics as well. Actually, it does appear that there is merit to treating actual abstract mathematics as partially constructive. When I published on ALPO and B, I did not relate it to SRM ideas.

Now it is a mistake in your appendix to Ch. 9 to say that I can’t quantify over all real numbers; given that we have the class R of “all” real numbers in W, we can express various propositions containing both universal and existential quantification over R. Of course, we do not have any physical language itself in W, so we can’t express directly that “there is a [physical] point corresponding to every triple of real numbers.” But we can formulate mathematical models of physical reality using triples of real numbers to represent the assumed continuum of physical space, and quadruples to represent that of physical space-time, and so on; moreover, we can quantify over “nice” kinds of regions of space and space-time as represented in these terms. So your criticism cannot be an objection to what is provided by the system W and the development of analysis in it.

There is a research program that I have been suggesting that I haven’t had the time to get into – namely, systematically introduce physical notions directly into formalisms from f.o.m. I conjecture that something striking will come out of pursuing this with systematic imagination.

As to the philosophical significance of this work, the conservation theorem shows that W is justified on predicative grounds, though it has a direct impredicative interpretation as well. When you say you disagree with my philosophical views, you seem to suggest that I am a predicativist; others also have mistakenly identified me in those terms. I am an avowed anti-platonist, but, as I wrote in the Preface to In the Light of Logic, p. ix, “[i]t should not be concluded from … the fact that I have spent many years working on different aspects of predicativity, that I consider it the be-all and end-all in nonplatonistic foundations. Rather, it should be looked upon as the philosophy of how we get off the ground and sustain flight mathematically without assuming more than the structure of natural numbers to begin with. There are less clear-cut conceptions that can lead us higher into the mathematical stratosphere, for example that of various kinds of sets generated by infinitary closure conditions. That such conceptions are less clear-cut than the natural number system is no reason not to use them, but one should look to see where it is necessary to use them and what we can say about what it is we know when we do use them.” As witness for these views, see my considerable work on theories of transfinitely iterated inductive definitions and systems of (what I call) explicit mathematics that have a constructive character in a generalized sense of the word. However, the philosophy of mathematics that I call “conceptual structuralism” and that has been referred to earlier in the discussion in this series is not to be identified with the acceptance or rejection of any one formal system, though I do reject full impredicative second-order arithmetic and its extensions in set theory on the grounds that only a platonistic philosophy of mathematics provides justification for it.

I am curious as to where your anti-Platonist view kicks in. I understand that you reject per se on anti-Platonist grounds. Presumably, you do not expect to be able to interpret in a system that you do accept? Perhaps the only candidate for this is Spector’s interpretation? Now what about ? This is almost interpretable in and interpretable just beyond. So you reject but accept the target of an interpretation? What about ? How convincing are ordinal notation systems as targets of interpretations – or more traditionally, their use for consistency proofs?

Here is my view. There are philosophies of mathematics roughly corresponding to a lot of the levels of the interpretation hierarchy ranging from even well below EFA (exponential function arithmetic) to perhaps and without choice, and perhaps beyond. These include your philosophy. Most of these philosophies have their merits and demerits, their advantages and disadvantages, which are apparent according to the skill levels of the philosophers who advocate them. I regard the clarity of the associated notions as “continuously” degrading as you move up, starting with something like a 3 x 3 chessboard.

I decided long ago that the establishment of the following Thesis – which has certainly not yet been fully established – is going to be of essential importance in any dialog. Of course, exactly what its implications are for the dialog are unclear, and it may be used for unexpected or competing purposes in various ways by various scholars – just like Gödel’s first and second incompleteness theorems, and the Gödel/Cohen work on AxC and CH.

THESIS. Corresponding to every interesting level in the interpretation hierarchy referred to above, there is a sentence of clear mathematical interest and simplicity. I.e., which is demonstrably equivalent to the consistency of formal systems corresponding to that level, with the equivalence proved in EFA (or even less). There are corresponding formulations in terms of interpretations and conservative extensions.

Furthermore, the only way we can expect the wider mathematical community to become engaged in such issues (finitism, predicativity, realism, Platonism, etcetera) is through this Thesis.

Harvey