The scenario I'm analyzing is the following: I have the set of clauses

$${ ( \neg A \Rightarrow B ),\, ( B \Rightarrow A ),\, ( A \Rightarrow ( C \wedge D ) ) }$$

and I have to prove the proposition $$(A \wedge C \wedge D)$$ using only Modus Ponens if possible. Well, the solution says me that just using MP the proposition is not possible to be proved. I wonder why it is not possible. I mean are there precise conditions or it is just because I have no "facts" (for example as $A$ or $\neg A$ that would mean having propositions with an exact value) in my set of clauses and so I cannot infer anything?


Basically, yes.

Modus Ponens is the rule of inference $\{X, X\to Y\} \vdash Y$ .   Without anything pairs of the form $X$ and $X\to Y$ you have nothing on which to use the rule.

Note: it is possible to infer the conclusion from those clauses; just not with only modus ponens to work with.

If you assume $\lnot A$ then using modus ponens on that and the first clause, and modus tollens with it and the second clause, will provide contradictory conclusions.   Hence inferring $\lnot\lnot A$, which will infer $A$ (unless you are restricted to intuitionalistic or constructive proofs).   If you prove $A$ then using modus ponens with that and the third clause proves the rest.


I think because you need a proof from contradiction:

Suppose $\lnot A$. Then MP gives $B$ by the first clause. Then MP again gives $A$ by the second clause. But we assume $\lnot A$, so we have a contradiction.

So $\lnot \lnot A$ holds, and then if we have the rule of Tertium non datur (excluded third), we have that $A$ holds, and then the third clause by MP gives $C \land D$, so in total (but this uses the a rule to introduce $\land$!) we know that $A \land C \land D$.

But we need at least two extra rules as well, and the excluded third. So in an intuitionistic logic (which does have MP, and the intro $\land$ rule) we could never prove $A \land C \land D$, but only $\lnot \lnot A$, using a $\lnot$-introduction rule.

  • $\begingroup$ There exist alternatives to a proof by contradiction to prove this. We could use the law of Clavius CCNppp, conjunction introduction CpCqKpq, and hypothetical syllogism CCpqCCqrCpr. Hypothetical syllogism and CNab and Cba yields CNaa. The law of Clavius and CNaa yields a. Modus ponens and CaKcd yields Kcd. Conjunction introduction and a and Kcd yields KaKcd. $\endgroup$ – Doug Spoonwood May 14 '16 at 17:32
  • $\begingroup$ @DougSpoonwood is this intuitionistically valid? $\endgroup$ – Henno Brandsma May 14 '16 at 17:33
  • $\begingroup$ No, it's not intuitionistically valid, since the law of Clavius does not appear in intuitionistic logic. $\endgroup$ – Doug Spoonwood May 14 '16 at 17:36
  • $\begingroup$ @DougSpoonwood But isn't the proof of the law of Clavius via contradiction? $\endgroup$ – Noah Schweber May 14 '16 at 20:12
  • $\begingroup$ @NoahSchweber Not necessarily. The law of Clavius could be an axiom (e. g. Lukasiewicz's 3 axiom system {CCpqCCqrCpr, CCNppp, CpCNpq}). The law of Clavius can get proved from CpCCNqqq, or really any sound and complete axiom system for propositional calculus. Note that unless we can derive some instance of $\alpha$ and N$\alpha$ in an axiomatic context, no proofs happen via contradiction. Very few authors seem to work with contradictory systems, and thus in their systems no proofs happen via contradiction. $\endgroup$ – Doug Spoonwood May 15 '16 at 0:45

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.