自然演繹とは？

しぜんえんえき

仮定の導入・消去を基本とし、人間の推論スタイルを形式化したゲンツェンの証明体系だよ。

自然演繹とは、ゲンツェンが考えた証明の体系で、「仮定を立てて、使ったら消す」という自然な推論の流れを形式化したものだよ。各論理記号（∧、∨、→ など）に「使う規則」と「作る規則」が決まっているよ。コンピュータの型理論とも深く関係しているよ。