Tag Archives: SRM

Re: Paper and slides on indefiniteness of CH

This note touches on three matters.

1. A correction to the SRM = strict reverse math system I presented.

The error and its correction are quite interesting. I’m writing a new paper on SRM which will have the right statement and break new SRM ground.

2. Formulations of the IMH = inner model hypothesis.

3. Concerning my need for a response to the Fields Medalist as to “why should I believe a subtle cardinal exists or is consistent?”

I wrote

  1. Linearly ordered integral domain axioms.
  2. Finite interval. [x,y] exists.
  3. Boolean difference. A\setminus B exists.
  4. Set addition. A + B = \{x+y: x \in A\text{ and }y \in B\} exists.
  5. Set multiplication. A\times B = \{xy: x \in A\text{ and }y \in B\} exists.
  6. Least element. Every nonempty set has a least element.
  7. n^0 = 1. m \geq 0 implies n^{m+1} = n^m \times n. n^m is defined only if m \geq 0.
  8. \{n^0,\dots,n^m\} exists.

and said that the above is a conservative extension of EFA = exponential function arithmetic = \textsf{I}\Sigma_0(\text{Exp}).

8 needs to be changed to

8. \{0+n^0,1+n^1,...,m+n^m\} exists.

This issue is not a problem in SRM formulations with finite sequences — we can get away with postulating that (n^0,n^1,...,n^m). In any case, one first proves that 1-7 above is conservative over PFA = polynomial function arithmetic = \textsf{I}\Sigma_0(\text{Exp}).

About IMH. Sy has just written to Pen Maddy,

“I am sorry that you take such a negative view of this programme’s philosophical merits. But at least you may have interest in the math that comes out of it!”

It appears that to some extent, Sy has followed a model of thought that I indicated in an earlier email. Namely, he felt some Foundational Traction with IMH, and then developed and fine tuned an associated philosophy. This is, for various reasons, evidently not received positively clearly by Pen and Peter, and to some extent, not by Hugh and John either.

I can see some Foundational Traction in the IMH. However, it needs to be reformulated in order to have more. I quote from “On the consistency strength of the Inner Model Hypothesis“:

The Inner Model Hypothesis (IMH): If a statement \varphi without parameters holds in an inner model of some outer model of V (i.e., in some model compatible with V), then it already holds in some inner model of V.

Equivalently: If a statement \varphi is internally consistent in some outer model of V then it is already internally consistent in V. This is formalised as follows. Regard V as a model of Gödel-Bernays class theory, endowed with countably many sets and classes. Suppose that V^* is another such model, with the same ordinals as V. Then V^* is an outer model of V (V is an inner model of V^*) iff the sets of V^* include the sets of V and the classes of V^* include the classes of V. V^* is compatible with V iff V and V^* have a common outer model.


They show that, using some PD (and hence a big enuf large cardinals by Martin/Steel), for all reals x of sufficiently high Turing degree, the least transitive model of ZFC containing x satisfies IMH. They also use IMH to get models of strong kinds of measurable cardinals using inner model theory for strong kinds of measurable cardinals (Mitchell). There seems to be good deep higher set theory here.

If I were writing that paper, I would have included some friendly warmup material to allow casual and semi-casual readers to get more out of it. In particular, a warmup proof that 0^\# comes out of IMH, presumably using Jensen’s original covering theorem. And maybe a second warmup for 0^\dagger. Also, there may be strategic warmups for the construction of models of IMH. But maybe there are some expositional notes on IMH that are more friendly??

The formulation is somewhat awkward for any kind of intrinsic treatment of set theoretic maximality. Clearly IMH has something to do with maximality, but the philosophy gets strained under the present formulation of IMH (at least the formulation from this IMH paper).

IMH as a statement in class theory paradoxically is formulated in terms of outer models of V. But according to maximality, V doesn’t have any (proper) outer models. So the outer models of V must be taken to be imaginary.

So one way to go is this:

INFORMAL HYPOTHESIS. If a sentence holds in some imaginary transitive model of ZFC containing all ordinals, then it holds in some actual transitive model of ZFC containing all ordinals.

