[FOM] The unreasonable soundness of mathematics

[Mario Carneiro]

On Sun, May 1, 2016 at 2:33 PM, Timothy Y. Chow <tchow at alum.mit.edu> wrote:

> On Sat, 30 Apr 2016, Mario Carneiro wrote:
>
>> Now let's suppose that the correspondence fails somehow, so that computer
>> B has proven |- P(42) but computer A has found that P(42) is false.
>> Assuming that the theory used by computer B is sufficiently powerful, it
>> will be able to formalize the abstract machine states of computer A, and
>> thereby will also prove |- not P(42), and hence the theory is inconsistent
>> (and the proof of this is reasonably sized too). Thus the correspondence
>> reduces to a consistency problem for the theory of computer B.
>>
>
> The trouble I see is this.  If I were an ultrafinitist, I would have no
> idea what you're talking about when you speak of "abstract machine states
> of computer A."  I know what specific machine states of computer A are when
> I see them.  But I don't know what you mean by the word "abstract" here,
> let alone what you mean by "formalizing" them.  Yes, I can see people
> writing down formalizations and claiming that they're "abstracting"
> something, but it's all black magic and hocus pocus as far as I'm concerned.


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.

Given this, we have *by construction* a relationship between the behavior
of computer A, and the "abstract" specification of it, which can be thought
of as being the operation of some Platonic machine if one likes; and this
latter model is faithfully represented in computer B, where we can make
statements at a higher level regarding its operation. This allows us to
prove a statement of the form "as long as computer A continues to satisfy
its specification, it will never find a counterexample to P(n)", so that we
can be sure that any counterexamples discovered by computer A are an
indication of hardware failure or limitations, or a bug in the
implementation of the spec.

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160502/bcef4383/attachment.html>