[FOM] Unsoundness?/Random Sentences

[Harvey Friedman]

On May 24, 2009, at 5:37 PM, Nik Weaver wrote:

> Harvey Friedman wrote:
>
>> WHAT WOULD EVIDENCE OF THE NON ARITHMETICAL SOUNDNESS OF ZFC LOOK  
>> LIKE?
>
> Well, what would evidence of the arithetical soundness of ZFC look  
> like?


Since Weaver is making the suggestion that ZFC is consistent but not  
arithmetically sound, and at least implicitly suggesting that people  
do research surrounding this topic, the burden of proof is on Weaver  
to give some indication as to what such research would constitute.

As I wrote in my previous posting, http://www.cs.nyu.edu/pipermail/fom/2009-May/013712.html

I do not see any avenue of research on Weaver's suggestion other than  
simply looking for inconsistencies in set theories. Conventional  
wisdom is that this is entirely hopeless. Do you have an idea for this?

The burden of proof is not on me concerning research on evidence of  
the arithmetical soundness of ZFC, but I can still offer two well  
known answers, which I believe are implicit in Goedel:

1. Continue proving from big set theories, various arithmetical  
theorems. Then wait and see if they are later proved using "innocent"  
systems such as PA or even EFA (exponential function arithmetic).

This happened in a rather interesting way with Laver's use of very  
large cardinals to prove theorems about free left distributive algebras.

This also is probably happening with FLT. The existing proof is  
formalized just beyond ZFC, then can be observed to use less and less,  
down to around the highly impredicative system of 3rd order  
arithmetic. There is now a manuscript of Angus MacIntyre sketching a  
proof of FLT in PA. I don't know if number theorists have examined it  
for correctness, yet. I conjectured long ago that FLT is provable in  
EFA.

There were many postings on where FLT can be proved on the FOM list a  
few years back. It is a stark example of where mathematicians readily  
accepted impredicative methods (and extremely impredicative methods,  
in fact) even to prove a trivially stated universal sentence in PA(0,S, 
+,dot,exp). I find that I am having to push hard to convince  
mathematicians to even think at all about removing the heavy  
impredicativity involved in the proof! So even as the impredicativity  
may be being removed, this still tells us something interesting about  
the mathematical community.

On the other hand, we do have good evidence that the mathematical  
community really does care about the related but different issue:  
effectivity. There are loads of Pi02 and Pi03 theorems in mathematics  
where we don't have decent bounds. In the case of Pi03, lots of  
important cases where we don't have any recursive bounds, let alone  
"reasonably recursive".

2. Find some concepts that are far removed from set theory, and  
develop principles which are either "more evident" than ZF is, or  
"disassociated with set theory but highly plausible", and use them to  
prove the formal statement "ZF is arithmetically sound". Attempts to  
carry this out are embodied in my Concept Calculus program.

> On May 24, 2009, at 1:50 PM, Timothy Y. Chow wrote:
> Harvey Friedman <friedman at math.ohio-state.edu> wrote:
>> WHAT WOULD EVIDENCE OF THE NON ARITHMETICAL SOUNDNESS OF ZFC LOOK  
>> LIKE?
>
> One example would be a proof of "ZFC is inconsistent" in ZFC.
>
> Actually, what I think is more interesting is Nik Weaver's implicit
> suggestion that a random sentence in the first-order language of
> arithmetic is undecidable in PA.  Is there any way to make this  
> precise?
>
> Tim

Any proof in ZFC of "ZFC is inconsistent" would immediately give an  
inconsistency proof in ZFC + 'there exists an inaccessible cardinal".  
So my earlier posting http://www.cs.nyu.edu/pipermail/fom/2009-May/013712.html 
  applies.

In contrast to implicit suggestions concerning the arithmetic  
unsoundness of ZF, looking at "random sentences" probably leads to a  
very reasonable research topic. I have thought about this kind of  
thing myself, without generating any results.

I think we need to proceed slowly on this. First, what do we know  
about the following much easier (I think) problem?

For each n, let TAUT(n;not,and,or) be the number of propositional  
formulas with at most n occurrences of letters, using only not, and,  
or, which are tautologies.

What can we say about the asymptotic behavior of TAUT(n;not,and,or) as  
n goes to infinity?

Harvey Friedman