Can proof by contradiction work without the law of excluded middle?

Question

I was recently thinking about the validity of proof by contradiction. I’ve read for the past few days things on intuitionistic logic and Godel’s theorems to see if they would provide me answers to my questions. Right now I still have questions lingering (perhaps related to the new material I read) and was hoping to get some answers

(WARNING: you are about to proceed to read content with very confused foundations in logic, take everything with a grain of salt, its suppose to be a question and not an answer, there are many misunderstandings in it).

I think my main question is, once we showed that not A leads to some contradiction, so not A must be false, then we go and conclude that A must be true. That part sort of makes sense (especially if I accept the law of excluded middle as something that makes sense) but what bothers me is sort of how proof by contradiction actually occurs. First we start with not A and then we just apply axioms and rules of inferences (say mechanically) and see where that takes us. It usually reaches a contradiction (say A is true or $\neg \varphi$ and $\phi$ is true). The we conclude that not A must be false, so A is true. Thats fine. But my question is, what sort of guarantees do formal systems have that if I applied the same process but started with A that I would not also get a contradiction there? I think that there is some hidden assumption going on in proof by contradictions that if similarly did the same process in A one would not reach a contradiction, what sort of guarantees do we have that would not happen? Is there a proof that’s impossible? In other words if I had a Turning Machine (TM) (or super TM) that went forever, that tried all the logical steps from every axiom starting from the supposedly true statement $A$, what guarantees that it does NOT HALT due to finding a contradiction?

I then made some connections with my past question with Godel’s incompleteness theorem that goes something like this:

A formal system F that con express arithmetic cannot prove its own consistency (within F).

This basically made it clear to me that if thats true then consistency i.e. guaranteeing that A and not A won’t happen is impossible. Therefore, it made it seem to be that proof by contradiction just implicitly assumes that consistency is guaranteed somehow (otherwise why would it just go ahead and conclude that A is true by proving not A is not possible if it didn’t already know that consistency and contradiction where fine, for any pair of statement A and not A)? Is this incorrect or did I miss something?

Then I thought, ok lets just include in our axioms the rule of excluded middle and then all problems are solved. But then I realized, wait if we do that we are just defining the problem away instead of dealing with it. If I just force my system to be consistent by definition that doesn’t necessarily mean it actually is consistent…right? I’m just trying to make sense of these ideas and I am not quite sure what to do but this is what I am realizing after a few days of reading stuff and watching videos in nearly every aspect of these concepts, contradiction, exclusive middle, intuitionist logic, Godel’s completeness and incompleteness theorems…

Related to this, it seems that its essentially impossible to actually directly prove that something is false without the rule of excluded middle (or contradiction). It seems that proof systems are good at proving true statements but to my understanding are incapable of directly showing that things are false. Perhaps the way they do it is more indirectly with contradiction (where they show something must be false or bad things happen), or excluded middle (where knowing the truth value of only one A or not A gives us the truth of the other) or providing counter examples (which basically shows that the opposite is true so indirectly uses law of excluded middle). I guess perhaps I really want a constructive proof that something is false?

I think if I could know that if I prove not A is false (say I accept contradiction) then that it really is ok and I don’t need to apply all the inference rules and axioms infinitely on A and I am guaranteed that A won’t reach a contradiction. If that were true then I think I could accept proof by contradiction more easily. Is this true or do Godel’s second incompleteness guarantee I can’t have this? If I can’t have this then, what puzzles me is how its even possible of so many years of mathematicians doing maths that we have not found a inconsistency? Do I need to rely on empirical evidence of consistency? Or for example, I prof F is consistent by showing superF proves F but since I will never actually need superF and just F, then I can’t be content that truly works?

---

I just noticed that my complaint also generalizes to direct proofs. Ok so if I did a direct proof of A then I know A is true...but how do I know that if I did a direct proof of not A that I wouldn't also get a correct proof? Seems the same question just slightly different emphasis....

Answer 1

