Analysis and formal proofs.

Question

Ever since I started learning formal logic I've had these kind of doubts: Is analysis ever studied in a completely axiomatic/formal proofy way?

What I mean is, given a set of axioms and inference rules, to prove things via formal proofs.

Example:

Let $f: \Bbb R\to \Bbb R: x\mapsto x$.

Theorem. $f(a)=0\iff a = 0$.

Proof:

Assume $f(a)=0$. \begin{eqnarray*} \forall x\, f(x)&=&x \quad \text{Definition of $f$.}\tag 1\\ f(a)&=&0\quad \text{Hypothesis.}\tag 2\\ f(a)&=&a\quad \text{Instantiation of 1.}\tag 3\\ a&=&0\quad \text{Substitution Axiom (Lines 2, 3).}\tag 4 \end{eqnarray*} Thus we have that $f(a)=0\implies a=0$, the other arrow is pretty trivial, as this one was, but this was just an example, as is the "substitution axiom".

Is analysis studied or treated in this way in any book you know?

Answer 1

Your question is a very good one. It is my personal opinion that textbooks can be improved a lot by making the logical structure of proofs clearer, because many students do not have the proper grasp of logic to construct the structure on their own, not to say verify with absolute confidence that the proof is correct. It is definitely possible to do proofs in analysis (and of course every other branch of mathematics) in a manner that you suggest, and probably the most suitable format for such kind of presentation is Fitch-style natural deduction, where assumptions are clearly shown via indentation by putting the statements that depend on it under the assumption. Same for universally quantified variables. This is directly analogous with contexts in programming languages for if-statements and for-loops.

That said, formal reasoning constitutes only one part of mathematics, and an equally important part is the intuition about the mathematical structure itself. A good exposition of a mathematical theorem must not only give a sufficiently formal proof to establish its validity but also give a good explanation of the techniques used in the proof, including the intuitive ideas in and an outline of the proof, which would be obscured by a purely symbolic proof. Of course, yet another aspect that must not be neglected is the motivation for the theorem itself.

In any case, you might be interested in reading about Automath, which was one of the first formal proof systems amenable to computer verification, developed by De Bruijn (somehow few people know about his contribution here!), and an entire textbook Foundations of Analysis by Edmund Landau had been translated into Automath by L.S. van Benthem Jutting and computer-checked. Largely forgotten, Automath heavily influenced later proof systems including Mizar, which has one of the largest libraries and is still actively used. One other major proof system is Coq, which has a rather different underlying formal system based on type theory instead of set theory. But actually type theory is actually closer to how most mathematicians think, and proofs that are verified in Coq's constructive logic translate naturally and easily to programs that witness the theorem's correctness, which notion is captured by the Brouwer-Heyting-Kolmogorov interpretation.

Answer 2

As already pointed out by Miller, every proof goes like that - "behind the scenes". user21820 has pointed out another important aspect of mathematical exposition, namely the emphasis on core ideas and the motivation of results. I would like to add another reason as to why most books do not present proofs like the one you have demonstrated: it quickly gets unwieldy, and the texts would risk becoming too long.

It is my opinion that an author should, in general, write enough to enable the user to fill in the details, and not more.

Depending on your level, Fundamentals of Abstract Analysis (Gleason) may just be the book you are looking for. A quick look at the table of contents will reveal that there is a great emphasis on foundations, rigour, and construction.

Foundations of Analysis (Landau) has already been mentioned, and as the author himself writes, contains a construction of the basic number systems written in "merciless telegram-style".