An obvious candidate for “imaginary transitive model of ZFC” is given by class forcing, where of course one does not get involved with any actual generic objects – because V is in fact maximal and so generic objects don’t really exist. I.e., on this interpretation, a sentence holds in an “imaginary transitive model of ZFC” if and only if it is forced by all conditions in some appropriate class forcing that does exist. Appropriate means that it is ZFC friendly.

I guess that this is equivalent by Jensen coding to INFORMAL HYPOTHESIS. There is a real number x such that the following holds. If a sentence holds in some imaginary transitive model of ZFC containing all ordinals, then it holds in some inner model of L[x].

Now class forcing seems to be too technical to be a satisfactory interpretation of “imaginary transitive model of ZFC”. Instead, we can simply require that a sentence be consistent with a strong form of the axioms and rules of inference of infinitary logic applied to ZFC. This seems more general than class forcing. Using definable cone determinacy and Jensen coding, it does appear that the infinitary proof rule formulation can be shown to be consistent – by throwing it into countable models, where the infinitary axioms and rules of inference are complete and hence give actual models to do Jensen coding on.

Thus on this formulation, countable models only appear in a consistency proof, and not in the actual formulations.

With regard to my question about what the best answer is to that senior Fields Medalist who asks “Why is there a subtle cardinal, or why is it consistent with ZFC?” There is the following exchange so far on the FOM.

Rupert McCallum writes:

William Tait wrote an essay that appeared in “The Provenance of Pure Reason” called “Constructing Cardinals from Below” which discussed a set of reflection principles that justify SRP. Unfortunately Peter Koellner later observed that some of the reflection principles he considered were inconsistent. I wrote down my own thoughts in a recent Mathematical Logic Quarterly article about how one might find principled grounds for distinguishing the consistent ones from the inconsistent ones.

I sent in to FOM:

I’m sure that the FOM readers would be most interested if you could give a simple brief account of the ideas behind some of the reflection principles that work – at least in the sense that they can be obtained from standard large cardinal hypotheses. Of course, subtle cardinals themselves are based on a very simple idea – but that idea would not normally be characterized as reflection.

For just subtle, we have \kappa is essentially subtle if and only if \kappa is a cardinal such that for all binary relations R on kappa, there exists infinite \alpha < \beta < \kappa such that the sections of R at \alpha,beta agree below \alpha.

Note that essentially subtle is closed upward, so it is not quite the same as being subtle. HOWEVER, the first subtle cardinal is exactly the first essentially subtle cardinal. ALSO “there exists a subtle cardinal” is equivalent to “there exists an essentially subtle cardinal”.

If FOM readers relate to your simple brief account, they can of course delve into publications. FOM readers can also get a chance to interact online starting from what you write.


PS: Maybe I see how to do this using some arguable reflection using multiple universes. Let’s consider two universes V and V', where V' is longer than V. Let’s not worry about the most philosophically honest way to formalize this just yet.

Let R be a binary relation on V and let \varphi be a sentence that holds in (V',V,R). “Reflection” says that there exists kappa in V such that \varphi holds in (V',V_kappa, R|V_kappa). This seems to prove Con(ZFC + “there exists a subtle cardinal”). I think that if you use V,V',V'',V''',\dots then you will get Con(SRP).

Re: Paper and slides on indefiniteness of CH

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 actual mathematics.

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 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 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 \textsf{Z}_2 per se on anti-Platonist grounds. Presumably, you do not expect to be able to interpret \textsf{Z}_2 in a system that you do accept? Perhaps the only candidate for this is Spector’s interpretation? Now what about \Pi^1_1\textsf{-CA}_0? This is almost interpretable in $\textsf{ID}_{<\omega}$ and interpretable just beyond. So you reject \Pi^1_1\textsf{-CA}_0 but accept the target of an interpretation? What about \Pi^1_2\textsf{-CA}_0? 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 j:V_{\lambda+1}\to V_{\lambda+1} 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 \Pi^0_1 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.