# Tagged Questions

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.

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

### Hilbert's (cancelled) 24th problem

Hilbert's 23 problems, ten of which were presented at the 1900 ICM in Paris, are too famous for any mathematician to not know. If one reads the descriptions of the problems in Hilbert's paper, one ...
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 "...
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 ...
4k 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 ...
973 views

### Godel on recursion-theoretic hierarchies

At the end of his excellent article, "The Emergence of Descriptive Set Theory" (http://math.bu.edu/people/aki/2.pdf), Kanamori writes: "Another mathematical eternal return: Toward the end of his ...
5k views

### What's a magical theorem in logic?

Some theorems are magical: their hypotheses are easy to meet, and when invoked (as lemmas) in the midst of an otherwise routine proof, they deliver the desired conclusion more or less straightaway&...
2k 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 ...
551 views

### Why is there no connection between fast-growing functions and complex analysis

I found myself wondering the other day whether the fast-growing functions from natural to naturals that are studied by people like proof theorists are the restriction to the naturals of analytic ...
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 ...
3k views

### Proofs of Gödel's theorem

I am interested in different contexts in which Gödel's incompleteness theorems arise. Besides traditional Gödelian proof via arithmetization and formalization of liar paradox it may also be obtained ...
970 views

### Deep theorems and long proofs

I ran across this discussion by Daniel Shanks, "Is the quadratic reciprocity law a deep theorem?." Solved and Unsolved Problems in Number Theory. Vol. 297. AMS, 2001. p.64ff. which made me ...
3k views

### Writing “Semi-Formal” Proofs

I am very interested in proofs. I have taken an undergraduate course called "Logic and Set Theory" which I found very interesting, but ultimately unsatisfying. My biggest disappointment has to do ...
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 ...
851 views

### Does Taranovsky's system of ordinal notations make sense?

Dmytro Taranovsky has a Web page on which he claims to define a system of ordinal notations strong enough to provide an ordinal analysis of full second-order arithmetic. I think (perhaps unjustly) ...
712 views

### Goodstein's theorem without transfinite induction

Goodstein's theorem is an example of a theorem that is not provable from first order arithmetic. All proofs of the theorem seem to deploy transfinite induction and I've wondered if one could prove the ...
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 ...
1k views

### Proof theoretic ordinal

In Ordinal Analysis, Proof-theoretic Ordinal of a theory is thought as measure of a consistency strength and computational power. Is it always the case? I. e. are there some general results about ...
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 need?...
582 views

### Can ZFC prove it cannot derive an inconsistency in $n$ steps?

Let $Con(\mathtt{ZFC}, n)$ denote the statement "$\mathtt{ZFC}$ cannot prove the contradiction within $n$ steps (or better within $n$ symbols) within a given proof system (say a natural deduction to ...
29k 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 ...
854 views

### Proof-Theoretic Ordinal of ZFC or Consistent ZFC Extensions?

Let the proof theoretic ordinal $\alpha$ of a theory $T$ be the least recursive ordinal such that $T$ does not prove that $\alpha$ is well-founded. This ordinal is intended to quantify in some sense ...
2k views

### Consequences of technically proving anything in Coq (on at least Linux) exploiting a bug? [closed]

Technically, it is possible to prove anything in Coq proof assistant [1] (on at least Linux) due to a programming feature (or bug). This seems tractable when validating large proofs. Human analysis ...
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. ...
2k views

### Deduction theorem

Is there an axiomatic system where the deduction theorem does not hold?
840 views

### Time in Girard's Geometry of Interaction

Jean-Yves Girard writes at the end of his paper "Towards a Geometry of Interaction", page 105, that we have three intuitions about the nature of time: time is logic modulo the order of rules, time ...
607 views

### Is there a consistent arithmetically definable extension of PA that proves its own consistency?

I asked this on stackexchange with no answer. The negation would be the obvious generalization of Gödel's second incompleteness from r.e. extensions of PA to any arithmetically definable extension of ...
343 views

### What metatheory proves $\mathsf{ACA}_0$ conservative over PA?

Simpson's book shows $\mathsf{ACA}_0$ is conservative over $\mathsf{PA}$ in the natural way by model theory using definable subsets. Of course, $\mathsf{ACA}_0$ being conservative over PA is ...
828 views

### Von Neumann's consistency proof

In the paper Zur Hilbertschen Beweistheorie, John Von Neumann has proposed a consistency proof for a fragment of first-order arithmetic (the fragment without induction and with the successor axioms ...
766 views

### Reverse mathematics of Hilbert's Theorem 90

What is known, and what is published, on the reverse mathematics of the nest of results called Hilbert's Theorem 90?
254 views

### Nontrivial upper bounds on proof-theoretic ordinals of strong theories: do we have any?

Motivated by Consistency of Analysis (second order arithmetic) and Proof-Theoretic Ordinal of ZFC or Consistent ZFC Extensions?, I have the following question: Are there any examples of strong ...
454 views

### Is it possible for a theorem to be constructive only in a non-constructive metatheory?

There are several theorems in category-theoretic logic which say something like, "any proposition in X logic that is provable in topos logic assuming (the law of excluded middle and) the axiom of ...
313 views

### How to measure the strength of Zermelo over bounded Zermelo?

Bounded Zermelo is Zermelo set theory with only bounded separation. It has the same strength as simple type theory or MacLane set theory or ETCS. It is a finitely axiomatized fragment of Zermelo, so ...
1k views

### Are there non-diagonal proofs for Cantor's continuum and Godel's incompletness theorems?

There is a formal definition for the notion of a formal proof. Question 1. Is there any formal definition for the notion of a diagonal formal proof? Consider the following theorems both proved by ...
1k views

### Does formalizing math require search and creativity, or is it near-mechanical?

I remember reading somewhere that it takes about a week to convert a page of math into something a proof-assistant like Isabelle or HOL Light would accept. Is this type of conversion something that ...
1k 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 ...
2k views

### Understanding the nature and structure of proofs; Reverse Mathematics and Proof Theory. Prerequisites? Good introductory texts?

I'm still studying maths at undergraduate level, but intend to continue exploring topics in pure maths after I have graduated, so am thinking already about what directions I'd like to persue now, (as ...
785 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 ...
420 views

### Algorithmic complexity of formal proof verification?

In this question, suppose $S$ is some popular real-world automated proof system that is stronger than or equivalent to Peano Arithmetic. I would be happy with a positive answer to the following for ...
493 views

### Left-bracketed Ackermann function also not primitive recursive?

The original Ackermann function $\varphi\colon \mathbb{N}\times\mathbb{N}\times\mathbb{N}_0\to \mathbb{N}$ as defined in [1] was invented to prove that there is a function that is recursive but not ...
304 views

### Intutionistic Robinson Arithmetic

By Friedman translation $HA$ and $PA$ prove the same $\Pi_2$ formulas. Is it true for Intutionistic Robinson arithmetic(Robinson axioms with intutionistic logic) and classic Robinson arithmetic? ...
404 views

### Does any lower bound on proofs of FLT improve Shepherdson 1965?

In 1965 Shepherdson proved that FLT is independent of the fragment of PA that uses only open induction and signature $0,S,+\times$. Indeed $2x+1\neq 2y$ is independent of that fragment. Schmerl ...
320 views

### Large cardinals arising from alternate set theories

My question is whether there are model-theoretic large cardinal axioms associated with $NFU$ - or more generally, with set theories other than $ZFC$. Large cardinal properties generally come in one ...
497 views

### What is known about the reverse mathematics of algebraic number fields?

I know work on the reverse mathematics of countable algebraic field extensions including Galois theory, notably including Dorais, Hirst, and Shafer http://arxiv.org/pdf/1209.4944v2.pdf. But algebraic ...