[FOM] The unreasonable soundness of mathematics

[Mario Carneiro]

On Mon, May 2, 2016 at 2:27 PM, Timothy Y. Chow <tchow at alum.mit.edu> wrote:

> 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.
>

I would consider the equivalence of (1) and (2) to be a "solved problem" in
this context; it is simply a matter of having a mathematical model for
computation, such as Turing machines or computable functions. Once you are
making a statement in the prover about an abstract model of computation, it
is only a few more steps (well, maybe more than a few, but certainly a
feasible number) to get to a purely mathematical statement such as sqrt(2)
is irrational.


> 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.
>

It sounds like what you are objecting to is the very concept of a
"specification". Let's break it down, then, to a really simple component,
like an AND gate. Now an AND gate has a specification, a.k.a. a
mathematical model to which the physical component is supposed to adhere.
The specification will say something like "return 1 if both inputs are 1,
otherwise 0", but the hardware has to work with messy reality, so it
actually measures voltage on its input lines and produces some other
voltage, with some range of voltages interpreted as 1 and a disjoint range
for 0, with some fuzz in the middle.

This yields a kind of "interpretation function" from the real voltage to
the "abstract state", which might not be total (because there are bad
states and indeterminate states). Using this function, one can test that
when the inputs are valid, the outputs are valid and map to the correct
abstract state, according to the specification. If it performs correctly
for all inputs (or at least a representative sample of inputs), then we
accept the component as performing to spec. Assuming the components have
sufficiently small failure rates, composing components will continue to
maintain the low-level correspondence. Eventually you can work your way up
to the full computer.

Now you haven't said this yet, but one might argue that if you actually try
to build a model all the way from the bottom like this, it will be much too
complex. The reason why this is possible is because computers are designed
with several extra layers of abstraction (on top of the basic mathematical
model of all the low-level circuitry), so that the model simplifies at each
stage. (This is in principle provable within a formal system, in fact
that's basically what formal verification is about.)

This is all totally down-to-earth stuff as far as I can tell. Abstraction
is such a useful concept that it's hard to avoid the term, but there is no
need to assume the (ultrafinitist) "existence" of these mathematical
models. A specification is a relationship between a physical object and a
description of "correct" behavior that constitutes a sort of "idealized
machine". By performing local testing, we can ensure that individual
components meet the specification, and on the other side the idealized
machines have perfect composition properties, which makes them amenable to
mathematical study.

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