7
$\begingroup$

Recently I got interested in predicative foundations, mostly because of Laura Crosilla's work and because Agda employs a predicative type theory.

From the point of view of a predicative foundation to arithmetic, for instance as proposed in Nelson's book, the consistency of Peano Arithmetic and even of PRA is entirely unclear. From the point of view of a predicative foundation to set theory, such as CZF or Kripke–Platek set theory, the consistency of impredicative set theories such as IZF, ZF or ZFC is entirely unclear.

Question. Impredicative foundations such as PRA or ZF seem to be consistent. I'm wondering whether there are any arguments explaining this apparent consistency from the point of view of predicative arithmetic or predicative set theory. Surely there are no formalizable such arguments, since the impredicative systems encompass their predicative analogues, but I'm also interested in informal, philosophical or somewhat vague arguments.

Analogue. A mathematician who commits to constructive foundations for philosophical reasons (as opposed to practical reasons) believes that classical systems such as PA and ZF prove lots of falsehoods. Hence the argument "PA and ZF are consistent because their axioms are true, when interpreted to refer to the actual numbers respectively the actual sets" doesn't work for her. But she can still understand why PA and ZF are consistent, since the double negation translation provides embeddings of PA into HA and ZF into IZF. Hence the consistency of classical systems is no deep mystery to her, and because she can also in many cases extract constructive content from classical proofs, she can even appreciate the usefulness of classical systems. I'm looking for similar arguments for "predicative vs. impredicative" instead of "constructive vs. classical".

Improve this question
$\endgroup$
12
  • $\begingroup$ You may know of this already, but for others: Timothy Chow, in The Consistency of Arithmetic, gives a variant on Gentzen's proof of the consistency of PA (Theorem 2). One doesn't have to rely on "PA ... [is] consistent because [its] axioms are true, when interpreted to refer to the actual numbers ..." Instead, one has to believe a primitive recursive sequence decreasing sequence of ordinals stabilises. $\endgroup$
    – David Roberts ♦
    Commented Feb 17, 2019 at 23:58
  • $\begingroup$ To pick apart your question, I guess if one works in a predicative framework where one can take the power class of a set, and this isn't a set, then you are worried there's no way to 'simulate' the impredicative behaviour of the power set? $\endgroup$
    – David Roberts ♦
    Commented Feb 18, 2019 at 0:05
  • 1
    $\begingroup$ @IngoBlechschmidt Right, my apologizes I don't think my comment was clear. My point was that I think that there should be a clear distinction between people like Nelson on the one hand and people like Feferman on the other. Asking why we should believe PRA is consistent and asking why we should believe ZF is consistent are two completely different questions, even if the motivation for both beliefs can be called 'predicativism'. $\endgroup$
    – Not_Here
    Commented Feb 18, 2019 at 0:26
  • 1
    $\begingroup$ A devotee of predicative math may look down on some supposed evidence for the consistency of impredicativity — once you know how to take ordinary applied math and make it predicative, the fact that people have applied it without contradiction on an impredicative basis may be less impressive. $\endgroup$
    – user44143
    Commented Feb 18, 2019 at 1:07
  • 1
    $\begingroup$ Regarding the consistency of PRA, I very much doubt that anyone who does not already find its consistency obvious will find any argument (formal or informal) for its consistency convincing. $\endgroup$
    – Timothy Chow
    Commented Feb 18, 2019 at 19:13

2 Answers 2

Reset to default
10
$\begingroup$

From the point of view of what you call predicative set theory --- I would say "predicativism given the natural numbers" --- I don't think there are any known arguments for the consistency of ZF, and such a thing seems very unlikely. The proof-theoretic strength of natural predicative theories are quite weak, generally around the level of PA. You can push this up a bit, but in order to show that ZF is consistent you would need proof-theoretic ordinals vastly beyond anything that anyone thinks is predicative.

