Comment author: elseif 12 November 2012 10:33:50PM *  0 points [-]

ω-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.

Comment author: Incorrect 13 November 2012 01:42:55AM 0 points [-]

Therefore a theory could be ω-consistent because it fails to prove P(n), even though P(n) is true in the standard model.

I thought for ω-consistency to even be defined for a theory it must interpret the language of arithmetic?

Comment author: Incorrect 12 November 2012 08:00:53PM *  0 points [-]

Just use the axiom schema of induction instead of the second order axiom of induction and you will be able to produce theorems though.

But you wont be able to produce all true statements in SOL PA, that is, PA with the standard model, because of the incompleteness theorems. To be able to prove a larger subset of such statements, you would have to add new axioms to PA. If adding an axiom T to PA does not prevent the standard model from being a model of PA+T, that is it does not prove any statements that require the existence of nonstandard numbers, then PA+T is ω-consistent.

So, why can't we just keep adding axioms T to PA, check whether PA+T is ω-consistent, and have a more powerful theory? Because we can't in general determine whether a theory is ω-consistent.

Perhaps a probabilistic approach would be more effective. Anyone want to come up with a theory of logical uncertainty for us?

Gap in understanding of Logical Pinpointing

6 Incorrect 12 November 2012 05:33PM

I had originally found myself very confused by how the second order axiom of induction restricted PA to a single model, leading to this discussion where I thought doing so would violate the incompleteness theorem.

What I misunderstood is that while the axiom schema of induction effectively quantifies over properties definable in PA, the SOL version quantifies over ALL properties, including those you can't even define in PA.

This seems like a really subtle point that wasn't obvious to me from the article, knowing FOL but not SOL. I actually realized my mistake when I saw that Eliezer was representing properties as sets in the visual diagram.

Anyway, I thought others might benefit by learning from my mistake. Also, I'd like to point out that this definition of the natural numbers yields no procedure that lets you produce theorems of PA as second-order logic has no computable complete definition of provability. Just use the axiom schema of induction instead of the second order axiom of induction and you will be able to produce theorems though.

Comments (13)
Comment author: Eugine_Nier 04 November 2012 03:18:08AM 0 points [-]

What's wrong with second order resolution?

Comment author: Incorrect 04 November 2012 04:56:55AM *  0 points [-]

There's no complete deductive system for second-order logic.

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.

Comment author: Eugine_Nier 03 November 2012 11:03:28PM 1 point [-]

But the axiom schema of induction does not completely exclude

Eliezer isn't using an axiom schema, he's using an axiom of second order logic.

Comment author: Incorrect 03 November 2012 11:57:49PM *  1 point [-]

I don't see what the difference is... They look very similar to me.

At some point you have to translate it into a (possibly infinite) set of first-order axioms or you wont be able to perform first-order resolution anyway.

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: Viliam_Bur 03 November 2012 05:49:09PM *  1 point [-]

Not sure if I understand the point of your argument.

Are you saying that in reality every property P has actually three outcomes: true, false, undecidable? And that those always decidable, like e.g. "P(n) <-> (n = 2)" cannot be true for all natural numbers, while those which can be true for all natural numbers, but mostly false otherwise, are always undecidable for... some other values?

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? I do not believe this is possible but I may be mistaken.

I don't know.

Let's suppose that for any specific value V in the separated chain it is possible to make such property PV. For example "PV(x) <-> (x <> V)". And let's suppose that it is not possible to make one such property for all values in all separated chains, except by saying something like "P(x) <-> there is no such PV which would be true for all numbers in the first chain and false for x".

What would that prove? Would it contradict the article? How specifically?

Comment author: Incorrect 03 November 2012 06:29:50PM 1 point [-]

Are you saying that in reality every property P has actually three outcomes: true, false, undecidable?

By Godel's incompleteness theorem yes, unless your theory of arithmetic has a non-recursively enumerable set of axioms or is inconsistent.

And that those always decidable, like e.g. "P(n) <-> (n = 2)" cannot be true for all natural numbers, while those which can be true for all natural numbers, but mostly false otherwise, are always undecidable for... some other values?

I'm having trouble understanding this sentence but I think I know what you are asking about.

There are some properties P(x) which are true for every x in the 0 chain, however, Peano Arithmetic does not include all these P(x) as theorems. If PA doesn't include P(x) as a theorem, then it is independent of PA whether there exist nonstandard elements for which P(x) is false.

Let's suppose that for any specific value V in the separated chain it is possible to make such property PV. What would that prove? Would it contradict the article? How specifically?

I think this is what I am saying I believe to be impossible. You can't just say "V is in the separated chain". V is a constant symbol. The model can assign constants to whatever object in the domain of discourse it wants to unless you add axioms forbidding it.

Honestly I am becoming confused. I'm going to take a break and think about all this for a bit.

Comment author: Incorrect 03 November 2012 05:14:16PM 1 point [-]

Could someone please confirm my statements in the new sequence post about first-order logic? I want to be sure my understanding is correct.

http://lesswrong.com/lw/f4e/logical_pinpointing/7qv6?context=1#7qv6

In response to Logical Pinpointing
Comment author: Incorrect 03 November 2012 09:34:29AM *  2 points [-]

"Because if you had another separated chain, you could have a property P that was true all along the 0-chain, but false along the separated chain. And then P would be true of 0, true of the successor of any number of which it was true, and not true of all numbers."

But the axiom schema of induction does not completely exclude nonstandard numbers. Sure if I prove some property P for P(0) and for all n, P(n) => P(n+1) then for all n, P(n); then I have excluded the possibility of some nonstandard number "n" for which not P(n) but there are some properties which cannot be proved true or false in Peano Arithmetic and therefore whose truth hood can be altered by the presence of nonstandard numbers.

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? I do not believe this is possible but I may be mistaken.

Comment author: Incorrect 03 November 2012 09:59:14AM *  1 point [-]

If our axiom set T is independent of a property P about numbers then by definition there is nothing inconsistent about the theory T1 = "T and P" and also nothing inconsistent about the theory T2= "T and not P".

To say that they are not inconsistent is to say that they are satisfiable, that they have possible models. As T1 and T2 are inconsistent with each other, their models are different.

The single zero-based chain of numbers without nonstandard numbers is a single model. Therefore, if there exists a property about numbers that is independent of any theory of arithmetic, that theory of arithmetic does not logically exclude the possibility of nonstandard elements.

By Godel's incompleteness theorems, a theory must have statements that are independent from it unless it is either inconsistent or has a non-recursively-enumerable theorem set.

Each instance of the axiom schema of induction can be constructed from a property. The set of properties is recursively enumerable, therefore the set of instances of the axiom schema of induction is recursively enumerable.

Every theorem of Peano Arithmetic must use a finite number of axioms in its proof. We can enumerate the theorems of Peano Arithmetic by adding increasingly larger subsets of the infinite set of instances of the axiom schema of induction to our axiom set.

Since the theory of Peano Arithmetic has a recursively enumerable set of theorems it is either inconsistent or is independent of some property and thus allows for the existence of nonstandard elements.

View more: Prev | Next

Powered by Reddit Powered by Reddit