I suppose you can’t prove a statement like “No matter how many times you expand this infinite family of axioms, you’ll never encounter a non-standard number” in first-order logic? Should I not think of numbers and non-standard numbers as having different types? Or should I think of > as accepting differently typed things? (where I’m using the definition of “type” from computer science, e.g. “strongly-typed language”)
Sorry I didn’t answer this before; I didn’t see it. To the extent that the analogy applies, you should think of non-standard numbers and standard numbers as having the same type. Specifically, the type of things that are being quantified over in whatever first order logic you are using. And you’re right that you can’t prove that statement in first order logic; Worse, you can’t even say it in first order logic (see the next post, on Godel’s theorems and Compactness/Lowenheim Skolem for why).
Thanks. Hm. I think I see why that can’t be said in first order logic.
...my brain is shouting “if I start at 0 and count up I’ll never reach a nonstandard number, therefore they don’t exist” at me so loudly that it’s very difficult to restrict my thoughts to only first-order ones.
This is largely a matter of keeping track of the distinction between “first order logic: the mathematical construct” and “first order logic: the form of reasoning I sometimes use when thinking about math”. The former is an idealized model of the latter, but they are distinct and belong in distinct mental buckets.
It may help to write a proof checker for first order logic. Or alternatively, if you are able to read higher math, study some mathematical logic/model theory.
Thanks!
I suppose you can’t prove a statement like “No matter how many times you expand this infinite family of axioms, you’ll never encounter a non-standard number” in first-order logic? Should I not think of numbers and non-standard numbers as having different types? Or should I think of > as accepting differently typed things? (where I’m using the definition of “type” from computer science, e.g. “strongly-typed language”)
Sorry I didn’t answer this before; I didn’t see it. To the extent that the analogy applies, you should think of non-standard numbers and standard numbers as having the same type. Specifically, the type of things that are being quantified over in whatever first order logic you are using. And you’re right that you can’t prove that statement in first order logic; Worse, you can’t even say it in first order logic (see the next post, on Godel’s theorems and Compactness/Lowenheim Skolem for why).
Thanks. Hm. I think I see why that can’t be said in first order logic.
...my brain is shouting “if I start at 0 and count up I’ll never reach a nonstandard number, therefore they don’t exist” at me so loudly that it’s very difficult to restrict my thoughts to only first-order ones.
This is largely a matter of keeping track of the distinction between “first order logic: the mathematical construct” and “first order logic: the form of reasoning I sometimes use when thinking about math”. The former is an idealized model of the latter, but they are distinct and belong in distinct mental buckets.
It may help to write a proof checker for first order logic. Or alternatively, if you are able to read higher math, study some mathematical logic/model theory.