Some Results on Classical Semantics and Polymorphic Types

In the first chapter we consider the simply typed-calculus over one ground type with a discriminator which distinguishes terms, augmented additionally with an existential quantifier and a description operator, all of lowest type.