Assume that it is undecidable whether P=NP. Is there notation for this statement?

I have come across "¬□¬(P=NP)", which supposedly means that it is not provable, but it's clunky and not exactly the same meaning.

Reading some undecidability proofs didn't yield anything either.

  • $\begingroup$ Never seen a symbol for this. $\endgroup$
    – Wuestenfux
    Dec 1 '21 at 16:47
  • 1
    $\begingroup$ Such notation, if it exists, is not very important or common, and in most cases should not be used. Such notation is for blackboards, while the speaker says aloud the actual words. I guess you could use the notation on a T-shirt, though. $\endgroup$ Dec 1 '21 at 16:52
  • 1
    $\begingroup$ $\lnot\square\lnot(P=NP)$ actually means that P≠NP is not provable. If you want to say that P=NP is not provable you write $\lnot\square(P=NP)$. $\endgroup$
    – MJD
    Dec 4 '21 at 13:22
  • $\begingroup$ There is no symbol for undecidability. $\endgroup$
    – markvs
    Dec 4 '21 at 21:53

The notation $$\vDash C$$ is often used, in proof theory, model theory, and elsewhere, to mean that a certain system can prove the claim $C$. Sometimes the system is clear from context, and sometimes one writes something like $$\vDash_{\def\S{\mathscr S}\S} C$$ to mean that $C$ can be proved in system $\S$. ($\S\vDash C$ is sometimes used similarly.) The symbol $\not\vDash$ means “does not prove”.

To assert that $C$ is undecidable in some system $\S$, one could write $$(\not\vDash_\S C)\land(\not\vDash_\S\lnot C)$$

and in intuitionistic logics one could shorten this to $$\not\vDash_\S C\lor\lnot C$$ because proving $A\lor B$ in intuitionistic logic requires proving either $A$ or $B$. Intuitionistic logic is probably the right setting for this sort of inquiry, since “$p$ is undecidable” means exactly that neither $p$ nor $\lnot p$ can be proved.

The $\vDash$ symbol's precise meaning is rather subtle, and in different contexts it can mean different things. Depending on what kind of provability one is interested in, it might be more appropriate to use $\vdash$.

Gödel's famous incompleteness proof used the notation $\operatorname{Bew}(x)$ to mean that $x$ is provable. (The German word for “provable” is beweisbar.) One sometimes sees $\operatorname{Prov}(x)$ and similar.

The modal logic operator $\square$ can be used to mean “provable”, if that is the modality one is considering. (In other modalities, it will mean something else.) If $\square p$ means that $p$ can be proved, then $\square\lnot p$ means that $p$ can be disproved, and $\lnot\square\lnot p$ means that $p$ cannot be disproved. In modal logic $\diamond$ is nearly always an abbreviation for $\lnot\square\lnot$ so that if $\square p$ means that $p$ is provable, then $\diamond p$ is the usually weaker assertion that $p$ is not disprovable.

Wikipedia has an article on $\vDash$ (double turnstile) which will have more details and to related issues. The Stanford Encyclopedia of Philosophy article on provability logic may also be helpful.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.