# Tagged Questions

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-* ...

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?
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 ...
267 views

### Goodstein's theorem without transfinite induction

Is it possible to prove Goodstein's theorem without transfinite induction? Is there such a proof?
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 ...
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 ...
10k views

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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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+...
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 ...
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: ...
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 ...
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, ...
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. ...
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 ...
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 ...
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. ...
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 ...
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....
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 ...
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 ...
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 ...
627 views

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/...
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 ...