In the Stanford Encyclopedia of Philosophy article “Negation”, among much else, a summary of negation as impossibility and unecessity is given. This view of negation requires some sort of relational semantics similar to that for Intuitionistic Logic or Modal Logic. SEP credits Ripley (2009) for introducing this view of negation. The definitions for the impossibility and unnecessity operators follow respectively:
$\mathcal M, \mathit w \vDash \sim P$ iff for all $\mathit v$ such that $\mathit w R \mathit v$, $\mathcal M, \mathit v \not \vDash P$
$\mathcal M, \mathit w \vDash \neg P$ iff there is a $\mathit v$ such that $\mathit w R \mathit v$ and $\mathcal M, \mathit v \not \vDash P$ where $\mathit R$ is the accessibility relation between states, $\mathcal M$ is a model and $\mathit w, \mathit v$ are states.
As far as I know, the only logics that consider how these negations interact includes another kind of accessibility relation “$\le$” which is defined as a partial order. I am interested in a simpler approach that basically enriches the semantics for Intuitionism with these negation operators. That is, I’m not interested in defining a second relation, and I would assume the Heredity Principle, i.e. that if some atomic formula is verified at some state $\mathit w$ then it is verified at any state accessible from $\mathit w$. Is it known if this treatment of unnecessity and impossibility operators already exists? I’ve been able to verify that if $\mathit R$ is reflexive and transitive, then a unique double negation elimination holds, namely $\vDash \sim \neg P \implies P$. Further I’ve verified that LEM holds for $\neg$ but not for $\sim$, that $\neg P \land \neg \neg P$ is not a contradiction, and that Pierce’s Law does not hold. Further, I’ve verified that Classical Logic is obtained by making $\mathit R$ reflexive and Euclidean. If anyone has seen this or can recommend literature that is similar, I’d be grateful.
Edit: in the literature that I’ve seen, these operators go by “impossibility” and “unnecessity”, but I think “refutability” and “unprovability” are more natural since this logic is meant to be an enrichment of Intuitionism.
Negation is fundamental in what is most often called theory theory of Logic ,a study which I prefer to categorise as Dialectic, the name used traditionally among Greeks, Romans and all the many brilliant dialecticians of medieval and premodern times- I need only mention a few greats- Plato, Aristotle, Chrysippius, Abelard, Occam, Buridan, Albert of Saxony and finally and possibly the greatest and most learned of them all, the German phenomenon of learning and intelligence , Leibnitz who could justly say: " je ne meprise presque rien"(I am interested in almost everything) In short I fully agree with. We are in total syncatathetic accord, the only slight difference being that my approach is from a slightly different angle,one which categorically rejects the principle of the excluded middle as incompatible with dialectic which I conceive of as the art and science of correct argumentative dialogue.
All those thinkers were certainly aware of the two forms of negation ascribed to the writer whom I thank for rousing me from my rather sceptical slumbers and inspiring me to write this reply What I am doing now in replying to hersh(he or she) is an exemplification of dialectic, the art of persuasive argument in which some person in some form of dialectical exchange though the medium of language,spoken or written seeks to convince hisher(his or her) hermeneutic agency (interpretor/s) with regard to "something" which hersh is propounding which they may accept(assent to),or reject in one or other of two ways,to wit, absolutely, where the lector(or auditor) as judicative party contraposits the contention of the author of the dialectical proference , by dianoetic (mental) activity concluding to be false(wrong, untrue) and is mentally disposed to assert the contradictory opposite prosertion (positive or negative linguistic expression) in relation to what the author of the discursive discourse has asserted . Clearly,however, the judicative party may not contraposit the proposition proferred by the exponent : hersh may regard the opinion laid down as no definitely and categorically wrong : hersh may dissent from the expressed opinion, regarding as not established by the argument proferred by the exponent and thus for the time being considering the opinion as neither proved nor disproved ,a proposition as yet undecided by the criteria of the judicative in that particular dialectical episode but capable of being decided either way in some future dialectical episode given better information and better arguments