Mathelの補足②
Mathelは高い表現力と分かりやすい仕様を両立するよう開発されています。
通常の数学で使用される表現はすべて可能、使用例を見ればすぐに自分でも使えるものを目指して。
ただし不明な点はエージェントに聞くべきです。
\(\mathbb{W}_2\)(\({\tt x}\)\({\tt y}\),p→\({\tt x}\)\({\tt y}\),p) … \({\tt /}\)
使用例として \(x \notin X\) ≃ \(\neg ( x \in X )\)
集合の量化だけでなくクラスの量化もできます。 \(\forall X P\) や \(\forall X P\) のように。
\(P\) はv^-Formで命題を動く変数です。
通常の数学で使用されなくても良いものであれば導入されます。
例えばクラスが「集合となる」ことを表す述語 \(\dot\exists\) があり、次で定義されます。
Exi. … \(\dot\exists C \Longleftrightarrow \exists X \, ( X = C )\)
MathelはRusselのパラドクスを端的に表現できます。 \(\neg \dot\exists \{ x \mid x \notin x \}\)
翻訳には4段階必要です。 ≃ \(\neg ( \exists X ( \forall x ( x \in X \Leftrightarrow \neg ( x \in x ) ) ) )\)
\, \; \! { } _ ^ はtex cmdになるだけのwordです。
\(\text{id}\) というword(s,s)があります。「\(X\)上の恒等写像」は \(\text{id} X\) ではなく \(\text{id} _ X\) とされることが多いです。
Mathelの補足③
次のような条件付きの形でもslash計算ができます。Cap. … \(\mathcal{X} \neq \emptyset \Longrightarrow \bigcap \mathcal{X} = \bigcap \mathcal{X}\)
\(\mathrm{P} \Longrightarrow \mathrm{A} \Leftrightarrow \mathrm{B}\) と \(\mathrm{A} \Longleftrightarrow \begin{cases} \mathrm{P} \Rightarrow \mathrm{B} \\ \neg \mathrm{P} \Rightarrow \mathrm{A} \end{cases}\) が論理同値であることに注意しましょう。