nLab proof

Idea

The interesting conception of the propositions-as-types principle is what I call Brouwer’s Dictum, which states that all of mathematics, including the concept of a proof, is to be derived from the concept of a construction, a computation classified by a type. In intuitionistic mathematics proofs are themselves “first-class” mathematical objects that inhabit types that may as well be identified with the proposition that they prove. Proving a proposition is no different than constructing a program of a type. In this sense logic is a branch of mathematics, the branch concerned with those constructions that are proofs. And mathematics is itself a branch of computer science, since according to Brouwer’s Dictum all of mathematics is to be based on the concept of computation. But notice as well that there are many more constructions than those that correspond to proofs. Numbers, for example, are perhaps the most basic ones, as would be any inductive or coinductive types, or even more exotic objects such as Brouwer’s own choice sequences. From this point of view the judgement $t\in A$ stating that $t$ is a construction of type $A$ is of fundamental importance, since it encompasses not only the formation of “ordinary” mathematical constructions, but also those that are distinctively intuitionistic, namely mathematical proofs.

An often misunderstood point that must be clarified before we continue is that the concept of proof in intuitionism is not to be identified with the concept of a formal proof in a fixed formal system. What constitutes a proof of a proposition is a judgement, and there is no reason to suppose a priori that this judgement ought to be decidable. It should be possible to recognize a proof when we see one, but it is not required that we be able to rule out what is a proof in all cases. In contrast formal proofs are inductively defined and hence fully circumscribed, and we expect it to be decidable whether or not a purported formal proof is in fact a formal proof, that is whether it is well-formed according to the given inductively defined rules. But the upshot of Gödel's theorem is that as soon as we fix the concept of formal proof, it is immediate that it is not an adequate conception of proof simpliciter, because there are propositions that are true, which is to say have a proof, but have no formal proof according to the given rules. The concept of truth, even in the intuitionistic setting, eludes formalization, and it will ever be thus. Putting all this another way, according to the intuitionistic viewpoint (and the mathematical practices that it codifies), there is no truth other than that given by proof. Yet the rules of proof cannot be given in decidable form without missing the point. (Harper)

Definition

• In type theory

• Formal proofs

In type theory

In type theory, a proposition is identified with the type of all its proofs (the propositions as types-aspect of computational trinitarianism). Here a proof consists of exhibiting a term of the corresponding type (showing that it is inhabited), hence a proof is a typing judgement for a term of the type representing the proposition.

See also proofs as programs.

Formal proofs

A formal proof is whatever is called a ‘proof’ in a formal system; a formal system for mathematics then gives rules for producing a proof in the above sense.

Typically, a formal system is inductively defined, and hence its proofs are fully circumscribed; this is the case for deductive systems such as natural deduction, sequent calculus, and Hilbert systems. Gödel's theorem suggests, however, that no such system can encapsulate all of mathematics.

Remark

(meaning of “formal”)
Generally, people tend to speak of formal arguments when referring to arguments by formalism, hence by purely symbolic manipulations following syntactic rewrite rules.

Beware that the quality of such arguments depends drastically on how good the formalism is — with the result that the term “formal” appears in practice in two different and almost opposite meanings:

1. If it is granted that the syntactic rules properly reflect the intended logic in its most fine detail, then a formal argument via these rules is the most rigorous hence the strongest form of argument. This is the sense in which formal proof is understood in mathematics.

2. But if the syntactic rules employed actually fail to reflect all intended aspects of a given problem, then the formal arguments based on these rules are superficial arguments, may not account for the actual detail in question, may give conclusions that are considered wrong and hence constitute a weak form of argument.

The second sense is, incidentally, the sense in which reference to “formal argument” is typically used in physics (for instance when manipulating the integrand of a path integral as if one were dealing with an actual integral).

But also mathematicians sometimes speak of “formal computations” in this second sense of “superficial argument by overly naïve formalism” (for instance when disregarding issues of convergence in analysis).

See also:

• Wikipedia: Formal computation

• MathOverflow: Why do people use “formal calculation” to describe informal calculations?

Relation to observation in physics

In (Jaffe-Quinn 93, p. 2) it was claimed that

the role of rigorous proof in mathematics is functionally analogous to the role of experiment in the natural sciences

Remarks

After making this statement about proof as observation, the article by Jaffe-Quinn goes further to suggest that the analogue in physics of speculation and conjecture in mathematics is the realm of theoretical physics, and then maybe even further in suggesting that mathematics could reasonably be purely “theoretical” in this sense. These further claims were considered faulty by several authors (math/9404229).

(Saunders MacLane in particular argued for theorems and proofs as the final goal of a piece of developed mathematics, and emphasized the explanatory function of proofs. This in contrast with experiment in physics, which is neither considered as the final goal nor as playing an explanatory role.)

