17
$\begingroup$

When is a proof or definition formal?

I've been searching for an explanation of when or proof or definition is formal.

Sometimes, authors call their proofs or definitions informal without further explanation.

I've an idea that a formal proof is derived directly from the axioms (with references to already proven statements), or are the requirements less strict?

When is a definition formal? May words whose meaning follow only from the context be used in a formal definition, or should each use of a word be explicitly defined?

$\endgroup$
2
  • $\begingroup$ If you are familiar with vectors and polynomials (i..e vectors spaces and polynomial rings), then you may find it helpful to compare their nonrigorous informal high-school presentations with their rigorous formal algebraic presentions (both of which are discussed at length in prior questions here). $\endgroup$ Apr 6 '17 at 16:40
  • 1
    $\begingroup$ Except for specific machinery designed and used mostly by logicians, there is no precisely defined thing as a "formal" proof, just as there is no precisely defined thing as a "detailed" proof or a "persuasive" proof. $\endgroup$
    – vadim123
    Apr 6 '17 at 16:55
14
$\begingroup$

It's not a very clear-cut line. There's also a complication, because mathematicians often use certain styles of language in a formal proof, making the proof sound more formal-in-the-colloquial-English-sense. They do this to signal "this is a formal-in-your-sense proof". The converse is also true.

Here's an informal intensional definition:

A formal proof is basically one where nothing is hidden.

(The definition of "nothing" is flexible, depending on the level of the proof. A formal proof aimed at world-class mathematicians may miss out more details than a first-year undergraduate formal proof, which is not allowed to miss out many details at all.)

One may use words whose meaning follows only from context, as long as it's clear what the meaning is; that's not hiding anything. A proof can skip out details and still be formal, as long as it tells you how to complete the details: that's hiding stuff but making it clear that the stuff is a) hidden, and b) easy to recover.

Here's an informal extensional definition.

A proof which leaves large chunks to the reader is informal: it hides large amounts of detail. A definition which misses out some annoying special cases (perhaps to make the statement more slick) is informal. A proof which pedantically goes over every statement is formal. A proof in which every statement clearly follows from earlier statements or from axioms/hypotheses is formal.

$\endgroup$
1
  • 8
    $\begingroup$ "A formal proof aimed at world-class mathematicians may miss out more details than a first-year undergraduate formal proof, which is not allowed to miss out many details at all" - and a formal proof targeted for computers is going to be even more explicit. $\endgroup$ Apr 6 '17 at 18:01
7
$\begingroup$

The problem here is that the answer depends on whether "formal" is formally or informally defined:)

If it is formally defined it would probably be defined as a mathematical term and the requirement of the proofs and definition would be quite strict. They would probably need to be formulated in a formal language adhering to certain rules. Normally one does not see these kind of definitions and proofs.

Otherwise the term "formal" would have a more relaxed meaning and one would not require a formal definition or proof to adhere to some very strictly defined standards. In this case one would mean that formal means more strict formulation than informal (which is more sloppy formulation) - where you draw the line is depending on context.

Also which one is used can also be seen in context. If you don't see any formal language (note however that a formal language can look natural) or formal definition of "formal" it would most probably be used in the second meaning.

$\endgroup$
1
  • 2
    $\begingroup$ Informally, I'd say this is formally wrong. $\endgroup$
    – jpaugh
    Apr 6 '17 at 15:30
7
$\begingroup$

