2021-01-10から1日間の記事一覧

全称限量子とタプル

(X∋x Px) がパラメトライズ(インデックス、パラメトリック)族だとする。これを全称束縛すると、∀x∈X.Px となるが、これは タプル 〈Px〉x∈X と書いても同じ。 x∈X. Px 命題族 -------------------- ∀x∈X.Px 単一命題 x∈X. Px 型族 ------------------- Π(P…

自然演繹とLean

Leanの推論規則 - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。https://leanprover.github.io/logic_and_proof/nd_quickref.html に自然演繹のまとめがある。それに従うが、双含意〈bi-inplication〉は除く。 論理記号 導入 消去 Implication ラムダ抽象…