Full Schemas and Categoricity

FullSchemasandCategoricityHandout (this topic does not yet exist; you can create it)"> FullSchemasandCategoricityHandout

Slide 1: Thanks

Thanks for inviting me.

Slide 2: Full Schemas and Categoricity

What I intend to do today is introduce the notion of a schema from scratch, complete with a formalized logic, and prove that a suitable version of arithmetic is in a suitable sense categorical. Today will be the first time that I have presented such a result by itself, instead of along with allied results about other logics. I have tried to restrict myself to the case at hand, but if some unnecessary generality seems to have crept in, it probably has: I've failed to expunge it in adapting earlier more general accounts.

Slide 3: Full Schemas

J. H. Harris—and, following him, McGee—says that the rules of logic are open ended—they apply not just in the present language but in any extension of it, whether that extension has been envisioned or not.

Slide 4: Full Schemas

We do in fact take our logical rules to be open ended: Consider, for example, the rule or, for that matter, its informal counterpart in natural language. We do not stop to reëvaluate the rule when moving to an expanded vocabulary or even when introducing modalities—all the new formulas are automatically to be allowed into the rule. As McGee puts it for the case of reductio ad absurdum:

We do not accept reductio ad absurdum because we have surveyed the forms of expression found in English and found that its expressive power is circumscribed in such a way as to validate the rule.

Slide 5: Full Schemas

For example, the rule of a formalized logic in a language is not, if the rule is to reflect our ordinary usage,

if is a formula of , then from infer ,

but rather,

if and are any formulas whatsoever, then from infer .

Slide 6: Full Schemas

The notion of 'any formula whatsoever' is, of course, hopelessly vague. I see no reason to provide a precise account here, and indeed some reason not to: since our formalism is going proxy for natural language, we should surely avoid unnecessary commitment to a particular semantics.

Slide 7: Full Schemas

That is all very well, but how can we live with rules as imprecise as the one just suggested? The rule expresses a very precise idea: It is used to express a commitment that however we expand or modify our language in the future, we shall always continue to uphold certain principles, in this case, the conjunction elimination principle. Even imprecise rules have clear cases of application, and we shall only need the rules of logic and mathematics in clear cases in this work. Given that we shall only be interested in clear cases, we have no present reason to worry about the ambiguity of the formulation.

Slide 8: Formalizing rules of logic

The "open ended" rules of logic are clearly in a certain sense very general, but what is the nature of that generality? We surely do not, if at all possible, wish to understand (or its natural language counterpart) along the lines of

Slide 9: Formalizing rules of logic

It is not even clear that the universally quantified "formula" is well formed: the turnstyle '' is not a part of the language, but a symbol that is used to specify a rule—from the antecedent, infer the consequent.

Slide 10: Formalizing rules of logic

If the formula is not well formed, it is surely not an appropriate way in which to understand the relevant generality. But even if we brush such niceties aside, expressing the generality of the open-ended rules of logic using quantification will still be deeply problematic.

Slide 11: Formalizing rules of logic

To use such a formalism would be to employ the formalism of logic in introducing that very formalism—an undesirable circularity that can be avoided. One might even consider it to be worse than a circularity, since it requires the comparatively sophisticated notion of quantification even to introduce sentential logic.

Slide 12: Formalizing rules of logic

To make the circularity more stark, consider how we would apply the rule universal universal specification: to show that, say, is a valid inference.

Slide 13: Formalizing rules of logic

We would first apply UUS to UUS (circularity!) with , and to obtain

Slide 14: Formalizing rules of logic

We would then apply MP (Actually, meta--modus ponens, since '' is not in the language. But we have already agreed to put such considerations aside.) to UUS and the formula immediately above to yield knocking off the first quantifier (), and then apply UUS twice more. We would have to apply UUS to use the rule UUS.

Slide 15: Formalizing rules of logic

The point is entirely parallel to one made by Quine in "Truth by Convention." There is nothing inconsistent about describing what we mean by universal specification in this circular way, but it eliminates the possibility of telling any straightforward story about how quantification could be introduced or learned, and it ignores the existence of a pre-quantificational mechanism that has generally been thought to exist and to play a genuine role in our reasoning: the schema.

Slide 16: Formalizing rules of logic schematically

