7
$\begingroup$

I am currently reading about elementary function arithmetic and Harvey Friedman's grand conjecture.

In Number theory and elementary arithmetic, Jeremy Avigad expressed Fermat's last theorem, divisibility, primality, ordered pairs, etc. But where can I find how basic objects from analysis such as real numbers are defined in EFA?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
13
$\begingroup$

They aren't. Analysis requires a richer language. Note the particular restriction in Friedman's conjecture:

...whose statement involves only finitary mathematical objects (i.e., what logicians call an arithmetical statement)

(link added for context). Statements about real numbers, let alone more complex (:P) objects, do not fall under this heading.

Improve this answer
$\endgroup$
7
  • 1
    $\begingroup$ This makes sense, thank you for your answer. What about rational numbers? I guess you could write them as pairs, but was it actually done? $\endgroup$
    – user507115
    Commented Jun 14 at 20:01
  • 1
    $\begingroup$ @richardIII Yes, rational numbers - even algebraic numbers - are no more complicated than naturals or integers in this sense. I don't know a particularly good source on this, but the basics are surely folklore (e.g. that EFA proves, appropriately formalized, the statement "the rationals from a dense linear order without endpoints" and so on). $\endgroup$
    – Noah Schweber
    Commented Jun 14 at 20:06
  • 1
    $\begingroup$ Maybe worth noting that many theorems we recognize as theorems about real numbers can be phrased purely in terms of rationals. For example, "$\sqrt{2}$ is irrational" can be phrased as the equivalent statement "There is no rational number $x$ such that $x^2=2$" And more subtle ones can also be phrased this way. One can even make a statement equivalent to "Pi is transcendental" in EFA, albeit in a pretty convoluted way. $\endgroup$
    – JoshuaZ
    Commented Jun 15 at 1:38
  • 4
    $\begingroup$ Reals, sequences of reals, or continuous real functions can be defined in $\mathrm{RCA}^*_0$, which is a conservative extension of EA (that Friedman calls EFA). $\endgroup$
    – Emil Jeřábek
    Commented Jun 15 at 6:05
  • 1
    $\begingroup$ @EmilJeřábek CODES for continuous real functions can be defined there. $\endgroup$
    – Sam Sanders
    Commented Jun 15 at 9:23