On kinds of negation 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.
 A: 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
A: On negation taken more generally:
There are two principal types of negation -firstly where the negational act applies to a whole prosretion(sentence which if asserted could be appropriately considered true or false(correct or wrong) by a judicative party ,a complex term which I define as categorising any single persons acting autonomously or(inclusive: either one or the other or both)any group of people communicating interlocutively with the intent to  consider opinions and express the publicly in a cooperative irenic and consensual manner:secondly where the negational act applies to some part(constituent) of a given prosertion . Those distinctio have  been adverted to by many good linguists  such as Jaspersen,Helmslev, Pierce and have been revived by that excellent linguist and philosopher Klima, to whom we are indebted for a brilliant  translation of  the work of Jean Buridan,an author whose work is a compendium of all that is best in Medieval linguistics and dialectic.
