book集

!txt min.thmel — 最小の Thmel（2026-09-01 須田さん）
!txt
!txt ★★★**Formel は {s,c}-ソート言語なので、backendへ送るときもソートを保つ**。
!txt   素の `◀` は一階翻訳を通らない。Prover+へはソートを一項述語にした相対化、Vampire+へは
!txt   多ソートTFFとして送り、元の関係 `◀sc` を確かめる。
!txt   `-|` だけが、Thm全体を `|0` で「高階言語」へ翻訳し（c-Formが残っていれば失敗）、
!txt   結果の `◁` のThmを確かめる（`0_tutorial_jp/3.book`「Thmの変換」「論理」節の `(P ◀ Γ)|0` が正本。
!txt   ★★2026-09-14夜 訂正＝以前ここは「単ソートの関係 `◀1` を確かめる」だったが、
!txt   goal・sosを個別に翻訳する規則はBookに無い（須田さん指摘）ため撤回。中身（FCL→TFL・cvt）は
!txt   不変で、名前だけ `|1` から `|0` へ変わった＝「`|0`は以前の`|1`」（須田さん））。
!txt
!txt ★`backend` は**宣言**＝どの文字がどの投げ先を指すか（prf の段 `G ◀ Γ p;` の `p`）。
!txt ★`target` は**制限**＝ここに書いていない投げ先へ投げる綴りは理由付きで拒否される。
!txt ★★2026-09-14＝**`s=satallax+` を追加**（`-| … s;`＝単ソートMCL→TFLのみ。多ソート`--| … s;`・
!txt   命題変数量化`---| … s;`はまだSatallax+ backend実装の対象外＝この本が書けるのは`-| … s;`だけ）。
backend p=prover+ v=vampire+ s=satallax+ h=hyperion
target p v s h

!txt ★★★**この本の対象言語が持つソート**（2026-09-02 須田さん「.thmelファイルで指定する。
!txt   min.thmelではs,cのみ。少なくとも最初の説明では f は出さないで欲しい」）。
!txt   ★**Formel は {s,c}-ソート言語**なので、min はその2つ。
!txt   ★**`f`（関数値のソート）は書かない**＝`\fn` / `ap` / `Rest` を送るときに翻訳の側で生まれる
!txt     ソートで、min.formel はその語を持たない。**書いていないソートが出たら理由付きで拒否される**
!txt     （`target` と同じ「制限」）。
!txt   ★**効くのは多ソートを送る道**＝Vampire へ出す TFF の型宣言（`tff(mathel_s: $tType).` …）。
!txt     相対化して Prover9 へ送る道の Ax は、これとは別に**実際に出たソートだけ**に添える
!txt     （型宣言は仮定を増やさないが、非空性の公理は仮定を増やすため）。
sort s c

!txt ★**翻訳の宣言**＝この本が使ってよい翻訳。一階翻訳と{s,c}ソート翻訳の両方（2026-09-06 須田さん決定）。
!txt   ★★min は `--|` の `inference` 行を持たない＝この本では `--|` は書けない（2026-10-09 注）。
!txt   ★2026-10-04 現状へ直した＝以前ここにあった「`◀ … v;` は Thm査読を通らない」は古い。今は通る（0_tutorial_AI/3.book の例）。
!txt   ★★★2026-09-06 その2＝翻訳の名前を`TFL`/`TML`から論理の添字`1`/`sc`へ戻した
!txt   （`◀1`/`◀sc`と同じ添字）＝「対象言語に新しい名前を立てる」よりも「使う論理の名前で
!txt   直接呼ぶ」方が説明が要らない、という判断（`0_tutorial/3_Thmel.book`（旧）「一階翻訳、
!txt   {s,c}ソート翻訳」節）。
!txt   ★★★2026-10-09 須田さん「min.thmel では Wc. を sos に追加しない」＝min は Wc.（〇.＝gram に c を含む語の定義・
!txt   旧名 W+.）を足さない。足すのは `--|` の行 `(goal ◀ sos)|cls-elim +sos Wc.` を書いた本だけ（default・zf）。
!txt   ★★2026-09-14夜＝`-|` が使う翻訳の名前を `1` から `0` へ改称した（`|0`＝Thm全体への翻訳。
!txt   下の「一階翻訳の宣言」を参照）。`L_1`（prover+が判定する論理）という名前自体は不変で、
!txt   変わったのは`.thmel`内部の翻訳トークンの綴りだけ。
translate 0 sc

