Proof for the Rule of Absorption in Propositional Logic?

Question

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)"?

Answer 1

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.

Answer 2

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.

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

Answer 3

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)

Answer 4

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.