John Barwise and John Etchemendy,  Language, Proof and Logic
LP&L  has a number of exercises. Many of them you will be able to do in the Widget 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). The B&E syntax is that the quantifers do not have brackets around them so a quantified formula might look like ∀x(A(x)→B(x,x)). Notice that the 'arguments' to a predicate have brackets around them, and if the arguments are a list they will be separated by commas. You can use proper subscripts (shown above) on variables (or constants or predicates). For example, ∀x₁(A(x₁)→B(x₁,x₁)).
The software employs the upper case letters A-Z, perhaps followed by subscripts, to be predicates, so, for example, R, S₁, T₁2 are all predicates. But the software permits an extension. The software allows us to write Red(x) to mean that the predicate Red is applied to the variable x (and these new style of predicates can also optionally be followed by subscripts). So Red, Soft₁, Tiger₁2 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)
- 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.
Exercise: Roll your own
[In the widget below:- Click once to select, click again to un-select. Select one item to extend the Tree, select two to close a branch. Select one or two for extending by Analytic Consequence (depending what inference you are trying for). Select two for extending with identity.]