TorqueDrifter comments on Logical Pinpointing - Less Wrong

62 Post author: Eliezer_Yudkowsky 02 November 2012 03:33PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Article Navigation

Comments (338)
Tags: seq_epistemology meaning numbers logic proofs math

Comments (338)

You are viewing a single comment's thread. Show more comments above.

Comment author: TorqueDrifter 03 November 2012 06:39:01PM 0 points [-]

Can you give me a property P which is true along the zero-chain but necessarily false along a separated chain that is infinitely long in both directions?

Pn(x) is "x is the nth successor of 0" (the 0th successor of a number is itself). P(x) is "there exists some n such that Pn(x)".

Comment author: Incorrect 03 November 2012 11:08:38PM *  1 point [-]

I don't see how you would define Pn(x) in the language of PA.

Let's say we used something like this:

Pn(x) iff ((0 + n) = x)

Let's look at the definition of +, a function symbol that our model is allowed to define:

a + 0 = a
a + S(b) = S(a + b)

"x + 0 = x" should work perfectly fine for nonstandard numbers.

So going back to P(x):

"there exists some n such that ((0 + n) = x)"

for a nonstandard number x, does there exist some number n such that ((0+n) = x)? Yup, the nonstandard number x! Set n=x.

Oh, but when you said nth successor you meant n had to be standard? Well, that's the whole problem isn't it!

Comment author: TorqueDrifter 04 November 2012 12:08:08AM 0 points [-]

But any nonstandard number is not an nth successor of 0 for any n, even nonstandard n (whatever that would mean). So your rephrasing doesn't mean the same thing, intuitively - P is, intuitively, "x is reachable from 0 using the successor function".

Couldn't you say:

  • P0: x = 0
  • PS0: x = S0
  • PSS0: x = SS0

and so on, defining a set of properties (we can construct these inductively, and so there is no Pn for nonstandard n), and say P(x) is "x satisfies one such property"?

Comment author: Incorrect 04 November 2012 01:17:30AM 2 points [-]

An infinite number of axioms like in an axiom schema doesn't really hurt anything, but you can't have infinitely long single axioms.

∀x((x = 0) ∨ (x = S0) ∨ (x = SS0) ∨ (x = SSS0) ∨ ...)

is not an option. And neither is the axiom set

P0(x) iff x = 0
PS0(x) iff x = S0
PSS0(x) iff x = SS0
...
∀x(P0(x) ∨ PS0(x) ∨ PS0(x) ∨ PS0(x) ∨ ...)

We could instead try the axioms

P(0, x) iff x = 0
P(S0, x) iff x = S0
P(SS0, x) iff x = SS0
...
∀x(∃n(P(n, x)))

but then again we have the problem of n being a nonstandard number.

Powered by Reddit Powered by Reddit