[FOM] The unreasonable soundness of mathematics
Timothy Y. Chow
tchow at alum.mit.edu
Sun May 1 14:33:22 EDT 2016
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.
Tim
More information about the FOM
mailing list