[FOM] The unreasonable soundness of mathematics
Timothy Y. Chow
tchow at alum.mit.edu
Mon May 2 14:27:42 EDT 2016
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?
More information about the FOM