June 2001
Intermediate to advanced
2128 pages
82h 43m
English
The ideas we have discussed so far have been directed toward proving theorems of the system
of elementary type theory, which lacks the axioms of Extensionality and Descriptions of the full system
of classical type theory. Of course, to prove a theorem A
ο of
, one can in principle prove [H
o
⊃ A
o
] in
, where H
o
is an appropriate conjunction of axioms of Extensionality and Descriptions, ...
Read now
Unlock full access