I think you're reading too much into what I'm saying. I'm not suggesting that second order arithmetic is useful as a mathematical framework to talk about reasoning, in the way that first-order logic can. I'm saying that second order arithmetic is a useful way to talk about what makes the natural numbers special.
I'm also not suggesting that second order arithmetic has anything deep to add relative to a naïve (but sufficiently abstract) understanding of induction, but given that many people don't have a sufficiently abstract understanding of induction, I think it usefully illustrates just how broadly induction has to be understood. (To be clear, I'm also not suggesting that second order arithmetic is the one true way to think about the natural numbers, only that it's a useful perspective.)
Consider a non-logician mathematician to whom the induction principle is not primarily a formal statement to be analyzed, but just, well, induction, a basic working tool. Given a large proof as you describe, ending in an application of induction. What would be the benefit, to the mathematician, of viewing that application as happening in second-order logic, as opposed to first-order set theory? Why would they want to use second-order anything?
I'm not claiming there is any such benefit. This is the wrong question to ask; neither Eliezer's original post nor my comment were written for an audience of mathematicians concerned with the optimal way to do mathematics in practice.
Let G be the arithmetical statement expressing the consistency of ZFC. There are models of set theory in which G is true, and models in which G is false. Are you saying that second-order arithmetic gives us a better way, a less ambiguous way, to study the truth of G?
No, I am not saying that.
The way I see it, different models of set theory agree on what natural numbers are, but disagree on what subsets of natural numbers exist.
If there are models where G is true and models where G is false then different models of set theory don't agree on what natural numbers are.
This ambiguity is not resolved by second-order arithmetic; rather, it's swept under the carpet. The "unique" model "pinpointed" by it is utterly at the mercy of the same ambiguity of what the set of subsets of N is, and the ambiguity reasserts itself the moment you start studying the semantics of second-order arithmetic which you will do through model theory, expressed within set theory. So what is it that you have gained?
No, the ambiguity is not resolved by second-order arithmetic. The ambiguity is not resolved by anything, so that doesn't seem like a very useful objection.
Also, note that I didn't refer to either a unique model nor to pinpointing. (I'm aware that Eliezer did, but you're replying to me.) What I said was: "[S]econd order arithmetic gives us a universal way of picking the natural numbers out in any situation. Different models of set theory may end up disagreeing about what's true in the natural numbers, but second order arithmetic is a consistent way of identifying the notion in that model of set theory which lines up with our intuitions for the what the natural numbers are"
I think this critique undervalues the insight second order arithmetic gives for understanding the natural numbers.
If what you wanted from logic was a complete, self-contained account of mathematical reasoning then second order arithmetic is a punt: it purports to describe a set of rules for describing the natural numbers, and then in the middle says "Just fill in whatever you want here, and then go on". Landsburg worries that, as a consequence, we haven't gotten anywhere (or, worse, have started behind where we started, since no we need an account of "properties" in order to have an account of natural numbers).
But, thanks to Gödel, we know that a self-contained account of reasoning is impossible. Landsburg's answer is to give up on reasoning: the natural numbers are just there, and we have an intuitive grasp of them. This is, obviously, even more of a punt, and the second order arithmetic approach actually tells us something useful about the concept of the natural numbers.
Suppose someone produces a proof of a theorem about the natural numbers---let's say, for specificity, they prove the twin primes conjecture (that there are infinitely many twin primes). This proof proceeds in the following fashion: by extensive use of the most elaborate abstract math you can think of---large cardinals and sheafs and anabelian geometry and whatnot---the person proves the existence of a set of natural numbers P such that 1) 0 is in P, 2) if x is in P then x+1 is in P, and 3) if x is in P then there are twin primes greater than x.
Second order arithmetic says that this property P must extend all the way through the natural numbers, and therefore must itself be the natural numbers, and so we could conclude the twin primes conjecture.
The rest of this proof is really complicated, and uses things you might not think are valid, so you might not buy it. But second order arithmetic demands that if you believe the rest of the proof, you should also agree that the twin primes conjecture holds. This is actually worth something: it says that if you and I agree about all the fancy abstract stuff, we also have to agree about the natural numbers. And that's the most we can ask for.
To phrase this differently, second order arithmetic gives us a universal way of picking the natural numbers out in any situation. Different models of set theory may end up disagreeing about what's true in the natural numbers, but second order arithmetic is a consistent way of identifying the notion in that model of set theory which lines up with our intuitions for the what the natural numbers are. That's a very different account than the one offered by first order logic, but it's a valuable one in its own right.
One more phrasing, just for thoroughness. Landsburg passes off an account of the natural numbers to Platonism: we just intuit the natural numbers. But suppose you and I both purport to have good intuitions of the natural numbers, but we seem to disagree about some property. So we sit down to hash this out; it might turn out that we have some disagreement about what constitutes valid mathematical reasoning, in which case we may be stuck. But if not---if we agree on the reasoning---then eventually the disagreement will boil down to something like this:
You: "And since 0 is turquoise and, whenever x is turquoise, x+1 is also turquoise, all the natural numbers are turquoise."
Me: "Wait, those aren't all the natural numbers. Those are just the small natural numbers."
You: "What? What are the small natural numbers?"
Me: "You know, the initial segment of the natural numbers closed under the property of being turquoise."
You: "There's an initial segment of the natural numbers which includes 0, is closed under adding 1, but isn't every natural number?"
Me: "Sure. The small natural numbers. Haven't you heard of them?"
You: "Wait, are there any initial segments of the small natural numbers which include 0 and are closed under adding 1?"
Me: "Sure. The tiny natural numbers, for starters."
You: "Look, you're using the word 'natural numbers' wrong. It means..." and then you explain the second order induction axiom. So apparently whatever I thought was the natural numbers was some other bizzarre object; what the second order induction axiom does for a Platonist is pin down which Platonic object we're actually talking about.
I'm a fan of Enderton's "A Mathematical Introduction to Logic". It's short and very precisely written, which can make it a little difficult to learn from on its own, but together with a general familiarity with the subject and using wikipedia for additional examples elaboration, it should be perfect.
Perhaps LessWrong is a place where I can say "Your question is wrong" without causing unintended offense. (And none is intended.)
Yes, for ω-consistency to even be defined for a theory it must interpret the language of arithmetic. This is a necessary precondition for the statement you quoted, and does not contradict it.
Work in PA, and take a family of statements P(n) where each P(n) is true but independent of PA, and not overly simple statements themselves---say, P(n) is "the function epsilon n in the fast growing hierarchy is a total function". (The important thing here is that the statement is at least Pi2---true pure existence statements are always provable, and if the statements were universal there would be a different ω-consistency problem. The exact statement isn't so important, but not that these statements are true, but not provable in PA.)
Now consider the statement T="there is an n such that P(n) is false". PA+T has no standard model (because T is false), but PA+T doesn't prove any of the P(n), let alone all of them, so there's no ω-consistency problem.
ω-inconsistency isn't exactly the same thing as being false in the standard model. Being ω-inconsistent requires both that the theory prove all the statements P(n) for standard natural numbers n, but also prove that there is an n for which P(n) fails. Therefore a theory could be ω-consistent because it fails to prove P(n), even though P(n) is true in the standard model. So even if we could check ω-consistency, we could take PA, add an axiom T, and end up with an ω-consistent theory which nonetheless is not true in the standard model.
By the way, there are some papers on models for adding random (true) axioms to PA. "Are Random Axioms Useful?" involves some fairly specific cases, but shows that in those situations, random axioms generally aren't likely to tell you anything you wanted to know.
Everyone seems to be taking the phrase "human Gödel sentence" (and, for that matter, "the Gödel sentence of a turing machine") as if its widely understood, so perhaps it's a piece of jargon I'm not familiar with. I know what the Gödel sentence of a computably enumerable theory is, which is the usual formulation. And I know how to get from a computably enumerable theory to the Turing machine which outputs the statements of that theory. But not every Turing machine is of this form, so I don't know what it means to talk about the Gödel sentence of an arbitrary Turing machine. For instance, what is the Gödel sentence of a universal Turing machine?
Some posters seem to be taking the human Gödel number to mean something like the Gödel number of the collection of things that person will ever believe, but the collection of things a person will ever believe has absolutely no need to be consistent, since people can (and should!) sometimes change their mind.
(This is primarily an issue with the original anti-AI argument; I don't know how defenders of that argument clarify their definitions.)
Took the survey. I just missed last year's, so I was glad to get to participate this year.