The schema is another, more primitive, form of generality that will do the job of introducing logical rules without any attendant circularity: we can take and the other logical rules to be schemas used to declare that any substitution instance is valid. In that case, and are schematic variables, and to say that the schema is open ended is to declare that the variables are what I have elsewhere called full schematic variables: 'full' is added to indicate that what counts as an acceptable substitution instance is open ended and automatically expands as the language in use expands.

Slide 17: Full schemas are not implicitly universally quantified

We may use the following example to see how a schema differs in conception from a universally quantified formula, even an implicitly universally quantified formula. The sentence is a truth bearer, and it is indeed true. In contrast, the schema , with a schematic variable is not a truth bearer at all, though it does deserve some sort of honorific, since it can be used to declare that all of its suitable instances are true. The free schematic variable in a schematic formula, like an ordinary free variable, prevents the formula from being a truth bearer.

Slide 18: Schematic generality is not referential generality

The schematic variable cannot be regarded as a free referential variable: it does not take on values and has no domain. To assert that a formula involving a schematic variable is an axiom schema does not commit us to any true axioms involving a schematic—or any other kind of—free variable: Rather, it commits us to closed instances of the schema as axioms.

Slide 19: Full schemas

The idea that schemas are involved in the basis of logic has been endorsed by Quine and schemas are arguably employed by Russell—his typical ambiguity—and Hilbert.

Slide 20: Full schemas

Full schemas are used by Feferman (who introduced them as early as 1977, in discussing Gödel-type independence phenomena, by Tyler Burge in his theory of truth, by McGee in his theory of "How we learn mathematical language," and by Field, Parsons, and I—we have all taken mathematical induction to be a full schematic principle. In each case, full schemas are used to codify the idea that certain principles are open ended—that we are committed to upholding them even through additions to and modifications of our language. The same applies to the axiom of replacement of set theory, as I shall argue below.

Slide 21: Full schematic generality is not referential or substitutional generality

The case against assimilating schematic generality to that of referential or substitutional quantification is strongest in the case of a full schema: Full schemas, which are the ones of chief interest to us here, are explicitly required to allow new instances as our language expands, and so the very idea of a full schema is incompatible with the notion of a fixed domain or substitution class.

Slide 22: Full schematic generality is not referential or substitutional generality

Quantificational variables are only auxiliaries for quantification: formulas with free variables are not truth bearers. One might therefore wish to avoid the notion that anything is a consequence of a formula with a free variable. One can, for example, infer from as well as from , and so perhaps one might wish to argue that the schematic version of is really just an alternative notation for the more familiar universally quantified sentence, perhaps construing the hypothesized implicit quantifier as referential, perhaps as substitutional. That cannot be made to work for several reasons.

Slide 23: Full schematic generality is not referential or substitutional generality

A schematic variable cannot be viewed as a free variable, whether substitutional or referential, one that could be bound by a quantifier, since schematic and quantifiable variables have different inferential roles: If is a schematic variable, one can infer from , but that is not so if is a quantifiable variable—in that case in some proof systems the formula cannot appear in a proof at all, while in those that do allow it, the inference is valid only if does not occur free in any of the premises of the argument. No such proviso is required in the case of a schematic variable.

Slide 24: Full schematic generality is not referential or substitutional generality

Schematic variables are more closely allied to substitutional than to referential quantification: When we give a schema that is not full, we typically restrict the schematic variable to all terms or formulas in a language, not to a range of all objects or properties in a domain. Intuitively, however, no schema has a domain of application like the substitution class of a substitutional quantifier—a schema isn't used to make a general assertion about a class of possible instances.

Slide 25: Full schematic generality is not referential or substitutional generality

A schema provides a general method of obtaining particular assertions about suitable instances. Thus, for example, one can infer from and , but not, if is a schematic letter, from and , since the schema, rather than making an assertion about all numbers, which is what is required to reach the conclusion, provides a mechanism for making assertions about particular numbers.

Slide 26: Full schemas

To summarize, schematic variables are neither referential nor substitutional variables. Schematic generality has important preformal differences from the generality of substitutional universal quantification. Finally no universally quantified sentences can have the same consequences as does a suitable corresponding full schema.

Slide 27: Full schematic categorical axiomatization of arithmetic

Full schemas codify the open-ended principles that will make it possible to provide categorical axiomatizations of the natural numbers. We therefore discuss the formalism of axiom schemas in sufficient detail to provide the background for a categoricity proof. We shall only need to employ schemas in one or two first-order schematic variables and two or three second-order schematic variables, and we reserve the letters , , , and for the purpose. We allow them to have subscripts so that in principle we have infinitely many schematic variables of each order.

Slide 28: Full schematic logic

In our applications the schematic variables will have various numbers of substitutable places. We leave it to the reader to determine the number of substitutable places of a schematic variable by counting the number of terms enclosed in parentheses immediately following it. In this work we shall always allow extra places for parameters. For a fully general treatment, we would have to specify infinitely many schematic variables of each order and number of places.

Slide 29: Substituting for schematic variables

For any term or formula , variables , and terms , let (1) </span>\atop{t_{1},\dots ,t_{n}}}\!\right]\!\!\right]$" /> denote the result of simultaneously replacing every free occurrence of every , , in by and renaming bound variables as necessary to prevent collisions with the (free) variables of the terms .

