1

I want to prove this using only Necessitation Rule, Distribution Axiom and Reflexivity Axiom from modal logic (their combination is sometimes called modal system T).

As I can't conclude that ¬Lp ∨ Lp is equivalent to Lp → Lp, I have no idea how to proceed.

Improve this question
11
  • 1
    Everi tautology is provable in modal logic; thus use ¬α ∨ α.
    – Mauro ALLEGRANZA
    Commented Apr 4, 2017 at 16:59
  • 1
    And then I get L(¬p∨p) but I want to prove ¬Lp∨Lp
    – Akira
    Commented Apr 4, 2017 at 17:03
  • 1
    NO; α can be a formula whatever, also Lp.
    – Mauro ALLEGRANZA
    Commented Apr 4, 2017 at 20:00
  • 1
    Every tautology from propositional logic yes, but that is not the case in ¬Lp∨Lp. We are talking about a specific system here (T). We cannot simply replace α with Lp, in case that is what you meant. Guidance for the proof itself will be appreciated.
    – Akira
    Commented Apr 4, 2017 at 20:22
  • 1
    The system T is the one specified already in the OP: 'A basic modal logic M results from adding (M) to K. (Some authors call this system T.)' - SEP. According to the Necessitation Rule we may infer that L(¬p∨p), as consequence of ¬p∨p being a theorem. ¬Lp ∨ Lp will not follow immediately. Using the schema ¬α ∨ α will involve further assumptions I do not wish to include.
    – Akira
    Commented Apr 4, 2017 at 22:11

1 Answer 1

Reset to default
1

I think there is a point not enough clear in your question...

The most familiar logics in the modal family are constructed from a weak logic called K (after Saul Kripke). [...] A variety of different systems may be developed for such logics using K as a foundation. [...]

K results from adding the following to the principles of propositional logic [...] [emphasis added].

The last statement means that the axioms and rules (and meta-logical concepts) of propositional logic still apply, like e.g. modus ponens.

In particular, this means that in system K we can use the concept of propositional tautology as well as the "standard" completeness of the propositional part with regard to the truth functional semantics.

All this long premise to say that a formula ¬α ∨ α of K is still a tautology, and thus provable, for α whatever.

Thus, substituting with Lp for α we get ¬Lp ∨ Lp.

The reason is simple: if Lp is true, then clearly ¬Lp is false, and thus, by truth table for ∨, ¬Lp ∨ Lp is true, and the same with Lp false.

For a detailed proof, see e.g. Edward Zalta, Basic Concepts in Modal Logic (1995): Ch.3.2 Tautologies are Valid.

Improve this answer
4
  • 1
    The use of truth tables is mostly irrelevant in modal logic. I believe this solution is too simplified. I agree and accept that the rules of propositional logic still apply, I do not agree however to the proof of ¬Lp ∨ Lp by default, as it involves possible worlds and not merely a truth table tautology. The difficulty in building a proof theory for such arbitrary 'p' strengthen this point.
    – Akira
    Commented Apr 5, 2017 at 6:41
  • ¬Lp ∨ Lp remains true regardless of any possible world, because our logic only has two values for evaluation - T /F. Lp returns evaluates to either T or F and the statement ¬Lp ∨ Lp is T regardless of which arm becomes true. What feature of system K or any other modal system interacts negatively with this?
    – virmaior
    Commented Apr 5, 2017 at 7:12
  • @Akira - truth table procedure still works because you can "embed" it into more complex Kropke semantics. Of course, you can prove every tautology with the rule of the propositional calculus. Use them and you will get the proof you need.
    – Mauro ALLEGRANZA
    Commented Apr 5, 2017 at 7:16
  • 1
    @MauroALLEGRANZA I am looking for a formal proof indeed, but cannot find one without assuming that a proposition with an operator is a tautology. I wanted to avoid it, or for the very least provide a convincing reasoning. I understand the motivation behind it and am thanking you for clarifying it.
    – Akira
    Commented Apr 5, 2017 at 7:29

You must log in to answer this question.

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