An example of the tree widget in use (and we are showing a different parser here to the earlier ones)
The logical symbols in use are ¬ ∧ ∨ → ↔ ∀ ∃ .
Determine whether these arguments are valid (ie try to produce closed trees for them)
a) ∀x(F(x)→G(x)), ∃x¬G(x) ∴ ∃x¬F(x)
b) ∀x(F(x)→∀yG(y)), F(a) ∴ ∀xG(x)
c) ∀x(A(x)→B(x)), ∀x(¬A(x)→C(x))∴ ∀x(¬B(x)→¬C(x))
d) ∃xF(x),∀x(¬G(x)→¬F(x)),∀xM(x) ∴ ∃xG(x)∧∃xM(x)
[In the widget below:- Click, or touch, once to select. Click again to unselect. Select one item to extend the Tree, select two lines or formulas to close a branch. [Select two for extending with identity.]]
You will be able to do your own examples in the Widget below.
You can try your own exercises here.
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). In the syntax we prefer 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₁)).
- 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.
- The iPad, and similar, keyboards have a little trick that might catch you out. If you type a single letter, say 'a', they will automatically put it in upper case to 'A' because they assume you are starting a sentence. But, actually, if you are instantiating a quantifier you have to use lower case.
Exercise: Roll your own