84

First of all, in practice when we say "Conjecture A is equivalent to Conjecture B," what we mean is "We have a proof that Conjecture A is true iff Conjecture B is true." We can have such a proof without having a proof of either conjecture, so this is a meaningful situation. Of course, it will (hopefully) later become trivial, when we prove or disprove the ...


69

Mathematics does have its own version of the replicability problem, but for various reasons it is not as severe as in some scientific literature. A good example is the classification of finite simple groups - this was a monumental achievement (mostly) completed in the 1980's, spanning tens of thousands of pages written by dozens of authors. But over the ...


66

Noah Schweber's answer is in some sense the "right" answer, and I would have said something similar if he hadn't beaten me to it. However, I think that it's worth pointing out that reverse mathematics isn't necessarily the end of the story. The Wikipedia entry on Sperner's lemma says (as of this writing): In mathematics, Sperner's lemma is a ...


50

There are probabilistic proofs of existence. Do they fall into one of your three categories? For example, prove the existence of a real number that is normal in all bases: To do it, we show that "almost all" real numbers (according to Lebesgue measure) have that property. Therefore at least one real number has the property. And the point is: this "almost ...


43

One way to say rigorously what it means for two true theorems to be equivalent is to find a meaningful way to generalize both of them to statements that aren't always true, and then prove that they're true in the same situations. For example: Observe that the fundamental theorem of algebra is equivalent to $0 = 0$, but in a trivial sense since they are ...


42

It’s not very clear to me what you mean by “steps”. One might interpret it as the number of lines in a Hilbert/natural deduction proof, but then there are infinitely many proofs with a fixed number of steps, so this is inconsistent with the argument outlined in the question. So, let me use a measure that has the property that there are only finitely many ...


36

There's some evidence that precisely the opposite can be said: that Euler is aware of the fallacies of proving theorems by example (of course, this does not necessarily mean he has never used it). One memorable instance is his Exemplum Memorabile Inductionis Fallacis, where he described how he was almost led to conjecture a recursive formula for a particular ...


33