(The generally accepted ordinal limit of predicative theories is $\Gamma_0$, but this is incorrect. I do not say "I believe" or "it seems": the analysis that concludes $\Gamma_0$ is hopelessly wrong. I explain why in this paper.)

I realize that you are only asking for an "informal" argument, but I don't see how that really helps. Looking at the question from the point of view of proof-theoretic ordinals, I think it's clear that ZF is utterly out of reach.

The best a predicativist can do with ZF may just be to assign some credence to its consistency based on the fact that no inconsistency has been found yet. I'm not sure how strongly that evidence should be weighed. It's also true that the consistency of ZF is implied by various, arguably natural arithmetical statements; Harvey Friedman is known for his work on this. Possibly that could be considered more reason to believe consistency.

I want to emphasize, though, that people often talk about consistency as if that is the only thing that matters. Surely, if you are a predicativist, you should care not only about whether ZF is consistent, but also about whether it proves true arithmetical theorems. You want it to be arithmetically sound, not just consistent. For instance, if ZF proves that Turing machine $x$ halts on null input, for some specific value of $x$, we should care about whether this is actually the case. It could well be consistent while proving false statements of this type. I made this point here.

EDIT: in the comments, Ingo Blechschmidt suggests that "(apparent) consistency of impredicative systems is an unexplainable mystery from a predicative point of view". I'd say this is less of a mystery than it seems, when you remember that there have been many formal systems for various types of impredicative mathematics over the years which did turn out to be inconsistent. Most notably, the very first, Frege's Grundgesetze.

So instead of saying "Wow, all these formal systems for impredicative mathematics turned out to be consistent, isn't that amazing!" we should say "Wow, all these formal systems for impredicative mathematics turned out to be consistent, except for the ones that didn't. Maybe not so amazing."

Improve this answer
$\endgroup$
7
  • $\begingroup$ It would be epic if we can prove that any inconsistency proof of ZF must be impredicative. Then predicativists will have to deny it, so they would in fact claim that ZF is consistent. $\endgroup$
    – Asaf Karagila ♦
    Commented Feb 18, 2019 at 8:10
  • 3
    $\begingroup$ @Asaf that's some impressive classical logic you got there... $\endgroup$
    – David Roberts ♦
    Commented Feb 18, 2019 at 12:23
  • $\begingroup$ @AsafKaragila: I assume you're joking, but in any case if ZF is consistent then in principle there exists a predicative proof of this fact. One just checks, case by case, that no $n$ is the Godel number of a proof of $0=1$. The proof has length $\omega$, but predicativists (of the type we're discussing) would be fine with that. $\endgroup$
    – Nik Weaver
    Commented Feb 18, 2019 at 13:27
  • 1
    $\begingroup$ Yes, to clarify my previous comment, it was intended to be read with a tongue heavily buried in one's cheek. $\endgroup$
    – Asaf Karagila ♦
    Commented Feb 18, 2019 at 13:28
  • 2
    $\begingroup$ @IngoBlechschmidt : While it's true that formal proofs may not give you any joy if you're seeking explanations of the consistency of (say) large cardinal axioms, one frequently used technique for justifying large cardinal axioms is reflection. One can of course debate whether a reflection argument counts as a convincing "explanation," but it does at least illustrate the possibility of an informal justification of a consistency (or even a soundness) claim. But of course appealing to reflection is anathema to a predicativist. $\endgroup$
    – Timothy Chow
    Commented Feb 19, 2019 at 21:17
3
$\begingroup$

Last week, I learned from Ulrik Buchholtz that there are proof-theoretic reductions from certain impredicative systems to certain predicative ones. While these fall short of predicatively explaining the apparent consistency of full ZFC, they do establish predicative meaning for certain impredicative principles. For instance, one can make sense of $\Delta^1_1{-}\textrm{CA}$ in $\textrm{ACA}_{<\varepsilon_0}$.

https://math.stanford.edu/~feferman/papers/reductive.pdf

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .