Explosion and Cut Required

[Harvey Friedman]

Concerning Richard Heck's posting of
https://cs.nyu.edu/pipermail/fom/2022-June/023395.html

Boolos is implicitly arguing that since this is an inference in (f,s,=),,
that if first order logic is sufficient for the logic of mathematics, then
we have a real problem -- that that inference in first order logic is
absurdly long, and so can't possibly be viewed as the right way to
formalize this inference in (f,s,=).

However, if we view this inference as NOT an inference in logic, but
rather an inference in wider mathematics, then the issue is resolved.

Thus we get to the problem of just what is logic and just what goes beyond
logic to mathematics? Boolos is implicitly saying that it has to be logic
and not mathematics if the primitives are exactly the most basic kinds that
arise in the most basic logic inferences, and we have validity. This is
where his argument is not convincing.

Here is how I look at it. Firstly I claim that first order logic is
required for a formalization of mathematics. At least a version of it which
is restricted in certain ways from the usual and maybe bigger in other ways
through the use of sugar. The restrictions might be like one only considers
rather small formulas. We know from the formalization of mathematics that
one encounters only small formulas, and one needs abbreviation power. So
already from the get go there is some serious work needed to get a handle
on just what an adequate form of predicate logic for the formalization of
mathematics must have. Of course, as I have said repeatedly, explosion and
cut in various guises is absoutely required..

But it seems that no matter how one modifies first order logic for actual
formalization, one has a certain kind of equivalence. Perhaps the notion of
equivalence here needs to be better understood.

So we "need at least first order logic". Now we want to claim that there is
a fundamentally important notion of IRREDUCIBILITY. It is clear that we can
"reduce" say weak second order logic to first order logic through the
addition of nonlogical mathematical notions with their appropriate
mathematical axioms.

So the idea is that first order logic is distinguished as THE UNIQUE
IRREDUCIBLE VEHICLE FOR THE ADEQUATE DIRECT FORMALIZATION OF MATHEMATICS.

I anticipate serious work on explicating "unique", "irreduciable",
"adequate", and "formalization" here.

Harvey Friedman
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220607/29be1231/attachment-0001.html>