# Proof for the Rule of Absorption in Propositional Logic?

I know there is a "formal proof" for the "rule of absorption" that employs the "law of excluded middle". It is presented in Wikipedia (and I think it is Russell's): https://en.wikipedia.org/wiki/Absorption_(logic)#Formal_proof.

It is also obvious how it could be done by way of a "conditional" or "indirect" proof.

However, is there a "formal proof" in propositional logic for the "rule of absorption" that does NOT assert the "law of excluded middle (or non-contradiction)" as a rule of inference or employ a "conditional (or indirect) proof"?

That is to say, can a "formal proof" be constructed in propositional logic (natural deduction or otherwise) that goes from the premise p⊃q to the conclusion p⊃(p∙q) WITHOUT using the "law of excluded middle (LEM)" as a rule of inference or employing a "conditional proof (CP)" or "indirect proof (IP)"?

• Out of curiosity and considering you're not accepting the answer using a truth table, how do you define the truth-functional operation of a conditional for the purposes of your question? (normally one does so with a truth table) Jun 15 '17 at 2:38
• It is not that I am not accepting the answer. Of course, a truth table shows us not only that going from p⊃q to p⊃(p∙q) is valid but moreover that p⊃q and p⊃(p∙q) are equivalent statements (which makes Copi's applying absorption as a rule of implication curious, but I digress). Bottom line, I am just wanting to know about its proof in so-called natural deduction, and whether or not it can be done without CP or LEM (it seems that it cannot be, which is revelatory regarding absorption's applicability in philosophical logic). That is all! Jun 24 '17 at 0:44
• I think you're misunderstanding my above comment. I'll try to re-express it. (1) the function p⊃q is normally defined by a truth table (en.wikipedia.org/wiki/Material_conditional). As in, p⊃q is precisely the function that produces the output the truth table dictates. (2) answer below uses truth table to derive p⊃(p∙q). (3) you object to answer since truth table presupposes bivalence and/or LEM. (4) Wouldn't it follow that your objection also applies to definition of p⊃q ? Jun 24 '17 at 1:26
• Put another way, if (3) is a problem, then isn't (1) a problem too? And if (1) isn't a problem, then (3) doesn't seem to be one either.... So it seems you should either give a definition of p⊃q that is not a truth table or accept the validity of the proof via truth-table. Jun 24 '17 at 1:28
• I can tell you must be frustrated but I think my point is simpler (and / or on a different level?) than what you're responding to... To state clearly, I agree that it may be impossible to accomplish such a proof without CP, LEM, or truth tables. Where I'm lost is how you can define ⊃ without giving it the standard truth table we expect. Jun 30 '17 at 10:38

The rule of absorption can be proved via truth table (which is neither a "conditional proof" nor an "indirect proof") like so:

``````P Q | P ⊃ Q | (P ∙ Q) | P ⊃ (P ∙ Q) | (P ⊃ Q) ≡ [P ⊃ (P ∙ Q)]
-----------------------------------------------------------
0 0 |   1   |    0    |   1         |         1
0 1 |   1   |    0    |   1         |         1
1 0 |   0   |    0    |   0         |         1
1 1 |   1   |    1    |   1         |         1
``````

But, if truth tables presuppose the law of excluded middle, then it would seem that the rule of absorption is not provable within the constraints you've imposed.

• Thanks for your answer, Jayson! I am, however, not looking just to prove/demonstrate that the "rule of absorption" is valid. Knowing it is valid, I am looking for a "formal proof", a formal deduction, (so-called) natural deduction or otherwise, for the "rule of absorption". That said, you did directly answer my question with your last sentence... in (per what I had written in my message before it got edited out) the "straightforward" way I have come to anticipate (having messed with this for quite some time), that is, "NO!" Do you really think that is the bottom line? Jun 10 '17 at 4:40
• Jayson, also, one other thought... Is it that truth tables presuppose the "law of excluded middle" or the "principle of bivalence"? If the latter, then your answer was more on point than you or I were giving it credit for being. That said, I am ultimately looking for the "formal deductive proof", which we both seem to believe does not exist. XD Jun 10 '17 at 5:33
• The idea that the truth value of P, and the truth value of Q have to be either 0 or 1 is the LEM, right? If you want not to presume the LEM, you would have to include options for where either one was still undecided. You would also need a standard of implication that does not automatically assume that the implication always has a truth value.
– user9166
Jun 15 '17 at 1:03
• @Stegfucius I'd say they presuppose bivalence, but that bivalence as a property of the semantics relies on LEM in the meta language used to state the semantics. At the very least, the intuition regarding truth being an "on" or "off" property of propositions seems to be what motivates both LEM and bivalence. If the semantic values of propositions aren't regarded as truth values, it's hard to see why you'd insist there are only two. For instance, consider an intuitionist who replaces "truth" with "proof", or the construction of Boolean valued models beyond the two element Boolean algebra. Jun 15 '17 at 2:32
• Well, truth table is powerful tool. At least for binary logic. Jun 23 '18 at 8:19

This is only a partial answer because it uses conditional elimination and conditional introduction which may be prohibited. However, it does not use the law of excluded middle (LEM).

As I understand the comments there is some question about the prohibition of rules for conditionals if one allows a conditional in the premise and a conditional in the conclusion. If one uses conditionals to state the proof, rules for manipulating the conditional should be specified.

The proof was made using Kevin Klement's natural deduction proof editor and checker.  