There are also two books by Tao, Analysis I and Analysis II, containing constructions of the basic number systems, set theory, and most standard "introductory real analysis" (limits, continuity, series, differentiation, Riemann and Lebesgue integration, metric spaces, uniform convergence, Fourier series, etc). (Beware that the author has intentionally left many of the theorems as exercises for the reader. It is the author's view that the subtleties of the subject are best grasped this way.) As mentioned in the books, the focus is on rigour and foundations.

Answer 3

On the larger question, rather than being all of one or the other, there is actually a gradation between theorem-provers and proof-checkers. In reality, when a pure or applied mathematician lays out a proof, they're actually only listing a series of conjectures or lemmas, each one comprising a "step" in the proof that is small enough to be "obvious without further elaboration". A proof-checker that meets the users of mathematics on this level is then functioning as a proof-checker only to connect the steps, but also as a theorem-prover to prove each "conjecture" or "lemma" - that is to "fill in the missing steps".

As to the issue of Automath, itself: rumors of its demise are exaggerated, and all "was"-s and other past tense should be changed to "is"-s. It's still here, and it's back.

Version 4.2 was written in C in the late 1990's; a reference to the page and software can be found under the "Automath" entry in the nCategory cafe: https://ncatlab.org/nlab/show/Automath

We're locally maintaining a version 4.3 that may be distributed soon, in the future, once we get everything cleared. It will include many of the enhancements and repairs whose current absence are called out below.

So, yes, the infrastructure for Automath actually serves quite well as a foundation for a tractable higher-order formalism powerful enough to embody real analysis. The deficiencies don't lie with the underlying type theory, but mostly with the language itself.

The formalization of real number theory in terms of Automath - the "Grundlagen" file - was heavily labor-intensive, largely because of the cumbersome features of the original versions of the language: particularly its inability to do more intelligent polymorphism, the absence of type inheritance, the lack of prefix/postfix/infix notation (like Prolog), the lack of support for symbolic language (that is, no UTF-8 or other UNICODE support) and the absence of any significant support for equational logic.

All operators in Automath are polymorphic, in a style similar to Hindley-Milner, but the polymorphism parameters are matched only by exact match to their declaration and all parameters are treated as polymorphism parameters! No distinction between Hindley-Milner parameter versus function argument is made.

If there are any parameters that mismatch then all the parameters from that point onward have to be explicitly specified. For instance, assuming we had infix notation available, if we were to define the composition as an operator of the type: $$(f: B → C, g: A → B) ↦ f∘g: A → C$$ it would have to be declared as an operator taking 5 arguments, not 2! $$f: B → C, g: A → B ↦ Comp(A,B,C, f,g): A → C,$$ when it is actually meant to be a polymorphic operator $Comp<A,B,C>(f,g)$. You couldn't really exploit the advantages of infix notation for the operator.

When called, say on functions $$a: B → D, b: A → B$$ you could omit the parameters $A$ and $B$, but would have to explicitly cite the parameter $D$ and write it as $Comp(D,a,b)$, instead of as just $a∘b$. Similarly, if it were called on functions $$a: D → C, b: A → D$$ it would have to be called with both of the last two parameters explicitly cited, as $Comp(D,C,a,b)$, instead of as just $a∘b$.

Cases like this are replete in the Automath rendering of the Grundlagen book, and it cascades, as each layer is built on top of the one underneath it.

The digitized book also force-fit a boolean logic framework, instead of using the native facilities for logic already contained in a dependent types formalism. It was not a constructive or intuitionistic translation of the book, but was grounded in classical logic, with the logic built on the Automath formalism as an extra layer. It would be a much more difficult exercise to try and directly implement Grundlagen in terms of the facilities already natively-present in the Automath type theory or in any higher-order constructive or intuitionistic type theory formalism built on top of it.

Martin-Löf can be more effectively used, but it does not contain the double-negative rule, nor any of the watershed rules that distinguish classical logic from intuitionistic logic. So, that would be a difficult exercise.

As for the relation between the two: there is a widespread misunderstanding of how they are or should be connected. The usual account you will hear is that Automath's type system is a "flattened" version of those seen in contemporary dependent-types formalisms like Martin-Löf; because it uses the same abstraction/application for both objects and types, while Martin-Löf treats object abstractions as lambdas, and type abstractions as pi's - or dependent products.

This is actually the wrong way of looking at it. Automath was designed to be an "assembly language" layer to higher level languages (or "superposed languages" as deBruijn called them) like Martin-Löf. It actually represents a layer beneath Martin-Löf which - when made explicit - actually simplifies the presentation of Martin-Löf's formalism(!)

In Martin-Löf, the product type is defined in a somewhat cumbersome way by conditional rules. If $A$ is a type, and $B(x)$ is a type, for each $x ∈ A$, i.e. if one has a type function $B: x ∈ A → type$, then $(Πx∈A)B(x)$ is the product type, whose members are the lambda abstractions $λb = (λx∈A)b(x)$ of functions $x ∈ A ↦ b(x) ∈ B(x)$, which can be converted back to functions by the "application" operator $Ap(λb,a) = b(a)$.

Automath would actually represent the layer beneath all of this - the functions themselves. So, one would treat $A$ as a type (I'll use $∙$ to denote "type"), and $B$ as of $[x,A]∙$ (which is permitted in some versions of the Automath language, like versions 4.2 and 4.3, and is considered as a subtype of $∙$.) The $[x,A]$ is Automath's native abstraction operator - its version of $λx∈A$.

It's an abstraction operator underlying that of Martin-Löf and which is frequently referred to tacitly in Martin-Löf's presentation. The function application $b(a)$ native to Automath would then be represented as $<a>b$ (or just $b<a>$ in version 4.3), and the product type $(Πx∈A)B(x)$ would just be $ΠB$ - with the prefix operator $Π$ mapping an object $B$ of type $[x,A]∙$ to type $∙$. The $λ$ operator would be a map from a object $b$ of type $B$ to an object $λb$ of type $ΠB$; while the application operator $Ap(c,a)$ would map an object $c$ of type $ΠB$ and $a$ of type $A$ to type $Ap(c,a)$ of type $B<a>$; i.e. it maps the object $c$ back to a function $[x,A]Ap(c,x)$ has type $B$.

So, it's a layer beneath the layer seen in higher-order type theories which can also be used to directly embody all the other operators seen in Martin-Löf or similar theories.

The actual weakness of Automath lies not in its infrastructure, but in its lack of direct support for equational logic. It has no easy way to write out the β-rule $Ap(λb,a)$ = $b<a>$ or the η-rule, $λ([x,A]Ap(c,x))=c$ at the higher layer; or the other reductions rules seen in Martin-Löf. The versions of the β-rule and the η-rule in Automath correspond to the ones tacitly used at the deeper, informal, layer throughout Martin-Löf's presentation.