How to justify that $\neg A \vee A$ has a sense?

Question

We do substitutions from the set of axioms that we have to prove some statement.

I can't understand what actions we should do to go from (1) to (2). What kind of substitution should be made?

The screenshot is from Opera Magistris v4 page 143 https://archive.org/details/OperaMagistris/page/n143/mode/2up?view=theater

Answer 1

Huh! This is a (horribly!) defective proof.

First, we know it is defective, since line 2 is not a logical truth (tautology), and in this system we only prove logical truths, meaning that every line need to be a logical truth by itself.

I am pretty sure that the author meant line 2 to be $A \to (A \lor A)$. Indeed, that statement would be the result of substituting the formula $A$ for the letter $B$ in line 1.

But, this is not the only thing that is going wrong in this proof:

The author lists 7 and A1 as the justification for line 8, but I am not exactly sure how the author intends to accomplish that. I think that the author thinks that given that A1 says that $(A \lor A)$ implies $A$, the author seems to want to use this to replace $A \lor A$ with $A$ in line 7. However, there is no rule that allows you to do such a thing, and in fact, that could easily lead to invalid inferences! For example, just because $A$ implies $B$ does not mean that $A \to C$ implies $A \to C$.

Third, the author claims that PA5 is Axiom 5 from Russell and Whitehead, but it is not that at all. In fact, the A5 listed here is not even a logical truth! The right axiom is:

$$PM5. (B \to C) \to ((A \lor B) \to (A \lor C))$$

but that brings me to:

Fourth: line 3 is neither an instance of the defective A5, nor of PM5.

Instead, line 4 is an instance of PM5.... but I see no way it can be obtained from line 3

Fifth, the author says that line 9 is obtained through Modus Ponens on line 8, but Modus Ponens requires a second line, which the author does not indicate. However, that other line would either have to be $A \to A$, or $((A \to A) \to (A \to A)) \to (A \to A)$, neither of which occur earlier in the proof. What would make sense, is to do a Modus Ponens on A1 and line 7.

So .. here is what a proper proof would have looked like:

1. $A \to (A \lor A) \ \text{(instance of A2)}$
2. $((A \lor A) \to A) \to ((\neg A \lor (A \lor A)) \to (\neg A \lor A)) \text{(instance of PM5)}$
3. $((A \lor A) \to A) \to ((A \to (A \lor A)) \to (A \to A)) \text{(3 and property of $\to$)}$
4. $(A \lor A) \to A \ \text{(instance of A1)}$
5. $(A \to (A \lor A)) \to (A \to A) \text{(3 and 4, Modus Ponens)}$
6. $A \to A \text{(1 and 5, Modus Ponens)}$
7. $\neg A \lor A \text{(6 and property of $\to$)}$

I think this is what the author intended to do, but it ends up looking nothing like it. What a mess!! Please stop using this source!!

Answer 2

As per the answer above, Ax.5 is simply wrong.

Using the correct one, with the substitution: $\lnot A$ in place of $A$, we have:

1. $(B→C) → ((\lnot A∨B)→(\lnot A∨C))$,

that is equivalent [by the definition of $\to$] to:

2. $(B \to C) → ((A \to B)→(A \to C))$.

Applying the substitution: $A \lor A$ in place of $B$; $A$ in place of $C$, we get:

3. $((A \lor A) \to A) \to [(A \to (A \lor A))\to (A \to A)]$.

Using Ax.1 and Modus Ponens, we get:

4. $(A \to (A \lor A))\to (A \to A)$.

Using Ax.2 [with the substitution: $A$ in place of $B$] and MP we get:

5. $A \to A$.

Finally, we have to rewrite is using the def. of $\to$ to get:

$\lnot A \lor A$.