Re: Why?

Alan Smaill wrote:
If your classical analogue is set theory (and you're not interested in
the details of the representation of notions from analysis) then you
can look for example at the axiomatisation of the Calculus of Constructions
in wikipedia (this is the base system implemented in Coq):

en.wikipedia.org/wiki/Calculus_of_constructions

Thanks, Alan. This gives me a good signpost to follow, and incentive to
get more conversant in lambda calculus as well.

MoeBlee

.

Loading