# Proof for the Rule of Absorption in Natural Deduction?

I know there is a "formal proof" in "natural deduction" 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 the proof could be done by way of a "conditional" or "indirect" proof.

However, is there a "formal proof" in "natural deduction" 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 proof in "natural deduction" be constructed 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) Commented 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! Commented 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 ? Commented 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. Commented Jun 24, 2017 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. Commented Jun 30, 2017 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? Commented 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 Commented 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
Commented Jun 15, 2017 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. Commented Jun 15, 2017 at 2:32
• Well, truth table is powerful tool. At least for binary logic. Commented 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.

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.

• I don’t see how using axioms that validate the admissibility of the Deduction Theorem counts as using it; after all, cut-free proofs don’t somehow lose that aspect once cut’s admissibility is proven. Commented Jun 25, 2023 at 15:57
• @PW_246 its a good point. in practice, conditional inference has not been employed. In principle, K, S are chosen for an easy proof of deduction, allowing us to do everything that conditional inference is "supposed to do". So we choose axioms and rules that allow us to derive the rule we say we don't want to use, and then when we use them, we say we haven't. Commented Jun 25, 2023 at 22:33
• in classical logic, connectives are interdefinable. So suppose I prove something using only &, ~, v, but not ->. Have I avoided conditional proof? Maybe. Commented Jun 25, 2023 at 22:37
• conditional proof (if you buy something along the line of Witt, Dummett) is intimately related to meaning of conditonal, whereas its not clear to me that structural rules bear the same relation to meaning. But I don't pretend that these are water tight arguments, only considerations in a fairly deep matter Commented Jun 25, 2023 at 22:58

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)

• Sweet! Thanks, PW_246! I was looking for the proof to be done in natural deduction, though. I could be wrong, but I think the reason it can be done in axiomatic systems of propositional logic, such as Hilbert systems, is that the law of excluded middle/formal tautologicality is built into the system via the axioms/rules. Indeed, that would be the case for both &-Intro and P3 there, right? Commented Jul 28, 2023 at 9:21
• No, this proof does not require the law of the excluded middle. In general, if a proof doesn’t need DNE in natural deduction, it doesn’t need LEM or something equivalent in the usual Hilbert axiomatic system. Commented Jul 28, 2023 at 11:04
• I understand... I am saying that axiomatic systems of logic incorporate formal tautologicality via their axioms/rules (and, therefore, imply the law of excluded middle). After all, both &-Intro and P3 are tautologies, a.k.a. necessary truths. Commented Jul 28, 2023 at 23:22
• The axioms I used are not sufficient to prove LEM by themselves. Commented Jul 29, 2023 at 0:05
• Of course, they cannot, but, with all due respect, I did not say that "the axioms you used are sufficient to prove ...," I said that "axiomatic systems imply ..." But, ANYway, &-Intro and P3 are tautologies (which is enough to make my point, as I see it, but I digress). Commented Jul 29, 2023 at 5:20