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

9
votes
5answers
2k views

List of Mathematical Impossibilities proved using special tools

It is always weird to see a proof that something is impossible, especially when the tools used in the proof have nothing to do(at a first sight) with the original statement of the problem. I know a ...
6
votes
1answer
611 views

Understanding various definitions of TREE($n$) in Friedman's finite form of Kruskal's tree theorem.

I was reading the Wikipedia article on Friedman's finite form of Kruskal's tree theorem, and am interested in the large numbers TREE(n). I would like to verify TREE(2)=3 myself, but find conflicting ...
2
votes
2answers
170 views

What is this proof syntax (Hoare 1974)?

I'm reading the seminal "Monitors" paper by Hoare. On page 4 he proceeds with a logical proof using syntax I've never seen before, and neither know what it's called or how to properly read it. ...
1
vote
1answer
227 views

subformula property (anchored proofs)

0 Hello, I would like to ask for some explanation on some property of propositional sequent calculus. The sequent calculus that I use here follows that of Stephen Cook, in "Logical Foundations of ...
2
votes
1answer
90 views

Quasi-interactive proof on real numbers

[This is a cleaner and simpler restatement of a question I asked earlier on Theoretical CS forum. Please re-tag as appropriate.] Suppose you have two oracles (black boxes) that represent real ...
4
votes
2answers
201 views

Are all proofs “short enough” to be computed?

The Completness Theorem in Propositional Logic says that a tautological statement has a derivation. Does this existence imply that this derivation consists of a finite formation sequence? I ...
4
votes
1answer
163 views

Formal proof involving $\varphi( v_k / v_l )$

I'd like to show that if $\varphi(v_k / v_l )$ and $\varphi(v_l / v_k )$ are admissible then $[\exists v_k \varphi(v_k)] = [\exists v_l \varphi(v_l)]$ where $[\varphi]$ denotes the equivalence class ...
5
votes
1answer
240 views

What are various proofs good for?

There are plenty of questions around here, which are proven to be right or wrong in various ways. I wonder, what one can learn from these differing ways of how to prove something, despite the fact ...
1
vote
2answers
508 views

Contradiction Theorem

I'm a beginner in formal logic. Can anyone of you help me with the proof of the following lemma: For any Theory $T$ and closed formula $\varphi$ it holds that $T \vdash \varphi$ if and only if ...
8
votes
2answers
1k views

Definition of “non-constructive proof”

I was wondering if it is possible to define exactly what a non-constructive (nc) proof is. I have often seen the concept associated with the use of principles such as the axiom of choice or the law of ...
9
votes
2answers
2k views

How can I learn about proofs for computer science?

I study computer science at a university. My school offers several courses where various proofs are expected, but there is no course that introduces the fundamental concepts of proofs and how to write ...
6
votes
4answers
404 views

Are there “essentially non-constructive” statements?

There exist constructive and non-constructive proofs. Sometimes, for a mathematical statement, we can have both non-constructive and a constructive proof. However, are there statements for which ...
3
votes
1answer
141 views

What is a relatively bound variable?

edit: Interestingly, the authors also state at one point that the choice of introduction rule is determined by the structure of the previous goal and the list of introduction rules; but at another ...
12
votes
2answers
266 views

Is it possible to formalize the relationship between different proofs of the same theorem?

Some theorems have many proofs. Examples include the Pythagorean Theorem and the Law of Quadratic Reciprocity. I was wondering if one could formalize the relationship between these proofs. Sure, they ...
8
votes
1answer
241 views

Reverse Mathematics of Well-Orderings

In Simpson's book, a well-ordered set $X$ is a linear ordering such that there are no functions $f : \mathbb{N} \rightarrow X$ which is decreasing. However, a familiar definition of well-ordering is ...
3
votes
3answers
350 views

Impossibility theorems

I've been wondering how you go about proving an impossibility e.g. when I looked up Abel's impossibility theorem it says nothing about the proof and only restates the theorem when I'd like to know how ...
3
votes
2answers
318 views

Formula $\Sigma_{1}$ in $Q$ but not $\Sigma_{1}$

A formula $\varphi$ is $\Sigma_{1}$ over a given theory $T$ if $T\vdash \varphi \leftrightarrow \psi$ for some $\psi \in \Sigma_{1}$. Is there a formula $\varphi$ in the language of arithmetic that ...
4
votes
1answer
401 views

Can it be shown that ZFC has statements which cannot be proven to be independent, but are?

I am familiar with the concept that a statement can be proven indepent such as in the case of the continuum hypothesis where both ZFC+CH and ZFC+(CH is false) are both proven consistent, but I would ...
4
votes
1answer
155 views

Proving premises working on a proof of the conclusion

like very much this site. Let's consider the following rules of a deduction system (due to Sch\"{u}tte). I'll write them all, but some of them may not be useful. WEAK RULES Rule 1: ...
6
votes
3answers
491 views

Justification of Proofs by Contradiction

Is there a validation for the technique of proof by contradiction? Or do those who use it take its validity as an axiom?
13
votes
7answers
6k views

Difference between “Show” and “Prove”

In many mathematics problems you see the phrase "prove that..." or "show that..." something is. What's the difference between these two phrases? Is "showing" something different from "proving" ...
4
votes
1answer
123 views

What's wrong with this inference in natural deduction?

Could anybody explain to me what's wrong with the following inference? Thanks. $--- u$ $P(a)$ $---- {\forall}I^a$ $\forall x . P(x)$ $---- {\forall}E$ $P(b)$ $------ {\supset}I^u$ $P(a) ...
4
votes
2answers
900 views

What is the so-called eigenvariable or parameter in natural deduction?

I am reading the Wikipedia article on Natural Deduction. In section 6, the presentation of intr and elim rules for the universal and existential quantifiers, it mentions a concept called ...
4
votes
1answer
149 views

algorithmic checking of proofs

Is it possible to check if a proof is correct algorithmically(especially with computer aid)? I ask this question because I find that a lot of time is taken up during lectures going through the proof ...
3
votes
3answers
295 views

Is there an intuitionistic proof of $\lnot p(a) \rightarrow p(b) \vdash \exists x p(x)$, what would Herbrand's Theorem say?

I am currently studying Herbrand's Theorem and wonder in which form it would hold for intuitionistic logic. I guess in intuitionistic logic we will have only one witness. To be practical I am ...
5
votes
1answer
133 views

Recursively defined systems are always consistent?

I was reading something which contained the following statement: It is a well-established mathematical result that theories consisting only of recursive definitions... are inherently consistent. ...
4
votes
4answers
479 views

Scapegoat Theory!

How to show that the Peano Arithmetic theory is not scapegoat? Note: Peano Arithmetic is a consistent theory. A theory T is scapegoat if for every formula $A$ with only one free variable there ...
18
votes
5answers
2k views

How to prove the mathematical induction is true?

I have no idea about the underlying theory from which the mathematical induction was derived. How to prove the mathematical induction is true?
8
votes
1answer
241 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
273 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 ...
11
votes
4answers
450 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
246 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
457 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
500 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 ...
11
votes
1answer
966 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 ...
14
votes
4answers
4k 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 ...
15
votes
7answers
2k views

Why do statements which appear elementary have complicated proofs?

The motivation for this question is : Rationals of the form $\frac{p}{q}$ where $p,q$ are primes in $[a,b]$ and some other problems in Mathematics which looks as if they are elementary but their ...
7
votes
1answer
418 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; ...
7
votes
1answer
354 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 ...
9
votes
1answer
438 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 ...
31
votes
4answers
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
465 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$ ...
63
votes
8answers
4k 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 ...
13
votes
6answers
2k 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 ...