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

0
votes
2answers
214 views

is it possible to prove the method of mathematical induction itself?

Since the method of mathematical induction follows some sort of 'algorithm', would the method itself be provable? namely, give that the method of mathematical induction is as follows: if S is a ...
2
votes
1answer
230 views

Proof the following proposition: for all $n \geq 0, \mathrm{fib}(n) \leq n!$

I am a comp science undergrad and just started to learn proof. And I have been thinking about this question for a few days. How should I present my answer? Do I have to use the Binet's formula? Or can ...
17
votes
5answers
1k views

If it takes infinite steps to prove a statement, is that a valid proof?

In Cantor's diagonal argument, it takes (countable) infinite steps to construct a number that is different from any numbers in a countable infinite sequence, so in fact the proof takes infinite steps ...
1
vote
2answers
140 views

Is a valuation of a logic formula always a trivial task? I.e. is it practically executable?

For a given structure for a quantified theory, is the valuation of any formula always practically executable? In the case of propositional calculus, where every formula has a certain degree, ...
2
votes
1answer
143 views

Sequent calculus - proofs as trees or sequences

First at all, I am new at proof theory, so excuse this perhaps redundant question. I am wondering what is the 'most appropriate' definition of a proof in a sequent calculus (e.g. LK). Proofs as trees ...
5
votes
3answers
633 views

Is the negation of the Gödel sentence always unprovable too?

The incompleteness theorem says that certain theories+deduction system contain at least one sentence (the Gödel sentence "$G$"), which can't be proven (in the system in which it holds). (i) Is ...
3
votes
3answers
433 views

What do we mean by an “Elegant Proof”? [closed]

What do we mean when we say that a mathematical proof is elegant? Of course one can say that the proof is beautiful, but what do we precisely mean when we say that a proof is beautiful ? Is there a ...
7
votes
1answer
139 views

Learning how to prove that a function can't proved total?

In proof-theory one can prove that in, say, Peano Arithmetic one can't prove a function $f$ total. Often this seems to mean $f$ is growing too fast to be provably total. I have some background in ...
4
votes
3answers
389 views

Aftermath of the incompletness theorem proof

This is somewhat of a minor point about the incompletness theorem, but I'm always a little unsure: So one proves that there is a formula which is unprovable in the theory of consideration. Okay, at ...
5
votes
5answers
363 views

Can we decide a conjecture is decidable without knowing a conjecture is correct or false?

Can we decide a conjecture is decidable without knowing a conjecture is correct or false? I asked this question because I assume that the millenium prize problem is already to be decidable, otherwise ...
4
votes
3answers
304 views

Impossibility of certain methods of proof?

There are many methods available for proving a given statement: direct proof, proof by induction, proof by contrapositive, proof by contradiction, etc. In some cases there is an obvious method that ...
3
votes
3answers
452 views

Statements true for all integers but not provable by induction

Is there any examples of statements P(n) such that "for all $n>1$, P(n)" is provable, but P(n)=>P(n+1) is not provable? (without using some mild deformation of "for all $n>1$, ...
3
votes
1answer
154 views

Lengths of proof

Let $f(n)$ be the length of the shortest statement whose shortest proof has length $n$ or more. What are the asymptotics of $f(n)$? With standard symbols and length counted by character. For any ...
4
votes
4answers
551 views

What is the difference between ⊢ and ⊨?

I want to know the difference between ⊢ and ⊨. http://en.wikipedia.org/wiki/List_of_logic_symbols ⊢ means ”provable” But ⊨ is used exactly the same: ...
4
votes
1answer
195 views

How does adding the full second order induction scheme affect the consistency strength of subsystems of second order arithmetic?

Following on from my question about $\omega$-models, I'm interested in the interaction between subsystems of second order arithmetic with restricted induction such as $\mathsf{RCA}_0$ and those which ...
2
votes
1answer
548 views

Proving or disproving expression with implies operators

I'm having a hard time reducing expressions involving "implies" operators. I did some reading about the actual meaning of the "implies" operator and browse for other Q&A on this website; however, ...
7
votes
2answers
275 views

Consistency of PA: why other proofs?

Completeness theorem affirms that a formal first order system is consistent iff it has a model. The FOL number theory(PA) or First Order Arithmetic has a model, which is the natural numbers structure. ...
9
votes
5answers
1k 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
630 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
233 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
91 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
202 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
165 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
241 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
525 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 ...
9
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
1k 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
409 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
269 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
359 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
347 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
404 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
499 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
124 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) ...
5
votes
2answers
925 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
150 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
296 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
135 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
243 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
275 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
451 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
249 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
460 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 ...