The n-Category Café

and, denoted $\wedge$, (also called disjunction by logicians who wish to confuse me)

That’s not only confusing but malicious. And, denoted $\wedge$, is conjunction.

Hope that clears up some of your disfusion.

I think that’s about how I understand the difference. Implication is an “operation on truth-values/propositions/statements” which produces, given two such things $P$ and $Q$, another such thing $P\Rightarrow Q$ of the same type. By contrast, entailment is a statement about two such things, not itself a thing of the same sort. One might say that entailment belongs to the “metalogic” in which one describes the logic.

There do exist logical systems which do not include implication. One such system, which is of great importance in topos theory, is geometric logic. However, systems of this sort usually do include entailment. More simply, any poset which is not a Heyting algebra could be regarded as having a notion of “entailment” (namely $\le$) but no notion of implication.

Elementary logic books tend to obscure the distinction, since when you have implication, then you can reduce entailment to a notion of “truth”, since $P\vdash Q$ precisely when $\vdash (P\Rightarrow Q)$, i.e. when $P\Rightarrow Q$ is true/valid/provable.

Well, we tend to think of entailment as being “really true”, an external conclusion, while implication tends to be construed as an internal thing… you can think of it, if you like, as having two systems of logic which are supposed to mirror eachother.

I wonder if I can try to make things better by temporarily making this worse?

A sufficient condition for a logic being interesting to me is whether it admits a theory of categories of models; the case most familiar to me is first-order logic interpreted within set theory via the Tarski “definition of truth,” which is a fairly mechanical thing. One reason this makes things interesting is that a-priori you can define two sorts of entailment: one syntactic, $\vdash$, and the other semantic, which is usually denoted by $\models$.

Semantic entailment is defined relative to any universe, language, and meaning of truth by the condition that $\Theta \models \Phi$ precisely when all models verifying $\Theta$ also verify $\Phi$, where $\Phi$ is a proposition and $\Theta$ a set of propositions. This is potentially a very large relation. I.I.r.c., Goedel proved that under some conditions, the particular relation $\models$ is reasonably reducible to first-order logic finitary $\vdash$; these are among completeness and compactness theorems. Also, by definition, there are no models which verify false, so every such model also verifies true, so false semantically entails true. Though maybe that doesn’t help much?

There are theoretically useful logics which don’t enjoy compactness — a trivial example trying to get at what is really true about the natural numbers is a logic in the language of Peano arithmetic and having a deduction schema $$\{ \Phi[n] | n=0,S0,S S0, \dots \} \vdash \forall x: \Phi[x]$$ in which you can have proofs that are infinitely long; e.g., this system formalizes small instances of Goodstein’s theorem without quite mentioning $\epsilon_0$. And in this system there are theorems which aren’t reducible to tautologies. But this logic is still of limited practical use. For example, it also decides the twin primes conjecture, but knowing that doesn’t help us discern the answer.

Entailment and implication are in the same relationship as the Hom-functor and exponentials in a category.

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’.

What does it really mean that, for instance, false entails true?

Syntactically, regarding entailments from $false$, you might want to look up ex falso quodlibet, which Wikipedia calls the Principle of explosion. If you take $false$ to be equivalent to $\psi \wedge \not \psi$ for some proposition $\psi$, it’s not hard to see how any proposition can be derived from it.

Relevance logicians don’t buy into this, however, since they believe that $\psi$ would have to be relevant to the derived proposition.

Semantically, it says that any model in which false holds, true holds there too. But false never holds in a model, so this is vacuously the case.

Perhaps, rather than trying to simplify things, it’d be easier to understand if you make them more complex. Consider, for example, coming at it from the direction of CCCs as lambda calculi. But what if our lambda calculus is so simple that we can’t define higher-order functions? If we can’t have HOFs (i.e., functions cannot take functions as arguments) then that means the category doesn’t have exponentials. The calculus does still have functions, but it doesn’t have any way to pass them around; the functions are, in some sense, outside of the calculus itself. They’re not first-class.

The same thing holds for logics. Just as all term calculi have functions, all logics have some notion of validity (i.e., entailment). But that doesn’t mean that all logics have a way of internalizing it. Having implication in a logic is like having lambdas in a term calculus: it gives a language-internal mechanism for abstraction. In calculi we’re abstracting over subterms, in logics we’re abstracting over whether some given proposition is valid— but the important thing is that we’re doing this within the language, not just in our own thoughts. Thus, logics with implication can pass around these abstracted terms and can ask things like whether an abstract term is valid (instead of just asking whether all concretizations of it are valid).

In a way, the difference between entailment and implication is like the difference between conditionals and hypotheticals (some languages make a better distinction between those than English does).

Tom says:

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.

Simon says:

I don’t know how to think of this. Maybe I should just take this as the definition and not worry about how to think of it. But this is not how most mathematicians think of implication. “Implication is an internal hom” would not strike a chord with most mathematicians.

I think you are struggling with the question of primordial foundations: what is the absolute meta-context of logic and math, and what is internal math and internal reasoning?

We had a discussion about this on the $n$Forum recently, and it seems that Todd and Mike gave us the complete answer. Todd has been promising to write it all up in an $n$Lab page, since. I don’t know how far this has progressed, but I am still looking forward to it.

If I may try to summarize the situation, unqualified as I am:

In the beginning there is the FOL : first order logic. We all assume that we know what it means to reason in first order logic, we teach it to kids and – importantly – we can teach it to computers and see them implement it automatically and in reality . This is the outermost ambient meta logic.

Once we have this, we formulate theories in terms of first order logic. For instance the theory of sets . We may (and ultimately should) do this fully mechanically, as if we were programming a computer that reads in first order logic. Todd kindly went through the very instructive trouble of spelling out what this means in full detail at fully formal ETCS. This sets up the topos of sets $SET$ in the outermost ambient meta-logic.

Once we have this, we may decide to jump into $SET$ and now reason inside this. I think it is very analogous to starting with assembly language and writing a C-compiler in terms of it. Once you have done it, you may choose to write all further programs not in assembly anymore, but in C, and let the compiler turn it back into assembly code.

Once we are in the (very large) topos $SET$, we may define further frames, categories, toposes internal to it. And then reason internal to these, if we find this higher order language useful for our applications.

This gives us a hierarchy of internalizations. At each step there is a notion of implication (internal to that hierarchy level) and entailment (internal to the previous, ambient internalization level). This hierarchy has a root: first order logic. The outermost meta logic is that of FOL., and here we only have entailment. But nobody wants to spend his or her whole life here, just as nobody wants to write code in assembly forever. So as need be, we pass to higher level internalizations, and each time that we make such a step the internal logic of the previous step becomes the meta-logic of the next one, the implication of the previous step becomes the entailment of the next one.

The difference lies within the agent doing the reasoning. “a entails b” means, “If a is true, then b must be true under the same model”. “a implies b” means, “I, the agent, infer that b is true given that a is true.” If the agent reasons perfectly, it will infer only what is entailed and will infer everything that is entailed, and the set of entailed facts and implied facts will be equivalent.