Is there notation for undecidability?

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.

Solution 1:

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.