Let’s add a further observation to what I was saying about Brandom in the last post. I remarked that and (as defined) coincide in a classical framework. But now let be the usual consequence relation in an intuitionistic logic, and let be the derived consequence relation defined as described.
Suppose D + p is in Inc. Then, by definition, D + p q for any q, so we have, intuitionistically, D not-p. So inituitionistically again, D + not-not-p q for any q. That is to say D + not-not-p is in Inc. Hence, again by definition, not-not-p p (while of course we don’t have not-not-p p). So here and peel apart.
I don’t know whether there are cases of more impoverished frameworks which lack classical negation but where and do coincide. That’s why I was asking about general conditions for getting the round-trip equivalence. But my conjecture is that the impoverished cases aren’t going to be very interesting. (I’m encouraged in that thought by an email from Warren Goldfarb!)
Where does this leave us? It looks as though and typically peel apart, unless we are already assuming a classical framework (or something hobbled and uninteresting). So how could an inferentialist justify the claim that is the relation that matters (the one to feature in inferentialist definitions of connectives, etc.)? The suspicion must be that Brandom’s very idea of starting from Inc and defining a consequence relation from it will just beg the question against e.g. the intuitionist. But is that right?