There is actually a whole spectrum of "formality" in mathematics. In informal terms, "formal" it refers to what is considered as rigorous, but that is of course subjective.

  • Absolutely formal: Written in a language that can be verified by a program that implements some formal system. Check out Mizar and Coq, two well-known proof assistants based on two different foundational systems for mathematics.

  • Extremely formal: Written in a manner such that any logician is capable of translating it by hand into an absolutely formal version. For example, "$\forall x \in S\ ( P(x) )$" where "$P$" is a predicate can be written as a short-form for "$\forall x\ ( x \in S \to P(x) )$", where the latter is permitted in pure first-order set theory.

  • Obviously formal: Written in a manner such that all logicians will agree can be translated mechanically into an absolutely formal version. It may well be impractically troublesome to actually do it, but nobody doubts that it can be done. For example, consideration of symmetry such as in "Without loss of generality $a < b < c$, ..." can be done whenever all the previously deduced statements are symmetric under permutation of $a,b,c$ and $a,b,c$ come from a total order. The easiest way to absolutely formalize it would be to simply repeat the subsequent argument for each permutation, but it is prohibitive especially if there are a lot of symmetry considerations!

  • Provably formal: Written in a manner such that any logician can prove that it can be translated mechanically into an absolutely formal version. This is where it starts to get hairy, because one logician might use some meta-system MS to prove this, but another skeptical logician might reject some inference rule or axiom of MS that the first logician used. So the first logician might insist that an absolutely formal proof exists, but the second might insist that it does not exist. For example, ZF set theory proves that the Hydra game terminates. In particular the following play terminates: At step $n$, if the tree is just a single node then the game ends, otherwise we remove the right-most leaf node and then if its parent is not the root we duplicate the resulting parent subtree $n$ times. This holds even if the initial tree has depth $100$, and ZF additionally can prove that a weaker formal system called PA can prove it. But the shortest proof of this in PA will have more deductive steps than the number of particles in the observable universe! So a logician who rejects ZF but accepts PA might not believe that an absolutely formal proof exists...

  • Reasonably formal: Written in the standard of modern mathematics, that is, in sufficient detail to convince experts in that field of mathematics that it is rigorous and correct. Lots of steps may be skipped, and yet it may be considered perfect. For example, one may define the diameter of a finite graph with weighted edges to be the largest distance between two nodes in the graph, where distance between $x,y$ is defined as the minimum possible sum of weights along a path from $x$ to $y$. It is clear to any graph theorist that this is well-defined, even though technically one has to prove the implicit claims of existence of "minimum" and "maximum" here; it is not totally trivial!

  • Somewhat Informal: Written (or more often spoken) to fellow mathematicians in a manner that is not even reasonably formal, especially when diagrams are involved. You will find less diagrams in more formal proofs, simply because nearly all diagrams require some amount of intuitive interpretation by the intended audience to determine what the diagram is supposed to illustrate, and diagrams almost always depict a single instance and not the general case. Good diagrams will depict a non-trivial instance while bad diagrams may actually mislead viewers to make false assumptions! Also, informal mathematics often arises together with phrases like "it can be shown" and "this will be left as an exercise for the reader"...

  • Very informal: Done with vague words like "near" and "close" in analysis. This is sometimes sufficient to convince a fellow expert in the same field, but it is usually insufficient to enable mathematicians not in the same field to actually write down a formal proof without much effort. Worse still, informal proofs by non-mathematicians tend to be wrong, but often the flaws are not seen by other non-mathematicians.

$\endgroup$
5
  • 1
    $\begingroup$ "Absolutely Formal", but what if I find a bug in Coq or Mizar? I can't think of a program that doesn't have bugs. Seems to me like a better term is "As formal as we can make it" $\endgroup$
    – Dair
    Apr 6 '17 at 21:22
  • $\begingroup$ @Dair: Firstly, I said "can be verified by a program that implements some formal system", not that people are absolutely certain that Coq and Mizar do the job. ZFC is a formal system, and a proof in ZFC is considered absolutely formal. It is extremely easy to see that there is a program that can verify proofs in ZFC, and in a couple hundred lines of code at most. Also, the problem of bugs is not unique to Coq or Mizar, but it is far more unlikely (in the core software excluding all extensions) than errors in hand-written proofs. $\endgroup$
    – user21820
    Apr 7 '17 at 5:25
  • $\begingroup$ @Dair: Secondly, I think you do not know programming. It is trivial to write bug-free programs. Whether a piece of software is likely to have bugs depends on many factors, and four major ones are complexity of the implementation, competency and carefulness of the programmers, length of the source code, and the manner in which the software is built. Also, what if someone finds an inconsistency in ZFC? That will have far worse consequences than a bug in Coq or Mizar (which can be patched without affecting valid proofs)... $\endgroup$
    – user21820
    Apr 7 '17 at 5:40
  • 1
    $\begingroup$ @Diar: Also one would note if there is such a bug is present the program does not implement that formal system. The point with formal system is that proofs can be checked with some automaton (but not any automaton). $\endgroup$
    – skyking
    Apr 7 '17 at 8:17
  • $\begingroup$ @skyking: Right! It's an idealism but it's necessary otherwise we would just go into infinite regress if we keep questioning: who shall check the checker? =P This definition of "absolutely formal" simply means "there exists a perfect proof verifier program", and not that we are absolutely sure we have one. I'll also note that the very notion of formal systems already requires certain ontological assumptions such as the ability to concatenate arbitrarily long strings. Again, it's an abstract assumption but even if it doesn't hold in the real world we don't have an alternative. $\endgroup$
    – user21820
    Apr 8 '17 at 6:54
