8/12/2026
Welcome!
A problem with presenting logic is that many of the different authors use different symbols and different syntax for the logical expressions. We are just going to choose one (which we think is the best for the present purposes). If you would like something different, that is fine, the software here can run most all systems. Just go to the Preferences page and make your choice. Then the software will run what you would like. Many of the logical symbols look quite similar visually to other symbols, for example the logical 'or' is ∨ and that looks something like capital vee V or even lower case vee v . The software will do everything it can to make sense of your input—but sometimes you just plain have to use the right symbol. You are invited to scan over
These tutorials and
Colin Howson, [1997] Logic with trees ISBN: 0-415-13341-6
would work well together.
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.
Howson [1997] will give you enough background. Or you could look at the first five propositional tutorials in Easy Deriver
An alternative approach to doing the exercises using the Deriver web application
Deriver can run out of a web page. In some ways this is better in that the User can print proofs, save half finished proofs etc. If you would like to try that you might want to glance at Deriver in a web page Then you can launch Deriver from here Deriver20 [Default Parser]. You'll be opening the Exercises as the Tutorials progress.
Notation
Not all logicians, and logical texts, use the same symbols for the so-called 'logical connectives'. Nor do they use the same sequences of symbols for 'well formed formulas'.
Here are typical possibilities for symbols
'not' : ∼ (the 'tilde'), ¬ (looks like the top right corner of a box)
'and': ∧, & (the ampersand), . (just a period)
'or': ∨ (usually just this, vel)
'implication': ⊃ , →
'equivalence': ≡, ↔
'existential quantifier': ∃, ∑
'universal quantifier':∀, ∏
So, in a logic book, you might see (A&B)→C and that is just the same as (A∧B)⊃C.
And you might see (∀x)(Fx ⊃ Gxy) and that might be just the same as ∀x(F(x)→G(x,y)).
The software running here can easily manage or render any of these. But we should explain what we favor, and help you find what you prefer.
The 'default' system
We like the use of notation like R(a,b,c) for the application of a predicate R to the arguments or terms a, b, c, and the use of f(a,b,c) for the application of a functor or function f to the arguments a, b, c. In the simple form, this employs the upper case letters A-Z, perhaps followed by subscripts, to be predicates, so, for example, R, S₁, T₁₁ are all predicates. And it employs lower case letters ie [a--v], perhaps followed by subscripts, to be constant terms or functions. But an extension is useful.
Often, when working informally, authors will write Red(x) to mean that the predicate Red is applied to the variable x. The default system will accept this also (with these new style of predicates also optionally followed by subscripts). So Red, Soft₁, Tiger₁₁ are all predicates. The rule or convention here is that the first letter of a predicate is upper case, then any sequence of upper or lower case letters can follow, and the predicate can be completed with subscripts. So 'AVeryLongPredicate' is a predicate. A similar approach is applied to constant terms or functions, only this time, the term must start with a lower case letter ie [a--v]. So aFunctionAppliedToATerm(aTerm) is a perfectly good term of the form f(a). Variables, though, consist of lower case [w-z] only, optionally followed by subscripts [ie there can be no sequence of upper or lower case letters in between].
So the argument. Socrates is a man, All men are mortal, therefore, Socrates is mortal can be symbolized
M(s), ∀x(M(x)→M₂(x)) ∴ M₂(s)
But, the software will also accept
Man(socrates), ∀x(Man(x)→Mortal(x)) ∴ Mortal(socrates)
Notice here that there are no parentheses around the quantifiers (after all, the parentheses are not needed). [Of course, the reason brackets are needed for predicates, terms etc. is help determine what, say, Redbox, is supposed to mean, when predicates and terms need not have constant length.]
The default system also uses ~, &, v, →, ≡, so a typical formula is ∀x(F(x)&~H(x) → G(x,y))
Some background on Tableaux
The use of trees (or 'tableaux') in logic was pioneered by Beth, Hintikka, and Smullyan, and their use was brought into a teaching context by such books as the standard Jeffrey text. See
E.W. Beth, [1959] The Foundations of Mathematics
G.Gentzen, [1934-5] 'Untersuchungen uber das logische Schliessen', Mathematische Zeitschrift, vol 39, 1934-5, pp.176-210, 405-31
J. Hintikka [1955] ' Two papers on Symbolic Logic', Acta Philosophica Fennica, vol 8 1955
R.C.Jeffrey, [1967] Formal Logic: Its Scope and Limits
R.M. Smullyan, [1968] First Order Logic