Mike said, in part, that implication is something inside the logic and
entailment is something outside. Personally, I don’t tend to find
phrases such as ‘this is a statement in the logic, but that’s a
statement in the metalogic’, or ‘this is inside the formal system, but
that’s outside’, very compelling. Mathematics is in some sense one
big formal system; every mathematical statement we make has to be
logical. (You can’t say ‘the Riemann Hypothesis is true because your
mother says so’; or you can, but it won’t count as mathematics.) I
think that’s why I don’t find that narrative very helpful.

But as Andrej’s comment hints, *categorical* logic can make the logic/metalogic distinction perfectly precise. In particular, it can help to clarify the distinction between implication and entailment. I’ll have a go at explaining.

Let’s start with posets. Take a poset $P$ that, viewed as a category, is cartesian closed. Binary products give us a greatest lower bound $A \wedge B$ for each $A, B \in P$. The terminal object is a greatest element $1 \in P$. The exponential $B^A$ is usually written $(A \to B)$, and its universal property is that $A \wedge B \leq C$ if and only if $A \leq (B \to C)$.

**Lemma** Let $A, B \in P$. Then $A \leq B$ if and only if $1 \leq (A \to B)$, if and only if $(A \to B) = 1$.

*Proof* By the universal property of $\to$ and the fact that $1$ is greatest, $A \leq B$ iff $1 \wedge A \leq B$ iff $1 \leq (A \to B)$ iff $(A \to B) = 1$.

Now let $X$ be a set and $P$ the power set of $X$, ordered by inclusion. We have $A \wedge B = A \cap B$, $1 = X$, and $(A \to B) = X \setminus (A \setminus B) = (X \setminus A) \cup B$.

Suppose that you and I are doing some work together. We have a set $X$, and two particularly interesting subsets $A$ and $B$. We finish our discussion. Some hours later, I phone you and say:

Dude, $A \subseteq B$!

Or I might equivalently say:

Dude, every element of $A$ is an element of $B$!

(I’d be particularly likely to put it this way if we had adjectives for membership of $A$ and $B$: ‘dude, every ample element is Borromean!’) Or, I might equivalently say:

Dude, $x \in A \vdash x \in B$!

OK, I wouldn’t actually *say* this, but it does mean the same
thing. (Were I more conscientious, and not speaking down the phone, I would decorate that statement with some further notation to indicate that the ‘$x$’ mentioned is supposed to range over $X$.)

Those are three equivalent ways of saying the same thing. Here are a further three equivalent ways:

Dude, $(A \to B) = X$!

Dude, every element of $X$ is in $(A \to B)$!

Dude, $\vdash x \in (A \to B)$!

The absence of stuff to the left of the ‘$\vdash$’ means that the right-hand side is true under no assumptions at all on $x$. In this example it seems forced to mention $(A \to B)$ at all, but I guess there are circumstances where it’s natural.

The first three are equivalent to each other because they’re just different idioms for saying the same thing. The same goes for the second three. But the first three are equivalent to the second three exactly because of the lemma.

Now let’s try something more ambitious. Let $\mathcal{E}$ be a category (not necessarily $Set$) and $X \in \mathcal{E}$. There is a category $Mono(X)$ whose objects are monos $A \rightarrowtail X$ and whose maps are commutative triangles. It is in fact a preorder, i.e. each hom-set has at most one element. A **subobject** of $X$ is an object of $Mono(X)$ (or strictly speaking, an isomorphism class of objects), and we therefore have an order $\leq$ on subobjects of $X$. When $\mathcal{E} = Set$, this is the power set of $X$ ordered by inclusion.

Supposing that $\mathcal{E}$ is a topos (though that’s probably overkill), the poset $Mono(X)$ is cartesian closed. The greatest lower bound $A \wedge B$ of two subobjects $A \rightarrowtail X$, $B \rightarrowtail X$ is their pullback. The greatest element is $X \rightarrowtail X$. Finally, $(A \to B)$ is defined using exponentials in $\mathcal{E}$.

Now suppose that $X$ is an internal group. Consider the statement ‘if $x^6 = x^{15}$ then $x^2 = 1$’. (This is true in some groups in $Set$, and false in others; it says that there are no elements of order 3.) There is a subobject $A$ of $X$ that we might think of as $\{x \in X: x^5 = x^7\}$ — and if $\mathcal{E} = Set$, it’s exactly that. It’s defined as the equalizer of
$X \rightrightarrows X$
where the two maps are ‘6th power’ and ‘15th power’ respectively. There is
similarly a subobject $B$ of $X$ that we might think of as $\{x \in X: x^2 =
1\}$. Then there’s a further subobject $(A \to B)$.

By the lemma,

$A \leq B$ if and only if $X \leq (A \to B)$ if and only if $(A \to B) = X$.

Suppose I’ve discovered that $X$ *does* have these equivalent properties. I might communicate this to you by saying:

Dude, $A \leq B$!

A logician might communicate the same thing by saying:

Dude, $x \in A \vdash x \in B$!

Both those statements are about *entailment*. But using the result of the lemma, it would be equivalent to say:

Dude, $(A \to B) = X$!

A logician might communicate this by saying:

Dude, $\vdash x \in (A \to B)$!

This statement contains *both entailment and implication*. The entailment
is the $\vdash$, and the implication is the $\to$. It’s not going to be
possible to say something with implication alone, because $(A \to B)$ is not a
mathematical statement: it’s an object of $\mathcal{E}$. You can no more say,
‘Dude, $(A \to B)$!’ than ‘Dude, $\mathbb{R}$!’

The moral of all this: a statement in the metalogic is something that can be
prefaced with the word ‘Dude’.

## Re: Entailment and Implication

That’s not only confusing but malicious.

And, denoted $\wedge$, isconjunction.Hope that clears up some of your disfusion.