存在記号の除去規則について考える - 檜山正幸のキマイラ飼育記 (はてなBlog)「全称記号の導入規則について考える」の続編として、存在記号の除去規則について考えます。 存在記号の除去規則の背景は比較的に簡単な事実です。にも関わらず、記号を換えたり書き方を縦にしたり横にしたりのどうでもいいワチャワチャが事情を見えにくくしています。この記事によって、ワチャワチャな作業（記法のあいだの翻訳）に慣れて、その“どうでもよさ”（記法が変わっても内実は変わらないこと）を感じていただければ幸いです。 内容： 存在記号の除去規則 限量随伴性 引き戻しと存在限量子の随伴性 随伴性を証明に利用する 随伴性からサイド証明へ メタ循環構造 存在記号の除去規則 標準的な自然演繹における「存在記号の除去規則」は次の形に書かれます。 P(a) : : ∃x.P Q -------------[∃除去] Q僕は、自然演繹に愚痴を言い、悪態をついてます（「自然演繹はちっとも自然じゃない -- 圏論による
Amazon.co.jp: Type Theory and Formal Proof: An Introduction (English Edition): Nederpelt, Rob, Geuvers, Herman: Digital Ebook Purchas
