Because then the problem is not "Does this non-axiomatized stuff obey that theorem ?" but "Does that theorem follow from these axioms ?". One is a pure logic problem, and proofs may be checked by automated proof-checkers. The other directly or indirectly relies on the mathematician's intuition of the non-axiomatized subject in question, and can't be checked by automated proof-checkers.

Except insofar as the mathematicians, unknown to each other, have different ideas of what constitutes a valid rule of inference.

A logical system is a... (read more)

Also, of course, to put this in the context of the original post, if we're talking about second order logic, then of course there can be no automated proof-checkers.

You appear to be confused here. The rest of your post is good.

1jsalvatier7yDo you mean that there can be no automated proof-checkers which are sound and complete (and terminating)? Surely there can be useful sound checkers (which terminate)? The existence of Coq [] and other Dependently typed languages suggests that's true.

[LINK] Steven Landsburg "Accounting for Numbers" - response to EY's "Logical Pinpointing"

by David_Gerard 1 min read14th Nov 201247 comments


"I started to post a comment, but it got long enough that I’ve turned my comment into a blog post."

So the study of second-order consequences is not logic at all; to tease out all the second-order consequences of your second-order axioms, you need to confront not just the forms of sentences but their meanings. In other words, you have to understand meanings before you can carry out the operation of inference. But Yudkowsky is trying to derive meaning from the operation of inference, which won’t work because in second-order logic, meaning comes first.

... it’s important to recognize that Yudkowsky has “solved” the problem of accounting for numbers only by reducing it to the problem of accounting for sets — except that he hasn’t even done that, because his reduction relies on pretending that second order logic is logic.