Consider second-order Peano Arithmetic Z2, i.e. the two-sorted first-order theory with induction and comprehension. Remove the assumption about the totality of the successor relationship (the Successor Axiom), i.e. the assumption that every number is successored by a number. Call this theory FPA. FPA has as models the standard model (if it exists) and all the initial segments. FPA is "downward": if a natural number exists, it can prove all numbers less than that number exists, but none that are greater. So it cannot prove the infinity of the primes, but then this assertion isn't even true in all its models, e.g. {0,1,2,3} has two primes, and 2 is a member of the set, so the set of primes is finite in this model. FPA can, however, prove Bertrand's Postulate.

Are there any simple mathematical examples of assertions true in all models of FPA, provable in Z2, but not provable in FPA?

EDIT: On François' advice, I am adding here some clarifications which appear in comments.

Full comprehension is used.

Successoring is considered to be a 2-ary relationship, addition and multiplication to be 3-ary relationships. The usual axioms can be easily restated in these terms.

The logic is supposed to include variable n-ary relationships, for n = 1 but also for n > 1, which can be quantified over and whose existence can be proved using comprehension. So for instance, FPA is able to define size equivalence in the straightfoward fashion: A ~ B if and only if (there exists R)(R is a 1-1 function from A onto B). (In fact, given this apparatus, addition and multiplication can be defined from successoring, so one doesn't even need axioms about addition and multiplication, although this is a detail which should not affect the question asked.)

Induction can be considered to be: (P)(P0 & (n)(m)(Pn & Nn & Sn,m => Pm) => (n)(Nn => Pn)), where "N" is "is natural number" and "S" is successoring.

There are many ways to assert the infinity of primes. One way would be to define "a < b" as

(there exists x)(x > 0 & +(a,x,b)) and

"MP,n" (P has size n) as

P ~ {x : x < n}. Then

(not there exists n)(Nn & M{p : p is prime},n)

asserts the infinity of primes. Or one can state in via unboundedness: (n)(Nn => (there exists p)(p > n and p is prime)).

  • $\begingroup$ If you are really talking about a (two-sorted) first order theory, please don't call it "second order". This is confusing. (To me. Perhaps also to you.) And when you mention "comprehension", do you mean full comprehension, with quantifiers over both sorts allowed? $\endgroup$
    – Goldstern
    Jan 26, 2013 at 10:25
  • $\begingroup$ Yes, full comprehension. I'm not trying to be confusing, but I don't see why it is. Simpson uses this terminology all the time: "the language of second-order arithemtic is a two-sorted language," "the axioms of second-order arithmetic," "by second oder arithmetic we mean the formal system...," $\endgroup$
    – abo
    Jan 26, 2013 at 10:40
  • 1
    $\begingroup$ How is induction restated? $\endgroup$ Jan 26, 2013 at 18:09
  • 1
    $\begingroup$ "Then define '$P$ has size $n$' iff there exists 1-1 function from $\lbrace x \vert x \lt n\rbrace$ onto P." How are functions defined? (I don't see any pairing functions around.) $\endgroup$ Jan 26, 2013 at 18:14
  • 1
    $\begingroup$ Maybe you should add all of this to the question since there are lots of choices which aren't clearly equivalent. $\endgroup$ Jan 26, 2013 at 19:45

3 Answers 3


As I already mentioned in another thread for a slightly different theory, it is possible to give a complete description of models of FPA (I mean all models, giving a complete semantics for the many-sorted first-order theory, not just proper second-order models, which abo lists in the question and which I will henceforth call “standard”) in terms of more familiar theories:

  • Models where successor is total are exactly the models of $Z_2$.

  • Models where successor is not total. If $M\models I\Delta_0+\Omega_1$ and $0< a\in M$ is such that $M\models{}$ “$2^a$ exists”, we can form the following model $A_{M,a}$: its “first-order” sort consists of the submodel $[0,a)_M$ of $M$ (where successor, addition, and multiplication are considered as relations, not functions), and for every $n$, its “second-order” universe of $n$ary relations consists of $[0,2^{a^n})_M$, where $r< 2^{a^n}$ represents the relation $$\{\langle u_0,\dots,u_{n-1}\rangle\in[0,a)^n:M\models\mathrm{bit}(r,a^{n-1}u_{n-1}+\dots+au_1+u_0)=1\},$$ where $\mathrm{bit}(x,u)$ is the $u$th bit in the binary representation of $x$. (Note that the existence of $2^a$ implies the existence of $2^{a^n}$ by $\Omega_1$.) Then $A_{M,a}\models\mathrm{FPA}$: the main thing is that the validity of any (second-order) formula in $A_{M,a}$ translates to a formula in $M$ whose all quantifiers are bounded by some $2^{a^n}$, and $I\Delta_0+\Omega_1$ proves bit-comprehension for $\Delta_0$-definable subsets of logarithmically small intervals, which implies full comprehension in $A_{M,a}$.

    Conversely, every model $A\models\mathrm{FPA}$ where successor is not total is isomorphic to $A_{M,a}$ for some $M,a$ as above. I will sketch the argument below. FPA proves that $A$ has a largest element, and satisfies full first-order induction; this first-order theory is called $\mathrm{PA^{top}}$, and it is well-known that every its model $A$ can be extended into a model $B$ of $I\Delta_0$ so that $A$ is its submodel of the form $[0,a)$, and the standard powers $\{a^n:n\in\omega\}$ are cofinal in $B$ (unless $a=1$). The construction works as follows: for every $n$, elements of the interval $[0,a^n)$ in $B$ can be represented by $n$tuples of elements of $A$; one can define in $\mathrm{PA^{top}}$ the arithmetic operations on such $n$tuples in such a way that these $[0,a^n)$ form an increasing chain of models whose union is taken as $B$. In our case, we also have the second-order universes of $n$-ary relations, and these can be used to represent exponentially larger numbers: an $n$-ary relation from $A$ (i.e., a subset of $[0,a^n)$) will represent a number below $2^{a^n}$ in binary. In this way, we can extend $B$ into a model $M$ such that $B=\{x\in M:M\models2^x\text{ exists}\}$. Since any bounded formula in $M$ translates into a second-order formula in $A$, $M$ will satisfy $\Delta_0$ induction up to logarithmically small numbers (this is called length induction), which implies $I\Delta_0$. $M\models\Omega_1$ follow from the fact that $\{2^{a^n}:n\in\omega\}$ is cofinal in $M$. By the construction, $A\simeq A_{M,a}$.

    (The second part of the argument, viz. a correspondence of “second-order” models of arithmetic with bounded sets to “first-order” models with exponentially larger numbers is known as the RSUV isomorphism.)

This gives a characterization of provability in FPA: for any (second-order) sentence $\phi$, the construction above implicitly gives a first-order formula $\phi^*$ such that

$\mathrm{FPA}\vdash\phi$ iff $Z_2\vdash\phi$ and $I\Delta_0+\Omega_1\vdash\phi^*$.

Note that $\phi^*$ is a $\Pi^0_1$-sentence; conversely, every $\Pi^0_1$-sentence is equivalent to one of this form. Note that the standard models of FPA with non-total successor are $A_{\mathbb N,n}$ for some $n\in\mathbb N$, hence the question reduces to: find sentence $\phi$ such that $Z_2\vdash\phi$, $\mathbb N\models\phi^*$, but $I\Delta_0+\Omega_1\nvdash\phi^*$.

An example of such a statement is $\mathrm{Con}_Q$ (the formal consistency of Robinson arithmetic), formulated as a $\Pi^0_1$-formula of the form $\forall x\,\theta(x)$, where $\theta(x)$ is a formula whose all quantifiers are bounded to $x$, and atomic formulas are reformulated in such a way that they do not refer to any numbers above $x$. The translation $\phi^*$ is then essentially equivalent to $\forall x\,\theta(|x|)$, where $|x|$ is the length function, that is, the statement that $Q$ has no logarithmically short proofs of contradiction. This is not provable in $I\Delta_0+\Omega_1$. Thus, $\mathrm{Con}_Q$ is not provable in FPA, but it holds in all its standard models, and it is provable in $Z_2$.

Independent $\Pi^0_1$ statements (for weak or strong arithmetic) in the literature are mostly variants of consistency statements. While this is not a precise question, it is a sort of an open problem to find natural combinatorial $\Pi^0_1$ statements independent of particular fragments of arithmetic. Let me mention two principles which are conjectured to be unprovable in $I\Delta_0+\Omega_1$, and therefore would give the wanted example for FPA:

  • $\Delta_0$-$\mathrm{PHP}$: the pigeonhole principle. In the language of FPA, it is the following schema: for every formula $\phi(u,X,Y)$ (possibly with other parameters not shown), $$\begin{align}\forall u\,\neg[&\forall X\subseteq[0,u]\,\exists Y\subsetneq[0,u]\,\phi(u,X,Y)\\&{}\land\forall X_0,X_1,Y\subseteq[0,u]\,\neg(\phi(u,X_0,Y)\land\phi(u,X_1,Y))].\end{align}$$ (I.e., $\phi$ does not define an injective (multi-)function from $\mathcal P([0,u])$ into itself minus one set.)

  • $\mathrm{Count}_2(\Delta_0)$: the counting principle modulo $2$. In the language of FPA, it is the schema $$\begin{align}\forall u\,\neg[&\forall X\subsetneq[0,u]\,\exists!Y\subsetneq[0,u]\,\phi(u,X,Y)\\&{}\land\forall X,Y\subsetneq[0,u]\,(\phi(u,X,Y)\to X\ne Y\land\phi(u,Y,X))]\end{align}$$ for every formula $\phi(u,X,Y)$. (I.e., $\phi$ does not define a fixpoint-free involution on $\mathcal P([0,u])$ minus one set. In general, the mod $k$ counting principle would state that some canonical class of finite cardinality not divisible by $k$ cannot be partitioned into $k$-element subclasses, but it’s easier to state it just for $k=2$.)

  • $\begingroup$ I should have also mentioned that the weak pigeonhole principle, which is obtained from the pigeonhole principle by replacing $Y\subsetneq[0,u]$ with $Y\subseteq[0,u)$, is provable in FPA, since $I\Delta_0+\Omega_1\vdash\Delta_0$-WPHP. $\endgroup$ Jan 28, 2013 at 15:20
  • $\begingroup$ Very nice, Emil. Thanks very much. I once went through a paper that proved the Prime Number Theorem in I\Delta_0+exp and it seemed to me the proof went through in FPA. Would this be in error? Also, I would like to ask another question about provability in FPA. If I were to describe the system as x + y, where y is just the list of the Peano axioms which FPA uses, what is the shortest x which is clear? Following Goldstern: a many-sorted first order theory with one "lowercase" sort (for numbers) and infinitely many "upper-case sorts" (the nth sort being n-ary relations)? $\endgroup$
    – abo
    Jan 28, 2013 at 19:30
  • $\begingroup$ By the way, I can't upvote you because I'm not registered. Sorry. $\endgroup$
    – abo
    Jan 28, 2013 at 19:31
  • $\begingroup$ I’m sorry, but I don’t follow the x+y bit. As for PNT: this sounds plausible. While provability in FPA corresponds to $I\Delta_1+\Omega_1$, the numbers in the latter theory correspond to sets in the former. “First-order” consequences of FPA correspond to statements that are provable in $I\Delta_0+\Omega_1$ for logarithmically small numbers, which allows for a limited use of exponentiation. It quite often happens that statements provable in $I\Delta_0+\exp$ are provable for logarithmically small numbers in $I\Delta_0+\Omega_1$. (In fact, by a simple compactness argument, if $I\Delta_0+\exp$ ... $\endgroup$ Jan 29, 2013 at 14:36
  • $\begingroup$ ... proves $\forall x\,\phi(x)$ where $\phi$ is $\Sigma^0_1$, then $I\Delta_0\vdash\forall x\,(2^x_n\text{ exists}\to\phi(x))$ for some constant $n$, where $2^x_n$ is $n$-times iterated exponential of $x$.) I never looked in detail at the Cornaros and Dimitracopoulos paper, but Phuong Nguyen claims in cs.toronto.edu/~pnguyen/studies/prime.pdf that their proof works in $I\Delta_0(\mathrm{count})$, which holds for small numbers in $I\Delta_0+\Omega_1$, and a fortiori in the first-order part of FPA. (He only states it for a weaker form of PNT, but it is not clear to me whether ... $\endgroup$ Jan 29, 2013 at 14:41

Since FPA is a first-order theory, from the completeness theorem, if something is true in all its models, then it is provable in the theory. That can't really be what you're asking.

  • $\begingroup$ No, it's not, but I guess that's my fault. I'm talking about the models of the two-sorted theory considered as a second-order theory. $\endgroup$
    – abo
    Jan 26, 2013 at 8:56
  • $\begingroup$ So by "model" you mean a structure in which every subset of the first sort is represented by an element of the second sort? (I.e., a "full" second order model?) $\endgroup$
    – Goldstern
    Jan 26, 2013 at 10:32
  • $\begingroup$ Yes I'm talking about the full (standard) model. $\endgroup$
    – abo
    Jan 26, 2013 at 10:46
  • $\begingroup$ If $FPA$ is a truly second-order theory, what do you mean by "proved?" I.e., what proof system are you using for $FPA$? $\endgroup$ Jan 27, 2013 at 0:14
  • $\begingroup$ I mean proved in a theory with small and big letters, with full comprehension and induction as stated now in the question. Deductively, this can be considered a first-order theory with many sorts. But semantically, it can be considered a second-order theory. (I hope that makes sense!) $\endgroup$
    – abo
    Jan 27, 2013 at 6:46

This is not an answer, just an attempt at explicitly writing down my interpretation of the question. Too long for a comment.

Z2 and FPA are many-sorted FIRST ORDER theories, with one "lowercase" sort (for numbers) and infinitely many "uppercase" sorts (the n-th sort is for n-ary relations. There are predicates $Succ(x,y)$, $Add(x,y,z)$, $Mult(x,y,z)$ and $Element_n(x_1,\ldots, x_n,Y)$ (one for each $n$). However, we write $S(x)\sim y$ instead of $Succ(x,y)$; similarly $x+y\sim z$ instead of $Add(x,y,z)$, etc. Also we write $Y(x_1,\ldots, x_n)$ instead of $Element_n(x_1,\ldots, x_n,y)$. There is also a relation $\le$.

There are several groups of axioms. The first group says that successor, addition and multiplication are partial functions. The second group says that they satisfy the usual properties from Peano arithmetic whenever defined, e.g.

  • if $x+y\sim z$ and $S(z)\sim z'$ and $S(y)\sim y'$, then $x+y'\sim z'$.

I am not sure about the axioms for $\le$: Perhaps $0\le x$, and $S(y)\sim y' \to (x\le y' \leftrightarrow x\le y \vee x=y')$? Perhaps an axiom demanding that $\le$ is a total order? A discrete total order? (Feel free to edit.) And: "the domain of $S$ is downward closed".

In addition, Z2 (but not FPA) says that all functions are total.

The third group are the comprehension axioms: For every formula $\varphi(x_1,\ldots, x_n,\bar p)$ (where the parameters $\bar p$ may use come from all sorts), the universal quantification of $$\exists Y \ \forall x_1,\ldots, x_n \ [ Y(x_1,\ldots, x_n) \leftrightarrow \varphi(x_1,\ldots, x_n,\bar p)]$$

The fourth group is the induction axiom: $$ \forall Z: \quad [Z(0)\wedge \forall x \forall y\ ((Z(x)\wedge S(x)\sim y )\to Z(y))]\quad \to \quad \forall x \ Z(x) $$

The question is (correct me if I am wrong):

Assume that $\varphi$ is a formula (using any sorts) which is first order provable from Z2, and true in all standard models of FPA. Is $\varphi$ then first order provable from FPA?

(The standard models of FPA are: the natural numbers, and all truncated models. In all standard models, the uppercase sorts are interpreted as the respective power sets.)

  • $\begingroup$ Yes, to your question, except I'll make it into two. Are there any? Is there a simple, mathematical one (i.e. no fair talking about consistencies of theories and so on)? The axiom set itself that you are talking about is getting too complicated. There's a simpler way of writing the axioms which I'll state here. $\endgroup$
    – abo
    Jan 27, 2013 at 14:45
  • 1
    $\begingroup$ (x) = "for all x", [x] = "there exists x", "!" = "not" (0) Full comprehension schema (as you write) (1) N0 (2) (n)(Nn => [m](Nm & Sn,m)) (3) (n)(m)(m')(Nn & Nm & Nm' & Sn,m & Sn,m' => m = m') (4) (n)(m)(n')(Nn & Nm & Nn' & Sn,m & Sn',m => n = n') (5) (n)(Nn => ! Sn,0) (6) Induction (as you write) Consider this as Z2, and FPA as having the same axioms, only without (2). FPA (and Z2) can then define addition, multiplication, and <, and prove these have the usual properties (except totality). (If I get 2 upvotes on this comment, I'll re-edit my question. Ow I'll leave it here.) $\endgroup$
    – abo
    Jan 27, 2013 at 14:55
  • $\begingroup$ The answer to the question near the bottom is "no": the Gödel sentence for FPA, $G_{FPA}$, is true in all standard models of FPA, and is provable in $Z_2$ (because $Z_2$ can verify that the one-element model $\{0\}$ satisfies all the axioms of FPA, hence that FPA is consistent, and thus $Z_2$ is able to prove $G_{FPA}$). But $G_{FPA}$ cannot be provable in FPA (it does not matter whether FPA is "sufficiently strong" as long as it is true). The more interesting question is whether there is a more natural counterexample. I think that is an interesting question but I have no example in mind. $\endgroup$ Jan 27, 2013 at 19:20
  • 1
    $\begingroup$ @Carl. I am a little nervous about the example of G(FPA). FPA can consider the same one-element model and prove that it itself is consistent (using the Godel formula for consistency). This does not contradict the Second Incompleteness Theorem, because FPA is not "sufficiently strong". Why then is Z2 able to prove G(FPA) but not FPA? I guess you're asserting that Z2 can prove Cons(FPA) => G(FPA) while FPA cannot, but where exactly does the proof go wrong? $\endgroup$
    – abo
    Jan 28, 2013 at 6:25
  • $\begingroup$ @abo: I don't see how you formulate the notions "(finite) model" and "satisfaction" in FPA. The usual way to formulate it needs a little bit of arithmetic, which include (I think) totality of the basic functions. $\endgroup$
    – Goldstern
    Jan 28, 2013 at 13:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.