LP&L Trees [Tarski's World]
Last altered 6/29/11
John Barwise and John Etchemendy,  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.
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.