This section of the tutorials and
Richard Jeffrey, [1967-2006] Formal Logic: its Scope and Limits
would work well together (and it is an excellent book).
You need to know some propositional logic to be able to understand the tutorials to come. In particular, you need to know about the symbols used in propositional logic, truth tables, satisfiability, consistency, and semantic invalidity (by counter example). You do not need to know propositional rules of inference and derivations.
Jeffrey[1967-2006] will give you enough background.
Alternatively you could look at the first five propositional tutorials in Easy Deriver
You should perhaps also check Checking your computer is configured correctly and Writing Symbols (and Alternative Symbols)
Most of these pages load java applets and that means that they may take 20 seconds or so to load. [Your browser will then 'cache' the applets and subsequent work will proceed much more quickly.]
Jeffrey[1967-2006] uses pretty well the same symbols and notation as
Colin Howson, [1997] Logic with trees ISBN: 0-415-13341-6
The Notes on Howson are a little more current than the ones that used to be here. It seems wiser just to refer you to those Howson Trees.
[Send an email if you would like the earlier Jeffrey Notes re-published. The older Jeffrey[1967-2006] uses the minus sign '-' for negation. This is a little non-standard. It is also not a good idea, for the minus sign is used here both in arithmetic and in set theory. We will stay with the more usual '¬' for 'not'.
He also used to do something else 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.
[Howson does this, but with the addition of separating the arguments with commas and putting brackets around them, thus G(a,b,c).]]