Slide 30: Substituting for schematic variables, cont.

Given a schematic formula , variables , and a formula , where is a first- or second-order schematic variable that has substitutable places, we define (2) </span>\phi \!\right]\!\!\right]}$" /> or, usually, but less precisely, ,

Slide 31: Substituting for schematic variables, cont.

We define (3) </span>\phi \!\right]\!\!\right]}$" /> to be the formula that results from when, for every list of terms , every occurrence of in is replaced by (4) </span>\atop{t_{1},\dots ,t_{n}}}\!\right]\!\!\right]$" />,

Slide 32: Substituting for schematic variables, cont.

We must change bound variable in as necessary to prevent collisions with the free variables of (5) </span>\atop{t_{1},\dots ,t_{n}}}\!\right]\!\!\right]$" /> that are not among the (free) variables of the terms .

Slide 33: Substituting for schematic variables

For example, (6) </span>\!\right]\!\!\right] = (\forall x) (\exists v)(\exists u) R(u,x,y)$" />, where replaced to avoid a collision in (7) </span>\!\right]\!\!\right]$" /> and replaced to avoid a collision in (8) </span>\!\right]\!\!\right]$" />.

Slide 34: Substituting for schematic variables

The resulting formula may have free variables. We take them to be implicitly universally quantified.

Slide 35: Rule of inference for schematic variables

For any language , we introduce the substitution rule: from any formula in which has substitutable places, infer , where are any variables and is any term of if is a first-order schematic variable and any formula of if is a second-order schematic variable.

Slide 36: Full schematic logic

We now associate a full schematic theory with any base theory in a language . The base theory may include some formulas with schematic variables in them. We do not regard a theory as a set of sentences in a language as is usual, but instead as a function from languages to sets of axioms and rules.

Slide 37: Full schematic logic

If the schematic variable , whether of first or second order, has substitutable places, let stand for some fixed -tuple of distinct variables. The full schematic theory associated with over , , associates with each the theory with axioms and with the -substitution rule. When is empty, we refer to the corresponding theory as full schematic logic.

Slide 38: Full schematic logic

Let us define what it is for a structure to be a model of a full schematic theory in line with the redefinition of the notion of a theory.

Slide 39: Full schematic logic

An assignment satisfies the formula with respect to full schematic logic in a structure if is a structure for a language including , is an assignment for , and satisfies in the familiar sense every schematic-variable-free deductive consequence with respect to full schematic logic of in any language in any expansion of to a structure for a language including .

Slide 40: Full schematic logic

Let be a theory in a language . A structure is a model of the full schematic theory if every assignment for satisfies every formula in with respect to full schematic logic.

Slide 41: Full schematic logic

To say that any expansion has a certain property is not the universally quantified statement that every expansion has the property—that would require a notion of the class of all possible expansions, a notion to which I am not entitled. It is rather a full schematic metalinguistic statement that will let us infer, whenever we are given an expansion, that it has the property. That is a perfectly clear and formally precise account of a constraint on how we may expand our language. It can be used to represent our metaphysical commitments concerning models of a theory, that is for describing what properties we are committed to any model maintaining even as we revise our language.

Slide 42: Aside on vagueness

The models of vagueness introduced in the vagueness seminar were for a fixed language, but it would be routine to modify them to allow different languages at different leaves. Each full scheme would have each linguistic object of suitable kind (that is, of the right order and number and obeying whatever restrictions are imposed by the schema) of the total language as a potential substituend at each node. Of course, that would include different items at different nodes. I do not pursue the details further because typical cases of adding new items to the language that are of interest for our purposes are not cases in which it is vague whether a given item is part of the language, but cases of genuine change—additions to the language that are new and represent an expansion of our linguistic resources.

