Proof theory is an area of logic that studies proof as formal mathematical objects. For questions asking how to write proofs or for checking an informal proof, please use the proof-writing or proof-strategy tags instead.

learn more… | top users | synonyms

7
votes
1answer
226 views

On the existence of closed form solutions to finite combinatorial problems

Is it possible that a finite combinatorial problem may admit a closed form solution, and for it to be impossible in practice to prove the validity of this solution? I'm not sure if a rigorous ...
6
votes
2answers
269 views

Ideas about Proofs

If there are two different proofs for one theorem, at some level are the two proofs the same, or can they be fundamentally different? In other words, if you have two proofs of a theorem, can one show ...
12
votes
4answers
433 views

Existence Proofs

This may be a stretch, but are there examples of proofs that prove that a proof exists for a theorem. For example, if A is a theorem, and it is too tedious to prove that, is it possible to show that ...
1
vote
1answer
240 views

Complexity of verifying proofs

My question can be read on many levels and so I welcome answers to any reading. The general question is: What is the computational complexity of verifying a proof? One way of looking at a ...
11
votes
4answers
416 views

Is there a connection between length of sentence and length of proof?

My basic question is: "Do longer tautologies take longer to prove?" But obviously this is underdetermined. If you are allowed an inference rule "Tautological Implication" then any tautology has a 1 ...
2
votes
2answers
448 views

Proposed Restriction on Universal Instantiation (Natural Deduction)

I propose the following restriction on universal instantiation: UI may not be used to introduce new variables. The variable specified should be an "old" variable, i.e. it must already have been ...
8
votes
1answer
880 views

The Power of Lambda Calculi

A simple question here, which likely demands a somewhat complex answer... Or rather, a set of related questions. What are the advantages of typed lambda calculus over untyped lambda calculus in ...
13
votes
4answers
3k views

Why an inconsistent formal system can prove everything?

I am reading a Set Theory book by Kunen. He presents first-order logic and claims that if a set of sentences in inconsistent, then it proves every possible sentence. Since he does not explicitly ...
12
votes
7answers
1k views

Why do statements which appear elementary have complicated proofs?

The motivation for this question is : http://math.stackexchange.com/questions/4066/rationals-of-the-form-fracpq-where-p-q-are-primes-in-a-b and some other problems in Mathematics which looks as if ...
7
votes
1answer
387 views

Can Robinson's Q prove Presburger arithmetic consistent?

I made an assertion in What are some examples of theories stronger than Presburger Arithmetic but weaker than Peano Arithmetic? that Q has higher consistency strength than Pres, Presburger arithmetic; ...
5
votes
1answer
313 views

Intutive explanation of the PCP Theorem

The PCP theorem states that: Every decision problem in NP has probabilistically checkable proofs of constant query complexity and logarithmic randomness complexity. Can anyone give an ...
7
votes
1answer
397 views

Packing boxes and proof of Riemann Hypothesis

From Scott Aaronson's blog: There’s a finite (and not unimaginably-large) set of boxes, such that if we knew how to pack those boxes into the trunk of your car, then we’d also know a proof ...
27
votes
6answers
2k views

If all sets were finite, how could the real numbers be defined?

An extreme form of constructivism is called finitisim. In this form, unlike the standard axiom system, infinite sets are not allowed. There are important mathematicians, such as Kronecker, who ...
7
votes
3answers
419 views

Why are $\Delta_1$ sentences of arithmetic called recursive?

The arithmetic hierarchy defines the $\Pi_1$ formulae of arithmetic to be formulae that are provably equivalent to a formula in prenex normal form that only has universal quantifiers, and $\Sigma_1$ ...
55
votes
8answers
3k views

Are the “proofs by contradiction” weaker than other proofs?

I remember hearing several times the advice that, we should avoid using a proof by contradiction, if it is simple to convert to a direct proof or a proof by contrapositive. Could you explain the ...
11
votes
6answers
1k views

Aren't constructive math proofs more “sound”?

Since constructive mathematics allows us to avoid things like Russell's Paradox, then why don't they replace traditional proofs? How do we know the "regular" kind of mathematics are free of paradox ...