# Proving ¬Lp ∨ Lp

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.

• Everi tautology is provable in modal logic; thus use ¬α ∨ α. – Mauro ALLEGRANZA Apr 4 '17 at 16:59
• And then I get L(¬p∨p) but I want to prove ¬Lp∨Lp – Akira Apr 4 '17 at 17:03
• NO; α can be a formula whatever, also Lp. – Mauro ALLEGRANZA Apr 4 '17 at 20:00
• 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 Apr 4 '17 at 20:22
• 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 Apr 4 '17 at 22:11

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.

• 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 Apr 5 '17 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 Apr 5 '17 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 Apr 5 '17 at 7:16
• @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 Apr 5 '17 at 7:29