# Proving existence of a proof

1. Oct 2, 2008

### ila

Hi, I don't know if this has been discussed (or is trivial or even silly). I was wondering sometimes there is reliance on indirect proofs in mathematics. I was wondering can it be proven in any case where an indirect proof exists that a direct proof does not?

2. Oct 2, 2008

### arildno

I don't think your question is either trivial, or silly. I'm afraid that I don't know the answer, if there is one, hopefully, someone like Hurkyl or HallsofIvy might provide one.

3. Oct 2, 2008

### Tzar

I agree it is a very interesting question but depends on what we mean by "direct" proof. What makes a proof direct or indirect?

Certainly in mathematics one can prove the existence of certain objects and constructions without actually constructing them. In certain proofs, a heavy reliance on the axiom of choice can certainly lead to a an existence proof without any hope of actually constructing the example "hands on". (for example see the Banch Tarski paradox http://en.wikipedia.org/wiki/Banach%E2%80%93Tarski_paradox" [Broken])
I'm not sure if an example like this would be classified as an indirect proof though.

Last edited by a moderator: May 3, 2017
4. Oct 2, 2008

### Hurkyl

Staff Emeritus
I concur with Tzar's comment -- the question itself is somewhat vague. But I will try to give an answer that I think is in the spirit of the question!

Intuitionistic logic does not use all of the rules of inference you use in Boolean algebra. A couple particular things is that (P or (not P)) isn't a tautology, and P is not equivalent to not (not P).

In intuitionistic logic, you can still use the law of noncontradiction to prove a negative. In other words, if you devise a proof
P ==> Q and (not Q)​
then you can validly infer (not P). But if you were to try and prove a positive by deriving
(not P) ==> Q and (not Q)​
then you can only infer (not (not P)). In intuitionistic logic, this does not allow us to infer P!

A specific example of an interesting theorem that cannot be proven in intuitionistic set theory is this:
There exists a discontinuous function​
(where 'function' means a real-valued function whose domain is the reals)

In fact, there are models of intuitionistic set theory in which every such function is actually continuous.

5. Oct 2, 2008

### CaptainQuasar

Hmm, that's an interesting idea. You mean something like inductive versus deductive?

It's reminiscent of http://en.wikipedia.org/wiki/Gödel's_incompleteness_theorem#First_incompleteness_theorem":
(emphasis mine)

Last edited by a moderator: Apr 23, 2017
6. Oct 2, 2008

### Tzar

I've always struggled to understand that statement made by Godel. It makes sense (to me) that you can always ask a question which can not be proved nor disproved by your axioms. However, how can you claim a statement is true, if it is not provable in your theory???

7. Oct 2, 2008

### CaptainQuasar

Oh, I should have mentioned, I have no clue about what it actually means either, nor have I even tried to follow Gödel's proof. I didn't mean to be name-droppy, I was just pointing out the resemblance to ila's idea.

I see what you're saying, Tzar, and I've had the same thoughts; it seems to violate the basic concept of mathematical systems as being foundations upon Euclidean-geometry-like axioms. Maybe it has to do with the definition of "consistent, effectively generated formal theory", or perhaps the proof of the incompleteness theorem itself serves as the proof of the statements in question.

8. Oct 2, 2008

Godel's result states that in any axiomatic system there will always be questions which cannot be answered (problems that cannot be resolved) within that system

9. Oct 2, 2008

### CaptainQuasar

Hmmm, I noticed that in Wikipedia there's a footnote qualifying the quotation I posted above:

10. Oct 2, 2008

### Tac-Tics

It's misleading to say "there is a statement which is true, but not provable from within the theory". Truthiness is relative to the set of axioms you're working with. A system with more axioms might in fact be able to prove it, but no necessarily so!

It's more appropriate to say those statements can be neither be proven nor disproven in your formal system. They are not true. They are not false. They don't even show up to the party!

11. Oct 2, 2008

### Count Iblis

http://www.umcs.maine.edu/~chaitin/eesti.html" [Broken]

We all know what computer programs are. We define an elegant program to be a program such that no smaller program gives exactly the same output.

http://www.umcs.maine.edu/~chaitin/eesti.html#18" [Broken]

So, you encounter Gödel every day if you ask why downloading a certain program takes such a long time and if it was really not possible to have a significantly shorter program that would do the same job. Because if it is not possible, then the proof of that fact doesn't exist.

Last edited by a moderator: May 3, 2017
12. Oct 2, 2008

### Ben Niehoff

An indirect proof, as I understand it, is a proof that relies on reductio ad absurdum. That is, a non-constructive proof.

If a fact can be proved, we may always find an indirect proof of it. The proof of this is trivial:

1. Premise: S can be proved. Call its proof P(S).
2. Begin a proof of S by contradiction: Assume ~S.
3. But P(S) is a proof of S; therefore, S.
4. This gives (S and ~S), a contradiction.
5. Therefore the assumption in (2) is false.
6. Therefore S.

So, given that S has a proof, we can construct a (rather trivial) indirect proof of S.

However, given that S has a proof, we cannot necessarily find a direct proof of S. As someone else mentioned, there are many theorems in math on the existence of objects that cannot be directly constructed.

Therefore, when first attempting to prove some fact, you will probably have the most success by attempting a proof by contradiction. However, the proof you find might not be very satisfactory; i.e., it might not give you much intuition as to why the result is so.

13. Oct 2, 2008

### Dragonfall

Suppose we can prove that a proof exists without exhibiting it. Then can we prove THAT without exhibiting it? This would be something akin to "meta" or "2nd order" math/logic. It may have to do with the fact that we'd need to quantify over all proofs.

14. Oct 2, 2008

### Hurkyl

Staff Emeritus
First, people dis category theory... then people get Gödel wrong...

First off, the notion of axioms, provability, logical deduction -- these do not deal with 'truth'. Truth only comes into play when you decide to use a 'truth valuation' -- a function that assigns to each logical statement a 'truth value'. This happens most often when you consider a specific 'structure', and you 'interpret' logical statements as saying something about your structure, calling a statement 'true' iff it's a correct statement about your structure.

(Assuming number theory is consistent) A 'model' of number theory is a structure for which each of the axioms of number theory are correct. In this model, every statement of number theory is either true or false. Any statement that can be proven will be true, and any statement that can be disproven will be false. Those that can be neither proven nor disproven could go either way.

Logical theories can be 'complete' -- be such that all logical statements are either provable or disprovable. It's easy to construct trivial examples. For example, consider any model of number theory; we can take the set of all correct statements about this model and use them as the axioms for a logical theory. Gödel's incompleteness theorem says that if we use this trick, there doesn't exist any algorithmic method for identifying whether a statement is or isn't an axiom.

There are nontrivial examples of complete theories. (First-order) Euclidean geometry is a wonderful example (see Tarski's axioms for Euclidean geometry). Equivalently, the theory of real number arithmetic is also complete (see the axioms for a real closed field). Gödel's theorem, in this case, tells us that these theories are incapable of talking about number theory.

More explicitly -- you cannot use the arithmetic real numbers to ask question
Given a real numebr x, is it an integer?​

The basic idea of Gödel's proof is actally somewhat straightforward, and comes in several guises. The one I can state off the top of my head goes as follows:

* Describe how to do text processing with integer arithmetic
* Show how to use text processing to simulate the operation of a computer
* Write down the condition Halt(p) that expresses whether the program p ever finishes
* Write a program that is capable of computing Halt(p) whenever Halt(p) is provable or disprovable
* Invoke the fact, in general, the halting problem is not computable

15. Oct 3, 2008

### HallsofIvy

The specific question asked here can easily be answered in the negative: there exist very simple statements that can be proven both directly and indirectly.

A more interesting question is whether any statement that can be proved indirectly must have a direct proof. I think, but am not certain, that the answer to that is also "no". You might want to google on "constructive mathematics", a logical position that rejects indirect proofs entirely.