Proof expression $$ ((\neg C \vee B) \wedge ( A \rightarrow C) \wedge (B \rightarrow D) )\rightarrow \neg A \vee D $$

Attempt to proof

$$ 1. B \text{ (premise) } $$ $$ 2. B \rightarrow D (\text{premise}) $$ $$ 3. A \rightarrow D (\text{premise}) $$ $$ 4. D (\text{modus ponens 1,2}) $$ $$ 5. \neg A \vee D (\text{add 4}) $$

Is this correct?

  • 2
    $\begingroup$ First, you need to specify which proof system you're using. That said, your current proof (sketch) would work if you had $B$, but you don't have $B$; you only have $\neg C\lor B$. Also, your uses of rules should specify the subderivations they are based on, e.g. a use of Modus Ponens should specify which earlier established results you're using, e.g. "modus ponens, 1,2" and similarly for "Add". $\endgroup$ – Derek Elkins left SE May 10 '19 at 23:37
  • $\begingroup$ $(\neg C \vee B)$ is equivalent to $( C \rightarrow B)$. Then use the chain of implications to go from $A$ to $D$. $\endgroup$ – Bernard Massé May 10 '19 at 23:51

So let's try this one step at a time. You wish to show the following implication is true:

$$((\neg C \vee B) \wedge ( A \rightarrow C) \wedge (B \rightarrow D))\rightarrow \neg A \vee D$$

Lets take a quick look at the truth table for $P\rightarrow Q$:

$$\begin{matrix}P&Q&P\rightarrow Q\\ T&T&T\\ T&F&F\\ F&T&T\\ F&F&T \end{matrix}$$

Whenever we want to prove a statement $P\rightarrow Q$, we note that it is always going to be true if $P$ is false. So the conclusion is that in order to prove $P\rightarrow Q$ true, it suffices to assume $P$ is true, and then show $Q$ is true as a result.

So that being said, in order to prove your implication from above, we assume the antecedent (the $P$ part):

$$(\neg C \vee B) \wedge ( A \rightarrow C) \wedge (B \rightarrow D),\tag{1}$$

and then we must show that as a result of assuming this proposition true, that $\neg A\vee D$ must be true.

Now when formulating your proof with inference rules, it's probably a good first try to use $(1)$ as inspiration for your premises. Since we assume $(1)$ is true, we get that:

$$\neg C\vee B,\quad\quad A\rightarrow C,\quad\quad B\rightarrow D,$$

are all true. These make great premises to try, and (looking at your solution) it's clear you have understood this to some extent. An example of a solution using these premises is the following (only look at the spoiler if you want to spoil it):

1. $\neg C\vee B$ (premise)
2. $A\rightarrow C$ (premise)
3. $B\rightarrow D$ (premise)
4. $C\rightarrow B$ (logically equivalent to 1)
5. $A\rightarrow B$ (hypothetical syllogism, 2,4)
6. $A\rightarrow D$ (hypothetical syllogism, 5,3)
7. $\neg A\vee D$ (logically equivalent to 6)$\quad\blacksquare$

That being said, this is not the only way to prove this. Your solution comes half way to proving it another way, but it falls short in both that you did not complete the proof, and you would need to be a bit more formal with how you go about it.

The key mistake in your proof, as mentioned in the comments, is that you assume $B$ is true as one of your premises when it's not necessarily true. For all we know, $B$ could be false. You'd have to show such a thing. However, there is a way to utilize the argument you made: arguing by cases.

To do this, I want to show you an alternative, but extremely similar style of writing out these deductive arguments: Fitch notation. The idea is very straightforward

$$\def\ftc#1#2{\quad\begin{array}{|l}#1\\\hline #2\end{array}}\ftc{1. \text{ Premises go here}}{2. \text{ Conclusions go here}\\\ftc{3. \text{ premises of a sub-argument}}{4. \text{ conclusions of the sub-argument}}\\\vdots}$$

What Fitch-style notation lets us to is create sub-proofs in our proof seamlessly, much like lemmas. Otherwise, to be crystal clear with your previous method, the best way I can think of is to write a lemma argument off to the side as a brand new proof (if anyone knows a better way, let me know!).

So now your argument would start as follows:

$$\ftc{ 1.\,\neg C\vee B\\ 2.\,A\rightarrow C\\ 3.\,B\rightarrow D }{ \ftc{4.\,B}{ 5.\,D\quad\text{(Modus Ponens, 3,4)}\\ 6.\,\neg A\vee D\quad\text{($\vee$ introduction, 5)} }\\ 7.\,B\rightarrow(\neg A\vee D)\quad\text{($\rightarrow$ introduction, 4-6)}\\ \vdots }$$

and so this shows that you have created this lemma that $B\rightarrow(\neg A\vee D)$. What you would now need to do is make a lemma for $\neg B\rightarrow(\neg A\vee D)$, and the argument would finish as follows:

