One of the standard ways of proving the consistency of additional hypotheses with the basic axioms of an axiom system is by the construction of what may be described as ‘inner models.’ By starting with a domain of individuals assumed to satisfy the basic axioms an inner model is constructed whose domain of individuals is a certain subset of the original individual domain. If such an inner model can be constructed which satisfies not only the basic axioms but also the particular additional hypothesis under consideration, then this affords a proof that if the basic axiom system is consistent then so is the system obtained by adding to this system the new hypothesis. This method has been applied to axiom systems for set theory by many authors, including v. Neumann (4), Mostowski (5), and more recently Gödel (1), who has shown by this method that if the basic axioms of a certain axiomatic system of set theory are consistent then so is the system obtained by adding to these axioms a strong form of the axiom of choice and the generalised continuum hypothesis. Having been shown in this striking way the power of this method it is natural to inquire whether it has any limitations or whether by the construction of a sufficiently ingenious inner model one might hope to decide other outstanding consistency questions, such as the consistency of the negations of the axiom of choice and continuum hypothesis. In this and two following papers we prove some general theorems concerning inner models for a certain axiomatic system of set theory which lead to the result that as far as a fairly large family of inner models are concerned this method of proving consistency has been exhausted, that no essentially new consistency results can be obtained by the use of this kind of model.

Classical syntax and semantics make fundamental use of variables ranging over classes, relations, etc. In syntax, one speaks exclusively of such objects as symbols, formulae, terms, in short of what may be called (following Carnap) sign-designs. A sign-design is a class of similar concrete marks or sign-events or inscriptions or sequences of typographical characters. In semantics, in addition to sign-designs, one also speaks of the objects denoted or designated by the sign-designs called constants or of the objects which are values for the sign-designs called variables.

Interest in the possibility of a syntax and semantics based upon sign-events or inscriptions rather than upon sign-designs appears to have originated with Lesniewski and Tarski. Not until recently, however, in a paper by Goodman and Quine, has a purely inscriptional syntax been explicitly formulated. The discussion in that paper is confined to the syntax of one object language, but the methods developed are applicable to other systems as well and should suffice for many of the purposes of syntax.

In the present paper we make an attempt to construct a purely inscriptional semantics, in which, as with Goodman and Quine, sign-designs or classes of similar inscriptions in no way figure as values for variables. In rejecting such entities it might appear that the resulting semantics would be drastically curtailed. That the methods used here are of sufficient power to be of interest, however, is shown by constructing a definition of a semantical concept of truth for a given sample elementary object language L. The definition of a predicate for truth in L is given, and the predicate is shown to be adequate in essentially the sense due to Leśniewski, Kotarbiński, and Tarski.

There has recently been developed a method of formalising any fragment of the propositional calculus, subject only to the condition that material implication is a primitive function of the fragmentary system considered. Tarski has stated, without proof, that when implication is the only primitive function a formulation which is weakly complete (i.e., has as theorems all expressible tautologies) is also strongly complete (i.e., provides for the deduction of any expressible formula from any which is not a tautology). The methods used by Henkin suggest the following proof of the

Theorem. If in a fragment of the propositional calculus material implication can be defined in terms of the primitive functions, then any weakly complete formalisation of the fragmentary system which has for rules of procedure the substitution rule and modus ponens is also strongly complete.