Riemann Integration: FOL or SOL? Ok so to define Riemann integral you need to quantify over partitions. But in first-order logic you can't do that. But if you use a first-order axiomatic theory of sets (ZF for example), then quantifying over the universe is the same as quantifying over sets. Since partitions are sets, would it mean that Riemann integration can be done in first-order logic (in ZF)?

Questions:
$\rm\color{#c00}{a)}$ Is my reasoning correct? That is, can Riemann integration be done in first-order logic and more precisely in ZF?
$\rm\color{#c00}{b)}$ If the answer to $\rm\color{#c00}{a)}$ is yes, then what are the differences between a first-order and a second-order theory of Riemann integration?
$\rm\color{#c00}{c)}$ I've read that ZF is to be a framework for all of mathematics. Does this mean that all of mathematics can be done in first-order logic?
$\rm\color{#c00}{d)}$ Related to $\rm\color{#c00}{c)}$: what if my mathematical theory is that of classes (like the class of all sets)? Then this can't be done in first-order logic? Is there an axiomatic 'set' theory that treats of classes as well as sets?

Thank you very much.
 A: 
$\rm\color{#c00}{a)}$ Is my reasoning correct? That is, can Riemann integration be done in first-order logic and more precisely in ZF?

Yes under suitable translation. A more precise answer would require a more precise question.

$\rm\color{#c00}{b)}$ If the answer to $\rm\color{#c00}{a)}$ is yes, then what are the differences between a first-order and a second-order theory of Riemann integration?

The second-order theory of the reals does not have a countable model under full semantics, while the first-order theory of the reals does. Presumably, any theory of Riemann integration includes a theory of the reals, so it is likewise affected. Does this have any effect in practice? Apparently not. Full semantics has no effective deductive system, so even if you want to use second-order logic you would be using some deductive system that is complete for a different semantics, such as Henkin semantics. But Henkin semantics is equivalent to first-order semantics after a suitable translation, just like ZFC set theory was designed to be first-order but reflect a second-order intended semantics. So what you end up being able to prove in a second-order system of Riemman integration is surely going to be interpretable in ZFC already, unless your system includes some second-order axiom that cannot even be interpreted in ZFC.

$\rm\color{#c00}{c)}$ I've read that ZF is to be a framework for all of mathematics. Does this mean that all of mathematics can be done in first-order logic?

Almost all mathematics can be translated into ZFC, yes, but almost nobody would ever attempt literally that translation for much mathematics. Also, a small minority does mathematics in formal systems that are incompatible with ZFC, or investigates what mathematics would be like in such systems. NFU is one, whose language is the same as ZFC but whose axioms are inconsistent with ZF. One could even argue that all mathematics can be translated into PA, via the following fact: Given any practical formal system $S$ and any claimed proof $P$ of some statement $φ$ over $S$, there is a computable (and uniform) encoding of the statement "$S$ proves $φ$" as a sentence over PA denoted by "$\square_S φ$", such that PA proves "$\square_S φ$" iff $P$ is a valid proof of $φ$ over $S$, and we can computably determine whether it is so, and we can computably obtain the proof of "$\square_S φ$" from $P$ if it is so. Does that mean that PA suffices for all mathematics? Well in the above limited sense yes, but "$\square_S φ$" is devoid of meaning unless you interpret it in some 'stronger' system than PA, and down the rabbit hole you go.

$\rm\color{#c00}{d)}$ Related to $\rm\color{#c00}{c)}$: what if my mathematical theory is that of classes (like the class of all sets)? Then this can't be done in first-order logic? Is there an axiomatic 'set' theory that treats of classes as well as sets?

Look up Morse-Kelley set theory, which is a first-order theory that can reason about definable classes over ZFC, and is naturally strictly stronger. There is also second-order ZFC, and of course higher-order ZFC. How high would you like to go?

The bottom line is that whether you can do something in some formal system that can be interpreted to mean something is only meaningful if you think the syntax and the interpretation both make sense. If you strictly stick to the language of ZFC, then technically you cannot use the integral syntax nor function application syntax (namely like "$f(x)$"). You would object that it is enough if we have a (computable) uniform translation into the language of ZFC such that any statement about 'Riemann integration' is 'provable by normal means' iff their translations are provable in ZFC. (The quotes are because the term "Riemann integration" is not precise enough.) But that is too loose and will force you to also accept that 'Riemann integration' can be done in PA (as shown above in answer to (c)). You might turn around and argue that PA is merely capturing formal systems. Indeed, but can you describe what you mean by "Riemann integration" without a formal system?
