nLab
implication

Definitions

An implication may be either an entailment or a conditional statement; these are closely related but not quite the same thing.

Entailment is a preorder on statements within a given context (including which logic is being used). We say that $p$ entails $q$ semantically, written $p⊢q$, if $q$ can be proved from the assumption $p$. We say that $p$ entails $q$ syntactically, written $p\models q$, if $q$ holds in every model? in which $p$ holds. (These relations are often equivalent, by various soundness? and completeness? theorems.) Notice that while $p$ and $q$ are statements in some object language (the language that we are talking about), $p⊢q$ and $p\models q$ are statements in the metalanguage (the language that we are using to talk about the object language).

A conditional statement is the result of an operation on statements within a given context. If $p$ and $q$ are statements in some logic, then so is the conditional statement $p\to q$ (at least if that logic has a notion of conditional). Notice that $p$, $q$, and $p\to q$ are all statements in the object language.

Relation of these

Depending on what logic one is using, $p\to q$ might be anything, but it's probably not fair to consider it a conditional statement unless it is related to entailment as follows:

If, in some context, $p$ entails $q$ (either semantically or syntactically), then $p\to q$ is a theorem (semantically) or a tautology (syntactically) in that context, and conversely.

In particular, this holds for classical logic and intuitionistic logic.

You can think of entailment as being an external hom and the conditional as being an internal hom. In particular, we expect these to be related as in a closed category:

• $q\to r⊢(p\to q)\to (q\to r)$,
• $p\equiv \top \to p$,
• $\top ⊢p\to p$,

where $\top$ is an appropriate constant statement (not necessarily satisfying $p⊢\top$; compare linear logic with $lolli$ for $\to$ and $1$ for $\top$).

Most kinds of logic have a notion of entailment from a list of multiple premises; then we expect entailment and the conditional to be related as in a closed multicategory.

Just as we may identify the internal and external hom in Set, so we may identify the entailment and conditional of truth values. In the $n$Lab, we tend to write this as $\Rightarrow$, a symbol that is variously used by other authors in place of $⊢$, $\models$, and $\to$.

Heyting algebras

Although Heyting algebras were first developed as a way to discuss intuitionistic logic, they appear in other contexts; but their characterstic feature is that they have an operation analogous to the conditional operation in logic, usually called Heyting implication and denoted $\to$ or $\Rightarrow$. If you use $\to$ and replace $⊢$ above with the Heyting algebra's partial order $\le$, then everything above applies.