# What kind of math can be formalized in first order logic using PA axioms?

All concrete mathematics of the past can be conducted in Peano Arithmetic.

This is from "A Brief Introduction to Unprovability" by Andrey Bovykin.

Bovykin says that theorems of $\mathsf{PA}$ capture ‘ﬁnite mathematics’, that is the world of mathematical theorems that can be formulated in $\mathcal L = \{+, \times,< ,0,1\}$ and whose proof does not require the use of any notion of ‘inﬁnite set’ in an essential way.

He says ‘ﬁnite mathematics’ includes "all imaginable mathematics whose objects can be somehow ﬁnitely approximated or ﬁnitely encoded, including everyday ‘continuous’ mathematics".

I understand how $\mathsf{ZFC}$ can be a framework for `everyday mathematics' but I don't see how $\mathsf{PA}$ can be. For example, how can I even state the l.u.b. property of the reals using $\mathsf{PA}$?

• PA? Please define your terms. Try to write questions that are as good, clear, and findable via search as possible.
– Newb
Jul 5 '14 at 5:44
• For a large part of Number Theory, and stuff that can be encoded using Number Theory (much of discrete mathematics), first-order PA is powerful enough. Roughly speaking it is as powerful as the theory of hereditarily finite sets. Jul 5 '14 at 5:46
• @Newb: I updated my question. I hope it looks better now. Jul 5 '14 at 15:07
• @user672484 Indeed --- now, this is an excellent question.
– Newb
Jul 5 '14 at 18:00