6

The premises of the S5 system are:

□p → □□ p
◊p → □ ◊ p

(Note that □ is an actual square, not the missing-symbol placeholder).

What does the first one mean? If □p is what is necessary in all accessible worlds, how is there any difference between it and □□ p? Does the latter mean that p is necessary in all (accessible and not accessible) possible worlds?

Improve this question
10
  • 8
    On my machine I'm seeing empty boxes in place of the symbols. Could someone edit it with proper unicode characters, please?
    – Ted Wrigley
    Mar 11, 2020 at 18:03
  • 6
    @lemontree: Well that's just a dumb system of notation!
    – Ted Wrigley
    Mar 11, 2020 at 21:03
  • 11
    For anyone wondering if this is a rendering issue: the symbol is an actual box: fileformat.info/info/unicode/char/25a1/index.htm
    – user13267
    Mar 12, 2020 at 5:49
  • 8
    As absurd as this sounds, I suggest it might be worth including an image file repeating the notation simply because the immediate reaction of everyone has been "I'm getting the 'unknown character' placeholder".
    – chrylis -cautiouslyoptimistic-
    Mar 12, 2020 at 6:36
  • 5
    What the bl□□dy h□ll is happening to my computer?
    – Andrew Grimm
    Mar 12, 2020 at 11:08

2 Answers 2

Reset to default
13

In general □□ p and □ p are very different. Thinking in terms of Kripke frames, they only obviously coincide if the accessibility relation is transitive. This is true for Kripke frames validating S5, but not in general.

  • Consider a frame with three worlds a,b,c where a sees b and b sees c but a doesn't see c: then given a valuation making p true at b but false at a and c, world a satisfies ~p, □p, and ~□□p.

There are also important examples outside of the context of Kripke frames, provability logic being a huge example. In general, a theory can prove that it proves something without actually proving that thing: e.g. by Godel's incompleteness theorem, the theory T=ZFC+"ZFC is inconsistent" is consistent and hence does not prove 0=1 but it does prove that it proves 0=1. Interpreting "□" as "proves," we get that □□ p and □ p are not equivalent in the sense of T (the issue being that T is not Sigma1-sound). Indeed, Lob's theorem - which in provability logic is the scheme □(□p→p)→□p - is a very important example of this non-collapse even in the context of "nice" theories like ZFC.

Improve this answer
4
  • 2
    +1. A proper answer - I can (&should & will) delete my comment. Many thanks. Best - GLT
    – Geoffrey Thomas ♦
    Mar 11, 2020 at 20:24
  • Thank u for your detail answer! So does in S5 that accessibility is transitive We know that □□ p and □ p coincides. But are there have in this special case different meaning too? the latte r means it is true in all worlds that is true that p ? in the other word as Eliran said in the second answer □ p is about the notion of p and for example a 2+2=4 and □□ p about our knowledge of it as a necessary? is there such different? the first is about the worlds directly the second about our knowledge of worlds in a deeper case? @geoffrey-thomas
    – MHghasemi
    Mar 12, 2020 at 3:31
  • @MHghasemi Yes, a priori they mean different things: in the context of Kripke frames, "□p" means "In every accessible world, p is true" while "□□p" means "In every accessible world, □p is true" - or "p is true in every world accessible from an accessible world." We often think of accessibility as a kind of "plausibility:" world w is accessible from world u if, from u's perspective, w (while not actually the state of things as they are) is plausible. In some modal systems - like S5 - we happen to have that □p and □□p are equivalent in the sense of always being true in the same worlds.
    – Noah Schweber
    Mar 12, 2020 at 12:52
  • 1
    Now your interpretation of □□p as being about our knowledge of p's necessity is a bit flawed: you're mixing two interpretations of "□," namely "is known" and "is necessary." We need to stick with one interpretation (or work with a bi- or poly-modal logic): in this case, either "known knowns vs. mere knowns" or "necessary necessities vs. mere necessities" (or some other thing).
    – Noah Schweber
    Mar 12, 2020 at 12:54
6

To add to the existing answer, there's also epistemic logic, where □ is interpreted as knowledge (relative to a given subject).

Possible worlds in such a system are worlds that are consistent with the subject's current information. Since necessity is truth in all possible worlds, it means in epistemic logic that if something is necessary then it just follows from your information (its negation is inconsistent with your information). At least in an idealized sense, necessity is knowledge.

"□p" in epistemic logic means that you know that p, and "□□p" means that you know that you know that p. The two are not the same. For instance, if p is the statement that it's raining, then by knowing p you know something about the weather, but by knowing that you know p you know something about yourself. It's not obvious whether □□p follows from □p. The claim that it does is controversial in epistemology and is known as the KK principle.

Improve this answer
2
  • Thank you for actually explaining what the square means.
    – curiousdannii
    Mar 12, 2020 at 2:25
  • Thank u for y detail answer! So does in S5 that accessibility is transitive We know that □□ p and □ p coincides. But are there have in this special case different meaning too? the latter means it is true in all worlds that is true that p ? in the other word just as u said like epestimic logic we casn say □ p is about the notion of p and for example a 2+2=4 and □□ p about our knowledge of it as a necessary? is there such different? the first is about the worlds directly but the second about our knowledge of worlds in a deeper case? ( I accept.this latter is a part of these worlds too yet)
    – MHghasemi
    Mar 12, 2020 at 3:36

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .