2 High-level expressions

2.1 Holes

Mathematics is a game of transforming symbol strings. "Rules for transforming symbol strings" are also expressed.
"Something into which a Form is substituted when a rule is used" is called a "Form hole", and the following is used.
Form hole … $[lDP]
For example, the rule "swap the two sides of \(\mathbin{\rm o\!r}\)" can be expressed as \(P \mathbin{\rm o\!r} Q\) → \(Q \mathbin{\rm o\!r} P\) . (As a rule) \(X \mathbin{\rm o\!r} Y\) → \(Y \mathbin{\rm o\!r} X\) is the same.

Hole for a sequence of words … $_[lDP]
The [ｌDP] appearing below means "one full-width Latin letter followed by zero or more digits and '" (ｘ, etc.).
v-Form hole … [ｌDP]
v_-Form hole … [ｌDP]_

2.2 word alias

In general, words introduced as word+ exist for high-level expressions and are processed in the FCL conversion by a rule called lower.
The simplest example is the alias word: a "word identified with another in the FCL conversion", made for some purpose.
For example, there is an alias of \(,\) that differs only in its tex notation. ★Not available yet
word+(pp,p) … \(\text{and}\)

There are also logical-symbol aliases that differ only in binding strength.
word+(pp,p) … \({\bf ,}\,\)  \(\Longrightarrow\)  \(\Longleftrightarrow\)
lower … \(P {\bf ,}\, Q\) ≃ \(P , Q\)
lower … \(P \Longrightarrow Q\) ≃ \(P \Rightarrow Q\)
lower … \(P \Longleftrightarrow Q\) ≃ \(P \Leftrightarrow Q\)
The preced is \(\neg\) < \(\forall\) \(\exists\) < \(\Rightarrow\) \(\Leftrightarrow\) < \(,\) \(\mathbin{\rm o\!r}\) < \(\Longrightarrow\) \(\Longleftrightarrow\) < \({\bf ,}\,\).
Example　 \(P \Rightarrow Q \Longleftrightarrow \neg P \mathbin{\rm o\!r} Q\) ≈ \(( P \Rightarrow Q ) \Leftrightarrow ( \neg P \mathbin{\rm o\!r} Q )\)
Be careful with the following examples.　 \(P , Q \Rightarrow R\) ≈ \(P , ( Q \Rightarrow R )\) 　 \(P , Q \mathbin{\rm o\!r} R\) ≈ \(( P , Q ) \mathbin{\rm o\!r} R\)

2.3 word functions

The following words are also used often. In the gram, \({\tt x}\),\({\tt y}\),\({\tt z}\) take s, c or p.
word(p,p) … \(\neg\)
word+(\({\tt x}\)\({\tt y}\),p→\({\tt x}\)\({\tt y}\),p) … \({\tt /}\)
lower … \(A \stackrel{{\tt /}}{\mathbin{{\sf p}}} B\) ≃ \(\neg ( A \mathbin{{\sf p}} B )\)
The FCL conversion of \(x \neq y\) is \(\neg ( x = y )\) . In a formula, do not put a space between {/} and =.
Note that \(\mathbin{{\sf p}}\) is a hole for a binary symbol. ★We plan to tidy up the spelling of holes

2.4 Abbreviations

Abbreviations can also be used. In the FCL conversion they are processed by a rule called abbr (abbr processing comes before lower processing).
abbr … \(X_{1} , \cdots , X_{\tt n} \mathop{{\sf A}}\) ≈ \(X_{1} \mathop{{\sf A}} , \cdots , X_{\tt n} \mathop{{\sf A}}\)
\({\tt n}\) is something into which a natural number is substituted. \({\tt n\,{\text -}\,1}\) etc. can also be used. Handling such things is also the job of formel.
Example　 \(x , y \in A\) ≈ \(x \in A , y \in A\)
The following and others are also often used and help concise description.
　 \(X \subset Y \subset X\) ≈ \(X \subset Y , Y \subset X\)
　 \(\forall x \in X . x \in Y\) ≈ \(\forall x ( x \in X \Rightarrow x \in Y )\)