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

- 20.8k

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

Community wiki

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

- 38k

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

- 40.2k

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

- 109k

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

Community wiki

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

- 1,296

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

- 152k

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

- 30.9k

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

- 30.5k

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

- 68.9k

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.

- 11.8k

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

- 198k

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

- 38k

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

- 7,879

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$. ...

- 42.5k

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

#### Related Tags

proof-theory × 317lo.logic × 242

set-theory × 40

theories-of-arithmetic × 33

reference-request × 32

computability-theory × 31

reverse-math × 25

ordinal-analysis × 21

computational-complexity × 17

model-theory × 17

ordinal-numbers × 16

metamathematics × 16

foundations × 15

constructive-mathematics × 15

type-theory × 11

ho.history-overview × 10

mathematical-philosophy × 10

intuitionism × 9

soft-question × 8

nt.number-theory × 7

co.combinatorics × 6

large-cardinals × 6

proof-assistants × 6

linear-logic × 6

bounded-arithmetic × 6