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

4
votes
5answers
870 views

“Let $x \in A$”, beginning a proof of “$\forall x \in A$ …”, if A were empty [closed]

I work at a four-year teaching school, where we pride ourselves on teaching pure math, proof, and a rather obsessive carefulness of work. Recently I have been criticized for saying that "Let $x \in ...
5
votes
6answers
1k views

Difference between turnstile and implication

Hi, Does anyone know the difference between proving that |- phi ------------------ |- ( psi -> phi ) and proving that ...
4
votes
2answers
354 views

What is the depth of the “provability heirarchy”?

I am not a logician or set theorist, so hopefully this makes sense. Let $T$ be a theory which is expressive enough to make statements like "Statement $A$ has a proof in $T$"; for example, $T$ might ...
-1
votes
5answers
793 views

finding cutting edge papers and books

Hi all, what are the best strategies to find cutting edge papers and books on a field of mathematics? .. Example: 2-3 years ago I had to analyze a time series. I found a paper and showed that to ...
4
votes
3answers
479 views

Can a typing judgment admit essentially different derivations?

In any sort of type theory, there are a bunch of rules for constructing derivations of typing judgments such as $x:A,\; y:B(x) \;\vdash\; z:C(x,y)$. (I intend to include also judgments of the form ...
3
votes
1answer
532 views

Derivability conditions for Robinson arithmetic

Two pieces of hearsay I have encountered about Robinson's Q: Q fails to satisfy the Löb derivability conditions; Pudlák criticised the Löb derivability conditions and suggested rival, weaker ...
25
votes
6answers
3k views

Why can't proofs have infinitely many steps?

I recently saw the proof of the finite axiom of choice from the ZF axioms. The basic idea of the proof is as follows (I'll cover the case where we're choosing from three sets, but the general idea is ...
7
votes
6answers
21k 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 ...
20
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
825 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
884 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
918 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
845 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
478 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
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
1answer
3k 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
724 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
948 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 ...
10
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. ...
36
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 ...
33
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
787 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
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 ...
51
votes
28answers
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 ...
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 ...
51
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 ...