**5**

votes

**4**answers

1k views

### Zero-knowledge proof that 0 = 1

Suppose one day I came up with a proof that 0 = 1 in some formal system such as PA or ZFC that cannot prove its own consistency (unless it is inconsistent). Would it be possible to have a ...

**6**

votes

**1**answer

281 views

### Strength of Transfinite Induction on the Difference Hierarchy

I'm wondering if a particular theory of second order arithmetic has been studied or is known to be equivalent to some other theory.
Consider the formulas generated by $\Pi^1_1$ and $\Sigma^1_1$ ...

**4**

votes

**5**answers

879 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

**6**answers

1k views

### Difference between turnstile and implication

Hi,
Does anyone know the difference between proving that
|- phi
------------------
|- ( psi -> phi )
and proving that
...

**4**

votes

**2**answers

359 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

**5**answers

794 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

**3**answers

483 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

**1**answer

536 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

**6**answers

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

**9**

votes

**6**answers

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

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

836 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

889 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

938 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

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

**26**

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

487 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

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

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

**3**answers

728 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

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

**10**

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

**36**

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

**34**

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

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

**51**

votes

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

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

**61**

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