**3**

votes

**1**answer

1k views

### Proving inequalities over algebraic structures

I've been looking at proof techniques in formal systems like Coq and Agda recently, and encountered the newring tactic described here for proving equalities over ...

**6**

votes

**2**answers

1k views

### When is a statement provable?

We all know that Gödel showed that there, in a formal system, are true statements that are non-provable (undecidable). In ZFC, there's Kaplansky's Conjecture, the Whitehead problem, etc.
We can also ...

**16**

votes

**5**answers

3k views

### How do proof verifiers work?

I'm currently trying to understand the concepts and theory behind some of the common proof verifiers out there, but am not quite sure on the exact nature and construction of the sort of systems/proof ...

**7**

votes

**3**answers

2k views

### Most general formulation of Gödel's incompleteness theorems

Modern statements of Gödel's incompleteness theorems are usually in terms of first-order predicate logic. However, I've often read the claim that they extend to arbitrary formal systems that can prove ...

**4**

votes

**1**answer

883 views

### Can one really construct an “ordinal table”?

Many books describe how one can construct "by hand" a table of ordinals $1,\ 2,\ \ldots,\ \omega,\ \omega +1,\ \omega +2,\ \ldots,\ \omega\cdot 2,\ \omega\cdot 2 +1,\ \ldots,\ \omega^{2},\ \ldots,\ ...

**29**

votes

**3**answers

3k views

### Feit-Thompson Theorem: The Odd Order Paper

For reference, the Feit-Thompson Theorem states that every finite group of odd order is necessarily solvable. Equivalently, the theorem states that there exist no non-abelian finite simple groups of ...

**6**

votes

**1**answer

554 views

### How to locate the paper that established Robinson Arithmetic?

If I'm not mistaken, it was in his seminal paper “An Essentially Undecidable Axiom System”, published in
Proceedings of the International Congress of Mathematics (1950), 729–730,
where R.M. ...

**14**

votes

**5**answers

1k views

### Characterizing visual proofs

``Proofs without words'' is a popular column in the Mathematics magazine.
Question: What would be a nice way to characterize which assertions have such visual proofs? What definitions would one ...

**15**

votes

**2**answers

2k views

### Clarification of Gödel's second incompleteness theorem

I am sorry for the following question, because the actual answer to this question is in the beautiful works of Feferman and Jeroslow, but, unfortunately, I havn't any time to go into that specific ...

**34**

votes

**13**answers

3k views

### Examples of statements that provably can't be proved using a promising looking method

Motivation: In Razborov and Rudichs article "Natural proofs" they define a class of proofs they call "natural proofs" and show that under certain assumptions you can't prove that $P\neq NP$ using a ...

**4**

votes

**2**answers

2k views

### Independence of PA implies independence of PA union all true $\Pi_1$ statements

Prove that if a statement is independent of Peano Arithmetic (PA), then it's also independent of PA$_1$, where PA$_1$ is the union of the set of axioms in PA and the set of all true $\Pi_1$ ...

**0**

votes

**1**answer

5k views

### How to prove that the A* Algorithm is admissible (by induction)? [closed]

I've been struggling with this question for the past hour but I can't seem to get it.
We begin with the start node S. But what should be the induction hypothesis?
EDIT:
My bad, I was referring to ...

**11**

votes

**3**answers

778 views

### Reducing ACA₀ proof to First Order PA

According to the Wikipedia ACA0 is a conservative extension of First Order logic + PA.
http://en.wikipedia.org/wiki/Reverse_Mathematics
First of all I have a few questions about the proof:
a - What ...

**41**

votes

**4**answers

4k views

### What was Gödel's real achievement?

When I first heard of the existence of Gödel's theorem, I was amazed not just at the theorem but at the fact that the question could be made precise enough to answer: how on earth, even in ...

**5**

votes

**1**answer

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

**12**

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

**43**

votes

**7**answers

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

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

**56**

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

**9**

votes

**4**answers

3k views

### What does it mean to 'discharge assumptions or premises'?

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

**64**

votes

**16**answers

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