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

  • $\begingroup$ 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. $\endgroup$ – Mauro ALLEGRANZA Nov 8 '18 at 19:32
  • $\begingroup$ 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. $\endgroup$ – Mauro ALLEGRANZA Nov 8 '18 at 19:34
  • $\begingroup$ 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? $\endgroup$ – 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.

  • $\begingroup$ 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 $\endgroup$ – 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$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.