# Proof for $\lor$ Elim: rule in Soundness Theorem

So far I have been told to assume the line is invalid and then arrive at a contradiction.

Suppose the first invalid step derives the sentence $$C$$ by an application of $$\lor$$ Elim to the sentences $$A\lor B$$ and $$A$$ and $$B$$ appearing earlier in the proof. Let $$P_1,\ldots,P_n$$ be a list of all the assumptions in force at $$C$$. If this is an invalid step, $$C$$ is not a tautological consequence of $$P_1,\ldots,P_n$$.

Since $$C$$ is the first invalid step in $$p$$, we know that $$A\lor B$$, $$A$$ and $$B$$ are all valid steps, that is, they are tautological consequences of the assumptions in force at those steps.

Since $$\mathcal{F}_T$$ allows us to cite sentences only in the main proof or subproofs whose assumptions are still in force, we know that the assumptions in force at steps $$A\lor B$$, $$A$$ and $$B$$ are also in force at $$C$$. Hence the assumptions for those steps are among $$P_1,\ldots,P_n$$.

But I'm not sure how to carry this on...

• If so you are proving it by contradiction, i.e. you are assuming that the rule is not sound, i.e. that the rule produce a conclusion $C$ which is not a log cons of the premises. – Mauro ALLEGRANZA Nov 8 '18 at 19:32
• But the proof is by induction on the lenght of the derivation, and this means that $A \lor B$ and $A$ and $B$ are all log cons of the open assumptions. – Mauro ALLEGRANZA Nov 8 '18 at 19:34
• yes I think the first comment is correct. I have the soundness theorem and I want to prove the twelve rules. Do you know how this is done? Is proof by contradiction not a good approach? – MRT Nov 8 '18 at 19:37

There's no compelling reason to use proof by contradiction. The rule consists of a valid one in intuitionstic positive logic, so like anything else in intuitiionistic positive logic it can get proved without the use of proof by contradiction.

Suppose that (A $$\lor$$ B) is true, (A$$\rightarrow$$C) is true, and (B$$\rightarrow$$C) is true also. By the truth table for (A $$\lor$$ B) one of two cases gets satisfied. A holds true consists of one case, and B holds true for the other case. Suppose that A holds true. Then, by modus ponens C will follow. Similar reasoning shows that C holds for the other case. Since that exhausts all cases, C follows from the set of premises.

Note the above does NOT use $$\lor$$ in the reasoning. $$\lor$$ consists of an objective level construct, and is not as comprehensive as meta-linguistic case exhaustive analysis, since case exhaustive analysis could have many more cases than two, while $$\lor$$ as an objective level connective, defined by the definition of a well-formed formula, consists of a binary connective.

• Ahh I had three examples of other rules and they all involved a contradiction and then went on to say that the rest can be solved in the same way. To assume an invalid claim and then derive a contradiction by assuming that all the lines before are valid – MRT Nov 9 '18 at 8:56

Sketch of the proof

We have a derivation $$\mathcal D$$ of $$A \lor B$$ with assumptions in $$\Delta$$.

We have a derivation $$\mathcal D_1$$ of $$C$$ from $$A$$ with assumptions in $$\Delta_1$$ and a derivation $$\mathcal D_2$$ of $$C$$ from $$B$$ with assumptions in $$\Delta_2$$.

Let $$\mathfrak A$$ a model of $$\Delta \cup \Delta_1 \cup \Delta_2$$.

By induction hypothesis : $$\Delta \vDash A \lor B$$.

Two subcases : either $$\mathfrak A$$ is a model of $$A$$ or it is a model of $$B$$.

In the first subcase by induction hypothesis ($$\Delta_1 \vDash C$$) $$\mathfrak A$$ is a model of $$C$$.

In the second subcase by induction hypothesis ($$\Delta_2 \vDash C$$) $$\mathfrak A$$ is again a model of $$C$$ .

In both cases $$\mathfrak A$$ is a model of $$C$$.