models of "future of mathematics"?

[Harvey Friedman]

Caballero  https://cs.nyu.edu/pipermail/fom/2022-March/023203.html writes

"The mathematical version of the Eternal Symmetree could be as
follows. Let s_0, s_1, s_2, ... be a sequence of statements in ZFC
such that each statement of ZFC or its negation belongs to this
sequence, but not both. Assume that s_0 is a true statement. Consider
the following infinite tree labeled by statements of ZFC defined by
the (non-computable) rules:

(i) the root (at level 0) is the statement s_0;

(ii) given a vertex at level n, if s_{n+1} is consistent with the
statements in the path from the root to the current vertex, then
s_{n+1} is a descendant of the current vertex.

(iii) given a vertex at level n, if the negation of s_{n+1} is
consistent with the statements in the path from the root to the
current vertex, then NOT( s_{n+1} ) is a descendant of the current
vertex.

Every infinite path in the mathematical Eternal Symmetree is a "future
of mathematics" (physicists use the terminology "future boundary" for
the set of these paths). The mathematical observer will perceive the
acceptance or rejection of an undecidable statement as a truly random
event, just like the result of a measurement in quantum mechanics (at
least according to Hugh Everett III). Notice that pruning corresponds
to avoidance of contradictions."

This is a basic version of the well known construction in usual f.o.m.
of the tree of complete consistent extensions of a "true" sentence phi
in the language of ZFC. As Caballero points out, this is a non
recursive tree.

In f.o.m. one also considers the recursive (and much better than that)
tree which is larger and at height n one allows branches that have no
inconsistency proof (over ZFC) of size at most n.

In any case, I am rather startled at the suggestion that this is a
productive model of the "future of mathematics" in any meaningful
sense. My reaction is further intensified by the suggestion that "the
mathematical observer will perceive the acceptance or rejection of an
undecidable statement as a truly random event".

The idea that the acceptance or rejection of a statement in ZFC
undecided in ZFC is in any way a random event goes against nearly the
entire history of f.o.m. and seems utterly indefensible.

First of all the general mathematical observer isn't even looking at
any statements undecided in ZFC at all. Only a small subset ever does
and when this small subset looks at them, the last thing they are
doing is thinking randomly or making random choices.

For instance, the choice between "there exists a strongly inaccessible
cardinal" and "there does not exist a strongly inaccessible cardinal"
isn't looked at by many mathematical observers, but of the ones that
do, the idea that it is a random choice would be regarded as
completely wrong. These observers almost entirely choose the former
rather than the latter for quite a number of reasons some of which are
rather interesting.

Same for the choice between "Con(ZFC) and not Con(ZFC)".

Also the relatively few that are observing "the continuum hypothesis"
and "the negation of the continuum hypothesis" are not even remotely
regarding this as a "random choice".

So having said that your model of "the future of mathematics" is at
best a gross oversimplification of the reality of mathematical
thinking, if you can offer up something new about this model or
related models for f.o.m. then that could be interesting.

One problem with such a setup is that you need to choose an
enumeration of the sentences of ZFC. There is no known way to make
such an enumeration that isn't generally viewed as ad hoc. It seems to
depend (or known to depend) on the exact details of the syntax of the
language used to cast ZFC. Even primitive notation is subject to tiny
issues. But if one is talking about real mathematical observers, they
are not going to be looking at anything in primitive notation. They
are going to use the usual libraries built up from various work on
proof assistants. But which proof assistants? Which libraries? Your
description of your model of "the future of mathematics" provides no
hint as to how you want to deal with this, let alone the other
disconnects with mathematical practice I have discussed.

Of course if you have any interesting statement to make about ALL such
trees - specifically paths through them - then such could fit well
into our f.o.m. developments.

Harvey Friedman