**5**

votes

**1**answer

999 views

### Is there a known way to formalise notion that certain theorems are essential ones?

Suppose You ask a question beginning from "Why some structure is..." or "Why some object has property..." and several
answers arises. Which criteria do You
use to qualify which answer is correct?
...

**1**

vote

**2**answers

1k views

### What does the disjunction elimination rule say?

I read about two different versions of the disjunction elimination rule.
The first version (http://www.fecundity.com/logic/) says that:
if $\Sigma\vdash\phi_0\lor\phi_1$ and ...

**7**

votes

**6**answers

2k views

### Do you know any good introductory resource on sequent calculus?

I'm looking for a good introductory resource on sequent calculus suitable for someone who has studied natural deduction before. Books and online resources are both OK, as long as each rule of ...

**11**

votes

**4**answers

3k views

### Bourbaki's epsilon-calculus notation

Bourbaki used a very very strange notation for the epsilon-calculus consisting of $\tau$s and $\blacksquare$. In fact, that box should not be filled in, but for some reason, I can't produce a \Box.
...

**37**

votes

**7**answers

7k views

### Reductio ad absurdum or the contrapositive?

From time to time, when I write proofs, I'll begin with a claim and then prove the contradiction. However, when I look over the proof afterwards, it appears that my proof was essentially a proof of ...

**35**

votes

**15**answers

7k views

### Strong induction without a base case

Strong induction proves a sequence of statements $P(0)$, $P(1)$, $\ldots$ by proving the implication
"If $P(m)$ is true for all nonnegative integers $m$ less than $n$, then $P(n)$ is true."
for ...

**9**

votes

**4**answers

2k views

### cut elimination

What is the cut rule? I don't mean the rule itself but an explanation of what it means and why are proof theorists always trying to eliminate it? Why is a cut-free system more special than one with ...

**2**

votes

**3**answers

812 views

### Axiom systems and Information Theory

Is there a concept of "information" with respect to the axioms of a mathematical system?
Suppose we have a universe U of theorems. Suppose an axiom system A=(a1,a2,...) has the universe U as the ...

**18**

votes

**11**answers

2k views

### Are there any good nonconstructive “existential metatheorems”?

Are there any good examples of theorems in reasonably expressive theories (like Peano arithmetic) for which it is substantially easier to prove (in a metatheory) that a proof exists than it is ...

**55**

votes

**29**answers

6k views

### Can infinity shorten proofs a lot?

I've just been asked for a good example of a situation in maths where using infinity can greatly shorten an argument. The person who wants the example wants it as part of a presentation to the general ...

**7**

votes

**4**answers

3k views

### Discharging assumptions

When constructing proofs using natural deduction what does it mean to say that an assumption or premise is discharged? In what circumstances would I want to, or need to, use such a mechanism?
The ...

**63**

votes

**16**answers

5k views

### When are two proofs of the same theorem really different proofs

Many well-known theorems have lots of "different" proofs. Often new proofs of a theorem arise surprisingly from other branches of mathematics than the theorem itself.
When are two proofs really the ...