5
$\begingroup$

There is one aspect of "definitions" that is not exactly asked in your question, but is relevant to mathematics. There are actually two kinds of completely formal definitions, arising from two separate mechanisms: $ \def\nn{\mathbb{N}} $

  1. Definition by existential instantiation: When we have an axiom or a deduced sentence asserting the existence of some object, namely "$\exists x\ ( P(x) )$" where $P$ is some predicate, we can instantiate it and name a reference to it, by saying "Let $c$ be such that $P(c)$.". This is far more general than you might think. For example when you define a function $f : \nn \to \nn$ such that $f(0) = 0$ and $f(n+1) = 2f(n)+1$ for every $n \in \nn$, what you are actually doing is to invoke a theorem that says "$\exists f : \nn \to \nn\ ( f(0) = 0 \land \forall n\in\nn\ ( f(n+1) = 2f(n)+1 ) )$". Don't laugh! This is not necessarily a trivial theorem, depending on your choice of foundational system for mathematics. The bottom line is, such definitions are only valid if you can prove the existential statement that guarantees the existence of the object that you are giving a name to.

  2. Definitorial expansion: In some foundational systems, we are unable to use the above type of definition, simply because we cannot prove the required existential statement. For example in ZF set theory one can actually prove that there is no set $S$ whose members are exactly the sets that are not members of themselves. Namely, $\neg \exists S\ \forall x\ ( x \in S\ \Leftrightarrow \neg x \in x )$. But we still can define a predicate $R$ where $R(S) \overset{def}\equiv \forall x\ ( x \in S\ \Leftrightarrow \neg x \in x )$ for every set $S$. $R$ is not a set, but we can still talk about sets that satisfy $R$. For example, $R(\{\})$ because the empty-set is not a member of itself. This notion of definition can itself be formally defined as described in this post, and more details about the issue with Russel's paradox can be found in this post. This is also more common than you might think. For example in ZFC set theory, there is no function that maps every set to its cardinality, and so the cardinality notation in "$\#(S)$" or "$|S|$" cannot be defined using the first type of definition. But it can be defined via this type of definition. Similarly, when you define the diameter $diam(G)$ of every finite graph $G$, note that actually $diam$ is not a function in ZFC set theory, because there is no set of all finite graphs! But the notion of "finite graph" and $diam$ are both definable via definitorial expansion, and we can use $diam$ on any finite graph. Things get a bit messy with higher-order things like the family of functions on finite graphs. That cannot even be defined via definitorial expansion, but we can cheat in many cases. For example we can define even by mere existential instantiation the family of all functions on graphs whose vertices are a subset of $\nn$.

$\endgroup$
4
  • $\begingroup$ What do you mean by "Let $c$ be such that $P(c)$? What if there more than 1 $x$'s that satisfy $P$? $\endgroup$
    – user599310
    Sep 11 at 20:03
  • $\begingroup$ @user599310: That statement never said that $c$ is the only object satisfying $P(c)$, so why do you think there can be a problem if multiple objects satisfy $P$? Also, this is actually a basic deductive rule in first-order logic (∃elim in this post is one such system). $\endgroup$
    – user21820
    Sep 12 at 3:07
  • $\begingroup$ "We can instantiate it and name a reference to it". This is what I can't get. You are giving a name to some arbitrary object. Or in the case of the function f, what if there is more than one function that satisfies: $\exists f : N \to N \ ( f(0) = 0 \land \forall n \in N \ ( f(n+1) = 2f(n)+1 ) )$ ? $\endgroup$
    – user599310
    Sep 13 at 15:54
  • $\begingroup$ @user599310: As I said already, it is a basic rule in first-order logic. If you don't get that, then you need to learn basic logic. $\endgroup$
    – user21820
    Sep 13 at 18:20
