Condition of possibility = Co-Implication

Question

^{Sorry, but I do not know another place to post this question.}

Condition of possibility is an important philosophical concept. Naively, this concept could be formally defined this way:

$q$ is a condition of possibility of $p$ iff $\neg q$ implies $\neg > p$

the latter being equivalent with $p$ implies $q$. When we write $\hookrightarrow$ for is a condition of possibility of and $\rightarrow$ for implies we get

$q \hookrightarrow p$ iff $p > \rightarrow q$.

So, condition of possibility is something like co-implication.

My question is: While in category theory many concepts and co-concepts are treated as strongly related (= inter-definable) but each in its own right, and while in logic many concepts are treated as strongly related (= inter-definable) but each in its own right:

Why wasn't the - philosophically important - concept of condition of possibility found worthy of being named and treated in its own right in (formal) logic?

Answer 1

As the other responders noted, you first need to find a formal setting in which what you call "co-implication" is operationally distinguished from ordinary implication. Emil Jeřábek mentioned non-commutative logic, but I think he might have been too quick to dismiss its relevance here. In particular the "right implication" of non-commutative logic (distinguished from "left implication") seems to me to be what you are looking for.

Have a look at the "Lambek calculus" (introduced by Lambek in his 1958 article, The mathematics of sentence structure), and then more generally "categorial type logics". Lambek's original motivation was syntax of natural language, but eventually (following a 1983 essay by van Benthem) this idea became part of a general approach to relating natural language syntax and semantics.

Answer 2

You've answered your own question, in a way: if $q \hookrightarrow p$ is equivalent to $p \to q$ then the difference is only a matter of notation.

You say that

in logic many concepts are treated as strongly related (= inter-definable) but each in its own right

but until Gentzen came along it was common in logic (and still is in some quarters) to try to get away with as few connectives as possible, so that even implication would be defined away and not studied in its own right. In intuitionistic logic, however, and in non-classical logics generally, it's often not possible to define the usual connectives in terms of a subset of them. In particular, $p \to q$ intuitionistically implies $q \hookrightarrow p$ but not the other way round.

I don't know if intuitionistic logicians have studied $\lnot q \to \lnot p$ as a connective in its own right. I do know, though, that I wouldn't call it co-implication -- I would reserve that name for the category-theoretic dual, say $\leftarrow$, of implication, where $p \mapsto p \leftarrow q$ would be the left adjoint to $r \mapsto q \vee r$. Andrzej Filinski studied this in Declarative continuations (LNCS, I forget which volume) and Tristan Crolard in Subtractive logic (Theoretical Computer Science, again I don't have the exact reference to hand).

Answer 3

This “co-implication” is just ordinary implication where you plugged in different variables. If you take a compound formula $A\to B$, there is no telling whether it is an instance of $p\to q$ or $q\to p$. It is thus rather pointless to treat these two formally as separate connectives, unless you are in an unusual context (such as when you for whatever reason need a name for all $16$ binary Boolean connectives). There are more than one implication connectives in e.g. some substructural logics (in particular, non-commutative), but these have a different motivation.

Answer 4

(Maybe I'm missing something, but) $\neg q$ implies $\neg p$ is studied, as the contrapositive of implication (where that is $p$ implies $q$). Contraposition (the inference from $p$ implies $q$ to its contrapositive) is valid in a huge range of logics; I think in general that equivalences like this are studied in terms of validity, not in terms of the individual concepts, because historically the goal of logic has been to formalize reasoning. Contraposition itself is taken for granted because it is so often valid -- you have to really work at it to find a logic that doesn't validate the positive form. (I think some fuzzy logics don't validate it, but they don't even validate modus ponens. The reverse inference is easier to get rid of, e.g. it isn't valid in intuitionistic logic.)

(Also, wouldn't "co-implication" be more naturally the negation of implication, not its contrapositive?)