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

1k 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

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

**62**

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