[FOM] The unreasonable soundness of mathematics

[Timothy Y. Chow]

On Mon, 2 May 2016, Mario Carneiro wrote:
> I'll grant that the word choice was not the best there, since it indeed 
> seems that I am performing this illegal "abstraction" operation here. 
> But the key is the next part: we're not modeling a machine, we are 
> building a machine to fit a model. This so-called "abstract machine" is 
> a mathematical model, probably infinite, which in ultrafinite terms 
> cannot be fully understood/explored, and furthermore has no a priori 
> relation to reality. It has an ontological status no different from, 
> say, the definition of a group or the natural numbers.
>
> The way we connect this to an actual computer, our "computer A", is by 
> treating it as a specification for a machine, and building the computer 
> to meet the specification. That is, the computer is considered to "work" 
> if it is able to sustain a correspondence with the abstract model 
> sufficiently long and well enough for our purposes. A computer which 
> fails this correspondence is deemed to be defective, unless the failure 
> is due to a designed hardware limitation, in which case we must either 
> give up on the problem we were trying to solve or improve the hardware 
> of the machine.

I still serious difficulties with this account.

The first issue is that a proof assistant that (say) verifies proofs of 
"sqrt(2) is irrational" in PA is not, by anyone's account, directly 
describing an "abstract machine."  Taken at face value, the sentences of 
first-order arithmetic are talking about integers, not about machines. 
That is, there is a distinction between the following two assertions.

1. There do not exist positive integers A and B such that A^2 = 2*B^2.

2. An abstract machine that is programmed to search for positive integers
    A and B such that A^2 = 2*B^2 will not halt.

But for the sake of argument, let us go with 2 rather than 1, since that 
seems to be what you want to do, and because my objection applies in that 
case as well.

The main trouble is that if, as an ultrafinitist, I don't know what an 
"abstract machine" is, then I have no way of treating sentences involving 
the term "abstract machine" as a machine spec or checking if the concrete 
machine matches the spec.  Instead of "abstract machine" I might as well 
use the nonsense word "boojum."  If you give me rules for how to 
manipulate sentences involving the word "boojum" then I can happily verify 
whether the syntactic rules are being followed.  But if you then tell me 
to build a boojum then all I can do is stare at you blankly.

In other words, I claim that you're not being true to your own stated 
philosophical assumptions and you're sneaking some illegitimate 
assumptions in the door.  You're looking at sentences involving the term 
"abstract machine" and secretly saying to yourself, "I know what that 
means" when in fact there's no justification for that.  If abstract 
machines don't exist, and don't even make any philosophical sense, then 
how can we claim to know what the phrase "abstract machine" means?

Tim