$$\ftc{ 1.\,\neg C\vee B\\ 2.\,A\rightarrow C\\ 3.\,B\rightarrow D }{ \ftc{4.\,B}{ 5.\,D\quad\text{(Modus Ponens, 3, 4)}\\ 6.\,\neg A\vee D\quad\text{($\vee$ introduction, 5)} }\\ 7.\,B\rightarrow(\neg A\vee D)\quad\text{($\rightarrow$ introduction, 4-6)}\\ \ftc{8.\,\neg B\\\vdots}{\vdots\\\text{k. }\neg A\vee D}\\ \text{k+1. }\neg B\rightarrow(\neg A\vee D)\quad \text{($\rightarrow$ introduction, 8-k)}\\ \text{k+2. }B\vee\neg B\quad\text{(Law of excluded middle (!!!))}\\ \text{k+3. }\neg A\vee D\quad\text{($\vee$ elimination, 7, k+2, k+3)}\quad\blacksquare }$$

So given that you fill in the spots with the vertical dots with something that works, this proof technique works perfectly well. The following spoiler gives a sketch of an example argument:

$$\ftc{8.\,\neg B}{9.\,\neg C\quad\text{(disjunctive syllogism, 8, 9)}\\10.\,\neg A\quad\text{(Modus Tollens, 2, 10)}\\11.\,\neg A\vee D\quad\text{($\vee$ introduction, 11)}}$$

One very important thing to note about my answer to this question is that it is not extremely formal. I am leaving things out like conjunction elimination and other things that I took for granted because you seemed to understand that it is used implicitly. I hope that it doesn't confuse you further, but feel free to ask more questions.

P.S. the (!!!) beside the Law of Excluded Middle rule is to bring attention that we are using a rule that is commonly left out of logic to make weaker systems which sometimes are discussed. It's just nice to make note of where it got used here. If you find this interesting, then take a look at the wikipedia page and the outline of history there: https://en.wikipedia.org/wiki/Law_of_excluded_middle

| cite | improve this answer | |

I'm assuming this question is asked under the scope of propositional calculus. Overall this isn't really a well defined question, because the result would vary dramatically under different sets of axioms with different rules of inference and different type of proof structures used.

Let $\Gamma = \{(¬C∨B),(A→C),(B→D)\}$ be a set of WFFs. Convince yourself, using elimination rules of connectives, why it suffices to show for $\Gamma$.

We look at $\Gamma \cup \{A\}$ first.

Using $\space¬C∨B \cong C→B\space$ we can construct the following sequent:

$1.$ MP on $\phi_1=A,\phi_2=A\rightarrow C$ achieves $\{\phi_1,\phi_2\}\vdash C$ and because $CPL$ is monotonic we have $\Gamma \cup \{A\} \vdash C $.

$\\2.$ Identically to the first step in the proof, we use MP to achieve $\Gamma \cup\{A,C\}\vdash B $.

$\\3.$ Again, we use MP once more to achieve $\Gamma \cup\{A,B,C\} \vdash D$.

$\\4.$ Use introduction rules of logical connectives to achieve $D \vdash D \vee \neg A$, how you do this is completely dependent on the set of axioms you're using. If it is complete, then we will be able to introduce that claim since it is semantically correct.

Overall we see $\Gamma\space\cup \{A\}\vdash D∨¬A$. It is obvious that $\Gamma\cup \{\neg A\} \vdash \neg A$ using an axiom such as $A\rightarrow A$ therefore by arguments presented above we have $\Gamma\space\cup \{\neg A\}\vdash D∨¬A$.

Using dichotomy theorem concludes the proof.

| cite | improve this answer | |
  • 2
    $\begingroup$ I am going to go out on a limb here and say that the asker is not looking for this sort of rigour, and is more inclined towards a naive understanding of "propositional calculus". $\endgroup$ – anakhro May 11 '19 at 1:04
  • $\begingroup$ @anakhro I don't really agree. There's not really much reason to prove random propositional theorems except to explore and study formal proofs. $\endgroup$ – Derek Elkins left SE May 11 '19 at 1:27
  • $\begingroup$ @DerekElkins my point is that the asker won't understand this answer. It's not aimed at his skill level. $\endgroup$ – anakhro May 11 '19 at 1:45
  • $\begingroup$ @anakhro I tried to expose OP to a myriad of useful concepts in logic, such as elimination rules, dichotomy, deduction, completeness of an axiomatic system and monotonicity. None of these are terribly difficult or deep, and are usually seen in the first half (or even quarter) of every introductory course to logic. $\endgroup$ – Adar Gutman May 11 '19 at 12:56
  • $\begingroup$ @AdarGutman I think you could explain those things in a little more detail. I myself have taken several courses in logic and for some reason still can't come up with what "WFF" stands for. Several other acronyms go unexplained, and the turnstile notation goes unexplained. There is no issue with teaching/exposing someone new math, but you haven't taught anything. You just gave him the proof in a completely different format (that you have not explained) than he seems to be used to. $\endgroup$ – anakhro May 11 '19 at 15:04

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.