Can the distributive law be proven using only ∧-elimination/introduction and ∨-elimination/introduction?

I have been trying to figure out a logic problem for days now; I think I've made it so that my brain can only see one thing and can't look at it a different way. Basically, I need to prove the following:

A ∧ (B ∨ C) ⊢ (A ∧ B) ∨ (A ∧ C)

I found a proof for this, but it does not follow the constraints. It goes as follows:

A ∧ (B ∨ C)

A (1 ∧-elimination)

B ∨ C (1 ∧-elimination)

B (supposition) (setting up a conditional proof)

(A ∧ B) (1,3 ∧-introduction)

(A ∧ B) ∨ (A ∧ C) (3,4 ∨-introduction)

C (supposition)

A ∧ C (1,6 ∧ introduction )

(A ∧ C) ∨ (A ∧ B) (7 ∨ introduction)

(A ∧ B) ∨ (A ∧ C) (8 Commutation)

A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) (1,3-5,6-9 ∨ elimination)

A ∧ (B ∨ C) (1, Reiteration)

(A ∧ B) ∨ (A ∧ C) (Modus Ponens)

However, I am given the constraint that I can only use ∧/∨ elimination and introduction. I have looked at this for a while and can't figure out how to do that. Could somebody help me?


Your use of Disjunction Elimination is strange, and I'm curious what the precise rule in your textbook is. Anyway, I've included below how I'd do it.

$\begin{array}{llll}\{1\}&1.&A\land(B\lor C)&\small\text{P}\\\{1\}&2.&A&\small\text{1, $\land$E}\\\{1\}&3.&B\lor C&\small\text{1, $\land$E}\\\{4\}&4.&B&\small\text{A for $\lor$E}\\\{1,4\}&5.&A\land B&\small\text{2, 4 $\land$I}\\\{1,4\}&6.&(A\land B)\lor(A\land C)&\small\text{5, $\lor$I}\\\{7\}&7.&C&\small\text{A for $\lor$E}\\\{1,7\}&8.&A\land C&\small\text{2, 7 $\land$I}\\\{1,7\}&9.&(A\land B)\lor(A\land C)&\small\text{8, $\lor$I}\\\{1\}&10.&(A\land B)\lor(A\land C)&\small\text{3, (4), 6, (7), 9 $\lor$E}\\\end{array}$

Notes:

  1. The columns from left to right are dependencies, line number, formula, rule/reason for the formula (numbers in brackets indicate that the dependency introduced at that line is to be discharged)
  2. Conjunction Introduction allows us to conjoin the conjuncts left or right - from $A\vdash A$ and $B\vdash B$ we can derive $A, B\vdash A\land B$ and $A, B\vdash B\land A$. This may be presented as a left and right rule in your system
  3. Disjunction Introduction behaves the same as Conjunction Introduction - we can disjoin the disjuncts left or right
  4. Disjunction Elimination requires us to assume each disjunct in turn. If we can derive the same formula from each disjunct then we have derived that formula from the disjunction. Like with a Conditional Proof, Disjunction Elimination is a discharge rule - i.e., the conclusion we've derived by assuming each disjunct isn't dependent on those assumptions. The precise details of how it's arranged on the page depend on the system you're using, but the basic deets are the same
  5. Some systems will require that you use reiteration before conjoining terms in different scopes, so be mindful of that for your particular system