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, for example,
Here we are just trying a few samples to see if the software is running correctly.
John Barwise and John Etchemendy, [1999] Language, Proof and Logic
What follows are further Ana Con inferences.
John Barwise and John Etchemendy, [1999] Language, Proof and Logic
What follows are further Ana Con inferences.
John Barwise and John Etchemendy, [1999] Language, Proof and Logic
LP&L comes with a Normal or Standard Interpretation, and this certainly affects how trees should and can behave.
For example, the polyhedra are either tetrahedra, cubes, or dodecahedra. If a particular polyhedron is a cube it cannot be a tetrahedron, so Cube(a)&Tet(a) cannot be true and a branch containing Cube(a) and Tet(a) should close or be able to close.
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.
John Barwise and John Etchemendy, [1999] Language, Proof and Logic
LP&L [1999] has a number of exercises. Many of them you will be able to do in the Widget below.
Here are a few hints
2013
Colin Howson, [1997] Logic with trees Chapter 11
Set theory is an extensive topic introduced elsewhere. It can be written as a first order theory.
There is one axiom schema, Abstraction (or Comprehension), which can generate infinitely many axioms
∀y(yε{x:Φ[x]}↔Φ[y])
Axiom Schema of Abstraction (or Specification or Comprehension). The Set Builder Axiom Schema.
2013
Colin Howson, [1997] Logic with trees Chapter 9 & 11
It is common in this setting (which is arithmetic) to use functional terms like s(x), s(1), s(0) to mean the successor of x, 1, and 0, respectively. Equally common is the notation x', 1', and 0' to mean the same thing. The latter is quicker and shorter (though not semi-nmemonic)-- we will use it here.
To learn about the Uniqueness quantifier (a part of identity), and to be introduced to definite descriptions.
Uniqueness is central in mathematics, and definite descriptions is a core area in philosophical logic.
2013
Colin Howson, [1997] Logic with trees Chapter 9
Groups can be characterized by three proper symbols {=,+,0} (ie identity, one infix operator, we will use '+', and an identify element '0') and the three proper axioms
∀x∀y∀z((x+y)+z=x+(y+z)), (*associativity*)
∀x(x+0=x∧0+x=x), (*identity element, right and left*)
∀x∃y(x+y=0∧y+x=0) (*inverse*)