1
$\begingroup$

In https://plato.stanford.edu/entries/hilbert-program/ it is written that:

"Gödel had found the same result already independently: the second incompleteness theorem, asserting that the system of Principia does not prove the formalization of the claim that the system of Principia is consistent (provided it is). All the methods of finitary reasoning used in the consistency proofs up till then were believed to be formalizable in Principia, however. Hence, if the consistency of Principia were provable by the methods used in Ackermann's proofs, it should be possible to formalize this proof in Principia; but this is what the second incompleteness theorem states is impossible."

The crucial sentence for me is "All the methods of finitary reasoning used in the consistency proofs up till then were believed to be formalizable in Principia, however."

Do we still believe that all of the methods of finitary reasoning used in metatheory are formalizable in formal theories like PA or ZFC? What kind of evidence do we have here?

Intuitively, for me to accept the failure of Hilbert's program I would have to somehow convince myself that metatheory is formalizable in formal theory (I am not even sure what that means). But, I have doubts because some metatheory is being written in natural language in an intuitive way, such as, what is a proof, what is a deduction, what is a formula and so on. How can one formalize this in PA? I feel that we can formalize things about natural numbers which we use intuitively in metatheory by some PRA and then encode it in PA. But I am not sure whether we can formalize everything in metatheory in some formal system.

I hope my question is clear and I would be happy for any kind of suggestions and advice here.

$\endgroup$
5
  • 1
    $\begingroup$ I think some of what you are asking is essentially the question of Church's Thesis: what is and what is not an algorithm? Goedel's recursive functions (later generalized), Turing machines, Church's lambda-definability, they all turn out to be equivalent. Church's thesis is that the concept of procedure/algorithm (which is supposed to include all methods of finitary reasoning) is indeed captured by these formalizations. But this cannot be proven, it can only be disproven. But given that many independent attempts have all ended up coinciding, many/most people believe it is in fact true. $\endgroup$
    – Arturo Magidin
    Oct 31, 2018 at 5:41
  • $\begingroup$ @ArturoMagidin Very interesting, thank you for your comment. Can you please give some references (maybe textbooks) about this? $\endgroup$
    – Daniels Krimans
    Oct 31, 2018 at 6:42
  • 1
    $\begingroup$ Essentially all the work we do in the metatheory - finitistic or not - is formalizable in ZFC, just as almost all mathematics is formalizable in ZFC, sometimes with the addition of large cardinal axioms. The more interesting issue is not whether the metatheory is formalizable in strong theories, but whether the finitistic part of the metatheory is formalizable in weak theories such as PRA. We know that all the results of a basic standard logic course can be formalized in $\mathsf{ACA}_0$, a system of second-order arithmetic that is equiconsistent with PA. $\endgroup$
    – Carl Mummert
    Oct 31, 2018 at 14:03
  • $\begingroup$ @Carl Mummert Interesting. Can you please give some references for the statement ''essentially all the work we do in the metatheory is formalizable in ZFC''? $\endgroup$
    – Daniels Krimans
    Oct 31, 2018 at 15:59
  • 1
    $\begingroup$ @DanielsKrimans This is just the folklore that pretty much any “ordinary mathematics” can be formalized in ZFC. I’d be surprised (but interested!) if there were an authoritative modern reference on this. For what it’s worth, in Kunen’s set theory book, he sketches how to formalize group theory and topology in set theory, then includes as an exercise something like “convince yourself that 98.5% of mathematics can be formalized in Z” (where Z is a particular sub theory of ZFC). I think that book has some good stuff more specifically about formalizing model theory too. $\endgroup$
    – spaceisdarkgreen
    Nov 2, 2018 at 15:50

1 Answer 1

Reset to default
4
$\begingroup$

There is a literature on how we are to understand the idea of finitism as it occurs in the work of Hilbert and those influenced by him. This is historical-cum-philosophical discussion, not easily summed up in a snappy math.se post!

A good place to start is a famous paper by William Tait, "Finitism" Journal of Philosophy, 1981, 534-556 (available through Jstor), reprinted in Tait's book The Provenance of Pure Reason (OUP 2005), which argues that -- as Hilbert conceived finitism -- the limits of finitist reasoning are captured in PRA. Not everyone agrees with that: see the follow-up paper in Tait's book. There is discussion and more references in https://plato.stanford.edu/entries/hilbert-program/#2

$\endgroup$
1
  • $\begingroup$ Looks very good, thank you! $\endgroup$
    – Daniels Krimans
    Oct 31, 2018 at 10:07

You must log in to answer this question.

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