4
$\begingroup$

Personally, when I think of a formal definition I think of a concept explained with mathematical language instead of natural language.

For example, when we define the limit of a function $f$ at a point $a$ we can define it with both of these forms:

Definition 1: We call $l$ the limit of a function $f: R \rightarrow R$, if $$(\forall \epsilon \in R^+)( \exists \delta \in R^+)( 0<|x-a|<\delta \implies |f(x) - l| < \epsilon)$$

Definition 2: We call $l$ the limit of a function $f$ at $a$ if it is the number that the function tends to near $f(a)$ (if it exists).

Definition 1 is a formal definition, with mathematical language and citing all the necessary conditions in order to define the concept. Definition 2 lets the user imagine intuitively the concept but don't let the user work with the concept because he doesn't have the mathematical concept in order to deal with proofs.

Note that in both definitions we are defining the same concept, but the first one allows us to work with the definition avoiding the ambiguity - nevertheless, it is very easy to understand the concept in the second definition.

$\endgroup$
4
  • 1
    $\begingroup$ How is "We call $l$ the limit of a function $f:R\to R$, if exists, the number such that" mathematical language and not natural? If it is to work out you must have a formal language where these formulation using english-like phrases are allowed. Sure it could have been done, but then you could have formulated the formal language so that the second definition also is part of that language. $\endgroup$
    – skyking
    Apr 6 '17 at 7:25
  • $\begingroup$ Yes, I used natural language, but less than in the second definition. Also I used natural language only for saying you that the limit is $l$, this is, to put a name to the definition. However, i can Define the same concept more formally, for example, if you delete the first sentence and you define the "limit $l$ of a function" now you haven't natural language in the definition $\endgroup$ Apr 6 '17 at 7:30
  • 1
    $\begingroup$ It doesn't matter whether it's written with mathematical symbols, English, or some other language, what matters is that it is completely unambiguous. "There exists" has a direct translation to the mathematical symbol $\exists$. The difference here is that "very close" does not have an unambiguous meaning, for example. $\endgroup$ Apr 6 '17 at 16:29
  • $\begingroup$ I disagree about Definition 1 including natural language. The difference between formal and natural language is not "words vs symbols". Rather it is that in formal language everything is tied to precise concepts, while in natural language the concepts are vague or ill-defined, such as the "tends near" and "very close to" in Definition 2. $\endgroup$ Apr 6 '17 at 16:30
2
$\begingroup$

If you make a statement in mathematics, the question is, can you put the statement exactly in the mathematical framework, ie can you convey your thoughts mathematically so as not to lose any details. As an example say we take the limit definition. I make a statement as follows. "The value of a real valued function $f$ gets closer and closer to $L$ as $x$ gets closer and closer to $a$." Now, can we write this "formally" in mathematical languaage ? Of course we can. $\forall \: \epsilon>0, \exists\:\delta>0 \ni 0<|x-a|<\delta\implies|f(x)-L|<\epsilon$. More precisely $\lim_{x\to a} f(x)=L$. So we have translated an informal statement into a precise mathematical definition.

In case of proofs as well the situation is similar. The idea is to capture mathematically every possible details that are necessary in proving the result.

$\endgroup$
2
$\begingroup$

A formal proof is one where you don't attach an interpretation to what you write, and all steps are "mechanically" justified by explicit pre-established rules, be them axioms or other theorems.

For instance, when writing

$$a\ne0,ax^2+bx+c=0\\\iff\\ x^2+\frac bax+\frac ca=0\\\iff\\ x^2+2\frac b{2a}x+\frac{b^2}{4a^2}=\frac{b^2}{4a^2}-\frac ca\\\iff\\ \left(x+\frac ba\right)^2=\frac{b^2}{4a^2}-\frac ca,$$

