Keywords

1 Introduction

In our forthcoming paper (Enayat and Visser 2012) we explore satisfaction classes over a wide variety of ‘base theories’ ranging from weak fragments of arithmetic to systems of \(ZF\) set theory and beyond. This note provides a synopsis of some of this work in the context of the most popular base theory adopted in investigations of axiomatic theories of truth, namely \(PA\) (Peano Arithmetic).

The notion of a satisfaction class was first introduced and investigated by Krajewski in his 1976 paper (Krajewski1976). Two noteworthy accomplishments of (Krajewski1976) are the following results:

(1) If a countable model of a ‘base theory’ (such as PA) carries at least one full satisfaction class, then it has a countable elementary extension that carries continuum-many full satisfaction classes.

(2) Every model of \(ZF\) has an elementary extension that carries a full satisfaction class.

The question whether the analogue of (2) holds for \(PA\) remained open until the appearance of the joint work (Kotlarski et al.1981) of Kotlarski, Krajewski, and Lachlan in 1981, in which the rather exotic proof-theoretic technology of ‘ \(\mathcal{M}\)-logic’ (an infinitary logical system based on a nonstandard model \(\mathcal{M}\)), was invented to construct ‘truth classes’ over countable recursively saturated models of \(PA\).Footnote 1 This model-theoretic result can be used to show that the analogue of (2) does indeed hold for \(PA,\) which in turn can be used to show that \(PA^{ FT}\) is conservative over \(PA,\) where \(PA^{ FT}= PA\) + “ \( T\) is a full truth class”. The conservativity of \(PA^{ FT}\) over \(PA\) has attracted considerable philosophical attention, especially in relation to the grand debate concerning deflationism.Footnote 2

In this paper we present a perspicuous method for the construction of full satisfaction classes that is dominantly based on model-theoretic techniques (e.g., expanding the language, compactness, and elementary chains). As we shall see, our construction method is quite versatile and can be used to construct many (if not all) of the results that have hitherto been only possible to establish with the use of \(\mathcal{M}\)-logic machinery. Furthermore, the method can also be employed to build new types of full satisfaction classes (see Sect. 16.6).

We present the necessary preliminaries in Sect. 16.2, and then in Sect. 16.3 we concentrate on the basic form of our new construction of full satisfaction classes, where it is used to show that every model of \(PA\) has an elementary extension that carries a full satisfaction class. The versatility of the methodology of Sect. 16.3 is illustrated in Sect. 16.4, in which an appropriate modification of the method is used to construct truth classes for models of \(PA\). As explained in Sect. 16.5, certain arithmetizations of our construction can also be employed to establish that (1) \(PA^{ FT}\) is interpretable in \(PA\); and (2) the conservativity of \(PA^{ FT}\) over \(PA\) can be verified in \(PRA\) (Primitive Recursive Arithmetic). Finally, in Sect. 16.6 we briefly describe further applications of the methods introduced in this paper.

Acknowledgments. We are grateful to the editors of this volume for their interest in our work. Thanks also to Volker Halbach, Fredrik Engström, and James Schmerl for helpful feedback on preliminary drafts of this paper. We are particularly indebted to Schmerl for catching an inaccuracy in an earlier formulation of Lemma 3.1, and for his suggestion to distill the results of our paper (Enayat and Visser) in this form for wider dissemination.

2 Preliminaries

Definition 2.1

Throughout this paper \(PA\) refers to Peano arithmetic formulated in a relational language \(\mathcal{L}_{ PA}\) using the logical constants \(\left\{ ,\vee,\exists,=\right\}\). Note that in this formulation \(PA\) has no constant symbols; the arithmetical operations of addition and multiplication are construed as ternary relations; and conjunction, universal quantification, and other logical constants are taken as defined notions in the usual way.

It is well known that \(PA\) has more than sufficient expressive machinery to handle syntactic notions. The following list of \(\mathcal{L}_{ PA}\)-formulae will be useful here.Footnote 3

  • \(Form(x)\) is the formula expressing “x is the code of an \(\mathcal{L}_{ PA}\)-formula using variables \(\{v_{i}:i\in \mathbb{N}\},\) and the non-logical symbols available in \(\mathcal{L}_{ PA}\)”.

  • \(Asn(x)\) is the formula expressing “x is the code of an assignment”, where an assignment here simply refers to a function whose domain consists of a (finite) set of variables. We use α and its variants ( \(\alpha ^{\prime}\), \(\alpha _{0}\), etc.) to range over assignments.

  • \(y\in FV(x)\) is the formula expressing “ \( Form(x)\) and y is a free variable of x”.

  • \(y\in Dom(\alpha )\) is the formula expressing “the domain of α includes y”.

  • \(Asn(\alpha,x)\) is the following formula expressing “ \( \alpha\) is an assignment for x”:

