[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 


More information about the FOM mailing list