the first step is justified by the rule of division of an equality and by distributivity/associativity, the second by addition of a term to an equality and the third by a remarkable identity.

At no time do you have to think that the symbols represent numbers and the operators arithmetic computations. You apply the available rules and transform the expressions. So you are looking more at the patterns than at the content. The goal is to reduce human error.


This doesn't mean that the proof must be written in a symbolic form rather than as a narrative explanation. What matters is that all steps are clearly justified by a previously established truth. In practice some obvious justifications can be omitted, provided the intented readers can retrieve them.

$\endgroup$
6
  • 1
    $\begingroup$ I upvoted your answer just for the first sentence, but I actually disagree with with your following couple of paragraphs.Even writing out expressions like yours doesn't really make things clear in simple cases. For example, what's $\sqrt[3]{-1}$? Most people would say it's obviously $-1$ but it could be $e^{i\pi/3}$ if $-1$ is seen as a complex number. Or if someone says $f(x) = x - x$, does that really mean "f is the function that subtracts its input from itself", or does it mean $f(x) = 0$? Again, these mean different things when you plug in, say, any reasonable definition of $\infty$. $\endgroup$
    – user541686
    Apr 7 '17 at 1:11
  • $\begingroup$ @Mehrdad: in a formal setting, the rules that pertain are known upfront. For instance, if you are working with powers, $(a^b)^c=a^{bc}$ is true in the reals, but false in the complex. You shouldn't care about what $a,b,c$ are (they could be elements of an abstract field) but know what transformations are allowed. It is not a matter of clarity, it is a matter of rigor. $\endgroup$
    – user65203
    Apr 7 '17 at 6:42
  • $\begingroup$ I was responding to your claim that "At no time do you have to think that the symbols represent numbers and the operators arithmetic computations." I was saying that, in fact, you do have to pause and think what the notation means, because sometimes the meaning of something as simple as $-1$ is unclear and affects the results, as I showed. $\endgroup$
    – user541686
    Apr 7 '17 at 7:37
  • $\begingroup$ @Mehrdad: if you are in a context where $-1$ is ambiguous (in terms of its properties), then you are not working formally. $\endgroup$
    – user65203
    Apr 7 '17 at 7:45
  • $\begingroup$ Wha...? Ambiguity is something the reader decides, not you. You can totally be formal but still be misinterpreted because your writing is ambiguous. I've seen plenty of formal proofs where I got tripped up as to whether e.g. $x^2$ meant the second iterate or whether it meant the square of $x$. The steps were all rigorous & formal, nothing was wrong there. The notation was all explained in the beginning too. I still had to repeatedly stop and parse the notation again. Your assertion that you don't have to pause and think about notation in a formal proof is blatantly false. $\endgroup$
    – user541686
    Apr 7 '17 at 8:04
0
$\begingroup$

An formal statement/proof assumes that the problem structure is "sufficiently regular" for the conclusion to hold, and merely explains how to derive the conclusion assuming the unstated assumptions hold true.

Example of an informal statement:

The sum of an infinite geometric series with ratio $r$ is $$\sum_{k=0}^\infty r^k = \frac{1}{1-r}$$

This statement is informal since it is unclear whether this definition applies to some $r$ or all $r$; it does not explain whether it is intended to ascribe a sum to divergent series (sometimes possible).

A formal statement/proof is one that states all assumptions necessary for its conclusions to hold, except perhaps those that are blatantly obvious to the average audience.

Example of a formal statement:

The sum of an infinite geometric series with ratio $r$ is $$\sum_{k=0}^\infty r^k = \frac{1}{1-r}$$ if $|r|<1$; otherwise, we say the series diverges and does not have a sum.

This statement is formal since it explains its required assumptions ($|r|<1$) and does not leave the reader guessing as to whether $1+2+4+\ldots$ was intended to have a sum.

Nevertheless, neither statement is considered incorrect; both of them are correct with reasonable assumptions.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.