1/29/2020
Reading
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].]