4 章 はじめの部分の誤訳について

[Seasawher]

「型としての命題」の考え方に従って、Calculus of Constructionsでは、従属関数型と全称量化子を同一視する。つまり、任意の項 p に対して、∀ x : α, p は (x : α) → p の代替表現に過ぎず、p が命題のときは、後者の表現の方が自然である、と考えるのである。

原文は

The Calculus of Constructions therefore identifies dependent arrow types with forall-expressions in this way. If p is any expression, ∀ x : α, p is nothing more than alternative notation for (x : α) → p, with the idea that the former is more natural than the latter in cases where p is a proposition.

「後者」の部分は former なので，前者だと思います．

[aconite-ac]

ご指摘ありがとうございます。 明らかな誤訳ですので、ご指摘頂いた部分を修正後、同様の誤訳がないかどうか全文を確かめます。