You asked (I am making your question a bit crisper): "What formal guarantee is there that it cannot happen that both $\lnot p$ and $p$ lead to a contradiction?" You seem to worry that if logic is inconsistent, then proof by contradiction is problematic. But this is not the case at all.

If logic is inconsistent then proof by contradiction is still very much a valid rule of reasoning, but so is its negation, and the rule which says that from $1 + 1 = 2$ we can conclude that you are the next pope. An inconsistency in logic does not invalidate anything: quite the opposite, it validates everything!

There is another possible source of confusion: the title of your question may be read as implying that the law of excluded middle says that logic is consistent. That is incorrect. Consistency of logic amounts to “it is not the case that both a statement and its negation have proofs”, while excluded middle is the rule which allows us to prove statements of the form $p \lor \lnot p$.

---

Supplemental: I do not understand why this question is generating so much discussion. I have trouble understanding what the dilemma actually is, and as far as I can tell, the question arises from some sort of misunderstanding. If someone can elucidate the question, I will be grateful. Also, I would just like to draw attention to the following points:

1. Proof by contradiction and excluded middle are equivalent to each other, and so the title, as written, is non-sensical. Of course we cannot have one without the other, they are equivalent.

2. From what I can understand from the lengthy discussion in the question, the OP seems to be saying, or worrying, that an inconsistency in logic invalidates a proof. This is false, as I pointed out above. I would appreciate some sort of a response from the OP: can the OP see how an inconsistency in logic (i.e., being able to prove everything) does not invalidate any proofs?

3. I find it likely, but cannot really tell for sure, that the OP thinks that the law of excluded middle states that it is impossible for both $p$ and $\lnot p$ to hold (with a formula: $\lnot (p \land \lnot p)$). This is not excluded middle. It is sometimes called the law of non-contradiction, and it is provable (without excluded middle).

4. The OP thinks it is "impossible to directly prove that something is false without excluded middle". He is confusing proof of negation and proof by contradiction, which are not the same thing. The linked post has plenty of examples of constructive proofs that something is false. In fact, most proofs that something is false found in textbooks are already constructive.

5. Gödel's incompleteness is dragged in for a reason that I can discern. Gödel's incompleteness provides a sentence $G$ such that neither $G$ nor $\lnot G$ is provable. This does not imply that $G \lor \lnot G$ is unprovable (it is, by a simple application of excluded middle)! Neither does it imply that $\lnot G \land \lnot\lnot G$ holds, or some such. So how is Gödel's incompleteness relevant here?

P.S. I apologize for the previous version of the supplemental which was rude.

Answer 2

There are many interesting philosophical points that your post touches on.

Consistency of Boolean logic

The issue of consistency of proof theory in classical logic isn't as dire as you make it out to be. It basically reduces to the following:

We can define Boolean logic as a collection of logical operations functions on the truth values 1 and 0. But how do we know that 0≠1?

