**7**

votes

**6**answers

19k views

### Difference between a 'calculus' and an 'algebra'

What is really the conceptual difference between a calculus and an algebra.
Eg. Is SKI combinator calculus really a calculus?
A friend claims that free variables are fundamental for a calculus, and ...

**19**

votes

**1**answer

1k views

### Community experiences writing Lamport's structured proofs

About two years ago, I came across this paper by Lamport
http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-how-to-write.pdf
on writing proofs hierarchically. It changed how I wrote ...

**10**

votes

**4**answers

808 views

### How fast can the base-bumping function in Goodstein's theorem grow?

In the usual presentation of Goodstein's theorem, the base is bumped up by the "add 1" function. Does the theorem still hold when we replace this function by a fast-growing one (e.g. Ackermann or busy ...

**5**

votes

**1**answer

1k views

### Ackermann function in the Primitive recursive arithmetic

Hello.
I study primitive recursive arithmetic and have the following questions.
1) Is it possible to express in the PRA that Ackermann function is total?
2) If yes, is such expression decidable in ...

**3**

votes

**1**answer

874 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

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

**15**

votes

**5**answers

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

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

835 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,\ ...

**25**

votes

**3**answers

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

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

**13**

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

**13**

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

**33**

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

**3**

votes

**2**answers

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

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

**10**

votes

**3**answers

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

**39**

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

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

**6**

votes

**6**answers

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

**9**

votes

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

**33**

votes

**7**answers

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

**32**

votes

**15**answers

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

**8**

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

776 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

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

**51**

votes

**28**answers

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

**4**

votes

**4**answers

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

**50**

votes

**14**answers

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