Does this propositional logic equivalence touching inplication have a name : ( (A&B) -> (A&C) ) <-> (A -> (B->C) )?

Question

Stanford truth table generator tells me that the following formula is a tautology:

$\left(\left(A\land B\right)\Rightarrow\left(A\land C\right)\right) \Leftrightarrow \left(A\Rightarrow\left(B\Rightarrow C\right)\right)$

Does this equivalence have a standard name?

Remark : I came across this equivalence while working on the question asked in this post Proof Regarding If - Then Statement Regarding Sets

Answer 1

This is not an equivalence I have ever had the occasion to encounter ... thus I have not seen a name for it either ... but given as I have a good bit of experience with elementary logic and read quite a few books on the subject, it also means that it is uncommon and probably has never been named.

We can, however, derive it from a couple of other equivalences:

$$(A \land B) \to (A \land C) \overset{Implication}\Leftrightarrow$$

$$\neg (A \land B) \lor (A \land C) \overset{DeMorgan}\Leftrightarrow$$

$$\neg A \lor \neg B \lor (A \land C) \overset{Reduction}\Leftrightarrow$$

$$\neg A \lor \neg B \lor C \overset{Implication}\Leftrightarrow$$

$$A \to (\neg B \lor C) \overset{Implication}\Leftrightarrow$$

$$A \to (B \to C)$$

Of these, I would argue that the Reduction is the most 'central' equivalence, as that's the one that removes/introduces the duplicate of the $A$. I also sense a presence of the Exportation equivalence ... and indeed I can make that explicit like so:

$$(A \land B) \to (A \land C) \overset{Implication}\Leftrightarrow$$

$$\neg (A \land B) \lor (A \land C) \overset{DeMorgan}\Leftrightarrow$$

$$\neg A \lor \neg B \lor (A \land C) \overset{Reduction}\Leftrightarrow$$

$$\neg A \lor \neg B \lor C \overset{DeMorgan}\Leftrightarrow$$

$$\neg (A \land B) \lor C \overset{Implication}\Leftrightarrow$$

$$(A \land B) \to C \overset{Exportation}\Leftrightarrow$$

$$A \to (B \to C)$$

Indeed, this last one shows how you effectively go from $(A \land B) \to (A \land C)$ to $(A \land B) \to C$, i.e. you remove from the consequent what you already knew to be true in the antecedent. So, if anything is in need of a name here, I would say it is the equivalence of:

$$(A \land B) \to (A \land C) \Leftrightarrow (A \land B) \to C$$

Indeed, in Pairce's Existential Graphs, this equivalence would amount a 1-step application of Iteration/Deiteration... I do wish we had a name for it in classical boolean algebra. ... maybe a kind of 'Conditional Reduction'?

Answer 2

As with Bram28, I'm not aware of any name for this particular equivalence. In general, you shouldn't expect arbitrary theorems/equivalences to have names. You also shouldn't care too much about the names (which aren't consistently used anyway). You should care more about what rules are useful and/or fundamental.

To this end, here's a different derivation from Bram28's that has the benefit of being constructive (which shows that this equivalence is not particular to classical logic). I'll use two equivalences that are intimately connected to the very meanings of these connectives. Specifically, $$A\to (B\land C)\equiv (A\to B)\land(A\to C)$$ and $$(A\land B)\to C\equiv A\to(B\to C)$$ (These equivalences are internal forms of the adjunctions that characterize $\land$ and $\to$. The introduction and elimination rules for $\land$ and $\to$ can be read off from the adjunctions. Well, we usually incorporate an extra Cut into $\to$ elimination.)

We have $$\begin{align} (A\land B)\to(A\land C)&\equiv ((A\land B)\to A)\land((A\land B)\to C)\\ &\equiv (A\land B)\to C\\ &\equiv A\to (B\to C) \end{align}$$ where we've used the fact that $(A\land B)\to A\equiv \top$ which is readily derivable. This makes it clear that the main equivalence is $(A\land B)\to C\equiv A\to(B\to C)$ and this example just tacks on an extra trivially derivable $A$ in the consequent. The first equivalence quickly makes this evident.

Answer 3

Since a thing always implies itself, $(A \land B) \to (A \land C)$ is equivalent to $(A \land B) \to C$.

The relation $$\bigg( (A \land B) \to C \bigg) \iff \bigg(A \to B \to C\bigg)$$

is sometimes called Currying after its type theoretic dual:

For every function $\mathcal F : (A \times B) \to C$ there is an equivalent function which inputs $A$ and outputs function $\mathcal G : (B \to C)$

If you consider $$\bigg( (A \circ B) \to C \bigg) \iff \bigg(A \to B \to C\bigg)$$

then there is only 1 binary operator which satisfies $\circ$ so the proposition is also sometimes cited as a (constructive) definition for $\land$.