(note that I'm simply using 0 and 1 as abstract symbols for the two truth values; in particular, I am not assuming any notion of integer here)

We, of course, don't know that 0 and 1 are different. But Boolean logic is so ridiculously simple that rejecting this possibility is an extreme level of skepticism.

But classical propositional logic reduces to this. Recall that we can assign Boolean values to the atomic propositions in any fashion, and this extends to assigning a value to all propositions that can be constructed from the atomic ones.

The statement "from P you can deduce Q" is literally just an ordering relation; it means the same thing as the claim that "v(P) ≤ v(Q) holds for every function v assigning truth values to the atomic propositions".

The rules of inference for propositional logic are precisely the properties for working with the ordering ≤. Proof by contradiction, in particular, is the observation that if P ≤ 0, then P = 0.

And going back to your issue... if we knew both P ≤ 0 and ¬P ≤ 0,t hen after plugging in truth values we would ultimately conclude that 0=1; that true and false mean the same thing.

So, if you have confidence that "true" and "false" mean different things, then you should have similar confidence in the consistency of Boolean logic.

Proof by contradiction in intuitionistic logic

One should take careful note that proof by contradiction is better formulated as:

• If you can derive contradiction from P, then conclude ¬P

In fact, one might outright define negation to be the connective with this property. E.g. in Heyting algebra you will usually see ¬P defined to mean P→0.

Note, in particular, the special case

• If you can derive contradiction from ¬P, then conclude ¬¬P

What you described as "proof by contradiction" comes from identifying ¬¬P with P. Intuitionistic logic does not assume these are equivalent.

Consistency as a formal contract

There are more computational formalisms for encoding logic; see simply typed lambda calculus, dependent types, and in particular the "propositions as types" paradigm.

Without going into detail, contradiction is basically treated as formal contract. There is a type, which I will call 0, and there is the contract "these functions cannot be used to construct an element of type 0".

If such a system is so bold as to allow you to construct a function T → 0, then if it is really holding to the contract, it means it is similarly impossible to construct any objects of type T. This is a computational viewpoint on what a proof by contradiction means.

Ultimately this isn't much different than, for example, a C function that returns a pointer promising not to return a null pointer, or a C++ function promising not to throw an exception.

And going full circle, back to classical logic, that's really what we're doing.

We are offered formal contracts, such as "from Peano's axioms, the rules of inference will not allow you to derive a contradiction". If this contract really is upheld, then if you were able to show that ¬P implies a contradiction, then P cannot also imply a contradiction.

And if it were possible to violate the contract, we would simply say "Peano's axioms are inconsistent".

Answer 3

I think your question boils down to "when doing formal verification with some sort of formal logic, what sort of guarantee do I have that the logic is consistent?". And the answer is: none. That's something you have to assume. Formal verification doesn't eliminate all assumptions; it just helps you be clearer about what you are assuming, and maybe helps you ensure that you start from assumptions that seem reasonable.

If you work within a standard logic, generally most people are happy to assume the logic is consistent, even if they don't have a proof of that fact. It's true that we might someday discover that the logic is actually inconsistent... but most people believe this is not very likely.

In some cases one can prove that a logic is consistent, but that requires using another more powerful logic, where we have to assume that the second logic is consistent, so we still are left having to make some assumptions (assume that some logic is consistent). This could be taken as evidence that the first logic is likely consistent, if you believe that the second logic is likely consistent, but the reasoning has to bottom out somewhere -- there are some things we have to just assume, and cannot prove.

See, e.g., Hilbert's second problem and this discussion of the consistency of ZFC (and this and this and this and probably many more).

Answer 4

When used to guarantee the truth of a formal statement, all proofs implicitly assume the consistency of the system that they're based in. This is because if the system is inconsistent, the entirety of the system is broken, and all the work we did in that system is basically trash.

Because we can't prove that any system (or at least any complex system) is consistent within the confines of that system, we have to take it as an empirical truth rather than a formally provable truth. Basically, if mathematicians spend a long time working with a formal system and no contradiction is ever discovered, then that is empirical evidence in favor of the consistency of the system. In addition, we may use a more powerful system to prove the consistency of the system we're working with (although the consistency of this more powerful system would still be empirical - the buck stops somewhere).

At it's core, the situation in mathematics is identical to that of science. We build mathematics based off theories that seem correct based on all the information we have available about those theories, and like in science, you can't prove that a theory is correct; you can only prove it incorrect.

When we first started trying to base mathematics in set theory, we actually discovered that our first formulations of set theory were inconsistent because they allowed things like "let $S$ be the set of all sets that do not contain themselves." We had to throw out these formulations.

No matter which system of axioms we choose to base math on, there's always a danger that we'll discover a contradiction in that system. This is exactly why mathematicians don't introduce new axioms into mathematics: each new axiom has a chance of being incompatible with the axioms already in use, and all work that uses the new axiom would have to be completely re-evaluated.

Addendum: When I talk about a statement being true for a given system I mean that it cannot be disproven within that system if that system is consistent.