87 votes
Accepted

What does it mean to suspect that two conjectures are logically equivalent?

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 ...
69 votes

Replication crisis in mathematics

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 ...
68 votes

What does it mean to suspect that two conjectures are logically equivalent?

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 ...
  • 67.1k
50 votes
Accepted

"Strange" proofs of existence theorems

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 "...
44 votes
Accepted

Can ZFC prove it cannot derive an inconsistency in $n$ steps?

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 ...
43 votes

What does it mean to suspect that two conjectures are logically equivalent?

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 ...
37 votes
Accepted

Did Euler prove theorems by example?

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 ...
33 votes
Accepted

Time in Girard's Geometry of Interaction

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 ...
32 votes

Hilbert's (cancelled) 24th problem

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 ...
31 votes

When are two proofs of the same theorem really different proofs

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 ...
  • 29.1k
29 votes

Did Euler prove theorems by example?

"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 ...
26 votes

"Strange" proofs of existence theorems

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 ...
  • 19.6k
25 votes
Accepted

How can the simply typed lambda calculus be Turing-incomplete, yet stronger than second-order logic?

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 ...
  • 44.2k
22 votes

Can infinity shorten proofs a lot?

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. ...
22 votes
Accepted

What defines a "short proof"?

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 ...
21 votes

Hilbert's (cancelled) 24th problem

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 ...
  • 67.1k
20 votes

Euler's constant: irrationality and proof theory

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

Is there a consistent arithmetically definable extension of PA that proves its own consistency?

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,...
20 votes

The Halting Problem and Church's Thesis

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 ...
  • 44.2k
20 votes

What is the logical status of the sentence combining the ideas of Löb and Rosser, "this sentence is provable before any proof of its negation"?

As Akiva Weinberger conjectured, this depends on the implementation. Indeed, $0=0$ is a sentence of this type, i.e. $0=0$ is equivalent to the claim that there is a proof of $0=0$ that is shorter than ...
  • 119k
17 votes
Accepted

Von Neumann's consistency proof

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 ...
  • 14.6k
17 votes

"Strange" proofs of existence theorems

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'...
  • 38.4k
16 votes

Euler's constant: irrationality and proof theory

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 ...
16 votes

"Strange" proofs of existence theorems

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. ...
16 votes

Status of proof by contradiction and excluded middle throughout the history of mathematics?

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 ...
  • 17.7k
16 votes
Accepted

Status of proof by contradiction and excluded middle throughout the history of mathematics?

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 ...
  • 817
15 votes

Why is a cut-free system consistent?

For the Gentzen sequent calculus, cut-free proofs have the subformula property: every formula that occurs in a proof of $\Gamma \Rightarrow \Delta$ is a subformula of an element of $\Gamma\cup\Delta$. ...
15 votes

Has Apéry's proof of the irrationality of $\zeta(3)$ ever been used to prove the irrationality of other constants?

Regarding your second question, Apéry's amazing formula $$\zeta(3) = {5\over 2} \sum_{n\ge1} {(-1)^{n-1} \over n^3 {2n \choose n}}$$ has inspired the search for analogous formulas for other zeta ...
  • 67.1k
15 votes
Accepted

van der Waerden's theorem in Reverse Mathematics

There is a powerful combinatorial theorem, known as the Hales–Jewett theorem, which readily implies van der Waerden's theorem. On the other hand, the paper below by Matet exhibits primitive recursive ...
  • 14.6k
15 votes

Replication crisis in mathematics

How can we expect that increasingly complicated proofs are replicated when so few people can understand them in the first place? My answer to that is that we do not expect them to be replicated in the ...

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