5
$\begingroup$

Problem

From the formalist point of view, any mathematical statement should ultimately be an assertion about the derivability of a certain formula in a certain formal system, call it the background theory.

However, when reading mathematical texts, especially when they are about set theory and logic, it happens to me that I often don't know what the background theory is supposed to be.

For the mathematics outside logic and set theory, I usually assume without further thought that the background theory is ZFC or ZFC + Universes. I also tend to do the same for logic and set theory, but though this seems to be both much too strong and unnatural for many purposes, I find it hard to gain an intuitive idea about the sufficiency/adequacy of a background theory for a certain purpose.

Examples

  • If ZFC is consistent, then ZFC + GCH is consistent

    When reading everything in ZFC, this translates to

    $ZFC\vdash \text{Con}(ZFC) \to \text{Con}(ZFC + GCH)$

    which can be proved by forcing.

    However, the statement is of metamathematical and constructive nature, so it would more natural to use a finitistic, constructive background theory, call it T, and translate it to

    (*) $T \vdash \exists\text{ a function from inconsistencies of ZFC + GCH to inconsistencies of ZFC}$

    This is stronger than the finitistic consequence

    $T\vdash \exists\text{ a function from inconsistencies of ZFC + GCH to inconsistencies of ZFC + Con(ZFC)}$

    of the first interpretation. Now (*) is also true in the sense that the desired algorithm exists, but as far as I understand its proof really needs the additional observation that the forcing argument also works for models of finite fragments of ZFC, the consistency of which is proved in ZFC by the reflection theorem.

  • Goedel's Theorem: The recursive functions are precisely those provably total in Peano Arithmetic

    Again, I tend to view this as a single theorem in ZFC, and I feel comfortable with that, having in mind the treatment of recursive function within the framework of ZFC as discussed, say, in Kunen's 'The Foundations of Mathematics' and the possibility of constructing truth predicates for set models of first order theories like the standard natural numbers as a model of Peano Arithmetic.

    However, having encountered many situations where I was told that ZFC is too strong, I feel that again this is probably also formalizable in much weaker theories, ending up with the impression that the theorem can be stated in second order arithmetic, but not in Peano arithmetic -- however, I'm completely lacking confidence with that since I haven't seen much development of mathematics, e.g. [countable] model theory, in these theories.

Questions:

  • I'd like to hear about how more experienced people make up their mind in which background theory to read statements like the above. What is the 'standard theory' you use (if there is one), and what are the first checks that help you getting an intuition about which weaker theories might suffice?

  • Also, I'd be very happy about references to books which treat the question of choice of background theory carefully. For example, I found Kunen's "Set Theory" book a relief, as he never gets tired to indicate whether a theorem is meant to be a single formula inside a certain variant of ZFC he names, or rather a scheme in the metatheory, or a finitistic/algorithmic assertion such as (*) above.

$\endgroup$
  • $\begingroup$ I feel that I wrote about this a couple of answers before. $\endgroup$ – Asaf Karagila Oct 22 '14 at 14:51
  • 1
    $\begingroup$ I was somewhat right. This one seems very related (maybe it answers your question?) and I found a few more which aren't quite related. $\endgroup$ – Asaf Karagila Oct 22 '14 at 14:59
  • $\begingroup$ "For the mathematics outside logic and set theory, I usually assume without further thought that the background theory is ZFC or ZFC + Universes." I don't know the background theory here actually. What is the system for the first-order predicate calculus? Do we have a "natural deduction" style propositional calculus at work or a "Hilbert-Frege" style propositional calculus? Does the propositional calculus allow just propositional variables or functioral variables also? $\endgroup$ – Doug Spoonwood Oct 22 '14 at 15:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.