Philosophy Asked by Nick Doe on January 4, 2022

KW is defined as K + the axiom W:

□(□p→p)→□p. It is said to be valid on all finite transitive and irreflexive frames. Another way to interpret my question is, what exactly does finite mean here? Let’s try to falsify this axiom without the finite restriction.

```
1. □(□p→p) ∧ ¬□p in w0
2. □(□p→p) ∧ ◇¬p in w0
3. ¬p ∧ □p→p in w1
4. ¬p ∧ ¬p→¬□p in w1
5. ¬p ∧ ¬□p in w1
6. ¬p ∧ ◇¬p in w1
7. ¬p in w2
```

So if the frames were only transitive and irefflexive, this would serve as a countermodel for KW. So we must arrive to a contradiction through this property of being finite, or else W is falsifiable. How exactly does that happen?

Now I have “a hunch” as to why this could happen, and will only include it as a guess. Let’s take a frame {W,R} in which W only has w0, w1 and w2, where no frame can see itself and we have transitivity, i.e, w0Rw1, w1Rw2, then w0Rw2. From □(□p→p) we get □(¬□p ∨ p), so by applying K9 we get □¬□p ∨ ◇p, i.e ¬◇p→□◇¬p, i.e □¬p→□◇¬p. Now, since ¬p belongs to every world that w0 can see, □¬p is a truth of w0, and by modus ponens, □◇¬p. By transitivity, w0Rw2 ◇¬p is a truth of w2 as well, so there must be a world w3 in which -p is true, which can’t be the case, since W only has w0,w1 and w2.

Let me try to show that □(□p→p)→□p is true in all models given a frame {W,R} where W is {w0,w1,w2} and R is transitive and irreflexive:

```
w1: p is false
w2: p is false
Since p is false in w1, □p is false in w0.
Since p is false in w2, □p is false in w1. Therefore, □p→p is true in w1 by PC.
Since w2 does not see any worlds, □p is true at w2. □p→p is false at w2.
Since (□p→p) is not true in all worlds that w0 sees, □(□p→p) is false at w0. Since □p is false as well, □(□p→p)→□p is true in w0.
Since (□p→p) is not true in all worlds that w1 sees, □(□p→p) is false at w1. Since □p is false as well, □(□p→p)→□p is true in w1.
Since w2 does not see any worlds, both □(□p→p) and □p are true, so □(□p→p)→□p is true in w2.
w1: p is true
w2: p is false
Since p is false in w2, □p is false in w0, because w0 sees w2 due to transitivity.
Since p is false in w2, □p is false in w1. Therefore, □p→p is true in w1 by PC.
Since w2 does not see any worlds, □p is true at w2. □p→p is false at w2.
Since (□p→p) is not true in all worlds that w0 sees, □(□p→p) is false at w0. Since □p is false as well, □(□p→p)→□p is true in w0.
Since (□p→p) is not true in all worlds that w1 sees, □(□p→p) is false at w1. Since □p is false as well, □(□p→p)→□p is true in w1.
Since w2 does not see any worlds, both □(□p→p) and □p are true, so □(□p→p)→□p is true in w2.
w1: p is false
w2: p is true
Since p is false in w1, □p is false in w0.
Since p is true in w2, □p is true in w1. Therefore, □p→p is false in w1.
Since w2 does not see any worlds, □p is true at w2. □p→p is true at w2.
Since (□p→p) is not true in all worlds that w0 sees, □(□p→p) is false at w0. Since □p is false as well, □(□p→p)→□p is true in w0.
Since (□p→p) is true in all worlds that w1 sees, □(□p→p) is true at w1. Since □p is true as well, □(□p→p)→□p is true in w1.
Since w2 does not see any worlds, both □(□p→p) and □p are true, so □(□p→p)→□p is true in w2.
w1: p is true
w2: p is true
Since p is true in w1 and w2, □p is true in w0.
Since p is true in w2, □p is true in w1. Therefore, □p→p is true in w1.
Since w2 does not see any worlds, □p is true at w2. □p→p is true at w2.
Since (□p→p) is true in all worlds that w0 sees, □(□p→p) is true at w0. Since □p is true as well, □(□p→p)→□p is true in w0.
Since (□p→p) is true in all worlds that w1 sees, □(□p→p) is true at w1. Since □p is true as well, □(□p→p)→□p is true in w1.
Since w2 does not see any worlds, both □(□p→p) and □p are true, so □(□p→p)→□p is true in w2.
```

Therefore, given a frame {W,R} where W is {w0, w1, w2}, R is transitive and irreflexive and R: {w0Rw1, w1Rw2, w0Rw2}, □(□p→p)→□p is valid on that frame. That’s my hunch about what “finite” could mean, but I would really like to hear a proper answer.

A viewpoint I would suggest as a way to intuitively internalise the frame properties of **KW** system is to notice that it is equivalent to Gödel-Löb provability logic (**GL**), and necessity is conceptually a correlate of provability.

**GL** has several interpretations, in particular, arithmetical and computational. Besides, we may visualise it as realising our general notion of (formal) proof and the conditions on the accessibility relation **R** are fixed accordingly.

We can take '**p** is true' as '**p** is true *simpliciter*' and '**□p** is true' as '**p** is *provably* true' in a proof system **S**, coincidence of which cannot be assumed. Then, accessibility among nodes (possible worlds) turns out to be possibility of transitions among proof states presenting truth *simpliciter* and *provable* truth (with respect to **S**). Hence the frame properties:

A statement is required to not invoke itself as a justification of itself. That is, the proof states have to be connected non-reflexively, otherwise

*petitio principii*would follow.Obviously, the proof states (or steps) must be connected in a transitive fashion.

A proof must comprise finite number of states (like algorithm steps) to be admissible. The chain of states must end at some node, namely, it has to be well-capped (converse well-founded).

Answered by Tankut Beygu on January 4, 2022

Get help from others!

Recent Answers

- Peter Machado on Why fry rice before boiling?
- Jon Church on Why fry rice before boiling?
- haakon.io on Why fry rice before boiling?
- Joshua Engel on Why fry rice before boiling?
- Lex on Does Google Analytics track 404 page responses as valid page views?

Recent Questions

- How can I transform graph image into a tikzpicture LaTeX code?
- How Do I Get The Ifruit App Off Of Gta 5 / Grand Theft Auto 5
- Iv’e designed a space elevator using a series of lasers. do you know anybody i could submit the designs too that could manufacture the concept and put it to use
- Need help finding a book. Female OP protagonist, magic
- Why is the WWF pending games (“Your turn”) area replaced w/ a column of “Bonus & Reward”gift boxes?

© 2024 TransWikia.com. All rights reserved. Sites we Love: PCI Database, UKBizDB, Menu Kuliner, Sharing RPP