作成日：2026-10-18。状態：研究用の定義と手作業の導出。形式証明支援系による検証、実装、独立確認は未実施です。設計比較と D06、R4 の評価 と対応します。最終目標全体の証明ではありません。
1. 意味を固定する単位
一つの意味プロファイル L は、語彙、文、モデル、充足・含意、問い合わせの回答方法を定めます。プロファイルの版、理論 T、その依存先、データ D、用途と採用方針 P を固定して初めて、回答の再現を要求できます。
以下の S1〜S3 は、非空の台集合を持つ通常の一階述語論理で考えます。旧語彙 Σ には旧記録・問い合わせが使う記号を含め、個体名と型の解釈も固定します。新しいソート・関数・個体存在公理は、ここでの自動認定の対象外です。T と旧データ D のモデルがある場合には、その整合性も拡張で維持できることを示します。
これらは本プロジェクトが使う小さな十分条件です。先行研究の locality 全体を実装したものでも、任意の拡張の必要十分条件でもありません。十分条件による保証と併用の条件を区別する根拠は Cuenca Grau ほか、§5 にあります。
2. S1：新しい述語を既存の式で定義する
条件
旧 Σ にない n 項述語 N を一つ導入し、次の公理だけを追加します。
∀x1…xn (N(x1,…,xn) ↔ ψ(x1,…,xn))
ψ は旧語彙だけで書かれ、自由変数は表示した変数の範囲、型も旧側のものです。旧定義・旧データ・旧記号の解釈を変えず、N について別の条件を同時追加しません。
導出
T∪D の任意のモデル M を取ります。台集合と旧記号の解釈を変えず、N の解釈を「M で ψ を満たす組の集合」として定めた M+ を作れます。この M+ は追加定義を満たします。逆に追加後のモデルを旧語彙へ制限すると、元の T∪D のモデルです。
したがって、任意の旧語彙の文 φ に対して、前後の含意は一致します。定義追加後に φ が含意されても旧側で非含意だったと仮定すると、旧側の反例モデルを M+ に拡張できてしまい、矛盾します。逆方向は旧理論がそのまま含まれることから従います。
これは、条件内のすべての旧データ D・旧文 φについての小さな導出です。一つの記録で回答が一致したというだけの確認とは異なります。ただし、新語彙を含むデータの追加や、ψ の医学的正しさを保証しません。
多数の定義と併用
新述語 N1,…,Nk の右辺が、旧語彙とそれより前に定義した述語だけを参照するなら、依存順に同じ構成を繰り返せます。有限の依存非循環な定義群に拡張できます。
二つのモジュールの新述語が互いに異なり、それぞれ旧語彙と自モジュールの前の定義だけを参照する場合、両方の解釈を旧モデルの上に構成できます。追加順にも依存しません。相互参照を許す場合は、全体の依存順と定義の一意性を確認します。単独の結果だけを併用の保証に流用しません。
同名の述語の定義が異なる、古い定義を上書きする、循環する場合はこの認定から外します。それだけで意味が破綻したとはせず、別の証明・反例探索を要求します。N↔¬N は実際にモデルを失う例ですが、すべての循環定義がこの例と同じとはしません。
3. S2：空でもよい新しい下位概念
新述語 N を導入して ∀x(N(x)→ψ(x)) だけを加え、ψ は旧語彙の式とします。N に存在・非空・個別所属を要求しなければ、どの旧モデルでも N=∅ とする拡張が作れます。旧文の含意は S1 と同じ理由で保存されます。K02 はこの型です。
ここで N(a) という新観察を加えれば ψ(a) が新たに導けます。それは旧データ固定の定理の前提外で、必ずしも誤りではありません。定義拡張、データ追加、採用判断の変更を別に記録する必要があります。
K03・K04 のように A→N と N→B を加える場合、旧側の A を N に入れなければならず、N を空にする構成は使えません。新しい名前であることや、各モジュールに一枚の認定票があることだけでは安全を認定しません。
4. S3：有限回の保存と保証範囲
同じ L、旧語彙 Σ、旧データ集合 𝒟、問い合わせ集合 Q を固定し、各更新がこの範囲の回答を保存するとします。基底と等号の推移性により、どの有限の更新回数 n に対しても最初と n 回目の回答は一致します。S1・S2 は、その各段階を認定する具体的な入口になります。
新しい言語を必要とする更新、依存先の無断変更、記録の訂正、旧側へ新たな制約を加える更新には、この定理をそのまま適用しません。無限列の極限や、まだ定義していない全将来の意味を取り込めることも示していません。最終目標に対して示せたのは、条件内の拡張回数で保証が弱まらないことです。
5. C1：コア・意味言語が変わるとき
旧理論 T0 と新理論 T1、旧問い合わせ範囲 Q を固定します。文の移し方 e と、新モデルを旧モデルとして読む対応 r を別に定義します。
r : Mod(T1) → Mod(T0)
すべての M′∈Mod(T1), φ∈Q について
M′ ⊨ e(φ) ⇔ r(M′) ⊨ φ
さらに、旧理論の各モデル Mに対して r(M′)=M となる新モデル M′ があることを要求します。旧モデルを覆うこの条件まで成立すれば、T0⊨φ ⇔ T1⊨e(φ) が従います。旧側の反例を新側にも持ち上げられるため、新側でだけ旧文が確定することを防げます。
なぜ充足条件だけでは不足するか
旧側は A,B に制約なし、新側は A⊑B を加えたとします。文をそのまま移し、新モデルを同じ旧語彙で読めば、各モデル内の文の意味は変わりません。しかし、旧側の A={u},B=∅ というモデルは新側へ持ち上がりません。旧側で非含意だった A⊑B が新側で含意されます。モデル内の対応と、理論全体の意味保存は別です。
institution の原著でも文・モデルの対応と、推論を移す際のモデル側の条件を区別しています。Goguen・Burstall、§4.1、Definitions 32・34、Proposition 35。上の e/r の向きと範囲は本プロジェクトの契約です。原著の institution morphism の命名・向きをそのまま借りた定義ではなく、圏論的な全構造を実装・検証した主張もしません。
合成
0→1 と 1→2 がこの契約を満たし、第一の変換結果が第二の対象範囲に入るなら、e02=e12∘e01、r02=r01∘r12 と置いて充足条件を二回適用できます。各 r のモデル被覆も合成できます。したがって同じ保証範囲で含意を保存できます。
途中で射影や近似があった場合、保存を宣言できる Q を狭め、各段階と全行程の差を記録します。コア版を増やすだけでこの条件を満たしたとはしません。旧解釈を別に実行し続ける経路は、移した新解釈の保存とは別の再現手段です。
C1-a：役割付き関係へ移す具体的な構成
契約の存在だけで終わらせないため、型付きの関係表から役割付き事象へ移す一例を構成します。旧側の記号は四項関係 O(k,s,m,v) で、記録 ID、検体、方法、結果を表します。各引数の旧ソートは非空、Q はこの旧語彙の一階文です。旧理論 T0 に書かれた制約以外を暗黙には足しません。
新側では旧ソートを残し、新しい事象ソート E、活動する事象を選ぶ述語 Active、四つの役割関数 key,specimen,method,value を使います。旧 O は次の式へ移します。論理結合と旧ソートの量化はそのまま移し、変数捕獲を避けます。
e(O(k,s,m,v)) =
∃z:E (Active(z) ∧ key(z)=k ∧ specimen(z)=s
∧ method(z)=m ∧ value(z)=v)
新モデル M′ から、上の右辺が成立する四つ組を O の解釈にして旧モデル r(M′) を作ります。旧ソートの解釈は変更しません。原子式での一致と式の構造に関する帰納法から、充足条件が成立します。T1 は移した e(T0) とこの型構造で、旧側への無関係な制約は追加しません。同じ四つ組を持つ複数の原主張に別々の事象定数を割り当てても、被覆のために定数を同じ要素へ読めるよう、事象定数どうしの不等式（一意名仮定）は T1 に含めません。
任意の旧モデル M に対し、新 E の台集合を Oの四つ組の集合 ⊔ {予備要素} とし、Active は四つ組側だけ、各役割関数はその射影とします。予備要素の役割には各非空の旧ソートの任意の値を置けます。O が空でも E は非空です。旧ソートは固定したまま r(M′)=M となり、モデル被覆も示せます。よってこの条件では旧 Q の含意を保存します。
同じ値集合を持つだけでは足りず、四役割が同じ z に結び付くことが重要です。後から Active の全件数、事象の重複禁止、役割値の一意性を越えた業務制約等を加えるなら、旧 T0 と対応するか再確認します。旧語彙にない新 E 自体の問い合わせ、履歴・確率の意味、任意のグラフへの同様の保証はこの構成の対象外です。P0 でこの量化を一般に実行できるという主張でもありません。
6. R1：訂正しても過去の主張を消さない
履歴 H にある「h が φ を主張した」という記録と、用途別に φ を採用することを分けます。主張を記録しただけでは φ を事実として推論しません。用途・対象時点・参照時点・方針版 P を指定する選択 Select(H,P) が、採用した主張集合と理由を返します。
今回の最小方針は、明示的な訂正・撤回関係と人の確認状態を使う部分的な選択です。「最新なら正しい」「AI の確信度が高ければ確定」といった一般則は採用しません。裁定のない衝突は未解消として返します。
履歴を追記する場合、過去のスナップショットH0・定義T0・方針P0 を参照する問い合わせの入力は変わらないので、その解釈を再現できます。現在の Select(H1,P1) の結論まで一致するとは要求しません。この二つを区別することで、誤った知識の訂正と過去の記録の解釈を両立させます。
本方針は AGM の改訂演算や公準の採用ではありません。また、履歴の再現には原実体・意味仕様・依存先の保存と利用可能性が必要で、論理の式だけから運用上の永続保存は保証できません。
7. G1：関係を保持する表現
架空の二検体を次のように表します。記法は説明用です。
観察 e1: 検体=s1, 方法=m1, 結果=陽性
観察 e2: 検体=s2, 方法=m2, 結果=陰性
意味は各観察を単位とする役割付きの組です。「s1・s2、m1・m2、陽性・陰性」という三つの集合とは異なります。グラフ、関係テーブル、木のいずれでも、事象 ID と役割参照を通じて同じ結合を保持できれば、この有限例の問い合わせを保存できます。
二項の辺へ事象化する場合も、役割の必須性・多重度、参照の同一性、同じ観察への所属を定め、読み戻しで元の役割付き組に戻ることを確認します。グラフを使ったというだけで、任意の高階関係・時間・確率を表現できたとはしません。新しい役割の意味や制約は、別に定義して検証します。
8. U1：失った区別を出力だけから回復できない
二つの元記録 d1,d2 が異なる問い合わせ q の回答を持つのに、射影 f が f(d1)=f(d2) にしてしまうとします。f の出力だけを読む決定的な処理 g は、両方に同じ回答を返します。元の異なる正解を両方とも回復することはできません。
これは関数の同じ入力から同じ出力が得られることによる簡単な導出で、特定の外部論文の不可能性定理を引用したものではありません。失われた含量を原記録や採用済みの追加情報から回復する処理は可能ですが、それは f(d) 単独の復元ではなくなります。E13・E14 と、操作にない情報を接続先が要求する K14 に適用します。
この制約は最終目標の否定ではありません。新体系の設計では、区別を初めから保持すること、喪失した位置を記録すること、追加の観察が必要ならその必要性を明示することが重要になります。
9. 意味を表せる範囲と最初に計算する範囲
研究モデルでは有限アリティの関係、個体・事象、文脈付き主張、版付き定義と意味プロファイルを区別します。一階述語論理は S1〜S3 と K01〜K05 を形式化する最初の意味プロファイル候補です。任意の一階理論を完全判定する推論器を約束しません。
| 層 | 最初の検討範囲 | 範囲外 |
|---|---|---|
| 記録・参照 | 有限の役割付き事象、主張、明示的な欠落理由、定義・依存版の固定 | 暗黙の最新定義、既定の対象者・否定・確度の補完 |
| 計算プロファイル P0 の候補 | 有限記録に対する肯定・明示否定の参照、結合問い合わせ、有限の非循環な定義展開。否定による閉世界補完はしない | 任意の量化式・循環規則・一般の充足不能判定・存在証人の自動生成 |
| 保存の認定 | S1・S2 の構文条件と依存閉包を満たす更新を認定する手順 | 認定外の全更新の安全／危険の完全判定 |
| 別意味のモジュール | 明示的な意味定義、問い合わせ能力、旧側への接続または停止条件 | 任意プログラムを読ませれば自動的に意味を理解した扱い |
P0 の欠落した回答は「明示的に否定」ではありません。対応する問い合わせ断片で完全な回答が得られると示した範囲だけ「導けない」を返し、未対応の式・計算打切りは別状態にします。否定は観察・採用した主張の情報であって、全世界に対する知識の完全性を主張しません。
P0 だけの試作が動いても、存在問い合わせの K05 や意味能力変更を含む R4 全体への合格とはしません。表現モデル、形式的な分析、実装で動く断片を区別し、R6 で実装対象をさらに絞る場合は未対応を明示します。
K11 のための具体的な追加意味の小例
予測モジュール Prob-1 を、対象 a・区間 [t,t+7] の X について、可能な二つの状況 Ω={wX,w非X}、重み 7/10,3/10、事象 E={wX} を持つ有限確率モデルとして定義できます。モデル m が Pr(E)=7/10 と予測したことを記録します。確率の意味はこの重みの和です。X が実際に発生したとは主張しません。
対応済みの消費側は、対象・区間・モデル・事象・重みから予測の意味を取得します。未対応側は予測主張を未解釈として保持し、確定 X への変換を停止します。一般の連続確率・因果・校正・臨床的妥当性への対応はこの小例では示していません。P0 に数値の保存能力があるだけでは Prob-1 の意味対応に数えません。
10. 次の証明・反証
S1・S2 の認定条件を満たす追加と、満たさない K03・K04 を同じ手順で区別できるかを試作で確認します。G1 の結合と R1 の履歴を保持する具体的な内部表現を R6 で定め、読み戻しと問い合わせを検証します。C1-a では一組の表現間の e/r とモデル被覆を手作業で構成しました。確率・時間・異なる否定等の意味プロファイル間の同様の構成は未完了で、一般的な言語間保存の完成を意味しません。