I did my PhD thesis in Girard's team in Marseille (my supervisor was Laurent Regnier, himself a student of Girard's) so I have quite a bit of experience with his "excentric" way of communicating and I can attempt an exegesis ( :-) ) of this particular sentence (besides, I am quite familiar with both the philosophical and technical contents of what Girard ...


32

some recent contributions to Hilbert's 24th problem: Towards Hilbert’s 24th Problem: Combinatorial Proof Invariants, D.J.D. Hughes (2006) Hilbert’s 24th Problem & Computer-Assisted Formalized Mathematics, B.W. Paleo (2014) Hilbert’s 24th Problem, Proof Simplification, and Automated Reasoning, L. Wos the earliest work on Hilbert's 24th problem is by ...


28

"Proof by example" is a technique used by Euclid, who often proved results that hold e.g. for n integers in a typical case, say for 3 integers, as well as by Diophantus, who had to choose values for his parameters due to his lack of algebraic notation. I regard both versions as complete proofs. This is apparently not what Fraser is referring to; Euler did ...


26

There is a famous proof of the existence of two irrational numbers $a$ and $b$ such that $a^b$ is rational. The proof considers two cases: $\sqrt{2}^\sqrt{2}$ is irrational, or it is rational. In either case we can find such $a$, $b$. Then it applies the law of excluded middle to say one of these cases in fact holds. You can see a discussion of the proof ...


24

There is a very nice paper of Wagon, which can serve as a sort of case study. The paper presents fourteen different proofs of the following theorem. Theorem. If a rectangle $R$ is tiled by rectangles, each of which has at least one integer side, then $R$ itself has at least one integer side. If you have not thought about the problem, you may want to ...


22

The statement you quoted is somewhat sloppy, since there is no precise notion of a short proof for a single formula. There is, however, a notion of short proofs for a class $C$ of formulas, when the class contains formulas of arbitrarily high length. One says that $C$ admits short proofs if there is a polynomial $p(x)$ such that, for every natural number $...


21

Consider the following question of Erdos and Hajnal: Question (Erdos-Hajnal) Is there a finite $K_4$-free graph which, when the edges colored by $2$ colors, always contains a monocolored triangle. The question is answered by Shelah, and his argument uses infinity. I think this is the only known proof. Shelah's proof of the theorem is simply as follows: ...


20

If you're willing to accept a contrived statement, then it's not hard to get an explicit example, but this may not be the sort of example you're looking for. Following Gödel's approach, you can make a statement of the form "I have no formal proof of less than a hundred pages." (More precisely, you should use implicit self reference, along the lines of "...


20

As Carlo Beenakker's references indicate, we are still a long way off from having a satisfactory definition of the "simplicity" of a proof. There are some technical definitions of simplicity that can serve as helpful heuristics for automatic theorem provers, but they do not capture most aspects of our intuition for what "simplicity" means. The June 2015 ...


20

Yes, let $x$ be Chaitin's constant. Then both $x$ and $\gamma + x$ are uncomputable, therefore irrational.


20

The simply-typed $\lambda$-calculus is not stronger than second-order logic. The simply-typed $\lambda$-calculus has: product types $A \times B$, with corresponding term formers (pairing and projections) function types $A \to B$, with corresponding term formers (abstraction and application) equations governing the term formers and subtitution The simply-...


19

There is a body of very interesting work surrounding the proof complexity of various formulations of the well-known pigeon-hole principle, the fact that there is no injective function from a set of size $m$ to a set of size $n$, when $m\gt n$. It turns out that the difficulty of proving this depends on how much bigger $m$ is than $n$, and so we have actually ...


19

This isn't an answer but a proposal for a precise form of the question. First, here is an abstract form of Cantor's theorem (which morally gives Godel's theorem as well) in which the role of the diagonal can be clarified. Lawvere's fixed point theorem: Let $X, Y$ be objects in a cartesian closed category. Suppose $f : X \times X \to Y$ is a map such that $\...


19

Surprisingly, the answer is yes! Well, let me say that the answer is yes for what I find to be a reasonable way to understand what you've asked. Specifically, what I claim is that if PA is consistent, then there is a consistent theory $T$ in the language of arithmetic with the following properties: The axioms of $T$ are definable in the language of ...


19

The invocation of Church's thesis is not a religuous move but rather a warning to the reader that the author is describing informally an effective procedure which could be translated into a construction of a Turing machine (if one enjoyed such a thing). This is completely standard in computability theory. (And other branches of mathematics have a similar ...


17

I will attempt to answer your first question by describing the context of the von Neumann paper you have asked about. As is well known, Hilbert had earlier posed the problem of establishing the consistency of first order arithmetic (with full induction), and had suggested the development of the method of "$\varepsilon$-substitutions" (also known as "$\...


16

This is an instance of a general phenomenon: adding true $\Pi_1$ sentences to a reasonable theory doesn't change its proof-theoretic ordinal. $Con(T)$ is $\Pi_1$, so if $T$ is any consistent theory, $PA+Con(T)$ still has proof-theoretic ordinal $\epsilon_0$. This is a standard fact in the area, though I'm not sure it's included in the usual sources on ...


16

Yes, but this is nothing to do with $\gamma$. Let $a$ be any real number. Then there is $x$ so that $x$ and $a+x$ are both irrational. Proof (within ZF): the set of $x$ such that $x$ is rational is countable, the set of $x$ such that $a+x$ is rational is also countable. But $\mathbb R$ is uncountable.


16

Many existence proofs in analysis / probability follow this line of argument: 1. Construct a family of objects that approximately satisfy some desired property. 2. Show that the family is precompact. 3. Show that every accumulation point must satisfy the desired property. I suppose that to some extent this would often count as a constructive proof since in ...


16

This is the strangest existence proof I know; it is a nonconstructive proof that there exists a proof of a certain statement. In other words, we prove the statement by proving that a proof exists. I'm thinking of Lob's theorem. The Godel sentence is a number-theoretic assertion $G$ which informally says of itself that it cannot be proven in Peano Arithmetic ...


16

So far as I can tell, there was no debate about the validity of these methods before Brouwer. I rely on Colin McLarty's review of the key example in his 2007 paper "Theology and its discontents: David Hilbert's foundation myth for modern mathematics." The famous examples from before Hilbert, e.g. Archimedes's method of exhaustion, Euclid's proof that "prime ...


16

I want to echo the other answer, that Brouwer presents the first robust challenge to the Law of Excluded Middle (LEM), but I do want to add some history and background, and maybe recommend a related paper. The main paper by Brouwer is De onbetrouwbaarheid der logische principes or in English The unreliability of the logical principles published in 1908. ...


15

Here is an answer to Qiaochu's question Does Lawvere's fixed point theorem continue to hold for closed monoidal categories? As expected, the answer is "no". Define a graded set to be a set $X$ with a map $\mathrm{deg}: X \to \mathbb{Z}_{\geq 0}$. For $X$ and $Y$ graded sets, and $d \in \mathbb{Z}_{\geq 0}$, define a map $f: X \to Y$ to have degree $d$ ...


Only top voted, non community-wiki answers of a minimum length are eligible