We show that higher-order logic (HOL) can be axiomatized in S, the simply typed lambda-calculus with equational deduction. Unlike traditional formulations of HOL, S does not rely on pre-defined semantics of logical constants. First we show how deduction in traditional HOL can be simulated within S, thus proving S to be a general-purpose higher-order logical system. Afterwards we prove the completeness of S for first-order axioms. An important task of the thesis is to investigate in how far the usual logical constants and semantic structures can be axiomatized within S. We start by considering Boolean algebras, i.e. systems generated by Boolean axioms and show how they can be axiomatically extended by quantification. We define the identity test and show some important properties of identity in S. We axiomatize in S the usual semantic structure of HOL, thus showing that the semantic expressiveness of S matches that of traditional higher-order formalisms. Finally we analyze the deductive power of S in more detail and obtain interesting incompleteness results for specific instances of the system.
Bachelor's Thesis, Saarland University, 2005