Slide 43: Full schematic logic

The present definition is the correct one in the present setting. When a theory is defined, not for a single language, but for a single language and all of its expansions, it only seems natural to require not only that a model of the theory in the original language satisfy the theory, but also that expansions of the model continue to satisfy the theory in the corresponding expanded languages.

Slide 44: Peano Arithmetic with Primitive Recursion

Though primitive recursion is not a part of the axiomatic basis of Peano arithmetic, it is central to another standard arithmetic theory, namely, primitive recursive arithmetic. The first theory I wish to consider is a kind of amalgam of Peano arithmetic and primitive recursive arithmetic. The fact that primitive recursive arithmetic is a standard codification of what many have considered to be the most fundamental and basic properties of the natural numbers serves nicely to make the point that taking primitive recursion to be a fundamental part of the basis of arithmetic is not an ad hoc trick in defense of categoricity, but simply a recognition of the importance in that context of a long and deeply held view.

Slide 45: Peano Arithmetic with Primitive Recursion

The language of our schematic theory PAPR (full schematic Peano arithmetic with primitive recursion), which will be a first-order theory with two schemas, will be plus a functor that takes two formulas of our language plus four variables to a relation symbol of our language—we give a more complete specification below. Since we take the functor itself to be part of the language, relation symbols formed using it will be relation symbols of the language and, if we expand the language with new symbols then new relation symbols formed using them in conjunction with the functor will also become relation symbols of the augmented language.

Slide 46: Peano Arithmetic with Primitive Recursion

The axioms will be the successor axiom of Peano arithmetic, the induction schema, and an additional schema:

Slide 47: The primitive recursion schema

Slide 48: Substitution into the primitive recursion schema

I must explain how to substitute for and for in , where , , , and are any variables, and are any formulas, and and are any terms. For any formula , let be the set of free first-order variables in it.

Slide 49: Substitution into the primitive recursion schema, cont.

The relation symbol has places, where is the number of variables in The atomic formula that results from the indicated substitution into is , where is the variables (parameters) in listed in alphabetical order.

Slide 50: Substitution into the primitive recursion schema

We interpret the -substitution rule to apply to substitutions in the newly extended sense and extend it to apply to both and , and we similarly extend the definitions that employ the rule.

Slide 51: Full schematic primitive recursion

Since we are taking the functor to be in the base language, we shall be able to prove theorems about relation symbols constructed from by induction. In particular, we shall be able to prove that if there is a unique such that and for every and there is a unique such that , then is a well-defined function—I omit showing the parameters here and frequently below.

Slide 52: Addition

We can define addition by .

Slide 53: Multiplication

We can define multiplication by

Slide 54: The theory

PAPR has the conceptual advantage of employing a uniform primitive recursion schema instead of treating each primitive recursive definition separately. That, for example, makes it possible to prove in schematic form that if there is a unique such that and for every there is a unique such that , then is a well-defined function, instead of proving that separately for each primitive recursive definition.

Slide 55: The theory

