[FOM] The unreasonable soundness of mathematics

[Timothy Y. Chow]

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