2 Mathelia logic

2.1 The cvt+ conversion

We make a Thm conversion called |cvt+ as follows.
Apply |cvt, and to each c-Form (not a v_-Form) that still remains, assign a constant with gram (s,p). For example, assign \({\mathrm{X}}\) to \(\mathrm{X}\).
Then replace \(x \in \mathrm{X}\) with \({\mathrm{X}} ( x )\) (detailed rules are in the AI tutorial).
For example
　( \(\mathrm{X} = \mathrm{X}\) ◀ O )|cvt+ … \(\forall x ( {\mathrm{X}} ( x ) \Leftrightarrow {\mathrm{X}} ( x ) )\) ◀ O

2.2 -|

Mathelia specifies the following.
　If \(\mathcal{T}\)|cvt+|0 is not an error,　\(\mathcal{T}\) holds in \(\mathbb{L}_*\) \(\Longleftrightarrow\) \(\mathcal{T}\)|cvt+|0 holds in \(\mathbb{L}_\mathrm{H}\)
The following abbreviation is often used.
　\({\tt P}\) -| \(\Gamma\) … (\({\tt P}\) ◀ \(\Gamma\))|cvt+|0

Here is an example of a theorem using classes, about the center of an operation. We also try a "constant within the Book" (let |C_ := `…` on source line 64).
word(ss,s) … \(+\)
\(\mathrm{C}\) … \(\{ x \mid \forall y \; x + y = y + x \}\)
\(\forall u , v , w \; u + ( v + w ) = ( u + v ) + w \Longrightarrow \forall a , b \in \mathrm{C} . \, a + b \in \mathrm{C}\) \(\blacktriangleleft\) O

2.3 The elim conversions

We also make a Thm conversion called |cls-elim.
It replaces a c-Form of the comprehension form \(\{ x \mid P \}\) with a constant of gram (,c) (e.g. \(\mathrm{X}\)) and adds \(x \in \mathrm{X} \Leftrightarrow P\) to the sos.
When the comprehension contains free variables, it is replaced by a symbol taking them as arguments (detailed rules are in the AI tutorial).
For example
　( \(y \in \{ x \mid x = x \}\) ◀ O)|cls-elim … \(y \in \mathrm{X}\) ◀ \(x \in \mathrm{X} \Leftrightarrow x = x\)

We also make a Thm conversion called |fn-elim.
It replaces a Form of the form \(\lceil x \mapsto X \rfloor ( t )\) , an applied arrow function, with \({\mathrm{F}} ( t )\) using a constant of gram (s,s) (e.g. \({\mathrm{F}}\)), and adds \({\mathrm{F}} ( x ) = X\) to the sos.
When the arrow function contains free variables, it is replaced by a symbol that also takes them as arguments (detailed rules are in the AI tutorial).
For example
　( \(\lceil x \mapsto x + a \rfloor ( b ) = b + a\) ◀ O)|fn-elim … \(\mathbin{\mathrm{F}} ( a , b ) = b + a\) ◀ \(\mathbin{\mathrm{F}} ( a , x ) = x + a\)
A word that takes an arrow function without applying it (e.g. Rest) is first opened by its definition and then |fn-elim is applied (detailed rules are in the AI tutorial).

2.4 --|

A simple operation on Thms is +sos. (\({\tt P}\) ◀ \(\Gamma\)) +sos \(\Delta\) is \({\tt P}\) ◀ \(\Gamma,\Delta\).
Mathelia also specifies the following.
　\(\mathcal{T}\) holds in \(\mathbb{L}_*\) \(\Longleftrightarrow\) \(\mathcal{T}\)|fn-elim|cls-elim +sos \(\mathbb{W}_\mathrm{c}.\) holds in \(\mathbb{L}_\mathrm{Hsc}\)
The following abbreviation is often used.
　\({\tt P}\) --| \(\Gamma\) … (\({\tt P}\) ◀ \(\Gamma\))|fn-elim|cls-elim +sos \(\mathbb{W}_\mathrm{c}.\)
The prf of the theorem above (source line 66) also passes with -| changed to --|.
\(\forall u , v , w \; u + ( v + w ) = ( u + v ) + w \Longrightarrow \forall a , b \in \mathrm{C} . \, a + b \in \mathrm{C}\) \(\blacktriangleleft\) O
Whether the two definitions of \(\mathbb{L}_*\) are equivalent has not been shown in general. A Thm is reviewed under the specification that was written (even if the same Thm passes under both, that is not a proof of equivalence).
The .thmel also describes for which range of Thms the equivalence is accepted (currently not yet described).

2.5 An example of a theorem where -| is an error and --| is the same as ◀

The following Thm does not pass if --| on source line 97 is changed to -|, because \(x \in A\) remains after |cvt+.
\(x \in \mathrm{B}\) \(\blacktriangleleft\) \(x \in A\)
This sos is the (too strong) claim that "every x belongs to every class A_".
A proof that makes explicit the substitution of \(\mathrm{B}\) for \(A\) (source line 101) can also be written.
\(x \in \mathrm{B}\) \(\blacktriangleleft\) \(x \in A\)

If we view s-Forms as "things (kinds of things)" and c-Forms as "boxes", ∈_ is the word expressing "is in".
One box \(X\) divides things into two kinds: "in \(X\)" or "not in \(X\)". One box alone cannot distinguish three points (pigeonhole principle).
\(\neg \begin{cases} x_{1} \in X \not\Leftrightarrow x_{2} \in X \\ x_{2} \in X \not\Leftrightarrow x_{3} \in X \\ x_{3} \in X \not\Leftrightarrow x_{1} \in X \end{cases}\) \(\blacktriangleleft\) O

In fact, prover+ can also decide \(\mathbb{L}_\mathrm{1sc}\) by an operation called relativization. The two theorems above also pass with the v; at the end of the prf changed to p;.