Explosion and Cut Required

[Richard Kimberly Heck]

In response to Harvey's post, copied below...

Of course it's always possible to regard second-order logic as a 
first-order type theory and so regard the higher-order bits as math, not 
logic. So you might take Boolos's argument to show that mathematical 
reasoning is already implicated in quite 'ordinary' thinking. I didn't 
mean to suggest that the argument either decides or presupposes any 
question about whether second-order logic (or some of it) really is logic.

Actually, at the end of his life, George claimed no longer to understand 
the question whether second-order logic is 'logic', stated so baldly. I 
myself tend to be with Frege here and think of logic as comprising those 
principles of reasoning that are applicable no matter what the subject 
matter: Logic is the science of the most general principles of 
reasoning. Cases like George's can be modified to make it plausible that 
there's nothing specifically mathematical about the inference being made 
in that case. You get something like this in this paper 
<https://philpapers.org/rec/BOOTBI>.

Contrast the inferences that Jeffrey Ketland discusses in this paper:
https://www.jstor.org/stable/3329329
Those really do look mathematical, and so the argument he's making there 
against nominalism has some teeth. Then again, it's also possible to 
make a case that those inferences should really be formalized using 
non-first-order quantifiers like "There are just as many Fs as Gs". At 
the end of his (also too short) life, Aldo Antonelli was working on a 
paper arguing that there is a sense in which such quantifiers are 
first-order. See e.g. these slides <https://philpapers.org/rec/ANTFQ>. 
I've made a similar case here <https://philpapers.org/rec/HECTLO>.

I also that the notion of definition is very important and could use 
more discussion than it's usually given. Jamie Tappenden has done some 
good work on this. There are interesting cases, such as the definition 
of prime number, where there's an important question how the notion is 
best defined, even though the usual definitions are equivalent in the 
original context. So we can define primality in terms of non-trivial 
divisors or in terms of the law: If p | ab, then p | a or p | b. My 
understanding is that the latter is the 'right' definition, because it 
is what works best in general. But I could be misremembering the example.

Generally speaking, I think Harvey is right that there's some notion of 
formalizing 'actual reasoning' that's missed by folks like Tennant. 
Perhaps God does not need cut. We do.

In response to an earlier post of Arnon's, in which he suggested that 
'safety' might be a reason to reject second-order principles (or, at 
least, not regard them in the same way), it's not clear to me how this 
even addresses Boolos's argument. His claim was that, if you accept the 
inference in question:
     ∀n(f(n,1) = s1)
     ∀x(f(1,sx) = ssf(1,x))
     ∀n∀x(f(sn,sx) = f(n,f(sn,x))
     D1
     ∀x(Dx → Dsx)
     ∴ Df(ssss1,ssss1)
then the reasoning that convinces you of its validity is simply not 
first-order. It can't be, because any reasonable first-order version of 
that inference is mind-bogglingly long. Ketland, in his paper, tries to 
parlay this 'psychological' claim into an epistemological one.

Riki

On 6/7/22 19:54, Harvey Friedman wrote:
> 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 
> guisesis 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.
>
> Ianticipate serious work on explicating "unique", "irreduciable", 
> "adequate", and "formalization" here.
>
> Harvey Friedman
>

-- 
----------------------------
Richard Kimberly (Riki) Heck
Professor of Philosophy
Brown University

Office Hours: Monday 2-3, Wednesday 3-4
Monday: https://brown.zoom.us/j/92705928838
Wednesday: https://brown.zoom.us/j/99591098476
Personal link: https://brown.zoom.us/my/rikiheck

Pronouns: they/them/their

Email:           rikiheck at brown.edu
Website:         http://rkheck.frege.org/
Blog:            http://rikiheck.blogspot.com/
Amazon:          http://amazon.com/author/richardgheckjr
Google Scholar:  https://scholar.google.com/citations?user=QUKBG6EAAAAJ
ORCID:           http://orcid.org/0000-0002-2961-2663
Research Gate:   https://www.researchgate.net/profile/Richard_Heck