K

Logical System
girle

8/17/26

Reading

Rod Girle [2000] Modal Logics and Philosophy Chapter 3

K has the rules

{Non-modal propositional rules + Modal Negation + ◊R + □R}

These are described in Review of K Rules.

Basically what you have here are the restricted rules and little or nothing in the way of Access. Use of the possibility elimination rule will provide you with access to the generated world, and, with certain arguments, there may be explicit access given by the premises. But that is it. In particular, even though a formula may hold in a world, that by itself does not give access from that world to that world, so the inference.

a) ∴ □P ⊃P (invalid in K)

will be invalid.

Try to derive it as Tree1 below [switch the Rule Set to K, and do not use any of the Access Rules]. You should not be able to close the tree. You can also try using S5, and you should be able to succeed there.

There are a couple more for you to try

b) ∴◊~P⊃~□P

c) ∴□P⊃□□P (invalid in K)

 


 

Roll your own trees with K

Girle's Chapter 3 has a number of exercises. You can do them here (be sure to use the following logical symbols)

∼ & ∨ ⊃ ≡ ∀ ∃ ∴ □ ◊

  • You have to use the right (unicode/html) logical symbols. Check Writing symbols
  • The symbols in use here are ∼ & ∨ ⊃ ≡ ∀ ∃ ∴ □ ◊ ₁ ₂ ₃ ₄ ₅ ₆ ₇ ₈ ₉ (so copy and paste or drag and drop these). In the syntax, the quantifiers have brackets around them so a quantified formula might look like (∀x)(Ax→Bxy). Notice that the 'arguments' to a predicate do not have brackets around them. You can use proper subscripts (shown above) on variables (or constants or predicates). For example, (∀x₁)(Ax₁→Bx₁y₁).
  • When entering from a selection, the software will take a single formula (say, A) or a comma separated list of formulas (say, A,B,C) or a possibly empty comma separated list of formulas followed by ∴ and another formula (say, A,B,C ∴ D). In the last case it will load the negation of the conclusion.
  • Lightweight Input. Just type, cut and paste, or drag and drop, whatever you wish, into the lower text box (the 'Journal'). Then make a selection and hit the Start button.
  • Lightweight Output. You can write a tree out to the Journal (then copy it and paste it into WORD (for example)).
  • The iPad, and similar, keyboards have a little trick that might catch you out. If you type a single letter, say 'a', they will automatically put it in upper case to 'A' because they assume you are starting a sentence. But, actually, if you are instantiating a quantifier you have to use lower case.

[Switch the Rule Set to K, and do not use any of the Access Rules].