8/17/26
Epistemic Logic
The text
Rod Girle [2000] Modal Logics and Philosophy Chapter 10
will be a help here.
The symbolization <kappa><agent><proposition> as in
ΚbP
is intended to mean
'Person, or agent, b knows that P'.
[The Κ is the Greek letter kappa (upper case or lower case is fine), in html it is the symbol 'Κ' in unicode it is the symbol '039A' . Kappa may look like the English letter 'K', but it is different. The symbol palette will type kappas for you.]
The symbolization <rho><agent><proposition> as in
ΡbP
is intended to mean
'Person, or agent, b does not know that P is not the case'.
[The Ρ is the Greek letter rho (upper case or lower case is fine), in html it is the symbol 'Ρ' unicode it is the symbol '03A1' . Rho may look like the English letter 'P', but it is different. The symbol palette will type rhos for you.]
[Motivation behind the symbols and syntax. We would like to have a knowledge operator KbP, which is intended to mean 'Person, or agent, b knows that P'. Some details of import here partly result from the use of computers and sofware. First of all, the subscript 'b'. In web pages, the subscripting of a character is for the most part a display device, not something that is intrinsic to the character-- so there isn't, for example, a subscript x, there is only an ordinary x which is displayed in a subscript position. Unicode is similar, there are subscript numbers (1,2 etc.) but there are no subscript xs. So we couldn't do subscripts in a natural way even if we wanted to. Then there is the question of whether we do want to. We'd like to be able to symbolize 'Everyone knows P' ie to quantify over the agents. With subscripts this would be odd, (∀x)KxP -- the variable x in the scope wants to be in the scope and not as some kind of tag on the operator. (∀x)KxP looks better. Then there is the question of whether we might use an ordinary two place predicate, say Kxy, for the knowledge predicate. The problem here is that ordinary predicates apply to terms but in Kxy the x is a term, but the y is a proposition (ie a true/false statement or a well formed formula. So, Kxy is a mix between a predicate and a connective. One way out is to use a new kind of symbol and a new kind of formula. Kappa is the symbol and Κxy is the new kind of formula. (A similar approach is used with Rho.)]
Roll your own
Type your own entries into the next widget. The widgets can be configured to run a variety of symbol systems. This particular one is running 'Girle', so use these symbols for the logical connectives.
F ∴ F & G ∼ & ∨ ⊃ ≡ ∀ ∃ ∴ Κ Ρ ◊ □
- 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)).