This is a tutorial explains how to write a simple proof using the suggestion box. We will prove that union is commutative: (=_ (u. S T) (u. T S)).
We'll start by adding an expression for the union of two sets (u. S T). The union operator is written as u. in the editor. Since Ghilbert uses prefix notation the union operator u. comes in front of the operands S and T.
The expression (u. S T) now shows up as an argument on the proof stack. The suggestion box constantly looks at the expression on the bottom of the proof stack and compares it with the existing theorems in the database. If it sees a theorem that it can be apply to the expression, it suggests that theorem. In this case, it makes a single suggestion:
The suggestion is to define the union operation. Click the button. It now proves the definition of (u. S T). The union of S and T is defined as the set of all elements x for which x is in S or x is in T.
Notice that one part of the expression in the box is now highlighted. The ({|} x (\/ (e. x S) (e. x T))) part is highlighted. The highlighting is important because the suggestion box gives targets its suggestions towards the highlighted part. You can highlight another part of the expression by clicking on it. Click the left side of the equation and the whole equation will be highlighted:
Every time you highlight a different part of the expression, different theorems are suggested that are relevant to the highlighted part. Click on the right side until you have the OR ∨ part highlighted like this:
Suggestions now appear related to the highlighted OR ∨ operation. Commuting the OR operation is the key to our goal of commuting the union. Click the Commute ∨ button:
Now the order of (e. x S) and (e. x T) are reversed. Now click and highlight the entire right side of the equation ({|} x (\/ (e. x T) (e. x S))). A suggestion now appears that this expression can be simplified using the definition of union. Click on the simplify button:
We've now completed our proof that union is commutative. The proof contains three steps:
In the next tutorial, we will prove the same theorem in a different way. By proving it a different way, we can highlight other useful features of the suggestion box.
Prev | Main | Next: Suggestion Box - Union is Commutative Proof Revisited