9/16/08 10 Software
Reading
Richard Jeffrey, [1967-2006] Formal Logic: its Scope and Limits
Note
Jeffrey[1967-2006] does something notationally which we do not wish to follow. In the predicate logic he writes two place predicates infix. So, for example, 'Alice loves Bert' might be symbolized as 'aLb' . We prefer to write the predicates prefix, so we would write 'Lab'. Here is the reason. There are predicates of higher arity than 2. For example, 'Alice gives Bert a Cookie' , what happens to an infix convention here? should it be 'aGbc' or 'abGc' or what? The prefix convention makes it 'Gabc' . Jeffrey makes the situation worse by writing function applications as plain juxtaposition. So, for example, the function 'father of...' as in 'father of Alice' is written 'fa'; but then what is 'aGfa' ; is it a binary predicate applied to the term 'a' and the function application 'fa' or is it a ternary predicate applied to the terms 'a', 'f' and 'a'? We write function applications using parentheses, thus 'f(a)' so it is clear what the following formulas are
- G
- Ga
- Gab
- Gabc
- Gab(c)
- Ga(b)c
- etc.
Exercises
Jeffrey [2006] has a number of exercises. Many of them you will be able to do in the Applet below.
Here are a few hints
- 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).
- 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.
- Just type, cut and paste, or drag and drop, whatever you wish, into the lower text box. Then make a selection and hit the Start button.
Identity
You do trees with Identity, in the Jeffrey system. Read Tree Tutorial 5: Identity Rules [Howson] first, and note that Jeffrey's system is what we call a one rule identity system.