スケッチ #329

国籍の立証のトポス意味論：証明対象・support・必要書類 【位置づけ】 対話から作成したAI生成ノート．James Haydon の “Solving Passport Application with Haskell” に着想を得た数学的モデルであり，英国国籍法の完全な形式化ではない．法的地位の存在，証拠による立証可能性，個々の証明経路を区別する． 【構成】 有効性が確認された書類トークンの集合 D と，有限前提を持つ小さい規則系 R を固定する．法令・評価対象時点も固定し，書類の追加は既存の導出を無効化しないと仮定する．P = (P_fin(D), ⊆)，E = [P, Set] とする．これは P に共変，P^op 上の前層トポスである． 申請者 x の結論 Q_x を導く，具体的な証拠葉を持つ有限証明木 π の書類集合を S_π とし， Π_x(Γ) = {π | π は Q_x の証明木，S_π ⊆ Γ} と定義する．包含に沿って同じ木を送るので Π_x は E の対象となる．B_x = im(Π_x → 1) とすると， Γ ⊩ B_x ⇔ Π_x(Γ) ≠ ∅． B_x は「現時点の証拠から立証できる」という命題であり，外界における資格そのものではない．証拠解釈と規則が健全なら，有限木の帰納法により立証から外的資格が従う．逆向きには規則の網羅性と証拠の入手可能性が必要である． 【真理値と証明の区別】 Ω(Γ) = Up(↑Γ)，Ω(Γ ⊆ Δ)(U) = U ∩ ↑Δ． 分類写像は χ_{B_x,Γ}(*) = {Δ ⊇ Γ | Π_x(Δ) ≠ ∅} を与える．真理値は確信度ではなく，成功する将来の書類状態全体である． h_S = P(S,−) とすれば Π_x ≅ ∐_π h_{S_π}， B_x = ⋁_π h_{S_π} ∈ Sub_E(1)． 証明：Γ 成分で余積を評価すると，S_π ⊆ Γ を満たす各 π に一元が対応する．像を取ると存在の有無だけになり，join の式が従う． 従って，同じ書類集合を使う異なる証明木は Π_x に残るが B_x では同一視される．一方，十分な書類の組合せは B_x の上方閉集合として残る．たとえば a と b の両方，または c だけで足りる玩具例では， B = ↑{a,b} ∪ ↑{c}． その極小元 {a,b}, {c} が極小十分書類集合である．有限状態であることにより，任意の十分状態の内部に極小十分状態が存在するが，候補全体が有限とは限らない．理由提示には Π_x，書類候補の提示には B_x，費用最適化には追加の費用データが必要となる． 【否定についての注意】 Heyting 否定は Γ ⊩ ¬B_x ⇔ ∀Δ ⊇ Γ, Π_x(Δ) = ∅ である．これは「今は証拠がない」でも，「非英国人であることを立証した」でもない．後者には別の証拠対象と support が必要である．上の玩具例では空状態で B も ¬B も成立せず，排中律が失敗する． さらに P は directed なので，B が一箇所でも成立すれば ¬B = 0，¬¬B = 1 となる．証明：任意の Γ と十分状態 S に対して Γ ∪ S が共通拡張である．これは全書類の自由な併合を許したモデルの帰結であり，法的地位の性質ではない．入手不能性・情報の非両立性を表すには許される状態と拡張を制限する必要がある． 【再帰】 結論ラベル集合 A，直接証拠の対象 E_a，結論 a の規則 r の前提 a(r,1),…,a(r,n_r) に対して，E^A 上で F(Z)_a = E_a + ∐_{r:concl(r)=a} ∏_{i=1}^{n_r} Z_{a(r,i)} と置く．有限証明木の族 Π はこの多項式関手の初代数となる．根による分解が F(Π) ≅ Π を与え，任意の代数への一意射は木の構造再帰で得られる．support は直接証拠からの規則閉包の最小不動点であり，有限前提なので高さ有限の段階の合併で得られる．循環規則 A ⇒ A のみからは A は生成されない．有限証明による意味論は，探索手続の停止を保証しない． 【適用範囲】 反証・偽造の発覚で撤回される「現在の認定」は，単純な証拠包含に関する部分終対象では表せない．証拠評価と判断改訂には追加の意味論が必要である．法改正の時間と証拠増加の順序も区別しなければならない． 肯定的規則を幾何理論 T として形式化でき，support の最小閉包が E 内の T-モデル M を与える場合，分類トポスの普遍性から f_M:E→Set[T]，f_M^*U_T≅M を得る．E は証拠状態，Set[T] は規則の全モデルを担う．Horn 公理だけでは最小閉包や証明木は指定されない． 【参照】 James Haydon, Solving Passport Application with Haskell: https://jameshaydon.github.io/passport/ GOV.UK, Born outside the UK or stateless: https://www.gov.uk/check-british-citizenship/born-outside-the-uk-or-stateless HM Passport Office, Balance of probabilities: https://www.gov.uk/government/publications/balance-of-probabilities-caseworker-guidance/balance-of-probabilities-accessible Olivia Caramello, Topos Theory, Lectures 7–14: https://www.oliviacaramello.com/Teaching/Lectures7_to_14.pdf Olivia Caramello, Topos Theory, Lectures 21–22: https://www.oliviacaramello.com/Teaching/Lectures21_22.pdf