For question in Proof Theory, where "proofs" themselves are the object of mathematical investigation. It is not to be used to request a proof of some result.

learn more… | top users | synonyms

7
votes
6answers
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
1answer
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
4answers
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
1answer
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
1answer
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
2answers
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
5answers
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
3answers
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
1answer
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
3answers
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
1answer
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
5answers
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
2answers
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
13answers
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
2answers
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
1answer
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
3answers
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
4answers
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
1answer
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
2answers
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
6answers
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
3answers
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
7answers
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
15answers
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
4answers
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
3answers
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
11answers
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
28answers
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
4answers
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
14answers
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 ...