 There are non-syntactic models of various type theories, though these were developed later, for example (Scott, 1970), and make fairly strong set-theoretic cardinality assumptions, such as the existence of inaccessible cardinals. Much more relevant for the formalist are ‘term models’, syntactic models similar to the interpretations of languages which make use of their own symbols as the members of the domain, interpretations to be found in Henkin completeness proofs; and especially ‘syntactic semantic’ approaches, as in some interpretations of Per Martin-Löf’s intuitionist type theory (see the entry on  intuitionistic type theory),  or the ‘proof-theoretic semantics’ of Peter Schroeder-Heister  (see the entry on proof-theoretic semantics)  which eschew attempts to give meanings to types and terms by reference to ‘external’ truth-conditions: mathematical language is not to be taken as a representation of some independent reality. 