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)
    – virmaior
    Jun 15, 2017 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!
    – Stegfucius
    Jun 24, 2017 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 ?
    – virmaior
    Jun 24, 2017 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.
    – virmaior
    Jun 24, 2017 at 1:28
  • 1
    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.
    – virmaior
    Jun 30, 2017 at 10:38

4 Answers 4


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?
    – Stegfucius
    Jun 10, 2017 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
    – Stegfucius
    Jun 10, 2017 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, 2017 at 1:03
  • 2
    @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.
    – Dennis
    Jun 15, 2017 at 2:32
  • Well, truth table is powerful tool. At least for binary logic.
    – rus9384
    Jun 23, 2018 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.

enter image description here

Here is the proof of absorption using LEM in the cited Wikipedia article, "Absorption (logic)":

enter image description here


Here’s a Hilbert-Style proof using the axiom scheme from https://en.m.wikipedia.org/wiki/Hilbert_system

  1. P→(Q→(P&Q)) (&-Intro)

  2. (P→(Q→(P&Q)))→((P→Q)→(P→(P&Q))) (P3)

  3. (P→Q)→(P→(P&Q)) (1,2 MP)


I claim that there is no such proof, ie no such proof of A:= (p -> q) \implies [p -> (p \land q)] that does not use, as stated in OP, conditional proof, indirect proof, or LEM.

I will now use derivation to denote proofs in object language

We will work in intuitionisitc sequent calculus, without R->, since this rule corresponds to conditional proof, and intuitionistic calculus, since this rules out indirect or LEM. Suppose there exist such a derivation, that is a derivation of A. By cut elimination, there exists a derivation without cut. Now, by direct inspection of the (non structural) rules, we see that there is no way to introduce -> on the right. The only rule we can use is L->, from which we obtain \implies p, and our proof search thus terminates immediately.

The same idea works for ND, just via normalization instead of cut, and ->I instead of R->. Note that absorption is provable intuitionisitically, so its key that you disallow conditional proof for this to be the case.

How does this work in a Hilbert Style logic? Since we allow axioms K, S, we obtain a proof of deduction theorem, which is equivalent to allowing conditional proof. So if you don't want to allow conditional proof you must disallow those as well. In particular, in this case, you must disallow S.

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .