Mathematical Analysis · Model Theory · Reverse Mathematics
Comparing expressive power and metatheoretic properties: , Weyl's predicative analysis, and
Language and Ontology
Variables range only over elements of ; signature: . There is no symbol between numbers — the inner structure of numbers is syntactically inexpressible. Functions are limited to polynomials. Quantification over subsets and sequences is impossible; limits, continuity, and integrals cannot be expressed in general (only for polynomials). By Tarski's theorem the theory is complete and decidable; by the Löwenheim–Skolem theorem it has models of every infinite cardinality.
Two sorts: numbers (type 0: ) and sets of numbers (type 1: ). The comprehension scheme applies only to arithmetical formulas (without the quantifiers ). is introduced axiomatically as the least inductive set. Separable spaces (, , ) are coded via subsets of . Non-separable spaces () and arbitrary functionals require a third sort. The theory is "syntactic sugar" over (a conservative extension). As a recursively axiomatized two-sorted theory, it fits the standard Henkin semantics (completeness), without requiring uniqueness of the model (see the "Uniqueness of the model" row in the table).
We work inside , but the whole language is reduced to the cumulative hierarchy , started from (following the same scheme by which generates the von Neumann universe). At the base level of the hierarchy, the elements of are treated as effective atoms whose properties are exhausted by the complete theory of the model in the signature of an ordered field (unlike level II, where the language is only recursively axiomatized — see "Uniqueness of the model" in the table). This excludes the inner -structure of the numbers themselves from consideration. Above the base, however, all the constructions of are available: ordinals, cardinals, transfinite induction, and function spaces. Forms of choice are added as needed: countable choice (), dependent choice (), or full .
| Property / Landmark Theorems | Level I RCF 1st order over | Level II Weyl predicative 2nd order over | Level III atoms + forms of choice |
|---|
In the first column, the mark not definable is synonymous with "not expressible in the language": after the dot comes the typical reason — no 2nd order (subsets of ℝ, sequences, arbitrary covers, and so on); no ℕ; codes and σ-algebra — here σ-algebra refers to the need for a family of subsets of ℝ closed under countable operations (complement, countable union): this is how measurable sets and Lebesgue measure are defined; language I has no variable for arbitrary such families, nor for the measure itself as a function on them.
By codes we mean representing the objects of analysis (numbers, functions on an interval, classes of functions, elements of Lp) by sequences of natural numbers or other objects of second-order arithmetic, subject to predicativity restrictions; without this, even stating the theorems about measure and Banach spaces in the form given in the table would be unavailable.
Separately for the axiomatics: no set objects, ℕ is not singled out.
The row Uniqueness of the model: at level I — the Löwenheim–Skolem theorem for a countable first-order signature; at level II the formalization is two-sorted and recursively axiomatized, so Henkin semantics comes into play (completeness for such a language), and pairwise non-isomorphic models are possible; at level III, ZF is supplemented with the complete elementary theory of the model ℝ on the atoms, and the intended structure is fixed up to isomorphism.
© Nikolai Kazimirov · mathem.at