## With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

No credit card required

### 3.3 Extensional resolution

The ideas we have discussed so far have been directed toward proving theorems of the system $T$ of elementary type theory, which lacks the axioms of Extensionality and Descriptions of the full system $C$ of classical type theory. Of course, to prove a theorem A ο of $C$ , one can in principle prove [H o A o ] in $T$ , where H o is an appropriate conjunction of axioms of Extensionality and Descriptions, ...

## With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

No credit card required