LP&L Trees 6 Identity Samples

Logical System


John Barwise and John Etchemendy, [1999] Language, Proof and Logic

For the Tarski's World part of LP&L, a standard interpretation is used of various sized polyhedra on a chessboard. Here is a link to their screenshot of it Tarski's World.

Here we are just trying a few samples to see if the software is running correctly.


[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.]

1. ∃x(Cube(x)∧∀y(Cube(y) → y=x))  ∴  ∃x∀y(Cube(y) ↔ y=x) (p.377)

2. SameRow(a,a), a=b, b=c ∴ SameRow(a,c)