Review:
Tarski world
For this part of the lab, you will be exploring quantified statements in the toy setting called Tarski World (after the famous logician Alfred Tarski). There, for a given board, the universe consists of pieces of different shapes and sizes which have been placed in the cells of a board (see the example above).
For each shape and each size of a piece, you have a predicate,
as well as a few predicates describing relationship between pieces.
In our lab, we will have predicates Square(x), Circle(x), Triangle(x), Big(x),
Little(x), as well as NextTo(x,y), which is true iff y is
in a cell adjacent to x (left/right/above/below of x), Aligned(x,y), which is true if x and y are either in the same column or in the same row (not diagonal; every piece is aligned with itself), and EqualSize(x,y) which is true iff x and y
are both big or both little.
(Of course, you can use these predicates with any variable names, not
just x or y). More information about our Tarski world can be found here.
Now, you can write formulas such as $\exists x Big(x)$ or $\forall x Square(x) \to
\exists y Circle(y) \wedge NextTo(x,y)$, which says that every square has a circle
next to it; note that both these formula are true for the board on the picture (you might see the boards with pieces called "structures", and if a formula is true on a board, then such board is a "model" for this formula).
For conciseness, we will often use just the first letter (or an abreviation of the word) of the predicate
(so the formulas above would be $\exists x B(x)$ and $\forall x (S(x) \to \exists
y C(y) \wedge N(x,y))$
For the following exercises, it is more convenient to use Google Drawing rather than Bongo whiteboard. Open this template ; it will have two boards and all possible shapes already drawn. Then, one person in each room should make an editable copy of this template (by going to File/Make a copy), and share it with the rest of breakout room (by clicking on "Share", setting it so that everybody with the link can edit, and sharing the link in the group chat). Now, everybody in your group can work on it together in another window; you can also have one person share it inside Bongo (by doing "share screen"). Now, copy/paste the given pieces (shapes), and drag the copies to where you want them to be on the board (at most one piece per cell). You also have the list of special symbols which you can copy/paste into your formulas; if you have a stylus, you can write directly by selecting "scribble" under the line icon.
Exercise 1:
Make two more boards satisfying
$\forall x S(x) \to \exists y C(y) \wedge N(x,y)$ ).
Try to use different pieces, different numbers of pieces, and place them differently on the board.
Exercise 2:
For each of the boards you created, determine if the formula $\exists x \forall y \exists z E(x,y) \vee T(z) \wedge A(x,z) \wedge A(y,z)$ is true.
Exercise 3:
For each of these boards, write your own new formula which is true for that board, but not for the other one. Use quantified variables in all of your predicates.
Exercise 4:
Now, for each of your boards, write a formula which is false for that board, but would become true if you
add, remove or move one piece. State which piece needs
to be added/removed/moved and where.
Exercise 5 (if you have time):
For all the formulas you wrote, try to come up more examples of different boards that make them true, and boards that make them false.
