[FOM] 540: SRM/Comparability
Harvey Friedman
hmflogic at gmail.com
Mon Sep 8 00:03:51 EDT 2014
First some comments about SRM = strict reverse mathematics that go to the
heart of an issue in the formalization of mathematics. The following set of
axioms was presented, among many others, in
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#59:
1. Linearly ordered integral domain axioms.
> 2. Finite interval. [x,y] exists.
> 3. Boolean difference. A\B exists.
> 4. Set addition. A + B = {x+y: x in A and y in B} exists.
> 5. Set multiplication. AxB = {xy: x in A and y in B} exists.
> 6. Least element. Every nonempty set has a least element.
> 7. n^0 = 1. m >= 0 implies n^(m+1) = n^m x n. n^m defined implies m >= 0.
> 8. {n^0,...,n^m} exists.
> 4,5 together can be simplified in various ways. E.g., A+A, cA, and
> {1,4,9,16,...,n^2} exists.
> 1-8 is a formal system which is conservative over EFA = exponential
> function arithmetic. It is outright equivalent to the obvious form of
> EFA incorporating finite sets.
Furthermore, I also did this using finite sequences of integers
> instead of finite sets of integers, where concatenation of course
> plays a big role. There are advantages and disadvantages in the
> sequence approach. E.g., an advantage is that there is arguably more
> mathematics involving finite sequences than finite sets.
A main issue that I wanted to address there is this: CAN THE WHOLE OF
NORMAL MATHEMATICS BE FORMALIZED IN A CONSERVATIVE EXTENSION OF PA OR EVEN
A CONSERVATIVE EXTENSION OF EFA? CAN THE WHOLE OF NORMAL MATHEMATICS BE
FORMALIZED IN A SYSTEM PROVABLY CONSISTENT WITHIN EFA = exponential
function arithmetic?
Upon reflection, we some to realize that this had never been established.
The above arguably establishes that "the whole of normal mathematics cannot
be formalized in a system provably consistent within EFA".I am overdue
writing a paper that jumps off of where I left off, to replace EFA by PA
and by much much stronger systems. To put it positively, I am also looking
to relax "normal" and find a set of actual statements that cannot be proved
consistent in ZC or even ZFC or ZFC + LCs which are as close to normal
mathematics as I can make them. Of course, a good way to approach the ZFC +
LC situation is using my new independent statements, which I need to show
have their full power within a purely normal mathematical infrastructure.I
think that this is almost immediate over the version FSEQ - the finite
sequence version of the above. The maximal square versions of course need
infinite sets of finite sequences of rationals in fixed dimension, but I
think almost nothing needs to be used about them. So this is probably
already just about done via my new statements. I am preparing other ways
that don't rely on really ordinary well known statements. It is important
to have a wide variety. But it is still highly interesting to have other
ways of doing this based on raw material drawn from diverse areas of
mathematics.
This is not merely deeply knocking down a straw man. I believe that the
many anti foundational scholars in math logic implicitly believe that
normal mathematics does NOT have any logical strength, and is NOT subject
to Goedel phenomena. So this is definitely something for them to chew on.
I now turn to interpretation comparability.
INTERPRETATION COMPARABILITY CONJECTURE. For any two "natural" theories,
one is interpretable in the other.
I have been pushing the crucial importance of this conjecture for RM =
reverse mathematics. Here the appropriate form of "natural" is that used
when doing RM = reverse mathematics. More generally, say, one of our
standard systems from f.o.m., augmented with statements from the ordinary
mathematical literature, would be highly relevant. Even better would have a
good SRM type counterexample.
In http://www1.maths.leeds.ac.uk/~rathjen/Slow-Consistency-APAL.pdf a
"counterexample"
is given there involving lengths of proofs in formal systems, and ordinals
< epsilon_0. Their point is that they don't use self reference, as is made
clear in the paper. But the original Conjecture is wide open as originally
intended.
Often I give natural mathematically presented Templates of statements, and
conjecture that one can decide them using strong set theories. Sometimes I
can prove these Template conjectures if I strategically restrict the scope
of the Template. In each case, I believe that the infinite family of
statements are comparable under interpretability. I have never proved an
interesting result of this kind to date.
****************************************
My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
This is the 5
40
th in a series of self contained numbered
postings to FOM covering a wide range of topics in f.o.m. The list of
previous numbered postings #1-527 can be found at the FOM posting
http://www.cs.nyu.edu/pipermail/fom/2014-August/018092.html
528: More Perfect Pi01 8/16/14 5:19AM
529: Yet more Perfect Pi01 8/18/14 5:50AM
530: Friendlier Perfect Pi01
531: General Theory/Perfect Pi01 8/22/14 5:16PM
532: More General Theory/Perfect Pi01 8/23/14 7:32AM
533: Progress - General Theory/Perfect Pi01 8/25/14 1:17AM
534: Perfect Explicitly Pi01 8/27/14 10:40AM
535: Updated Perfect Explicitly Pi01 8/30/14 2:39PM
536: Pi01 Progress 9/1/14 11:31AM
537: Pi01/Flat Pics/Testing 9/6/14 12:49AM
538: Progress Pi01 9/6/14 11:31PM
539: Absolute Perfect Naturalness
9/7/14 9:00PM
Harvey Friedman
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140908/4cc7bb94/attachment.html>
More information about the FOM
mailing list