THE NORMAL INTERPRETATIONS

Abstract

In order to prove the completeness of a formal system of type theory, Henkin extends in (2) the method he himself had developed for the test corresponding to a first-order system. The result is that the logic of higher-order predicates is complete in a certain sense, provided that semantic notions are modified. In (1) the method is applied specifically to the second order and a semantic is defined, which we can call in a general sense to distinguish from that which would result from considering a special family of domains -each of which with all possible elements- and is described as standard. The basic notion to elaborate both semantics is that of interpretations of a formal second order language on a family of domains