89
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 ...
73
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
69
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 ...
51
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 "...
46
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 ...
38
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
30
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 ...
Community wiki
27
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 ...
27
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 ...
26
votes
How is it possible for PA+¬Con(PA) to be consistent?
As is being discussed in the comments, the non-standard proofs in non-standard models of $\mathsf{PA}$ are not trustworthy (in that they're not sound). I'll give a sort of 'toy model' illustrating the ...
25
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 ...
22
votes
Accepted
Has Apéry's proof of the irrationality of $\zeta(3)$ ever been used to prove the irrationality of other constants?
The proof of irrationality of $\displaystyle\sum_{n=0}^{+\infty}\frac1{F_n}$ (where $F_n$ is the $n$-th Fibonacci number) by RIchard André-Jeannin is an adaptation of the original Apery's proof of the ...
21
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'...
21
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 ...
21
votes
Brute force open problems in graph theory
The existence of a 57-regular "Moore graph" is one such problem.
We define the diameter of a graph $G$ to be the least $l$ such that any two vertices $u,v$ have a path between them using $\...
Community wiki
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 ...
17
votes
Has Apéry's proof of the irrationality of $\zeta(3)$ ever been used to prove the irrationality of other constants?
As Frits Beukers writes in http://www.staff.science.uu.nl/~beuke106/caen.pdf "Ironically all generalisations tried so far did not give any new interesting results. Only through a combination of ...
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
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 ...
16
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 ...
16
votes
Brute force open problems in graph theory
Elaborating on the comment of Wojowu, for what positive integers $q$
does there exist a bipartite graph $G$ with vertex bipartition $(A,B)$
satisfying: (a) $|A|=|B|=q^2+q+1$, (b) $G$ is regular of ...
Community wiki
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 ...
15
votes
Replication crisis in mathematics
Has this crisis impacted (pure) mathematics, or do you believe that
maths is mostly immune to it?
Immune to the replication problem, yes. But not immune to the attitudes which cause scientists to do ...
Community wiki
15
votes
Computational complexity theoretic incompleteness: is that a thing?
Consider the sentence $P(n)$ which says "This sentence has no proof shorter than $n$ characters." This sentence is true, and even has a proof - enumerate all strings of length $n$ and check ...
14
votes
Accepted
Let's keep adding once undecidable statements
Short answer: $ZFC_\alpha$ only makes sense for those $\alpha$ which have "nicely definable representations" - specifically, for the computable ordinals $\alpha$. (An ordinal is computable if there is ...
14
votes
Is there good reference for proof complexity?
These are three books that I know:
Logical Foundations of Proof Complexity
Bounded Arithmetic, Propositional Logic and Complexity Theory
Logical Foundations of Mathematics and Computational ...
14
votes
Accepted
How can we know the well-foundedness of $\epsilon_0$?
Let me use the notation $\omega_n$ for an exponential tower of $\omega$'s of height $n$, so $\omega_{n+1}=\omega^{\omega_n}$. Then $\epsilon_0$ is the supremum of $\{\omega_n:n\in\omega\}$. PA proves ...
13
votes
Accepted
The Halting Problem and Church's Thesis
Let me point out that there are really a family of Church-Turing
theses assertions.
On the one hand, for what is sometimes described as the weak
Church-Turing thesis, one imagines an idealized human ...
13
votes
Accepted
Cut-free proofs in ZFC
Yes, one can eliminate cuts polynomially for proofs in ZFC, PA, and similar theories that have nontrivial axiom schemata allowing arbitrary formulas.
For PA, replace a cut
$$\color{blue}{\dfrac{\...
Only top scored, non community-wiki answers of a minimum length are eligible
Related Tags
proof-theory × 360lo.logic × 279
set-theory × 46
theories-of-arithmetic × 42
computability-theory × 40
reference-request × 32
ordinal-analysis × 31
model-theory × 29
reverse-math × 26
computational-complexity × 23
ordinal-numbers × 19
foundations × 17
constructive-mathematics × 16
metamathematics × 16
type-theory × 15
ho.history-overview × 10
mathematical-philosophy × 10
proof-complexity × 10
co.combinatorics × 9
decidability × 9
intuitionism × 9
soft-question × 8
modal-logic × 8
formal-proof × 8
nt.number-theory × 7