# Deriver [Functional Terms, Identity, First Order Theories, Set Theory—Gentzen Syntax]

Logical System
###### 12/19/20

Welcome!

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
W.Hodges, Logic
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

### 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 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 parentheses 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₁ are all predicates. Variables consist of lower case [w-z] only, optionally followed by subscripts. There are no parentheses around the quantifiers. The howson system also uses ~, &, v, →, ≡, so a typical formula is ∀x(F(x)&~H(x) → G(x,y)).

Exercises

Each of the tutorials has its own exercises, which can be done quickly and easily out of their own web pages. However, sometimes a User might want to save a half-finished proof to come back to it later, or might want to print a proof, or might want to do totally new exercises not supplied here on this site. From a computer software point of view, those tasks are not easy to provide out of plain web pages. But, there is a web application 'Deriver' that will run out of a web page and provide those abilities.  Should you wish to use that, see Exercises for Deriver using the Deriver Web Application . Good advice is: start these tutorials without out it, but if you get to the point of wishing to save some work, then switch to the Deriver Web Application.