How can we explain the discrepancy between $\rightarrow$ (IF-THEN) and $\setminus$ (A-BUT-NOT-B)?

Question

Let $\mathbb{B} = \{0,1\}$ denote the Boolean domain, ordered in the usual way. Then $\mathbb{B}$ is a lattice. It has a join operation $\vee$ that coincides with "OR," a meet operation $\wedge$ that that coincides with "AND," and these distribute over each other. There is also a unique function $\neg : \mathbb{B} \rightarrow \mathbb{B}$ subject to the identities $$x \wedge \neg x = 0, \quad x \vee \neg x = 1.$$ This coincides with "NOT." In other words, $\mathbb{B}$ is a Boolean algebra.

We can define two further binary operations (namely $\rightarrow$ and $\setminus$) on $\mathbb{B}$ as follows, coinciding with IF-THEN and A-BUT-NOT-B.

$$x \rightarrow y = \neg x \vee y, \quad x \setminus y = x \wedge \neg y$$

Each is the negation of the other. But there's a HUGE discrepancy in how important and/or ubiquitous these two operations seem to be:

1. Introductory courses in logic and/or mathematics usually talk at length about IF-THEN, but they almost never mention A-BUT-NOT-B.

2. Software proof assistants almost always have support for the IF-THEN operation, but never (as far as I know) have direct support for the A-BUT-NOT-B operation.

3. Almost every theorem in mathematics is phrased using at least one explicit occurrence of IF-THEN, while almost no theorem is ever phrased using an explicit occurrence of A-BUT-NOT-B. This could be a purely linguistic phenomenon, except that:

4. Most mathematicians seem to think of IF-THEN as an actual "stand-alone" operation, yet at the same time, tend to think of A-BUT-NOT-B as a compound operation, built out of AND and NOT.

Question. How can we explain the discrepancy in importance between $\rightarrow$ (IF-THEN) and $\setminus$ (A-BUT-NOT-B)?

I would be satisfied with an explanation of why we tend to think of mathematics asymmetrically in general, as opposed to why the asymmetry exists in this particular case.

Answer 1

The table of your "A-BUT-NOT-B", which I'll call "L" with "0" for falsity and "1" for truth goes as follows:

L  0  1
0  0  0
1  1  0

Do any tautologies with just "L" exist? I'm not sure how to argue that none exist, but I'll guess that NO tautologies with "L" exist. Thus, we can't infer anything from any statement where the only connective is "L". On the other hand, there do exist tautologies with "C" (if-then). If there do not exist any L-tautologies, then there are no proofs where L is the primary connective involved in inferring to the last theorem of the proof. On the other hand, there exist plenty of proofs which use some sort of "C" connective.

Answer 2

Mathematicians use "A but not B" every time they provide a counterexample. This is a direct consequence of it being the negation of "A implies B."

An implication gives rise to at least one counterexample, so this structure is actually being used implicitly a good portion of the time when authors supply counterexamples.

The reasons for its absence as a formal "thing" and the reasons for preferring to emphasize "implies" are probably just a combination of tradition and habit. There is seemingly no need to elevate the importance of the negation of a particular construct to be equal with the construct.