LP&L Trees [Tarski's World]

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 some information about it Tarski's World.

It is possible, though maybe a little unusual, to use trees with such a standard interpretation. But to do so, the meanings of the predicates have to be respected; so, for example, if b is a cube (ie Cube(b)), then b is not a tetrahedron (ie not Tet(b)). This makes a difference to closing branches and trees. It also makes a difference to linear proofs. And LP&L accommodates the differences for its linear proof system Fitch by means a rule, or set of rules, called Analytical Consequence or Ana Con. We can adopt the same device for trees; we can devise an Ana Con tree rule to build in polyhedra and chessboards.

Becoming familiar with this rule is a good place to start with LP&L Trees. [For learning Trees in General you might want to look at Trees, perhaps Trees[Howson].]