$$ \left( Form(x)\wedge Asn(\alpha )\wedge \forall y(y\in Dom(\alpha )\leftrightarrow y\in FV(x)\right).$$
  • \(x y\) is the formula expressing “x is the code of an immediate subformula of the \(\mathcal{L}_{ PA}\)-formula coded by y”, i.e., \(x y\) abbreviates the conjunction of \(Form(y)\) and the following disjunction:

$$ \left( y= x\right) \vee \exists z\left( \left( y=x\vee z\right) \vee \left( y=z\vee x\right) \right) \vee \exists i\left( y=\exists v_{i}\ x\right).^{4}$$

\footnotetext{Technically speaking, this formula should be written so as to distinguish the logical operations of the meta-langauge with those of the object-language. For example, using Feferman’ s commonly used ‘dot-convention’, one would write:

$$ \left( y=\underset{\bullet}{}x\right) \vee \exists z\left( \left( y=x \underset{\bullet}{\vee}z\right) \vee \left( y=z\underset{\bullet}{\vee} x\right) \right) \vee \exists i\left( y=\underset{\bullet}{\exists}v_{i}\ x\right).$$

However, since the difference between the two kinds of operation will be always clear from the context, we have opted for the lighter notation.} The theory \(PA^{ FS}\) (read as “{ PA} with full satisfaction”) is formulated in an expansion of the language \(\mathcal{L}_{ PA}\) by adding a new binary predicate \(S(x,y)\). The binary/unary distinction is of course not an essential one since \(PA\) has access to a definable pairing function. However, the binary/unary distinction at the conceptual level marks the key difference between satisfaction classes and truth classes (the latter are discussed in Sect. 16.4) . \(PA^{ FS}\) is defined below with the help of a collection of sentences \(Tarski( S,F).\)

When reading the definition below it is helpful to bear in mind that \(Tarski( S,F)\) expresses:

F is a subset of Form that is closed under immediate subformulae; each member of \(S\) is an ordered pair of the form \((x,\alpha )\), where \(x\in F\) and α is an assignment for \(x;\) and \(S\) satisfies Tarski’s compositional clauses.

Definition 2.2

\( PA^{ FS}\):= \(PA\cup Tarski\left( S, Form\right)\), where \(Tarski( S,F)\) is the conjunction of the universal generalizations of the formulae \(tarski_{0}( S, F)\) through \(tarski_{4}( S, F)\) described below, all of which are formulated in \(\mathcal{L}_{ PA}\cup \{ F(\cdot ), S(\cdot,\cdot )\}\), where \(S\) and \(F\) do not appear in \(\mathcal{L}_{ PA}\).

In the following formulae R ranges over the relations in \(\mathcal{L}_{ PA}\); \(t,t_{0},t_{1},\cdot \cdot \cdot\) are metavariables, e.g, we write \(R\left( t_{0},\cdot \cdot \cdot,t_{n-1}\right)\) instead of \(R\left( v_{i_{0}},\cdot \cdot \cdot,v_{i_{n-1}}\right);\) and \(\alpha^{\prime}\supseteq \alpha\) abbreviates

$$\left( Dom(\alpha^{\prime})\supseteq Dom(\alpha )\right) \wedge \forall t\in Dom(\alpha )\alpha (t)=\alpha ^{\prime}(t).$$
  • { tarski} \(_{0}( S, F):=\left( F (x)\rightarrow Form(x)\right) \wedge \left( S(x,\alpha)\rightarrow \left( F(x)\wedge Asn(\alpha,x)\right) \right) \wedge\)

$$\left( y x\wedge F(x)\rightarrow F (y)\right).$$
  • { tarski} \(_{1,R}( S,F):=\)

    \(\left( F(x)\wedge \left( x= R\left( t_{0},\cdot \cdot \cdot,t_{n-1}\right) \right) \wedge Asn(\alpha,x)\wedge \bigwedge\limits_{i<n}\alpha (t_{i})=a_{i}\right) \rightarrow\)

$$ \left( S(x,\alpha )\leftrightarrow R\left( a_{0},\cdot \cdot \cdot,a_{n-1}\right) \right).$$
  • { tarski} \(_{2}( S, F):=\left( F (x)\wedge (x= y)\wedge Asn(\alpha,x)\right) \rightarrow\)

$$ \left( S(x,\alpha )\leftrightarrow S(y,\alpha )\right).$$
  • { tarski} \(_{3}( S, F):=\left( F (x)\wedge \left( x=y_{1}\vee y_{2}\right) \wedge Asn(\alpha,x)\right) \rightarrow\)

$$ \left( S(x,\alpha )\leftrightarrow \left( S\left(y_{1},\alpha FV(y_{1})\right) \vee S\left(y_{2},\alpha FV(y_{2})\right) \right) \right).$$
  • { tarski} \(_{4}( S, F):=\left( F (x)\wedge (x=\exists t\ y)\wedge Asn(\alpha,x)\right) \rightarrow\)

$$\left( S(x,\alpha )\leftrightarrow \exists \alpha ^{\prime}\supseteq \alpha S(y,\alpha ^{\prime})\right).$$

Definition 2.3

. Suppose \(\mathcal{M}\models \mathcal{L}_{ PA}\), \(F\subseteq M\), and S is a binary relation on M.Footnote 4

(a) \ S is an F-satisfaction classif \((\mathcal{M},S,F)\models Tarski( S,F).\) Footnote 5

(b) \Let \ \(\omega _{\mathcal{M}}\) be the well-founded initial segment of \(\mathcal{M}\) that is isomorphic to the ordinal \(\omega.\) We say that F is the set of standard \(\mathcal{L}_{ PA}\)-formulae of \(\mathcal{M}\) if \

$$F= Form^{\mathcal{M}}\cap \omega _{\mathcal{M}}.$$

In this case there is a unique F-satisfaction class on \(\mathcal{M}\), known as the Tarskian satisfaction class on \(\mathcal{M}\).

(c) S is a full satisfaction class on \(\mathcal{M}\) if S is an F-satisfaction class for \(F:= Form^{\mathcal{M}}.\) This is equivalent to \((\mathcal{M},S)\models PA^{ FS}.\)

Definition 2.4

\( _{0}= _{0}\) = the collection of \(\mathcal{L}_{ PA}\)-formulae all of whose quantifiers are of the form \(\exists x<y\) ϕ or \(\forall x<y\ \varphi\); \(_{n+1}\) consists of formulae of the form \(\exists x_{0}\cdot \cdot \cdot \exists x_{k-1}\ \varphi\), where \(\varphi \in _{n};\) and \(_{n+1}\) consists of formulae of the form \(\forall x_{0}\cdot \cdot \cdot \forall x_{k-1}\ \varphi\), where \(\varphi \in _{n}.\) Here k ranges over \(\omega\), with the understanding that k = 0 corresponds to an empty block of quantifiers; this convention leads to the pleasant consequence that \(_{n}\subseteq _{n+1}\) and \(_{n}\subseteq _{n+1}\) for all n.

Theorem 2.5

(Mostowski (Kaye 1991), (Hájek and Pudlák1993)) For each nonzero \(n<\omega\) there is a binary \( _{n}\) - formula \( Sat_{n}(x,y)\) such that

$$ PA\vdash Tarski( Sat_{n},\mathbf{}_{n}),$$

where \(\mathbf{}_{n}\) is ( the arithmetization of ) the set of codes of formulae in \( _{n}.\)

3 The Basic Construction

In this section we explain the basic methodology of building satisfaction classes using tools from model theory. The following lemma lies at the heart of the main result of this section.

Lemma 3.1

Let \(\mathcal{N}_{0}\models\) \ \( PA\) , \(F_{1}:= Form^{\mathcal{N}_{0}}\) , \(F_{0}\subseteq F_{1},\) and suppose S 0 is an F 0 -satisfaction class. Then there is an elementary extension \(\mathcal{N}_{1}\) of \(\mathcal{N}_{0}\) that carries an F 1 -satisfaction class \(S_{1}\supseteq S_{0}\) and \((c,\alpha )\in S_{0}\) whenever \(c\in F_{0}\) , \(\alpha \in N_{0}\) , and \((c,\alpha )\in S_{1}.\)

Proof

Let \(\mathcal{L}_{ PA}^{+}(\mathcal{N} _{0})\) be the language obtained by enriching \(\mathcal{L}_{ PA}\) with constant symbols for each member of N 0, and new unary predicates U c for each \(c\in Form^{\mathcal{N}_{0}}\). It helps to have in mind that the intended interpretation of U c is \(\{\alpha \in A_{c}:S_{1}(c,\alpha )\}\), where \(A_{c}:=\left\{ \alpha: \mathcal{N}_{1}\models Asn(\alpha,c)\right\}.\)

We first wish to describe a new set of axioms

$$ \Theta :=\left\{ \theta _{c}:c\in F_{1}\right\}$$

formulated in \(\mathcal{L}_{ PA}^{+}(\mathcal{N}_{0})\), where \(\theta _{c}\) stipulates ‘local Tarskian behavior’ for U c .

If \(R\in \mathcal{L}_{ PA}\) and \(\mathcal{N}_{0}\models c= R(t_{0},\cdot \cdot \cdot,t_{n-1})\), then

$$\theta _{c}:=\forall \alpha \left( U_{c}(\alpha)\leftrightarrow Asn(\alpha,c)\wedge R\left( \alpha (t_{0}),\cdot \cdot \cdot,\alpha (t_{n-1})\right) \right).$$

If \(\mathcal{N}_{0}\models c= d\), then

$$\theta _{c}:=\forall \alpha \left( U_{c}(\alpha)\leftrightarrow Asn(\alpha,c)\wedge U_{d}(\alpha )\right).$$

If \(\mathcal{N}_{0}\models c=d_{1}\vee d_{2}\), then

$$\theta _{c}:=\forall \alpha \left( U_{c}(\alpha)\leftrightarrow Asn(\alpha,c)\wedge \left( U_{d_{1}}(\alpha FV(d_{1}))\vee U_{d_{2}}(\alpha FV(d_{2}))\right) \right).$$

If \(\mathcal{N}_{0}\models c=\exists v_{a}\ b\), then

$$\theta _{c}:=\forall \alpha \left( U_{c}(\alpha)\leftrightarrow Asn(\alpha,c)\wedge \exists \alpha ^{\prime}\supseteq \alpha U_{b}(\alpha ^{\prime})\wedge Asn(\alpha ^{\prime},b)\right).$$

Let

$$ \Upgamma :=\left\{ U_{c}(\alpha ):c\in F_{0}\text{ and}(c,\alpha)\in S_{0}\right\} \cup \left\{ U_{c}(\alpha ):c\in F_{0} \text{ and}(c,\alpha )\not\in S_{0}\right\},$$

and let

$$ Th^{+}(\mathcal{N}_{0}):= {Th}(\mathcal{N} _{0},a)_{a\in N_{0}}\cup \Theta \cup \Upgamma.$$

We now proceed to show that \(Th^{+}(\mathcal{N}_{0})\) is consistent by demonstrating that each finite subset of \(Th^{+}(\mathcal{N}_{0})\) is interpretable in \(\left( \mathcal{N}_{0},S_{0}\right).\) To this end, suppose T 0 is a finite subset of \(Th\) \( ^{+}(\mathcal{N}_{0})\) and let C consist of the collection of \(c\in F_{0}\) such that U c appears in \(T_{0}.\) If \(C=\emptyset\), T 0 is readily seen to be consistent, so we shall assume that \(C\neq \emptyset\) for the rest of the argument.

Our goal is to construct subsets \(\left\{ U_{c}:c\in C\right\}\) of N 0 such that the following two conditions hold when U c is interpreted by U c :

  1. 1.

    [(1)] \(\left( \mathcal{N}_{0},U_{c}\right) _{c\in C}\models \{\theta _{c}:c\in C\},\) and

  2. 2.

    [(2)] For \(c\in C\cap F_{0},\) \(U_{c}=\{\alpha \in N_{0}:(c,\alpha )\in S_{0}\}.\)

We shall construct \(\{U_{_{c}}:c\in C\}\) in stages, beginning with the simplest formulae in C, and working our way up using Tarski rules for more complex ones. Recall that \(c d\) expresses “c is a direct subformula of d”. Define \(^{*}\) on C by:

$$c ^{*}d \,\text{iff}\, (c d)^{\mathcal{N}_{0}}\,\text{and}\, \theta _{d}\in T_{0}\cap \Theta.$$

Note that whenever \(c ^{*}d\), then for all \(c^{\prime} d\) we have \(c^{\prime}\in C\) and \(c^{\prime}\vartriangleleft ^{*}d\). The finiteness of C implies that \((C, ^{*})\) is well-founded, which in turn helps us define a useful measure of complexity for \(c\in C\) using the following recursive definition:

$$ rank_{C}(c):=\sup \{ rank_{C}(d)+1:d\in C\ \mathrm{and}\ d ^{*}c\}.$$

Note that for \(c\in C\), \(rank_{C}(c)=0\) precisely when \(\theta _{c}\not\in T_{0}\cap \Theta\). Next, let

$$C_{i}:=\{c\in C: rank_{C}(c)\leq i\}.$$

Observe that \(C_{0}\neq \emptyset\) (since C is finite and nonempty), and that if \(c\in C_{i+1}\), then the codes of all immediate subformulae of the formula coded by c are in \(C_{i}.\) This observation ensures that the following recursive clauses yield a well-defined U c for each \(c\in C.\)

  • \(\text{If} c\in C_{0} \,\text{then}\, U_{c}:=\left\{\begin{array}{l} \{\alpha :(c,\alpha )\in S_{0}\}, \mathrm{if}\ c\in F_{0}; \\ U_{c}:=\emptyset, \mathrm{if}\ c\not\in F_{0}.\end{array}\right.\)

  • \(\text{If} \,c\in C_{i+1}\backslash C_{i}\, \text{and}\, \c= d, \text{then}\\ U_{c}:=\left\{ \alpha \in A_{c}:\alpha \not\in U_{d}\right\}.\)

  • \( \text{If} c\in C_{i+1}\backslash C_{i}\, \text{and}\, c=a\vee b, \text{then}\\ U_{c}:=\left\{ \alpha \in A_{c}:\alpha FV(a)\in U_{a}\text{}\mathrm{or}\text{}\alpha FV(b)\in U_{b}\right\}.\)

  • \(\text{If} c\in C_{i+1}\backslash C_{i} \text{and} c=\exists v_{a}\ b, \,\text{then}\,\\U_{c}:=\left\{ \alpha \in A_{c}:\exists \alpha ^{\prime }\in N\ (\alpha \subseteq \alpha ^{\prime }\text{\ }\mathrm{and}\text{\ }\alpha ^{\prime}\in U_{b})\right\}\).

Note that in the first item above, the choice of \(U_{c}:=\emptyset\) when \(c\in C_{0}\) and \(c\not\in F_{0}\) is completely arbitrary.Footnote 6 Also, in the third item above where \(c=a\vee b,\) both a and b will be in C i , thanks to the properties of \(^{*}.\)

It is routine to verify, using induction on \(rank_{C}(c),\) that (1) and (2) hold for \(\left( \mathcal{N}_{0},U_{c}\right) _{c\in C}\). More specifically, if \(rank_{C}(c)=0\), then \(\theta _{c}\not\in T_{0}\cap \Theta\), so (1) is vacuously satisfied, and (2) is satisfied by design. On the other hand, when \(rank_{C}(c)>0\) then (1) is satisfied since U c is defined so as to comply with Tarski conditions; and (2) is satisfied since S 0 is an F 0-satisfaction class. This concludes the proof of the consistency of arbitrary finite subsets T 0 of \(Th ^{+}(\mathcal{N}_{0})\), which in turn shows that \(Th^{+}(\mathcal{N} _{0})\) has a model, i.e., some elementary extension \(\mathcal{N}_{1}\) of \(\mathcal{N}_{0}\) has an expansion \(\mathcal{N}_{1}^{+}\) of the form

$$ \mathcal{N}_{1}^{+}:=(\mathcal{N}_{1},U_{c})_{c\in F_{1}}$$

with the property that \(\mathcal{N}_{1}^{+}\models Th^{+}(\mathcal{N}_{0}).\) Let S 1 be the binary relation on N 1 defined via

$$ S_{1}(c,\alpha )\Leftrightarrow \alpha \in U_{c}.$$

It is evident that S 1 is an F 1-satisfaction class, \(S_{1}\supseteq S_{0}\) and \((c,\alpha )\in S_{0}\) whenever \(c\in F_{0}\), \(\alpha \in N_{0}\), and \((c,\alpha )\in S_{1}.\)

Theorem 3.2

Let \(\mathcal{M}_{0}\) be a model of \( PA\) of any cardinality.

  1. (a)

    If S 0 is an F 0 -satisfaction class on \(\mathcal{M}_{0}\) , then there is an elementary extension \(\mathcal{M}\) of \(\mathcal{M}_{0}\) that carries a full satisfaction class that extends S 0 .

  2. (b)

    There is an elementary extension \(\mathcal{M}\) of \(\mathcal{M}_{0}\) that carries a full satisfaction class.

Proof

Note that (b) is an immediate consequence of (a) since we may choose F 0 to be the set of atomic \(\mathcal{M}_{0}\)-formulae and S 0 to be the obvious satisfaction predicate for \(F_{0}.\) To establish (a), we note that by Lemma 3.1 there is an elementary extension \(\mathcal{M}_{1}\) of \(\mathcal{M}_{0}\) that carries an F 1-satisfaction class, where \(F_{1}:= Form^{\mathcal{M}_{0}}\). Lemma 3.1 allows this argument to be carried out ω-times to yield two sequences \(\left\langle \mathcal{M}_{i}:i\in \omega \right\rangle\) and \(\left\langle S_{i}:i\in \omega \right\rangle\) that satisfy the following properties for each \(i\in \omega\):

  1. 1.

    [(1)] \(\mathcal{M}_{i}\prec \mathcal{M}_{i+1}\);

  2. 2.

    [(2)] \(S_{i+1}\) is an \(F_{i+1}\)-satisfaction class on \(\mathcal{M} _{i+1}\) with \(F_{i+1}:= Form^{\mathcal{M}_{i}};\) and

  3. 3.

    [(3)] \(S_{i}=S_{i+1}\cap \{(c,\alpha ):c\in F_{i}\), \(\mathcal{M} _{i}\models Asn(\alpha,c)\}.\)

Let \(\mathcal{M}:=\bigcup\limits_{i\in \omega}\mathcal{M}_{i},\ \mathrm{and\ }S:=\bigcup\limits_{i\in \omega}S_{i}\). Tarski’s elementary chain theorem and (1) together imply that \(\mathcal{M}\) elementarily extends \(\mathcal{M}_{0}\). It is easy to see, using (2) and (3), that S is a full satisfaction class on \(\mathcal{M}\). ▪

Theorem 3.2, when coupled with the completeness theorem of first order logic, immediately yields the following conservativity result.

Corollary 3.3

\( PA^{ FS}\) is a conservative extension of \( PA\) .

Proof

Suppose not. Then for some arithmetical sentence \(\varphi\) we have:

  1. 1.

    [(1)] \( PA^{ FS}\vdash \varphi\), and

  2. 2.

    [(2)] \(PA\not\vdash \varphi.\)

Since (2) implies that \(PA\cup \{ \varphi \}\) is consistent, by the completeness theorem for first order logic, there is a model \(\mathcal{M}_{0}\models PA\cup \{ \varphi \}.\) On the other hand, by part (b) of Theorem 3.2 there is an elementary extension \(\mathcal{M}_{1}\) of \(\mathcal{M}_{0}\) that carries a full satisfaction class, and therefore by (1) \(\mathcal{M}_{1}\models \varphi.\) This contradicts the fact that \(\mathcal{M}_{1}\) elementarily extends \(\mathcal{M} _{0}.\)

Corollary 3.4

Every resplendent model of \( PA\) carries a full satisfaction class. In particular, every countable recursively saturated model of \( PA\) carries a full satisfaction class.

Proof

The first claim directly follows from the definition of a resplendent model. The second claim follows from the first claim, when coupled with the key result that countable recursively saturated models are resplendent (see (Kaye1991, Sect. 15.2) for more detail).▪

4 Truth Classes

With the exception of Krajewski’s original paper (Krajewski1976), what we refer to as a ‘truth class’ here has been dubbed ‘satisfaction class’ in the model-theoretic literature. More specifically, Krajewski (1976) employed the framework of satisfaction classes over base theories formulated in relational languages as in this paper, however, the later series of papers (Kotlarski et al.1981; Smith 1987,1989) all used the framework of truth classes over Peano arithmetic formulated in a relational language, augmented with ‘domain constants’. Later, Kaye (1991) developed the theory of satisfaction classes over models of \(PA\) in languages incorporating function symbols; his work was extended by Engström (2002) to truth classes over models of \(PA\) in functional languages.

As explained in this section, there is a simple canonical correspondence between truth classes over models of PA (in a relational language) and certain types of satisfaction classes, here referred to as ‘extensional’. The main aim of this section is to demonstrate that the method of building satisfaction classes in the previous section can be conveniently modified so as to yield full extensional satisfaction classes (and thereby: full truth classes) over appropriate models of \(PA\).

Within \(PA\) one can easily define an injective function \(c\) that yields the code for a constant symbol \(\overline{x}\) for each member x of the domain. This enables \(PA\) to internally represent the language \(\mathcal{L}_{ PA}^{+}=\mathcal{L}_{ PA}+\) ‘domain constants’. We can then add a unary \predicate \ \( T (x)\) denoting a truth class (instead of a binary predicate \(S(x,y)\) for a satisfaction class) to \(\mathcal{L}_{ PA}\), whose intended interpretation is “ x is the code of a true sentence \( \sigma\)”, where σ is an arithmetical sentence formulated in a language \(\mathcal{L}_{ PA}^{+}\). We will make this more precise in the following definition.

Definition 4.1

\(PA^{ FT}:= PA \cup Tarski( T)\), where \(Tarski( T)\) is the conjunction of the universal generalizations of \(tarski_{0}( T)\) through \(tarski_{4}( T),\) all formulated in the language \(\mathcal{L}_{ PA}\cup \{ T(\cdot )\}\), as described below.Footnote 7 In what follows \(Sent(x)\) is the \(\mathcal{L}_{ PA}\)-formula that expresses “ x is a formula of \(\mathcal{L}_{ PA}^{+}\) with no free variables”, and R ranges over relations symbols in \(\mathcal{L}_{ PA}\).

  • { tarski} \(_{0}( T):=\left( T(x)\rightarrow Sent(x)\right).\)

  • { tarski} \(_{1,R}( T):=\left( R(\overline{t} _{0},\cdot \cdot \cdot,\overline{t}_{n-1}) =x\right) \rightarrow \left( R(t_{0},\cdot \cdot \cdot,t_{n-1})\leftrightarrow T (x)\right).\)

  • { tarski} \(_{2}( T):=\left( x= y\right) \rightarrow \left( T(x)\leftrightarrow T(y_{1})\right).\)

  • { tarski} \(_{3}( T):=\left( x=y_{1}\vee y_{2}\right) \rightarrow \left( T(x)\leftrightarrow \left( T(y_{1})\vee T(y_{2})\right) \right).\)

  • { tarski} \(_{4}( T):=\left( x=\exists v_{i}\varphi \right) \rightarrow \left( T(x)\leftrightarrow \exists z\ T \left( \varphi \left( \overline{z})\right) \right) \right)\).

T is a full truth class on \(\mathcal{M}\) if \((\mathcal{M},T)\models PA^{ FT}.\)

Definition 4.2

\A substitution for a formula ψ of \(\mathcal{L}_{ PA}\) is a function

$$\sigma: FV(\psi )\rightarrow Var$$

such that σ respects substitutability in the ‘usual way’, i.e., if x is a free variable of ψ, then x is not in the scope of any quantifier that binds \(\sigma (x).\) Given ψ and σ as above, let \(\psi *\sigma\) be the formula obtained from ψ by applying the substitution σ, and A be the set of pairs \((\varphi,\alpha )\) such that α is an assignment for the formula \(\varphi.\) This allows us to define a key equivalence relation \(\thicksim \) on A by decreeing that \((\varphi _{0},\alpha _{0}) (\varphi _{1},\alpha _{1})\) iff there is some \((\psi,\beta )\in A\), and there are substitutions \(\sigma _{0}\) and \(\sigma _{1}\) for ψ, with

$$\varphi _{i}=\psi *\sigma _{i}\, \text{and}\, \beta =\alpha _{i}\circ \sigma _{i},\, \text{for}\, i=0,1.$$

In the above, \(\alpha _{i}\circ \sigma _{i}\) is the composition of \(\alpha _{i}\) and \(\sigma _{i}.\) It is important to bear in mind that, intuitively speaking, \((\varphi _{0},\alpha _{0}) (\varphi _{1},\alpha _{1})\) means that \(\varphi _{0}\) and \(\varphi _{1}\) are the same except for their free variables, and for all variables x and y, if x occurs freely in the same position in \(\varphi _{0}\) as y does in \(\varphi _{1}\), then \(\alpha _{0}(x)=\alpha _{1}(y).\)

  • An F-satisfaction class S is extensionalif for all \(\varphi _{0}\) and \(\varphi _{1}\) in F, \(\mathcal{M}\models (\varphi _{0},\alpha _{0}) (\varphi _{1},\alpha _{1})\) implies \((\varphi _{0},\alpha _{0})\in S\) iff \((\varphi _{1},\alpha _{1})\in S\).Footnote 8

The following proposition describes a canonical correspondence between extensional satisfaction classes and truth classes. The routine but laborious proof is left to the reader.

  • In what follows c is the \(\mathcal{M}\)-definable injection \ \(m\mapsto _{ c}\overline{m}\) \that designates a constant symbol \(\overline{m}\) for each \ \(m\in M,\) and \(\varphi ( c\circ \alpha )\) is the sentence in the language \(\mathcal{L}_{ PA}^{+}\) obtained by replacing each occurrence of a free variable x of ϕ with the constant symbol \(\overline{m}\), where \(\alpha (x)=m.\)

Proposition 4.3

Suppose \(\mathcal{M}\models PA\) , T is a full truth class on \(\mathcal{M}\) , and S is an extensional full satisfaction class on \(\mathcal{M}.\)

(a)\ \(\mathcal{S}(T)\) is an extensional satisfaction class on \(\mathcal{M}\) , where \(\mathcal{S}(T)\) is defined as the collection of ordered pairs \((\varphi,\alpha )\) such that \(\varphi ( c\circ \alpha )\in T.\)

(b)\ \(\mathcal{T}(S)\) is a truth class on \( \mathcal{M}\) , where \(\mathcal{T}(S)\) is defined as the collection of \(\varphi \in \mathcal{L}_{ PA}^{+}\) such that for some \(\psi \in \mathcal{L}_{ B}^{+}\) and some assignment α for ψ, \(\varphi =\psi ( c\circ \alpha )\) and \((\psi,\alpha )\in S\) .

(c)\ \(\mathcal{S}(\mathcal{T}(S))=S\) , and \(\mathcal{T}(\mathcal{S(}T))=T.\)

Before describing the construction of extensional satisfaction classes we need the preliminaries presented in Definition 4.4 and Lemma 4.5.

Definition 4.4

  1. (a)

    Given formulae \(\varphi _{0}\) and \(\varphi _{1}\) of \(\mathcal{L}_{ PA}\), we write \(\varphi _{0}\boldsymbol{approx} \varphi _{1}\) if there is a formula ψ, and substitutions \(\sigma _{0}\) and \(\sigma _{1}\) for \(\psi\) such that \(\varphi _{i}\boldsymbol{\approx} \psi *\sigma _{i}\) for \(i=0,1.\)

  2. (b)

    Given \(c\in Form^{\mathcal{M}}\), let \(\mathbf{TC}_{\mathcal{M}}(c)\) be the externally defined transitive closure of c with respect to the direct subformula relation, i.e.,

$$\mathbf{TC}_{\mathcal{M}}(c):=\bigcup\limits_{n<\omega}\mathbf{TC}_{\mathcal{M}}(c,n),$$

where \(\mathbf{TC}_{\mathcal{M}}(c,0):=\{c\}\) and

$$\mathbf{TC}_{\mathcal{M}}(c,n+1):=\{x\in M:x ^{\mathcal{M}}d \,\text{for some}\, d\in \mathbf{TC}_{\mathcal{M}}(c,n)\}.$$

The following lemma presents salient features of the two equivalence relations and \(\boldsymbol{\approx}\).

Lemma 4.5

Let \(\thicksim \) be as in Definition 4.2; and \(\mathbf{TC}_{\mathcal{M}}(c)\) and \( \boldsymbol{\approx}\) be as in Definition 4.4.

\((i)\) If \(d\in \mathbf{TC}_{\mathcal{M}}(c)\) and \(d\neq c\) , then \(\left( c\boldsymbol{\approx} d\right)\) .

\((ii)\) \(\boldsymbol{\approx}\) preserves the principal connectives, i.e., it relates negations to negations, disjunctions to disjunctions, and existential formulae to existential formulae with the same bound variable. Moreover, if \( c\boldsymbol{\approx} d\) , then \( c\boldsymbol{\approx} d;\) if \(c\vee d\boldsymbol{\approx} c^{\prime}\vee d^{\prime}\) , then \(c\boldsymbol{\approx} c^{\prime}\) and \( d\boldsymbol{\approx} d^{\prime};\) and if \(\exists t\) \ \( c\boldsymbol{\approx} \exists t^{\prime}\) \ \(c^{\prime}\) , then \( t=t^{\prime}\) and \(c\boldsymbol{\approx} c^{\prime}.\)

\((iii)\) If \((\varphi _{0},\alpha _{0}) (\varphi _{1},\alpha _{1})\) , then \(\varphi _{0}\boldsymbol{\approx} \varphi _{1}.\)

\((iv)\) If \(( \varphi _{0},\alpha _{0}) ( \varphi _{1},\alpha _{0}),\) then \((\varphi _{0},\alpha _{0}) (\varphi _{1},\alpha _{1})\) .

\((v)\) If \((\varphi _{0}\vee \varphi _{1},\alpha) (\varphi _{0}^{\prime}\vee \varphi _{1}^{\prime},\alpha ^{\prime})\) , then \(\left( \varphi _{0},\alpha FV(\varphi _{0})\right) \left( \varphi _{0}^{\prime},\alpha ^{\prime} FV(\varphi _{0}^{\prime})\right)\) and \(\left( \varphi _{1},\alpha FV(\varphi _{1})\right) \left( \varphi _{1}^{\prime},\alpha ^{\prime} FV(\varphi _{1}^{\prime})\right).\)

\((vi)\) If \(\varphi =\exists t\ \psi,\) and \( \varphi ^{\prime}=\exists t^{\prime}\ \psi ^{\prime},\) and \( (\varphi,\alpha) (\varphi ^{\prime},\alpha ^{\prime}),\) then \(t=t^{\prime}\) and for some e

$$(\varphi ,\alpha [t:e])\thicksim (\varphi ^{\prime },\alpha ^{\prime}[t^{\prime}:e]).$$

Footnote 9

The next Lemma presents a variant of Lemma 3.1 that is our main tool for constructing extensional satisfaction classes.

Lemma 4.6

Let \(\mathcal{N}_{0}\models\) \ \( PA\) , \(F_{1}:= Form^{\mathcal{N}_{0}}\) , \(F_{0}\subseteq F_{1},\) and suppose S 0 is an extensional F 0 -satisfaction class. Then there is an elementary extension \( \mathcal{N}_{1}\) of \(\mathcal{N}_{0}\) that carries an extensional F 1 -satisfaction class \(S_{1}\supseteq S_{0}\) and \((c,\alpha )\in S_{0}\) whenever \(c\in F_{0}\) , \(\alpha \in N_{0}\) , and \((c,\alpha )\in S_{1}\).

Proof

Let Θ and ▪ be as in the proof of Lemma 3.1, and let

$$ Th^{+}(\mathcal{N}_{0}):= {Th}(\mathcal{N} _{0},a)_{a\in N_{0}}\cup \Theta \cup \Upgamma \cup \Updelta,$$

where \(\Updelta:=\left\{ \Updelta_{cc^{\prime}}:c,\ c^{\prime}\in F_{1}\right\},\) and

$$\Updelta_{cc^{\prime}}:=\forall \alpha \forall \alpha ^{\prime}\left( (c,\alpha) (c^{\prime},\alpha ^{\prime})\rightarrow \left( U_{c}(\alpha )\leftrightarrow U_{c^{\prime}}(\alpha ^{\prime})\right) \right).$$

The proof of the lemma would be complete once we verify that \(Th^{+}(\mathcal{N}_{0})\) has a model. To this end, we shall demonstrate that every finite subset T 0 of \(Th^{+}(\mathcal{N} _{0})\) is interpretable in \(\mathcal{N}\). Let C be the collection of \(c\in F_{1}\) such that c appears in \(T_{0}.\) Also, let \(^{*}\) and \(rank_{C}(c)\) be precisely as in the proof of Lemma 3.1.

We can extend C to another finite set \(\overline{C}\) so that it satisfies a certain closure property, namely: whenever we have \(c\boldsymbol{\approx} c^{^{\prime}}\) and \(d ^{*}c\), where c, \(c^{\prime}\) and d are all in \(\overline{C}\), then there is some \(d^{\prime}\in \overline{C}\) such that \(d^{\prime }\vartriangleleft ^{*}c^{\prime }\) with \(d\boldsymbol{\approx} d^{^{\prime}}\). This can be done simply by adding any missing direct subformulae \(d^{\prime}\) by an appropriate recursion.Footnote 10 By replacing C by \(\overline{C}\) we may therefore additionally assume:

(#) If c and \(c^{\prime}\) are both in C with \(c\boldsymbol{\approx} c^{\prime}\), then \(rank_{C}(c)= rank_{C}(c^{\prime}).\)

As in the proof of Lemma 3.1, we then recursively construct \(\{U_{c}:c\in C\}\) such that:

(1) \(\left( \mathcal{N}_{0},U_{c}\right) _{c\in C}\models \{\theta _{c}:c\in C\}\) and

(2) For \(c\in C\cap F_{0},\) \(U_{c}=\{\alpha \in N_{0}:(c,\alpha )\in S_{0}\}.\)

It remains to show:

(3) \(\left( \mathcal{N}_{0},U_{c}\right) _{c\in C}\models \left\{ \Updelta_{cc^{\prime}}:c,\ c^{\prime}\in C\right\}.\)

We establish (3) by using induction on \(rank_{C}(c)\) to show that \(\forall c\in C\ P(c),\) where P(c) abbreviates:

$$\forall c^{\prime}\in C\ \left( \mathcal{N}_{0},U_{c}\right) _{c\in C}\models \forall \alpha \forall \alpha ^{\prime}\ \left( (c,\alpha) (c^{\prime},\alpha ^{\prime})\rightarrow \left( U _{c}(\alpha )\leftrightarrow U_{c^{\prime}}(\alpha ^{\prime})\right) \right).$$

If \(rank_{C}(c)=0\) and \((c,\alpha) (c^{\prime},\alpha ^{\prime})\), then by part \((iii)\) of Lemma 4.5 we have \(c\boldsymbol{\approx} c^{\prime},\) which in turn by (#) assures us that \(rank_{C}(c^{\prime})=0\). This makes it clear that P(c) holds when \(rank_{C}(c)=0\) since S 0 is assumed to be an extensional F 0-satisfaction class.

To verify the inductive step, suppose:

(4) P(x) holds for all \(x\in C\) with \(rank_{C}(x)=i.\)

Let \(c\in C\) with \(rank_{C}(c)=i+1,\) and suppose \((c,\alpha) (c^{\prime},\alpha ^{\prime})\), where \(c=\exists t\ d.\) Then \(c^{\prime}=\exists t^{\prime}\ d^{\prime}\), and \(d\boldsymbol{\approx} d^{\prime}\) by part \((ii)\) of Lemma 4.5. Observe that thanks to (#) we have:

(5) \(rank_{C}(c^{\prime})=i+1\) and \(rank_{C}(d)= rank_{C}(d^{\prime})=i\).

Now if \(\alpha \in U_{c},\) then \(\alpha [t:e]\in U_{d}\) for some e by (1), and therefore by part \((vi)\) of Lemma 4.5, we obtain:

(6) \((d,\alpha [t:e]) (d^{\prime},\alpha ^{\prime}[t^{\prime}:e])\).

Using (4), (5), and (6) we may now conclude that \(\alpha ^{\prime}[t:e]\in U_{d^{\prime}}\), which by (1) yields \(\alpha ^{\prime}\in U_{d}\), thus completing the verification of the quantificational case (by symmetry). A similar reasoning can be carried out for propositional cases. This concludes the proof of consistency of \(T_{0}.\)

The rest is precisely as before: the consistency of \(Th^{+}(\mathcal{N}_{0})\) implies that there is an elementary extension \(\mathcal{N} _{1}\) of \(\mathcal{N}_{0}\) that has an expansion \(\mathcal{N}_{1}^{+}:=(\mathcal{N}_{1},S)\models Th^{+}(\mathcal{N}_{0}),\) and the binary relation S 1 on \(\mathcal{N}_{1}\) defined via

$$ S_{1}(c,\alpha )\Leftrightarrow \alpha \in U_{c}$$

has the property that S 1 is an extensional F 1 -satisfaction, \(S_{1}\supseteq S_{0}\), and \((c,\alpha )\in S_{0}\) whenever \(c\in F_{0}\), \(\alpha \in N_{0}\), and \((c,\alpha )\in S_{1}.\)

Theorem 4.7

Let \(\mathcal{M}_{0}\models PA\). There is an elementary extension \(\mathcal{M}\) of \(\mathcal{M}_{0}\) that carries a full extensional satisfaction class.

Proof

Since the satisfaction class S 0 on the collection F 0 of atomic formulae of \(\mathcal{M}_{0}\) is extensional, we may use Lemma 4.6 instead of Lemma 3.1 in order to carry out the elementary chain argument of Theorem 3.2. ▪

By coupling Theorem 4.7 with part (b) of Proposition 4.3 we obtain:

Corollary 4.8

Every model of \( PA\) has an elementary extension that carries a full truth class.

Finally, the line of reasoning employed in the proof of Corollary 3.3 shows, using Corollary 4.8, that:

Corollary 4.9

\(PA^{ FT}\) is a conservative extension of \( PA\).

5 Arithmetization, Interpretability, and Conservativity\

Here we briefly discuss the arithmetizationof the constructions of the previous two sections, with an eye towards issues connected with interpretability and conservativity. As explained in (Enayat and Visser, Sect. 4) the compactness and elementary chain argument employed in the proofs of Theorems 3.2 and 4.7 can be implemented in the fragment \(I _{2}\) of PA with the help of the ‘Low Basis Theorem’ of Recursion Theory. Coupled with Orey’s Compactness Theorem, this can used to establish the following:

Theorem 5.1

(Enayat and Visser)\ \( PA ^{ FT}\) is interpretable in \( PA.\) Footnote 11

On the other hand, the technology of \(\mathrm{LL}_{1}\) -sets Footnote 12 of (Hájek and Pudlák 1993, Theorem 4.2.7.1, p. 104) can be used to show that the proofs of both theorems 3.2 and 4.7 can even be implemented in the fragment \(I _{1}\) of PA. In light of the fact that the statement “ \( PA^{ FT}\) is conservative over\ \( PA\) ” is a 2 -statement, and \(I _{1}\) is well known Footnote 13 to be 2 -conservative over \(PRA\) , we obtain the following:

Theorem 5.2

(Enayat and Visser) The conservativity of \( PA^{ FT}\) over \(PA\) can be verified in \( PRA.\) Footnote 14

Remark 5.3

The verification of the conservativity of \(PA^{ FT}\) \over \(PA\) within \(PRA\) was first claimed by Halbach in (Halbach1999), using cut-elimination.Footnote 15 Later, Fischer (2009) gave a proof, based on the cut-elimination argument in (Halbach1999), to show that \(PA^{ FT}\) is interpretable in \(PA.\) Unfortunately, a gap was discovered recently (by Fujimoto) in the cut-elimination argument in (Halbach1999), which in turn impaired Fischer’s interpretability claim. Happily, Leigh (2012) has succeeded in developing a proof-theoretic demonstration of the conservativity of \(PA^{ FT}\) \over \(PA\) that is implementable in \(PRA.\) Moreover, (Leigh2012, Theorem 1) can be used to verify the interpretability of \(PA^{ FT}\) \ over \(PA\), by using Fischer’s strategy in (Fischer2009).Footnote 16 Therefore, Theorems 5.1 and 5.2 can be arrived at via two completely different routes.

6 Further Results

In Sect. 16.4 we saw that the core methodology of Sect 3 can be fine-tuned to build full extensional satisfaction classes. Indeed, as shown in (Enayat and Visser 2012) one can strengthen Theorem 4.7 by imposing further desirable conditions on the satisfaction class S. For example, every model \(\mathcal{M}_{0}\) of \(PA\) has an elementary extension \(\mathcal{M}\) that carries a full extensional satisfaction class S that satisfies all of the following additional properties:

  1. 1.

    [(1)] \(Sat_{n}^{\mathcal{M}}\subseteq S\) for all \(n\in \omega\) (see Theorem 2.5 for Sat n ).

  2. 2.

    [(2)] If \(c\in Form^{\mathcal{M}}\) and \(\mathcal{M}\models\)c is an axiom of \(PA\)”, then S deems c to be ‘true’.Footnote 17

  3. 3.

    [(3)] If c and \(c^{\prime}\) are \(\mathcal{M}\)-formulae such that \(\mathcal{M}\models\)\(c^{\prime}\) is an alphabetic variantFootnote 18 of c ”, then \((c,\alpha )\in S\) iff \((c^{\prime},\alpha )\in S\).

Furthermore, the third condition above can be strengthened by accomodating a combination of extensional equivalence and alphabetic equivalence, thereby yielding truth classes that are closed under alphabetic equivalence. We have also shown that a small dose of condition (1) can be used to build full truth classes over models of arithmetical theories formulated in functional languages (this result will appear in the projected sequel to (Enayat and Visser)).

One can also use the method of Sect. 16.3 to build bizarre satisfaction classes. For example, as shown in (Enayat and Visser, Sect.  5), every model \(\mathcal{M}_{0}\) of \(PA\) has an elementary extension \(\mathcal{M}\) that has a full satisfaction class S that exhibits the following pathology:

$$\{a\in M:(\sigma _{a},\alpha _{ Null})\in S\}=\omega _{\mathcal{M}},$$

where \(\omega _{\mathcal{M}}\) is the well-founded initial segment of \(\mathcal{M}\) that is isomorphic to ω, and \(\sigma _{a}\) is defined for all \(a\in M\) by a recursion within \(\mathcal{M}\) via the following clauses:

  • \(\sigma _{0}:=\exists v_{0}\left( v_{0}=v_{0}\right)\) (or \(\sigma _{0}=\) any other logically valid sentence);

  • \(\sigma _{n+1}:=\left( \sigma _{n}\vee \sigma _{n}\right).\)