Proof theory is an area of logic that studies proof as formal mathematical objects. If you'd like advice on the presentation of a proof you have in draft, use proof-writing instead. If you'd like feedback on its validity, use proof-verification. If none of the above apply, you do not need a proof-* ...

learn more… | top users | synonyms

49
votes
2answers
1k views

Is it possible to prove a mathematical statement by proving that a proof exists?

I'm sure there are easy ways of proving things using, well... any other method besides this! But still, I'm curious to know whether it would be acceptable/if it has been done before?
13
votes
7answers
2k views

Is a counterexample considered a rigorous proof that a property is not true?

This is my follow-up question to my own query earlier: How can I algebraically prove that $2^n - 1$ is not always prime? Almost half of the answers said that I provided my own proof by giving ...
3
votes
2answers
267 views

Goodstein's theorem without transfinite induction

Is it possible to prove Goodstein's theorem without transfinite induction? Is there such a proof?
7
votes
1answer
2k views

Why can't reachability be expressed in first order logic?

I'm wondering why we can't express graph reachability in first order logic in pretty much exactly the same way we express it in second order existential logic. For SOL, one definition is : 1 . L is ...
4
votes
1answer
96 views

Proofs whose length depends on the input

This may be a question from proof theory, but I'm not sure, since I don't know any proof theory. What I will be asking about is what happens, if the length of a proof isn't fixed: I'm going to present ...
222
votes
15answers
10k views

Can every proof by contradiction also be shown without contradiction?

Are there some proofs that can only be shown by contradiction or can everything that can be shown by contradiction also be shown without contradiction? What are the advantage/disadvantages of proving ...
8
votes
1answer
230 views

Are coinductive proofs necessary?

I've been exploring corecursion in Coq (specifically, infinite streams of natural numbers) lately and so far any coinductive predicate I've constructed and its coinductive proof can be transformed ...
0
votes
2answers
237 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
237 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 ...
18
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
158 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, this ...
2
votes
1answer
180 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
786 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 ...
4
votes
3answers
707 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
183 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 ...
5
votes
3answers
438 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
391 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 ...
5
votes
3answers
358 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
595 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$, P(n)"=>"P(n)=>P(n+...
3
votes
1answer
165 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 ...
7
votes
4answers
2k 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
209 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
676 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, ...
8
votes
2answers
317 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. ...
11
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 ...
7
votes
1answer
778 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 ...
3
votes
3answers
203 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
295 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
95 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 numbers....
4
votes
2answers
208 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
171 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
248 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
627 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 $T,\...
10
votes
2answers
2k 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 ...
7
votes
4answers
447 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 ...
2
votes
1answer
149 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
309 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
251 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
428 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
385 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
469 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
184 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: \begin{...
6
votes
3answers
609 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
10k 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
127 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
1k 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 eigenvariable/...
5
votes
1answer
199 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
311 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
138 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. ...