logicpropositional-calculus
In a proof by contradiction, we first assume a proposition $P$ false, then prove some known truth to be false, then that would imply the assumption $P$ should really be true.
Do we really need to first assume the proposition $P$ false?
It seems it's okay to first assume proposition $P =$ true, derive some known truth to be false, then we know $P$ should really be false.
Is it the case??
Thanks
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}$$
Long comment
Maybe, a more lengthy approach can help, considering the case of a single atom $p$.
Let $F$ a formula and let $p$ a propositional symbol occurring in $F$. This means that the formula is a truth-function $F(p)$: for every truth value assigned to $p$, the truth table corresponding to $F$ will outputs a truth value.
But $F$ is a tautology: thus for every assignments of truth values to atoms, the truth table will produce the value TRUE.
Consider now the formula $F' := F[A/p]$, where $A$ is a formula whatever. Irrespective of the "form" of $A$, every assignment will output either TRUE or FALSE as truth value for the formula.
Thus, when $A$ is evaluated to TRUE, we have to consider the lines in the original truth table for $F$ where $p$ is evaluated to TRUE. Due to the fact that $A$ is a tautology, in those lines the formula $F$ has value TRUE; thus also $F'$ will have TRUE in those lines.
But also when in the original truth table for $F$ the atom $p$ is evaluated to FALSE, the corresponding lines for formula $F$ have value TRUE; thus also $F'$ will have TRUE in those lines.
The argument can be iterated, taking into account that a formula is an expression of finite length and thus only a finite number of atoms occurs into it.
Best Answer
We are considering the two methods of proof:
(1) To prove $P$, we assume $\neg P$ and derive a contradiction.
(2) To prove $\neg P$, we assume $P$ and derive a contradiction.
Both methods are valid, although in general (1) requires the Law of Excluded Middle to conclude $P$ from $\neg\neg P$. In my opinion, only method (1) is properly called "proof by contradiction." Method (2) is simply the ordinary way of proving a negation. Indeed, the negation $\neg P$ is sometimes defined as a shorthand for the implication $P \implies \bot$.
EDIT: According to Wikipedia both methods (1) and (2) are properly called "proof by contradiction."