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.
40
votes
8answers
2k 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
4answers
1k 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 ...
109
votes
13answers
4k 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 ...
24
votes
2answers
827 views
Proof by contradiction vs Prove the contrapositive
What is the difference between a "proof by contradiction" and "proving the contrapositive"? Intuitive, it feels like doing the exact same thing. And when I compare an exercise, one person proofs by ...
9
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 ...
6
votes
3answers
326 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 ...
6
votes
1answer
320 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; ...
3
votes
4answers
307 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:
...
21
votes
6answers
1k 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 ...
11
votes
4answers
378 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 ...
11
votes
6answers
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 ...
4
votes
1answer
100 views
Tricks for Constructing Hilbert-Style Proofs
Several times in my studies, I've come across Hilbert-style proof systems for various systems of logic, and when an author says, "Theorem: $\varphi$ is provable in system $\cal H$," or "Theorem: the ...
6
votes
1answer
171 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 ...
5
votes
2answers
250 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 ...
3
votes
0answers
179 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 ...
2
votes
3answers
191 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 ...
1
vote
0answers
50 views
Examining every mathematical result in purely formal, ZFC language.
My main interest is physics. However, being self-taught in mathematics for the most part, my proofs tend to be more intuitive than it is acceptable. Yet, I recognize my inaptitude in rigor, and I ...
1
vote
1answer
228 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 ...
3
votes
3answers
251 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 ...
3
votes
1answer
221 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 ...
2
votes
1answer
76 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 ...
1
vote
3answers
70 views
help for proving an equation by induction
For this equation:
$$-1^3+(-3)^3+(-5)^3+\ldots+(-2n-1)^3=(-n-1)^2(-2n^2-4n-1)$$
how can I prove this by induction?
When I set $n = 1$ for the base case I got:
$$-1^3 + (-3)^3 + (-5)^3 + \ldots + ...
1
vote
0answers
310 views
Consequences of technically proving anything in Coq (exploiting a bug)? [closed]
Technically, it is possible to prove anything in Coq proof assistant http ://coq.inria.fr due to a programming feature (or bug). This seems tractable when validating large proofs. Human analysis may ...
0
votes
1answer
119 views
Löb's theorem and provability
I learned Löb's theorem. As I understanding, if a statement is formed like "I am provable", the statement should be provable.
I want to ask further about Löb's theorem.
There is two sentences, P and ...
