1 Basics of Thmel

1.1 Header settings, props and Thms

Thmel is the software that handles inference relations between p-Forms. Its settings are written in a .thmel file.
If none is specified in the header, default.thmel is loaded. This Book is such a case.
The header line import /common/word_logic loads the words of logic (\(\top\), etc.). So this Book can use them without introducing them.

A p-Form of Formel registered as a constant of Thmel is called a prop.
For a prop \({\tt P}\) and a sequence of props \(\Gamma\), something of the form \({\tt P}\) ◀ \(\Gamma\) is called a Thm. \({\tt P}\) is sometimes called the goal and \(\Gamma\) the sos.
For example,　\(\top\) ◀ O　is a Thm. O is the empty sequence. Instead of a prop, a formula can also be written directly like `⊤` (a prop without a name).
When the sequence has two or more members, separate them with , in the source (displayed as "，").
When the reviewer reads a Thm, it converts each prop into FCL with Formel (this is called the eval of the Thm).

To put a prop in a Book, write a line starting with prop in the source. Besides using one registered in the DB, you can also make your own by writing <-.
To put a Thm in a Book, write a line starting with thm in the source. There is also prop/thm, which introduces a prop and writes the Thm at once (source line 133, etc.).
When you want to use the p-Form that a prop \({\tt P}\) points to inside a Form, write @\({\tt P}\). It is better not to overuse it.

1.2 Converting Thms

Converting a Thm into a Thm is important in Mathelia.
The logics each backend can handle differ (next section), so a Thm is converted into a Thm of a language that backend can handle before it is thrown.

The simplest example is converting the language a Thm belongs to.
Forms are a higher-order {s,c}-sorted language. Regarding a "higher-order language" as existing separately, we make a Thm conversion |0.
　If \(\mathcal{T}\) contains no c-Form as a sub-Form, \(\mathcal{T}\)|0 = (the natural translation of \(\mathcal{T}\) into the higher-order language); otherwise \(\mathcal{T}\)|0 is an error
Thms of the higher-order language are made with ◁ instead of ◀ (a symbol used only in explanations). Also, Forms are shown in green when we want to make clear that the language is different.
Example　(\(\top\) ◀ O)|0 \(=\) \(\top\) ◁ O
For a Thm \(\mathcal{T}\), the eval of \(\mathcal{T}\)|0 is obtained by evaluating \(\mathcal{T}\) and then computing |0.

1.3 Logics

A Thm is a formal thing. What gives meaning to a Thm is called a logic.
When a Thm \(\mathcal{T}\) can be handled in a logic \(\mathbb{L}\) and ◀ can be read as "can be inferred", we write \(\mathcal{T}\) holds in \(\mathbb{L}\).
In Mathelia, higher-order {s,c}-sorted logic \(\mathbb{L}_{\rm Hsc}\) and higher-order logic \(\mathbb{L}_{\rm H}\) are taken as known.
Usually their sublogics, first-order {s,c}-sorted logic \(\mathbb{L}_{\rm 1sc}\) and first-order logic \(\mathbb{L}_1\), are used.
For example, the axioms of \(\mathbb{L}_1\) include the equality axioms and the axiom of non-emptiness of the domain \(\exists x \, ( x = x )\) .

A backend "decides \(\mathbb{L}\)" means "it receives a Thm \(\mathcal{T}\) and returns 〇 when it could confirm \(\mathcal{T}\) holds in \(\mathbb{L}\)". The logic each backend decides is
　prover+ … \(\mathbb{L}_1\)
　vampire+ … \(\mathbb{L}_\mathrm{1sc}\)
　satallax+ … \(\mathbb{L}_\mathrm{Hsc}\)

1.4 Theorems and their prf

Mathelia specifies its own logic \(\mathbb{L}_*\). Things of the form \(\mathcal{T}\) holds in \(\mathbb{L}_*\) should be called "theorems".
If no "word whose gram contains c or ( )" occurs in \(\mathcal{T}\),
　\(\mathcal{T}\) holds in \(\mathbb{L}_*\) \(\Longleftrightarrow\) \(\mathcal{T}\) holds in \(\mathbb{L}_\mathrm{Hsc}\) \(\Longleftrightarrow\) \(\mathcal{T}\)|0 holds in \(\mathbb{L}_\mathrm{H}\)
The specification for when a "word whose gram contains c or ( )" occurs in \(\mathcal{T}\) is in 4.book.

In a Book, a prf is written after a Thm (it is not displayed, so when discussing a prf, look at the source file).
The prf after a Thm \(\mathcal{T}\) is something that can be regarded as a proof of \(\mathcal{T}\) holds in \(\mathbb{L}_*\).
A prf is what the reviewer looks at in the Thm review. Abbreviations for the backends are used: p=prover+ v=vampire+ s=satallax+ h=hyperion
A prf contains, for example, P ◀ Γ v;. Seeing it, the reviewer evaluates \({\tt P}\) ◀ \(\Gamma\) and throws it to vampire+.

For Thms in which no "word whose gram contains c or ( )" occurs, the following abbreviation is used (it just changes the language).
　\({\tt P}\) -| \(\Gamma\) … (\({\tt P}\) ◀ \(\Gamma\))|0
A prf also often contains P -| Γ p;. Seeing it, the reviewer evaluates \({\tt P}\) -| \(\Gamma\) and throws it to prover+.

"Which backend to throw to in which case" is summarized with measured examples in the AI tutorial.