# Tag Info

## Hot answers tagged proof-theory

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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