1 Basics of Formel

1.1 Header settings, words and Forms

The settings of Formel are written in a .formel file.
If none is specified in the header, default.formel is loaded. This Book is such a case.

A symbol used in Formel is called a word, and a "sequence of words" that satisfies the grammar is called a Form.
There are s-Forms, c-Forms and p-Forms.
One tends to say "an s-Form is a set", but care is needed. Use the former when looking at the form, and the latter when looking at the meaning. The same goes for "a c-Form is a class".
Forms make up a higher-order {s,c}-sorted language (though you will often use only the first-order part).

1.2 Basics of words

Usually a word is called up from those registered in the DB, and used after it is "introduced" in the Book. In the source, write a line starting with word.
word(ss,p) … \(\in\)
(ss,p) is the gram. A word also has data called tex; the tex of \(\in\) is \in. The gram and tex are stored in the DB.
For a gram (〇,△), the number of characters of 〇 is sometimes called the arity. The arity of \(\in\) is 2.
★At present you cannot create your own words, but when you can, you will also need to prepare the gram and tex.

Different words may have the same tex, so click often to check. The following word is also in the DB.
word(sc,p) … \(\in\)
When "reading" a Book, we arrange things so that you need not distinguish sets and classes each time.

Words with the same gram can be introduced together. For example, there are the following binary propositional connectives.
word(pp,p) … \(,\)  \(\mathbin{\rm o\!r}\)  \(\Rightarrow\)  \(\Leftrightarrow\)
A word also has data called its notation (see "Various notations" below), which may appear to the right of the gram at introduction, such as the R below.
word(vp,p)R … \(\forall\)

1.3 Variables and constants

Variables are special words and are registered in the .formel. default.formel registers the following.
v-Form (gram (,s)) … [lDP]
v_-Form (gram (,c)) … [lDP]_
[lDP] means "one Latin letter followed by zero or more digits and '" (x, X1', etc.).
\(x \in X\) and \(x \in X\) are p-Forms, but \(x \in X\) is not a Form. By the way, this example is made on purpose.
If specified in the .formel, \(\alpha\), \(\mathcal{X}\), etc. can be used as v-Forms.

The following v^-Form is a symbol of the higher-order language (in ordinary textbooks of first-order logic it is treated as a meta-symbol).
v^-Form (gram (,p)) … [lDP]^
\(\forall x P\) is a p-Form.

Constants are also registered. Just put | in front of a variable.
word(,s) … |[lDP]
word(,c) … |[lDP]_
word(,p) … |[lDP]^
\(\mathrm{x} \in X\) and \(x \in \mathrm{X}\) are also p-Forms. \(\forall \mathrm{x} P\) is not a Form.

1.4 Various notations

In the source of a Form, a half-width space separates words.
Only before and after \((\) \()\) may the space be omitted. Example　 \(x \in ( X )\)

A word of arity 2 is basically written infix.
In fact, a word of arity 1 or more also has data called preced (only the order matters; the larger the preced, the weaker the binding).
It is intended so that the expressions of ordinary mathematics can be used. Example　 \(x = y \Rightarrow y = x\) ≈ \(( x = y ) \Rightarrow ( y = x )\)
Words of equal binding strength are usually read from the left. Example　 \(P , Q , R\) ≈ \(( P , Q ) , R\)
The binding strength of the binary propositional connectives is explained on the next page.
\(\forall\) binds more strongly than the binary propositional connectives. Note that \(\forall x x \in A \Rightarrow x \in B\) ≈ \(( \forall x x \in A ) \Rightarrow x \in B\) , which differs from \(\forall x ( x \in A \Rightarrow x \in B )\) .

A word whose notation is R is right-associative, e.g. \(\forall x \forall y P\) ≈ \(\forall x ( \forall y P )\)
A word \({\tt w}\) whose notation is F is used in the form \({\tt w}\)(\({\tt x}_1\) , … , \({\tt x}_n\)).
If you set the notation of \(\in\) to F in your own Book, you would always write it like \(\in ( x , X )\) .

★At present the preced and notation of a word cannot be changed from those in the DB.

1.5 tex computation and FCL conversion

Formel processes an input Form in two directions: computing the tex notation, and converting to FCL (Formel Core Language).
FCL is a language in a form easy to handle inside the machine; it is a nested array. The FCL conversion of \(\forall x \forall y P\) is [\(\forall\), \(x\), [\(\forall\), \(y\), \(P\)]].
This is sometimes an issue in natural language too. What about I think that that that that that boy wrote is wrong.?
We have been writing \({\tt F}\) ≈ \({\tt G}\) when the FCL conversions of \({\tt F}\) and \({\tt G}\) are equal.

default.formel registers \, \; \! !, _ ^ as word tex_only.
They are used only for the tex display and are ignored in the FCL conversion. Example　 \(x \; \in X\) ≈ \(x \in X\)
This holds only when written as a single word separated by spaces. The _ in X_ is part of the spelling and is a different thing.
{ } are invisible parentheses. In the FCL conversion they are the same as ( ). Example　 \(P , { Q \mathbin{\rm o\!r} R }\) ≈ \(P , ( Q \mathbin{\rm o\!r} R )\)