Deriver [Functional Terms, Identity, First Order Theories, Set Theory—Gentzen Syntax]
The tutorials presented here look at some topics in logic to the level of intermediate to advanced Predicate Calculus. They build on the Tutorials of Easy Deriver which provided the introductory material to Propositional and Predicate Calculus.
The program, widgets, or Notes, should be accompanied by a suitable textbook, such as:
M.Bergmann, J.Moor, J.Nelson, The Logic Book
A.Hausman, H.Kahane, P.Tidman, Logic and Philosophy
C.Howson, Logic with Trees
R.C.Jeffrey, Formal Logic: Its Scope and Limits
H.Leblanc and W.Wisdom, Deductive Logic
B.Mates, Elementary Logic
M.D.Resnick, Elementary Logic
Unfortunately these textbooks use slightly different choices of rules and symbols one from another. To adjust to this the Notes are in different major sections, with the sections tailored to particular texts.
You are invited to review
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 parantheses around the quantifiers (after all, the parantheses 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))
The 'gentzen' system
This uses Rabc for the application of a predicate R to the arguments or terms a, b, c, and the use of f(abc) for the application of a functor or function f to the arguments a, b, c. i.e the predicates and atomic terms are of length 1. It uses the upper case letters A-Z 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. Variables, consist of lower case [w-z]. There are parantheses around the quantifiers. The gentzen system also uses ~, ∧, v, ⊃, ≡, so a typical formula is (∀x)(Fx∧~Hx ⊃ Gxy).
The 'howson' system
The Colin Howson book uses a notation like R(a,b,c) for the application of a predicate R to the arguments or terms a, b, c. It employs the upper case letters A-Z, perhaps followed by subscripts, to be predicates, so, for example, R, S₁, T₁2 are all predicates. Variables consist of lower case [w-z] only, optionally followed by subscripts. There are no parantheses around the quantifiers. The howson system also uses ~, &, v, →, ≡, so a typical formula is ∀x(F(x)&~H(x) → G(x,y)).