While all this does contradict some of Jaffe-Quinn’s claims, it may still harmonize with the statement above. Indeed, another perspective on the claim is that finding a proof is an observational or witnessing act, which resonates with the nature of proof in constructive mathematics, such as made manifest in the propositions as types-paradigm. This perspective sees proof as something more than merely establishing the truth of a proposition.

… to show that a proposition is true in type theory corresponds to exhibiting an element $[$ term $]$ of the type corresponding to that proposition. We regard the elements of this type as evidence or witnesses that the proposition is true. (They are sometimes even called proofs… (from Homotopy Type Theory – Univalent Foundations of Mathematics, section 1.11)

Thus a proof qua witness is a construction, and in more elaborated developments (for instance in intensional type theory) a formal proof is itself a mathematical object, with internal mathematical structure.

Proof methods

• refutation by contradiction

• proof by contradiction,

Libraries of formal proofs

Libraries of formal proofs formalized in some proof assistant:

• UniMath project

• Xena project

• ForMath project

• Archive of Formal Proofs

• The QED Project

Related concepts

• computational trinitarianism

• proof theory

mathematical statements

• theory

• judgement, assertion

• hypothesis, consequence

• axiom

• assignment

• definition (inductive, coinductive)

• lemma

• proposition/type (propositions as types)

• theorem

• proof/program (proofs as programs)

• example, counterexample

• conjecture, folklore

• exercise

• analogy

• tautology

• paradox

proof assistants:

based on plain type theory/set theory:

• Metamath

• Mizar, NuPRL, Isabelle, HOL

based on dependent type theory/homotopy type theory:

• Coq, Agda, Lean, Arend

based on cubical type theory:

• cubicaltt

• redtt

• yacctt

• RedPRL

• Cubical Agda

  • library and demos

  • 1lab (cross-linked reference resource)

based on modal type theory:

• Agda-flat: installation instructions

based on simplicial type theory:

• Rzk

For monoidal category theory:

• DisCoPy

For higher category theory:

• opetopic type theory

• Globular, homotopy.io

projects for formalization of mathematics with proof assistants:

• Archive of Formal Proofs (using Isabelle)

• ForMath project (using Coq)

• MathScheme

• UniMath project (using Coq and Agda)

• Xena project (using Lean)

Other proof assistants

• Andromeda

Historical projects that died out:

• The QED Project

References

General introduction to the notion of proof in modern rigorous mathematics:

• Jean-Yves Girard (translated and with appendiced by Paul Taylor and Yves Lafont), Proofs and Types, Cambridge University Press (1989) [ISBN:978-0-521-37181-0, webpage, pdf]

• Frank Quinn: Proof Projects for Teachers (2009) [pdf, pdf]

A brief exposition of the notion of proof and formal proof in constructive mathematics/type theory is in

• Robert Harper, Extensionality, Intensionality, and Brouwer’s Dictum, August 2012 (web)

• Robert Harper, Constructive Mathematics is not Meta-Mathematics, July 2013 (web)

Discussion of formal proof in view of proof assistants:

• Thomas Hales, Formal proof, Notices of the AMS 55 11 (2008) 1370-1379 [pdf]

• John Harrison, Formal proof – theory and practice (pdf)

• Jeremy Avigad, Kevin Donnelly, David Gray, Paul Raff, A formally verified proof of the prime number theorem (arXiv:cs/0509025)

• Jeremy Avigad, John Harrison, Formally Verified Mathematics, Communications of the ACM, Vol. 57 No. 4, Pages 66-75 (web)

• Jeremy Avigad, Formal verication, interactive theorem proving, and automated reasoning (2014) (pdf)

A discussion of the relation of mathematical proof to phenomenology of theories of physics is in

• Alexandre Miquel, The experimental effectiveness of mathematical proof (pdf)

Discussion of the statistics and reception of formal proof:

• Scott Viteri, Simon DeDeo, Epistemic Phase Transitions in Mathematical Proofs, Cognition 225 (2022) 105120 [arxiv:2004.00055, doi:10.1016/j.cognition.2022.105120]

Texts on genuine proof theory include

• Richard Statman, Structural Complexity of Proofs, 1974

Projects aiming to formalize parts of mathematics include

• ForMath

• The QED Project

• Xena (by Kevin Buzzard)

Consideration of the relation of mathematical proof to physics icludes

• Arthur Jaffe, Frank Quinn, “Theoretical Mathematics”: Towards a cultural synthesis of mathematics and theoretical physics, Bulletin of the AMS, Volume 29,Number 1, July 1993 (arXiv:math/9307227)