= 27d567bc2d48d9f40e9ccc20ea370b15)
Kindly comments on Logical Pinpointing - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (338)
I know that's what you're trying to say because I would like to be able to say that, too. But here's the problems we run into.
Try writing down "For all x, some number of subtract 1's cause it to equal 0". We can write the "∀x. ∃y. F(x,y) = 0" but in place of F(x,y) we want "y iterations of subtract 1's from x". This is not something we could write down in first-order logic.
We could write down sub(x,y,0) (in your notation) in place of F(x,y)=0 on the grounds that it ought to mean the same thing as "y iterations of subtract 1's from x cause it to equal 0". Unfortunately, it doesn't actually mean that because even in the model where pi is a number, the resulting axiom "∀x. ∃y. sub(x,y,0)" is true. If x=pi, we just set y=pi as well.
The best you can do is to add an infinitely long axiom "x=0 or x = S(0) or x = S(S(0)) or x = S(S(S(0))) or ..."
I think I'm starting to get it. That there is no property that a natural number could be defined as having, that a infinite chain couldn't also satisfy in theory.
That's really disappointing. I took a course on logic and the most inspiring moment was when the professor wrote down the axioms of peano arithmitic. They are more or less formalizations of all the stuff we learned about numbers in grade school. It was cool that you could just write down what you are talking about formally and use pure logic to prove any theorem with them. It's sad that it's so limited you can't even express numbers.