7/1/12 Under construction
Rod Girle  Modal Logics and Philosophy Chapter 10
will be a help here.
The symbolization <kappa><agent><proposition> as in
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
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 applet. The applets 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 ∼ & ∨ ⊃ ≡ ∀ ∃ ∴ Κ Ρ ◊ □