# Only one-way implication

This is a basic question about implication. In constructive logic, we have $$\Rightarrow$$ for implication and $$\Leftrightarrow$$ for bi-implication. If we want to express only one-way implication, we can perhaps have the following: $$(A\Rightarrow B)\wedge(B\not\Rightarrow A).$$ That is, $$A$$ implies $$B$$ but not vice versa. But as far as I know, $$\not\Rightarrow$$ is not a connective in the object language but is used at the metal-level. Is there any way to express $$B\not\Rightarrow A$$ in the object language? Thanks in advance!

• $B\wedge\neg A$? Nov 9, 2020 at 21:00
• Since you mention constructive logic, let me point out that, unless I've mad a mistake, $\neg(B\to A)$ is constructively equivalent to $\neg((\neg B)\lor A)$ (even though $B\to A$ is weaker than $(\neg B)\lor A)$) and also to $(\neg\neg B)\land(\neg A)$. But these are weaker than $B\land(\neg A)$. Nov 10, 2020 at 1:14
• At the meta-level, $==>$ is not used to express material implication, but logical implication : " A logically implies B iff there is no possible case in which A is true and B is false". Make sure you understand the difference between material implication and logical implication. See Seymour Lipschutz, Outline of set theory (additional chapter at the end of the book). Jun 29, 2023 at 7:56

$$\lnot (B \implies A)$$ equivalently, $$\lnot (\lnot B \lor A)$$ equivalently, $$B \land \lnot A$$

You can use material implication as

$$(P\implies Q)\iff (\lnot P \vee Q)$$

So, you can replace $$B$$ does not imply $$A$$ by $$\lnot( \lnot B \vee A)$$ or $$B \wedge \lnot A$$

If we want to express only one-way implication, we can perhaps have the following: $$(A\Rightarrow B)\wedge(B\not\Rightarrow A).$$ Is there any way to express $$B\not\Rightarrow A$$ in the object language?

It sounds like you want $$∀x(Ax→Bx)\;∧\;∃x(Bx∧¬Ax)$$ or, equivalently, $$∃y∀x\,\Big((Ax→Bx)∧By∧¬Ay\Big).$$

Notice that $$(A\to B)\wedge\color{red}{B \land\lnot A},$$ is tautologically equivalent to the simpler $$\color{red}{B \land\lnot A}.$$