Comments on A Neighborhood of Infinity: Generalising Gödel's Theorem with Multiple Worlds....

Godel's theorems are based on a correspondence...

2011-01-20T09:20:00.580-08:00

Godel's theorems are based on a correspondence between the meta mathematical act of proving in a theory (the actual manipulation of symbols ) and the behavior of some objects within the theory itself . Only without a clear distinction between those two can P(P(x)-> x) ->P(x) seem weird .

byorgey, A good example of this is the fact that ...

2011-01-07T14:54:55.839-08:00

byorgey,

A good example of this is the fact that if arithmetic is consistent then we can't prove the consistency of arithmetic. In other words, if a world contains ◊⊤ then the subworlds must contain the negation. I gave the rules for what propositions are inherited from a parent world but maybe I should also have pointed out that nothing else is inherited, so the child can contradict the parent.

It took me a long time to understand the solution ...

2011-01-07T12:39:23.356-08:00

It took me a long time to understand the solution to exercise 1. Finally it dawned on me that it is NOT a contradiction to have p in one world and not(p) in one of its subworlds! It makes sense in retrospect but wasn't obvious to me at first.

You might be interested in
Common sense for concurrency and inconsistency robustness using Direct Logic(TM) and the Actor Model on how to do this in a more powerful way without modal operators.

◻(◻p →p) →◻p Flip the direction of the arrow: ¬◻...

2010-12-17T21:31:31.072-08:00

◻(◻p →p) →◻p

Flip the direction of the arrow:

¬◻p→¬◻(◻p →p)

Definition of ◊:
◊¬p→◊¬(◻p →p)

◊¬p→◊(◻p∧ ¬p)

◊p→◊(◻¬p∧ p)

Löb's theorem holds for any p. So it also holds for ¬p. Giving:

◊p→◊(¬◊p∧ p)

Great post! I don't understand how you infer &...

2010-12-17T19:46:04.531-08:00

Great post! I don't understand how you infer "◊p →◊(p ∧¬◊p)" from "◻(◻p →p) →◻p". The closest I seem to be able to get is "¬◻p → ◊(◻p ∧ ¬p)". Are there some rules I'm missing?

@anonymous, The first thing to note is that ◊p sa...

2010-12-14T19:15:46.542-08:00

@anonymous,

The first thing to note is that ◊p says that p is consistent with arithmetic which implicitly implies arithmetic is consistent. So ◊p implies the consistency of arithmetic. So it's a pretty strong claim.

I think ex1 is invalid since it would break Godel&...

2010-12-14T16:30:32.751-08:00

I think ex1 is invalid since it would break Godel's theorem with p=◊⊤. Then I prooved that ex2,ex3 and ex4 are valid with your "subworlds" method but I'm suspicious because I can also proove this way that
◊p →◊(◻(◊q))
for any p and q (I found ¬◻(◊q) and ◻(◊q) in the same subworld thus the contradiction).
What to think about that ?

Great post. Looking forward to the implementation....

2010-12-13T22:31:31.723-08:00

Great post. Looking forward to the implementation.

@mjd And I read elsewhere that Smullyan made expli...

2010-12-12T10:57:54.295-08:00

@mjd And I read elsewhere that Smullyan made explicit something implicit in Beth. I've no idea as I've not seen Beth's work.

BTW These tableau are not analytic because of the Lob rule.

Wikipedia doesn't give a cite, but it attribut...

2010-12-12T09:52:42.882-08:00

Wikipedia doesn't give a cite, but it attributes the method of analytic tableaux to Beth, who predates Smullyan.

Brian, Let me expand on that. The worlds I've...

2010-12-12T08:10:00.578-08:00

Brian,

Let me expand on that. The worlds I've been talking about are the worlds of what is *provable* rather than worlds of what is *true*.

So it may seem weird that it's possible to have a world in which we have p and ◻¬p. But what this means is that we can't *prove* that there is a contradiction between them even though it seems obviously *true* that they can't both hold.

Doesn't help that at one point I said *true* instead of *provable* in the article. I've fixed that now.

Brian, It would be a contradiction if we had ◻¬p→...

2010-12-12T06:53:19.926-08:00

Brian,

It would be a contradiction if we had ◻¬p→¬p, but as I mentioned, this can't be proved.

This is great stuff but I'm having a bit of tr...

2010-12-11T22:35:58.386-08:00

This is great stuff but I'm having a bit of trouble interpreting this world:

p
¬◊p

This expands to:
p
¬¬◻¬p

Which simplifies to:
p
◻¬p

Which seems to meant the p is both true and we can prove that it's false? Is this part of a proof by contradiction?

Luke, It's no worse than Godel's second i...

2010-12-11T21:48:54.425-08:00

Luke,

It's no worse than Godel's second incompleteness theorem. If, in PA, we can prove ◊⊤ then we conclude that ◊⊤ is false!

This sounds like a fascinating series! Right up m...

2010-12-11T20:25:48.812-08:00

This sounds like a fascinating series! Right up my alley.

My head is spinning around the second phrasing of Lob's theorem: ◊p →◊(p ∧¬◊p). If p is consistent then it's consistent that (p is true and there is a proof of ¬p)? That seems to violate the soundness theorem. I would like a bit more exploration of the meaning of this sentence.

I had a hunch that box might be an issue. It's...

2010-12-11T18:49:06.152-08:00

I had a hunch that box might be an issue. It's frustrating because in some browsers every other logical symbol is incorrectly displayed as a box! I'll see what I can do...

The unicode symbol you've used for "box&q...

2010-12-11T18:24:24.935-08:00

The unicode symbol you've used for "box" appears as a weird glitch throughout for me. Might I suggest replacing "box" throughout by K (which has the great bonus of standing for "know")?

To me, a fatal flaw with this multiple worlds system is that if K(p)->p is valid, then so is K(K(p)->p). In words, "every infallible knower knows his infallibility". I've actually got not one but two preprints right now exploring epistemology when it's possible for an infallible knower NOT to know his infallibility... of course this requires a totally different approach than the multiple worlds one. You can see the obvious connection to Godel's Incompleteness Theorem, though.

Of course that's peanuts considering Lob's Theorem... which is why K works so much better as a new modal operator rather than a predicate symbol :P