3 Definitions and expansion by definitions

3.1 The sequence \(\mathbb{W.}\) collecting definitions

Among the first symbols in set theory are the following.
word(ss,p) … \(\in\)  \(\subset\)
\(\subset\) has the following definition. In general, 〇. is positioned as the definition of 〇.
⊂. … \(X \subset Y \Longleftrightarrow \forall x \in X . x \in Y\)
It is convenient to treat \(=\) as having a definition too, though \(\Longleftarrow\) is often called the axiom of extensionality.
=. … \(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)
The definition of a word denoting a set also includes that the set exists.

Automatic variables in a Book are used.
\(\mathbb{W}.\) is "the sequence of all props of the form 〇. (where the gram of 〇 does not contain c)". At this stage it is ⊂. =. .
\({\tt P}\) ◀ \(\mathbb{W}.\) is read "\({\tt P}\) is shown from the definitions". Writing the needed definitions one by one is tedious, so this form is preferred.
=.. … \(X = Y \Longleftrightarrow X \subset Y \subset X\) \(\blacktriangleleft\) \(\mathbb{W}.\)

In general, when throwing to Prover9 it is better to write only what is needed in the sos.
On source line 135, it can also be shown by putting ⊂. , =. in the sos instead of W. in prf =.. -| W. p; (length:37). But since the claim of the thm is ◀ W., we connect them at the end with =.. -| W. h;.
When \(\mathbb{W}.\) becomes an infinite sequence (e.g. when a definition of a word containing \({\tt n}\) is given), you cannot write -| W. p;.

3.2 slash computation

/ is a binary operation of Thmel; if there is no "word whose gram contains c or ( )", \({\tt A}\) / \({\tt P}\) is "\({\tt A}\) expanded by \({\tt P}\)". For example
=.. / =. … \(\forall x \, ( x \in X \Leftrightarrow x \in Y ) \Longleftrightarrow X \subset Y \subset X\)

For a sequence \(\mathcal{P}\), \({\tt A}\) / \(\mathcal{P}\) is also defined naturally.
Let us give the Thm above a new prf.
=.. \(\blacktriangleleft\) \(\mathbb{W}.\)
Note the first step of the prf on source line 148, =.. / W. -| O p;. Since the expansion has been computed in Thmel, it can be passed to Prover9 with sos O. The goal becomes a rather long formula, but the length drops to 28.
The second step =.. -| W. h; is a hyperion step; from what was shown in the first step, it removes the slash (from \({\tt A}\) / \(\mathcal{P}\) ◀ \(\Gamma\) to \({\tt A}\) ◀ \(\mathcal{P}, \Gamma\)).

// W. becomes / W. / W..
One / W. opens each subformula by one level, using the definition of its head word. The formulas produced by opening are opened by the next /.
W.!〇. (written without spaces) is the sequence W. with 〇. removed.
The same Thm can often be shown both by -| W. p; (putting the definitions in the sos) and by / W. -| O p; (expanding first). As definitions increase and the sos grows, expanding first becomes advantageous.