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

Question

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...

Answer 1

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.

Answer 2

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$.