Expressing "does not imply''

Question

In ordinary discourse, when we say that "$A$ implies $B$", we shall formalize it by writing the following: $$A\rightarrow B$$ But when we say that "$A$ does not imply $B$", we cannot formalize it as the following: $$\neg(A\rightarrow B)$$ Because by material implication, we have the following equivalences for the second formula: $$\neg(A\rightarrow B)\Longleftrightarrow\neg(\neg A\vee B)\Longleftrightarrow A\wedge\neg B$$ But the ordinary meaning of the sentence "$A$ does not imply $B$" is that $B$ does not follow from $A$: if $A$ is true, $B$ is either false or undecidable. I wonder how "$A$ does not imply $B$" is formally expressed in the object language (not at the meta-level). Thanks!

Answer 1

The formalization of a sentence in ordinary discourse claiming that "$A$ implies $B$" or "$A$ does not imply $B$" is outside the languages of propositional or first-order or higher-order logic. It is in the language of logical consequences, which roughly consists of pairs of (sets of)$-$propositional of first-order or higher-order$-$formulas.

When we use the expression "$A$ does not imply $B$" in ordinary discourse, we can mean two distinct things:

1. $\models \lnot (A \to B)$, which means that $\lnot (A \to B)$ is a valid (or provable) formula. This amounts to say $\models A \land \lnot B$, i.e. every structure satisfies $A$ but not $B$.

2. $A \not \models B$, which means that $B$ is not a logical consequence of (or is not provable from) $A$, so there exists a structure where $A$ is true and $B$ is false. This amounts to say $\not \models A \to B$.

The difference is essentially whether we mean "not" as part of the language of propositional logic, or as a negation of the relation of logical consequence. Usually, the intended meaning is 2.

Note that meaning 1 is stronger than meaning 2, in the sense that, given the formulas $A$ and $B$, if Point 1 holds then in particular Point 2 holds.

Answer 2

There is a way to express it in the object language, using modal operators. "$A$ implies $B$" in English often means "$⬜(A⇒B)$", which can be interpreted as "we can justify that $A⇒B$". So "$A$ does not imply $B$" in natural language often means "$¬⬜(A⇒B)$". Note that $¬⬜(A⇒B)$ does not imply $⬜¬(A⇒B)$, because it may be that both $¬⬜(A⇒B)$ and $¬⬜¬(A⇒B)$ hold.

For example, $x,y∈ℝ$ and $x≤y$ do not imply $x<y$, equivalently $¬⬜( x,y∈ℝ∧x≤y ⇒ x<y )$. And this is not equivalent to $⬜¬( x,y∈ℝ∧x≤y ⇒ x<y )$, which can be interpreted as "we can justify that $x,y∈ℝ$ and $x≤y$ and $x≥y$" (which is clearly nonsense).

There is in fact a connection between this formalization of English "implies" and meta-logic: This "$⬜$" can be taken as the provability operator from provability logic (where "$⬜$" is given a higher precedence than other logical operators), and so "$⬜(A⇒B)$" does in fact express "$⊢A⇒B$" internally, and is stronger than "$⬜A⇒⬜B$" (which expresses "$(⊢A)⇒(⊢B)$" internally. A distinguishing example is that PA (Peano Arithmetic) proves $⬜(¬⬜{⊥})⇒⬜{⊥}$ but (we strongly believe) does not prove $⬜(¬⬜{⊥}⇒⊥)$ (where "$⬜Q$" can be expressed in PA using Godel coding).