!txt ★★**`◀` が何を意味するかを綴る行**（2026-09-04 須田さん＝右辺は `◀1` ではなく `◀sc`）。
!txt   `◀sc` ＝ **{s,c}ソート論理と v^-Form のみを含むメタ論理**の推論関係（`0_tutorial_jp/3.book`「論理」節・旧 `0_tutorial/3_Thmel1.book`
!txt   「命題変数を含むThm」節が正本）。**ソートを消さない段**＝素の `◀` はここで検査する。
!txt   ★下の `-|` とは段が違う＝あちらはThm全体を `|0` で「高階言語」へ翻訳した後の段（`◁`）。
!txt   ★**各ソートの非空性は、この論理を名指しした時点で最初から入っている**（多ソート構造の
!txt     標準的な定義そのもの＝単ソート一階論理で領域が空でないのと同じ立場）。Mathelia が
!txt     足しているのではないので「暗黙」ではなく、**論理を正しく名指ししているだけ**。
!txt   ★**この行は式を1本も増やさない**＝ソート宣言そのものが持つ性質を、名前で引き受けている。
!txt   ★この行のとおり、素の `◀` の段は Wc. を足さない（2026-10-09・0_tutorial_jp/3.book の規定 `T holds in L_* ⟺ T holds in L_Hsc`）。
inference goal ◀ sos <-> goal ◀sc sos

!txt ★★**`|0`（Thm全体への翻訳）の宣言**（2026-09-01。旧称 TFL翻訳。★★2026-09-14夜＝
!txt   翻訳の名前を`1`から`0`へ改称し、右辺をgoal・sos個別の`◀1`から「Thm全体を`|0`で
!txt   変換する」形`(goal ◀ sos)|0`へ訂正＝`0_tutorial_jp/3.book`「Thmの変換」節の
!txt   `P -| Γ … (P ◀ Γ)|0`が正本。中身は不変、綴りだけの訂正）。**この行が無いと c を使った
!txt   Thm が査読で拒否される**（実測＝「この本の Thmel は「高階言語」への翻訳を持ちません」）。
!txt   ★`min.formel` は c を持つ（`∈_` `∀_ ∃_` `=_`）ので、この行は**必須**。
!txt   ★この行は `-|` の翻訳を引き受ける宣言であり、素の `◀` の検査経路は変えない。
!txt   ★★2026-10-07 須田さん「cvt が出てこないものを作るために min.thmel を用意した」＝**min は |cvt+ を掛けない**
!txt   （09-29 に default の -| を |cvt+|0 にしたとき、行の完全一致の都合でここも変えていたのを戻した）。
!txt   クラスの語（c-Form）を含む段は |0 がエラー＝査読の失敗。クラスは素の ◀（◀ … v;）で扱う。
inference goal -| sos <-> (goal ◀ sos)|0

!txt ★`--|` の行は書かない（2026-10-09）＝書くと Wc. を足すことになる（default.thmel の
!txt   `inference goal --| sos <-> (goal ◀ sos)|cls-elim +sos Wc.`）。min はクラスを素の `◀`（`◀ … v;`）で扱う。

!txt ★`search:` の印が付く行は**探索設定**＝同じ問題を同じ形で投げ、待つ長さだけが変わる。
prover9 search:seconds 10

common/min.thmel

`common/min.thmel`