On Fri, Aug 29, 2014 at 2:50 AM, Harvey Friedman wrote:

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.

There are different ways of isolating weak formal systems in which substantial portions of actual mathematics can be formalized; they each have advantages and disadvantages. I am of course familiar with your systems ALPO and B and appreciate your fine conservation results for those as having real metamathematical interest. But the price you pay to insure extensionality seems to be that they both employ (as you say) partial or full intuitionstic logic and thus are not as readily useful to represent current mathematics in which non-constructive arguments are ubiquitous.

And if it is just constructive mathematics that one wants to represent, Bishop has shown that extensionality is a red herring: every “natural” mathematical kind carries an appropriate “equality” relation, and functions of interest on such objects are supposed to preserve those relations. But the objects themselves can be interpreted as being explicitly given and the functions of interest are given by underlying computable operations. That is a way to have one’s constructive cake and eat it too. Incidentally, the model theorist Abraham Robinson also promoted thinking in terms of equality relations instead of extensionality for quite different reasons.

Simplicity is not really relevant here. The question was, what mathematical notions and principles concerning them are indispensable to (current mathematized) science? The answer provided by my system W is: no more than what can be reduced to PA. Formal systems that are reduced to PA like your fragments of set theory or fragments of 2nd order arithmetic may be formally simpler on the face of it, but one has to see what it takes to actually check to see what part of mathematics can be done on that basis. I contend that the simpler the formal system the less direct is that verification. My system W makes use of a less familiar formalism, but it is more readily used than others I have seen to carry that out. Witness the notes to which i have referred: “How a little bit goes a long way. Predicative foundations of analysis.”

The real issue you want to deal with is the formalization of the

actualmathematics.

Well, the only issue I dealt with in response to Hilary was the question of the formalization of scientifically applicable mathematics.

There is a “new” framework to, at least potentially, deal with formalizations of

actualmathematics 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 ACA_0″.. 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.

I remember your talking about the idea of SRM before you turned to RM. That was ages ago (c. 1970?). I am totally skeptical of this because the only way that an actual body of mathematics can be treated as a formal system is to be given as a formal system to begin with, and no mathematics of interest has that character (proof checking systems notwithstanding) Moreover, we understand different formalizations, e.g. of elementary arithmetic, as being essentially the same even though differing in formal details, because we understand them in terms of their intended meaning.

Consider analysis: say there are 100 textbooks on functional analysis, all covering essentially the same material. Which one is “the” text for your SRM? Ditto for every other part of mathematics.

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 don’t foresee any problems with that.

I conjecture that something striking will come out of pursuing this with systematic imagination.

Let’s see.

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 $\textsf{ID}_{<\omega}$ 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?

First, as a mathematician (specializing in logic and related topics), my work doesn’t hew in a direct way to my philosophy. I use current everyday set theory (sets, set-theoretical operations, cardinals, ordinals) like most every other mathematician. But one of my aims is to investigate what is really needed for what, and to see whether that has philosophical significance.

Second, proof theory does not make the consistency of this or that formal system any more convincing than what one was reasonably convinced of before. (See my article, “Does proof theory have a viable rationale?”) But the reduction of subsystems of classical analysis to constructive theories of iterated inductive definitions from below is significant for a generalized Hilbert’s program. In any case, I don’t have a red line.

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 $j:V \to V$ 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.

I am not out to get mathematicians generally engaged in such issues; it is a rare mathematician who does (Weyl, Brouwer, Hilbert, Bishop). But even if one is out to do that, I don’t think your Thesis (to whatever extent that may be verified) will serve to engage them any more in that respect.

Best,

Sol