The fragment of PAPR in the fixed language (where the last two relation symbols are the primitive recursive definitions of addition and multiplication given above is definitionally equivalent to PA, that is, that fragment and PA share a common extension by definitions. I shall therefore say, speaking somewhat loosely, that PA is included in PAPR.

Slide 56: The theory

The theory PAPR does not include primitive recursive arithmetic for the simple reason that primitive recursive arithmetic is formulated in terms of function symbols instead of relation symbols. It is, however, a straightforward exercise to show that primitive recursive arithmetic is included in an extension by definitions of PAPR, which I take to mean that PAPR incorporates primitive recursive arithmetic.

Slide 57: The theory

It is a deeper and more surprising fact, due to Gödel, that all of PAPR restricted to the base language is included in an extension by definitions of PA, and hence that PAPR restricted to that language is in effect merely a somewhat redundant formulation of PA. It is presumably for that reason that axiomatic theories like PAPR are not familiar. Nonetheless, PAPR is an axiomatization that employs only core ideas about the natural numbers.

Slide 58: The theory

When we consider adding a new unary relation to the base language of PAPR things become more interesting. (We consider adding a unary relation for definiteness—the same kinds of considerations would apply for any relation or function.) The theory PAPR automatically adds the requisite new instances of both the primitive recursion and induction schemas when the language is expanded.

Slide 59: The theory

Since we are adding the new symbols into the induction schema, we must establish that the addition is acceptable. I will offer two arguments for that. The first argument is direct: The use of primitive recursion in concert with new relations and even across domains without any presumption of a background theory is such a well-established part of traditional mathematical practice that no extra-mathematical objection to it could be tenable. It just is a part of standard mathematical practice that we do take arbitrary primitive recursive definitions to be unexceptionable, and we allow them into the induction schema freely. Moreover, that mathematical practice long antedates the idea of a background set theory, which provides some additional support for the common view that the practice does not require the presupposition of a background set theory.

Slide 60: The theory

The second argument for acceptability is that primitive recursive definitions of relations are acceptable because they are canonically equivalent to positive inductive definitions, which I shall argue below are acceptable on independent grounds.

Slide 61: The theory

The theory PAPR in the language formed by adding the new predicate to the base language has an extension by definitions that has as parts both PA and the theory of functions primitive recursive in . The proofs are straightforward extensions of the proofs of the comparable results without the new predicate .

Slide 62: The theory

Those facts provide an additional argument that the full theory PAPR is the best codification of our preformal intuitions concerning the natural numbers. It is the theory that extends in the way that reflects our unreflective expectations:

Slide 63: The theory

Anyone who understands primitive recursion automatically understands primitive recursion in additional relations. The idea is not so much a new one as an automatic extension of the old one. It is the theories PAPR that reflect that reality.

Slide 64: The theory

Perhaps surprisingly, PAPR is not an essentially new theory: it can be obtained as an extension by definitions of PA by straightforward application of Gödel's method.

Slide 65: The relativized theory

It is only when we consider the relativized theory PAPR that the reason for considering PAPR and not just PA becomes apparent. The theory PAPR is PAPR with the quantifiers in the axioms and schemas relativized to a unary predicate . Unrelativized formulas are allowed as substituends for the schematic letters in the substitution rule. In addition, we take PAPR to have the formulas and as axioms.

Slide 66: The relativized theory

The need for the additional axioms could be avoided by formulating the theory without constant or function symbols in the first place. Comparable axioms for addition and multiplication are not needed: they are theorems proved by induction.

Slide 67: The relativized theory

The two arguments mentioned earlier for believing the primitive recursion schema to be an acceptable addition to PAPR are equally arguments for believing the primitive recursion schema to be an acceptable addition to PAPR, where, of course, the schema is now taken to be relativized to .

Slide 68: The relativized theory

The raison d'être of PAPR is that it makes it possible to consider the natural numbers in conjunction with other systems. For example, consider the natural numbers along with a group. The axioms may be taken to be PAPR, where is the axioms for the group. Natural number exponentiation is

Slide 69: The relativized theory

Existence and uniqueness on the appropriate domains is readily proved by induction. With PAPR it is not necessary to add anything new to get exponentiation.

Slide 70: The relativized theory

Gödel's method does not apply in the present setting, since it does not yield codes for sequences of members of a group, and so PAPR is truly stronger than PA in the sense that for an arbitrary theory the theory PAPR need not be an extension by definitions of PA.

Slide 71: The relativized theory

The theory PAPR is my candidate for a codification of our basic preformal intuitions concerning the natural numbers. I shall not attempt to give here all my reasons for taking such primitive recursion to be central, resting content with noting that many such functions have historically been employed without the special notice that would have been required had they been essentially new (for example, natural number exponentiation of fractions, polynomials, and complex numbers and iteration of functions) and that those same functions are introduced today in secondary schools without any idea that a new method or procedure is being invoked: it is taken for granted, I believe quite rightly, that such procedures are an integral part of what has already been taught about the natural numbers.

Slide 72: Categoricity

Now that I have shown that PAPR is a natural, independently motivated theory of the natural numbers not introduced in an ad hoc way to solve the Skolem problem, we can see how it helps with that problem:

Slide 73: Categoricity

Theorem. Let be the theory in the language (9) </span>^{(+)}+\lnot{\text{Con(PA)}}$" />, where Con(PA) is the sentence asserting the consistency of PA used in Gödel's second incompleteness theorem, is (if PA is consistent) consistent but it has no models. Proof: A model in the ordinary first-order sense of this theory must be nonstandard, since PA is consistent, but PA has no nonstandard models by the categoricity theorem.

Slide 74: Acceptability

I do not know of a nontrivial necessary and sufficient condition for a full schematic theory to be satisfiable, certainly not one as straightforward as simple consistency, but there is a useful general sufficient condition. There is also an additional sufficient condition useful for some special cases, including PA.

Slide 75: Acceptability

My main interest in full schematic theories has been their use in characterizing mathematical domains. The full schematic principles of interest concern characteristics of the domain that survive the arbitrary addition of new relations. It is therefore natural to ask when the addition of a theory to a full schematic theory adds new relations without changing the domain. I shall call such an addition an acceptable addition. For example, adding to a theory of arithmetic is not acceptable, because satisfying it may require adding new elements (nonstandard numbers) to the domain.

Slide 76: Acceptability

If an addition to a full schematic theory is an acceptable addition, then any intended model of the full schematic theory can be expanded to a model of the addition. Thus, if a full schematic theory is satisfiable, so is the theory plus any acceptable addition.

Slide 77: Acceptability

The condition is sufficient, but it is surely not necessary. For example, large cardinal axioms are not acceptable additions to set theory—the whole point is that they add things to the domain. Nonetheless, there may well be good reason to allow adding on large cardinal axioms.

Slide 78: Acceptability

We can give the notion of an acceptable addition a mathematically precise explication as follows: an addition to a theory is acceptable with respect to a class of models if every model of in has an expansion to a model of .

Slide 79: Acceptability

Actually, we shall need a slightly more general definition to allow additions with free variables for parameters: an addition to a theory is acceptable with respect to a class of ordered pairs of the form , where is a model and is an assignment for , if every pair in is such that if is a model of then has an expansion to a model in which satisfies .

Slide 80: Acceptability

In the case of PA, the intended model is a smallest model. It is isomorphic, in a suitable sense, to a substructure of every structure that is a model of PA with respect to a fixed language. That follows from the following theorem.

Slide 81: Acceptability

Theorem. Let be a theory that is complete for atomic sentences (that is, if is an atomic sentence then either or is a consequence of ). Then, with respect to a fixed language, any model of in which every member of the domain is denoted by a closed term is a smallest model of .

Slide 82: Acceptability

The theory PA, and hence PA, satisfies the hypothesis: The intended model is one in which every member of the domain is denoted by a closed term. The atomic sentences are all variable-free equations, and PA suffices to prove all the true ones and to disprove all the false ones.

Slide 83: Acceptability

Proof: Let be a theory and be a model as in the hypothesis of the theorem. Let be the set of all atomic and negation atomic sentences that are consequences of . Then is a model of , and is a maximal consistent set of atomic sentences. Thus, is the atomic diagram of . Since every model of is a model of , it follows that is isomorphic to a substructure of every model of .

Slide 84: Acceptability

Since PA has a smallest model, it will be useful to show that any universal theory (that is, any set of formulas of the form , where is free of quantifiers) is an acceptable addition to any theory with respect to the class of smallest models of in a fixed language if is consistent:

Slide 85: Acceptability

Theorem. Suppose that some theory has a smallest model . Then can be expanded to a model of any universal theory that is consistent with .

Slide 86: Acceptability

Proof: Since is consistent, it has a model . Since is a smallest model of , we may as well assume that is a substructure of the reduct of to the language of . The substructure of with universe the universe of , call it , is thus a model of . Since is a submodel of and is a model of , it follows that is a model of —the theory , being universal, has the submodel property.

Slide 87: Acceptability

By the Matijasevi--Robinson--Davis resolution of Hilbert's tenth problem, there is a universal sentence in the language of PA that can be proved in PA to be equivalent to Con(PA). Since is universal, is satisfiable, by the theorem.

Slide 88: Acceptability

The preceding considerations now give us a justification for our intuitive preference of PA+Con(PA) over PACon(PA): By the theorem, if PA is consistent, PA, and therefore PACon(PA), is satisfiable in the base language, and therefore, by the categoricity result, PACon(PA) is not.

Slide 89: Acceptability of inductive definition

Next, we show that one can always add certain inductive definitions of new relations to any full schematic theory, that is, that such additions are acceptable additions to any full schematic theory with respect to the class of all ordered pairs of models and assignments for them.

Slide 90: Inductive definition

I shall introduce the notion of an inductive definition following Moschovakis, though my terminology is perhaps closer to that of Aczel. An -_ary operator_ on a set is a function from to . An -ary operator on is monotone if for all , if , then . A set is a fixed point of an -ary operator on if .

Slide 91: Inductive definition

Theorem. Every monotone operator has a fixed point, and indeed a least fixed point.

Slide 92: Inductive definition

The proof is straightforward: Define, for any ordinal , and let be the least ordinal whose predecessors form a set of cardinality the cardinality of . Then is the least fixed point (compare Moschovakis).

Slide 93: Inductive definition

Let be a structure for the language with universe , let be an -placed relation symbol not in the language , let be a formula in the language with all free variables among those displayed, and let be members of .

Slide 94: Inductive definition

The -ary operation on , the operation defined on by with parameters , is the operation that takes any to

Slide 95: Inductive definition

where is the expansion of to the language in which the interpretation of is and where the material in square brackets indicates the obvious assignment of objects to variables.

Slide 96: Inductive definition

If occurs positively in (that is, if the connectives and do not occur in and if no occurrence of in is inside the scope of a negation sign), then is monotone, as may be shown by an easy inductive proof (compare Moschovakis).

Slide 97: Inductive definition

When occurs positively in , we say that is an operation defined by a positive formula.

Slide 98: Inductive definition

Note that is a fixed point of if and only if any assignment that assigns to satisfies the formula in the structure .

Slide 99: Least fixed point

What one is normally interested in is not just any fixed point, but the least fixed point.

As it happens, none of the proofs in this work require the information that a given fixed point is least or greatest, and so the conditions for a fixed point to be least or greatest play no role in anything that follows.

Slide 100: Acceptability of positive monotone induction

Let be a theory for the language , let be an -placed relation symbol not in the language , and let be a formula in the language with all free variables among those displayed in which all occurrences of are positive.

Slide 101: Acceptability of positive monotone induction

Observe that the formula is an acceptable addition to with respect to the class of all pairs of models and assignments for them.

Slide 102: Acceptability of positive monotone induction

By the theorem above, for any model of and any assignment for , there is a fixed point of . Thus, satisfies in . We have shown:

Slide 103: Acceptability of positive monotone induction

Theorem. Let be a theory for the language , let be an -placed relation symbol not in the language , and let be a formula in the language with all free variables among those displayed in which all occurrences of are positive. If is a model of and are members of the universe of , then there is an expansion of in which are new constant symbols that denote that satisfies

Slide 104: Acceptability of positive monotone induction

Slide 105: Acceptable additions

The theorems on acceptable additions just proved provide powerful criteria for determining what can be added to full schematic theories, but they are not suited to play a foundational role. Their statements, not to mention the proofs given, make strong use of a background set theory. For present purposes, they are to be regarded merely as ex post facto justifications, and perhaps generalizations, of principles concerning acceptable additions that we take as basic, intuitive, and well-established parts of mathematical practice.

Slide 106: Acceptable additions

We can add any universal theory consistent with arithmetic to arithmetic, and we can add fixed points of operations defined by positive formulas to any full schematic theory. I take it that the operative sense of "can" in the last sentence is that the theory with the addition is acceptable in the pretheoretic sense that it only adds new relations, without the need for a change in domain or a change in the full schematic character of the theory

Slide 107: Acceptability

The notion of acceptability is an intuitive one that cannot be made mathematically precise without set-theoretic apparatus to which I am not entitled for my foundational purposes, but all I need is the result that the definition of a fixed point of an operation defined by a positive formula is an acceptable addition to any full schematic theory.

Slide 108: Back to arithmetic

Take variables to be implicitly bound to and variables to be implicitly bound to . That is, we take, for example, quantifications and to be abbreviations for and , respectively. This convention leaves us without a way to write ordinary, unbounded quantifiers, but that is not a serious problem, since we have virtually no use for such quantifiers.

Slide 109: Back to arithmetic

Introduce a new relation defined as ; introduce in a parallel way.

Slide 110: Back to arithmetic

We can then introduce bounded quantifiers , and so forth, as usual. Thus, for example, is an abbreviation for , which, in turn, is an abbreviation for , a formula in which the quantifier is interpreted in its ordinary sense.

Slide 111: Back to arithmetic

Define a new binary relation as follows, employing both the unprimed and the primed vocabulary: Note that the definition of is a definition of a fixed point of an operation defined by a positive formula, and that it is therefore an acceptable definition. The relation is the isomorphism we defined above using primitive recursion.

Slide 112: Acceptability of primitive recursion

To see that primitive recursive definitions of relations are acceptable, we note that the formula is a positive inductive definition of .

Slide 113: Acceptability of primitive recursion

The addition of is therefore acceptable, by the theorem on the acceptable addition of positive inductive definitions.

-- ShaughanLavine - 17 Mar 2005

Latex rendering error!! dvi file was not created.

Notes

1 , 4 , 5 : x_{1},\dots ,x_{n

2 , 3 : \bf P}\atop{\hat{x}_{1}\cdots\hat{x}_{n

6 : P}\atop{\hat{z}(\exists x) R(x,z,y)

7 : z}\atop{x

8 : P}\atop{ (\exists u) R(u,x,y)

9 : \mathbb P},{\mathbb P}'\}$% that is the union of the theory PAPR%$^{(+)U}$% and the primed version PAPR%$^{(+)U}{}'$% of the very same theory. Then there is a binary relation symbol %$I$% in the language such that the following formulas are theorems of %$T$%:

Categoricity

1. %$(\forall x)(U(x)\rightarrow (\exists y)(U'(y)\land (\forall z)(I(x,z)\leftrightarrow z=y)))$%
%$\quad$% (%$I$% is a function from %$U$% to %$U'$%),
2. %$(\forall x)(U'(x)\rightarrow (\exists y)(U(y)\land (\forall z)(I(z,x)\leftrightarrow z=y)))$%
%$\quad$% (%$I$% is one-to-one and onto),

Categoricity

3. %$I(0,0')$%,
4. %$(\forall x)(\forall x')(\forall y)(\forall y')(I(x,x')\land I(y,y')$% %\[\quad\rightarrow Sx=y\leftrightarrow S'x'=y')\]%,

Categoricity

5. for any variables %$w$%, %$x$%, %$y$%, and %$z$% and formulas %$\phi$% and %$\psi$% that are obtained from formulas of the base language of PAPR by bounding all quantifiers by %$U$%,

Categoricity

%\[(\forall x_{1})(\forall x'_{1})\dotsm (\forall x_{n})(\forall x'_{n})\]% %\[(I(x_{1},x'_{1})\land\dots\land I(x_{n},x'_{n})\]% %\[ \rightarrow{\mathbb P}(\hat{w}\phi ,\hat{x}\hat{y}\hat{z}\psi)(x_{1}\dots x_{n})\leftrightarrow\]% %\[\qquad{\mathbb P}'(\hat{w}\phi ',\hat{x}\hat{y}\hat{z}\psi ')(x'_{1}\dots x'_{n})),\]%

Categoricity

where %$n$% is the number of places of %${\mathbb P}(\hat{w}\phi ,\hat{x}\hat{y}\hat{z}\psi )$% and %$\phi '$% and %$\psi '$% are the primed versions of %$\phi$% and %$\psi$%.

Categoricity

In other words, in any model of %$T$%, %$I$% is an isomorphism between the unprimed and primed models of PAPR.

Categoricity

The theorem should be compared with work of Parsons, who noted that one can prove two models of arithmetic isomorphic via a primitive recursively defined isomorphism. The %$I$% of the theorem is %\[{\mathbb P}(\hat{w}w=0',\hat{x}\hat{y}\hat{z}z=S'y).\]%

Categoricity

The theorem does not require adding any symbols or definitions to the combination of the theory with the primed version. The theory PAPR%$^{(+)U}$% provides a class of functions, the primitive recursive functions, that can be defined between the natural numbers and other structures without a background notion of an extension. Thus, one can hold that we can successfully characterize the natural numbers with a fully formal theory, PAPR%$^{(+)U}$%, without any need for the ill-defined notion of acceptability of expansions of a language.

Why primitive recursion?

The very notion of a full schematic theory involves systematically adding new axioms to an antecedently given theory. There is, of course, no formal obstacle to adding any axioms whatsoever to any theory whatsoever. The main question is when the resulting theory will be satisfiable—when it will have a model, and in the case of full schematic theories, when it will have a model in our new specially defined sense.

Consistency is not enough

That question has a well-known answer in the case of ordinary first-order theories: by the completeness theorem, a necessary and sufficient condition for a theory to be satisfiable is that it be consistent. That condition is not sufficient for full schematic theories: for example, the theory %${\text{PA

10 : x_{1},\dots , x_{n},y_{1}, \dots ,y_{m

---