[Math] Can we continue a proof by contradiction even if we get to a contradiction

Question

consider the example below :

our set of premises are $\{ a , b , a \to c , b \to a \}$ and we want to prove $c$ is true .

someone has used proof by contradiction to prove this .

the proof :

1. assume $\lnot c $ is true

2. we also know $ \lnot c \to \lnot a $ is true so

3. $\lnot a$ is true. since we know $a$ is also true

4. then $\lnot a \land a $ is also true

5. but we also know that $\lnot a \land a$ ia false

6. so we know $(\lnot a \land a) \to \lnot b$ is true

7. so from 4 and 6 $\lnot b$ is true

8. so from 7 we know $\lnot b$ is true and we know $b$ is true

9. so $\lnot b \land b$ is true so we get to a contradiction .

since my argument was a valid one then one or more of my assumptions must be false since my only assumption (excluding axioms and definitions included in the premises ) is $\lnot c$ then $c$ is true .

the question is :

is the above proof a valid mathematical proof .

can a proof by contradiction continue and get to a second contradiction (line 9) based on it's first contradiction (line 5) ?

my teacher says even in the case of a proof by contradiction non of the steps should be a contradiction (except the last one when the proof ends ) !?

EDIT :

assume we use the proof by contradiction technique . it means we add the negation of the proposition we want to prove ($\lnot p$) to our assumptions ($A$) (the set of axioms and definitions we use in the specific field we want to use the proof) and we add all theses to our logical system $\Gamma$ (I'm mainly considering propositional and predicate logic) so we have

$$ \Gamma' = \lnot p \cup A \cup \Gamma $$

now if $p$ was provable from $A \cup \Gamma$ this makes $\Gamma'$ an inconsistent logical system in which we have no model for it meaning there is no interpretation which gives value True to all the sentences in $\Gamma'$ (in the semantic sense)

BUT we can assign each proposition a true or false value with our semantic rules (for example truth tables) but since we are in an inconsistent system and every proposition is provable in this system we shouldn't expect all the proven propositions to have value true with respect to our semantic valuation (or any other since there is no model for this system) . in other words an inconsistent system is not sound (the meaning of the soundness of a system is different from the soundness of an argument that we will discuss later)!

validating the above proof by means of syntax

one way of talking about a proof by contradiction is to use a system of proof based logical system (by which i mean something like a Proof calculus )
like what Taroccoesbrocco did below .

in this way we can define a valid mathematical (even a logical) proof as a proof that uses the set of definitions and axioms and possibly some previously proven theories (in the specific area of math we are interested in) and goes from one step of the proof to the other only by using the rules of proof calculus it uses .

in this way there is no problem in continuing a proof by contradiction even if we get to a contradiction as demonstrated by Taroccoesbrocco .( in this case natural deduction is the proof calculus we use and by the use of the rule EFQ we can continue the proof )

[1] validating the above proof by means of semantics

Here I want to defend the semantic proof I gave above.

If an argument is based on a contradiction it is a valid argument, regardless of whether it follows the rules of logic we use or not!

By definition an argument is valid iff, if the premises are true the conclusion is also true (i.e. every model of premises is also a model for the conclusion) but in the case of a contradiction it is impossible for our premise(s) to be true (there is no model for the premises) so by definition this is a valid argument.

In a proof by contradiction we know our system was consistent before adding $\lnot p$. We add the negation of the proposition we want to prove to our assumptions and logical system and ask whether the system remains consistent or not (i.e. is there a model that gives value true to $ \Gamma' = \lnot p \cup A \cup \Gamma $) if the new system becomes inconsistent (there is no model) then we know that our assumption was wrong and every model for $ A \cup \Gamma $ is also a model for $p$ so p follows from them!

(Note in the semantic viewpoint $\Gamma'$ is the set that contains propositions $\lnot p \cup A$ and all the sentences that are semantically derivable from them. For example via a truth table if we know $t \to s$ and $t$ are both true then $s$ must also be true.)

So the proof above considers the logical system $ \Gamma' = \lnot c \cup A \cup \Gamma $ and assumes there is a model for it. if a model really exists then it must give value true to $\lnot c \cup A$ and all their semantic derivations.
but as we continue the proof we want to give value true to both $\lnot b$ and $b$ and thus a true value to $\lnot b \land b$ but from our definition of a model (and semantic rules ) $\lnot b \land b$ is always false. So there does not exist a model for $\Gamma'$. So $p$ is proven.

In this way we can define a valid mathematical (even a logical) proof as a proof that uses the set of definitions and axioms and possibly some previously proven theories (in the specific area of math we are interested in) and gives them value true and goes from one step of the proof to the other only by using the rules of semantics (e.g. truth tables).

The apparent problem some users pointed out was that from step 5 the argument is based on the contradiction $\lnot a \land a$ being true. But there is no problem with that since we have deduced it in a semantic proof from previous steps and all the next steps are like that too. So the proof is a valid one.

Another apparent problem with proof is that it is unsound if we continue in step 5.

The definition of sound argument is one that is valid and all it's premises are true. ue to this definition the above argument is obviously and unsound one .
since some of it's premises are always false (contradictions) .

BUT this is independent of weather the proof is continued passed stage 5 or not because in the premises of our argument in step 4 we have both $\lnot a$ and $a$ so it is impossible for the premises to be true.

There is no problem when an argument becomes unsound in a proof by contradiction. Since at some stage of the proof and for some proposition $t$ we derive $\lnot t$ and in another step we derive $t$ so we always have these two contradictory propositions among our premises. Thus actually a proof by contradiction always contains this unsound argument.

At the end it seems to me that the ideas I gave in the syntax (proof calculus based) version of the proof seem more rigorous than the ones in the semantic version. I would be glad to get some ideas (specially about the semantic argument!).

Answer 1

Differently from Mauro Allegranza and Graham Kemp, I think that your proof is formally correct, even if it is unnecessarily tricky, inelegant and non-efficient.

I formalized your argument in natural deduction (see below), so this proves that your proof is correct.

Let $\pi_0$ be the derivation of $\lnot c \to \lnot a$ from $\{a \to c\}$ (this correspond to the step 2 of your proof)

Let $\pi_1$ be the derivation of $\lnot b \land b$ from $\{b, a, a \to c, \lnot c\}$ (this correspond to the steps 1, 3-8 of your proof)

Then, the derivation of $\pi_2$ of $c$ from $\{a, b, a \to c\}$ corresponds to your whole proof.

PS: To reply to Graham Kemp: I don't think that "once you've obtained a contradiction the proof has ended", I mean the proof is not forced to be ended. If you has proved that $\neg c, \Sigma \vdash \bot$ you can apply RAA (reductio ad absurdum) and get

$$\dfrac{\neg c, \Sigma \vdash \bot}{\Sigma \vdash c}$$

but you can also apply EFQ (ex falso quodlibet) and get $$\dfrac{\neg c, \Sigma \vdash \bot}{\lnot c, \Sigma \vdash d}$$ for any formula $d$, or you can also apply $\lnot_I$ (introduction of negation) and get $$\dfrac{\neg c, \Sigma \vdash \bot}{\Sigma \vdash \lnot\lnot c}$$