[FOM] 537: Pi01/Flat Pics/Testing

[Harvey Friedman]

http://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#82 - #84 are fully operational.

#82,#84 are frequently being updated, although we expect most of the
updates going forward to be for #82.

The new #84 is called FLAT MENTAL PICTURES. Here the idea is that very
simple conditions on the world W of objects allows us to construct
models of the iterative set theoretic universe V - where the
background is higher order logic formulated within a first order
system. This is material that can be used to develop the idea that

*the iterative concept of set is not fundamental and can be and should
be reduced to flat concepts such as equivalence relations, linear
orderings, and even just equality".

I have ambitious plans for going much further systematically with this.

Now please bear in mind that I don't hold views - I simply supply
hopefully good theorems that justify or attack views.

As Hillary Putnam has indicated, in different language, essentially
all views in the philosophy of mathematics put forward by top skilled
philosophers are equally convincing and equally non convincing -
although Hillary might make an exception for himself (smile). He wrote
"Why Nothing Works".

So that's why I am so willing to prove theorems that help or hurt
practically any view.

I am almost ready to update #83 TESTING THE CONSISTENCY OF MATHEMATICS
with material on testing the consistency of HUGE. This is in light of
the fact that I manage to give a rather unexpectedly clear explicitly
Pi01 sentence in #84 equivalent to Con(HUGE).

Now for something new on the implicitly Pi01 front. We can look for
maximal solutions to purely universal properties:

PROPOSITION 1. Every purely universal condition on subsets of
Q[-n,n]^k has a maximal solution whose sections at the x in
{0,...,n}^r< have the same negative part.

We now introduce partial functions. We look at partial f:Q[-n,n]^k
into Q[n,-n]. We say that f is regressive if and only if for all x in
dom(f), f(x) > max(x).

PROPOSITION 2. Every purely universal condition on regressive
functions from Q[-n,n]^k into Q[-n,n] has a maximal solution which is
either constantly 0 or constantly undefined on {1,...,n}^r<.

THEOREM 3. Propositions 1,2 are provably equivalent to Con(SRP) over WKL_0.

****************************************
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 537th 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

Harvey Friedman