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.

Conifold
  • 43,055
  • 4
  • 95
  • 182
Akira
  • 33
  • 3
  • 1
    Everi tautology is provable in modal logic; thus use ¬α ∨ α. – Mauro ALLEGRANZA Apr 04 '17 at 16:59
  • 1
    And then I get L(¬p∨p) but I want to prove ¬Lp∨Lp – Akira Apr 04 '17 at 17:03
  • 1
    NO; α can be a formula whatever, also Lp. – Mauro ALLEGRANZA Apr 04 '17 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 Apr 04 '17 at 20:22
  • What is "specific system T"? If it has restrictions on which formulas can be substituted into tautologies you need to be very specific about what they are. At least give a reference, or better yet put them into the OP. – Conifold Apr 04 '17 at 21:43
  • 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 Apr 04 '17 at 22:11
  • Assume the negation and use demorgan's law (Mauro has a nice proof for it here : http://philosophy.stackexchange.com/questions/29590/how-can-you-derive-de-morgans-law ) – virmaior Apr 05 '17 at 00:12
  • 1
    If you literally want to use only three modal rules you won't derive much of anything, especially because they only contain L and implication. What "system T" means is that all non-modal tautologies are also assumed and unlimited substitution into them is allowed. I am guessing you want to allow only something more austere, but what it is is unclear (but is better involve formulas connecting disjunction to implication). Whatever it is it will not be "system T". – Conifold Apr 05 '17 at 02:07
  • @Conifold my best guess is that he's worrying about discontinuous functions in terms of rejecting the use of ¬α ∨ α ... – virmaior Apr 05 '17 at 02:09
  • 1
    @conifold The rules of propositional logic apply, however more care should be payed when applied to quantified propositions as in first order logic. (especially if one wants to assume truth-tables). I still believe I am on system T according to its definition. – Akira Apr 05 '17 at 06:47
  • I still have no idea what you want to allow propositionally on modalized formulas, but defining implication in terms of negation and disjunction might be weaker than unlimited application of the excluded middle schema, and you can then derive the title formula using distribution. But if you wish to disallow substitution of modalized formulas into non-modal tautologies completely then it is simply not derivable. Because it has modalized formulas connected by a disjunction, and the T-axioms can only produce formulas where they are connected by implications. – Conifold Apr 05 '17 at 19:11

1 Answers1

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.

Community
  • 1
Mauro ALLEGRANZA
  • 36,790
  • 3
  • 36
  • 80
  • 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 Apr 05 '17 at 06: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 05 '17 at 07: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 05 '17 at 07: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 Apr 05 '17 at 07:29