Forcerar inte

Tecknet läses ”forcerar inte”.

Till exempel läses w ⊮ P som ”tillståndet w forcerar inte påståendet P”. En Kripkemodell beskriver möjliga tillstånd och deras relationer matematiskt. Reglerna anger vilka påståenden som gäller i varje tillstånd. Här uppfyller P inte dessa villkor i w. Snedstrecket negerar relationen mellan w och P; det är inte en del av P.

Skillnaden är viktig i intuitionistisk logik, där tillstånd kan representera växande information. P behöver inte vara fastställt i det aktuella tillståndet men kan bli det i ett senare. För att forcera ”inte P” måste P förbli ofastställt i alla nåbara senare tillstånd, även det aktuella. ”Forcerar inte P” och ”forcerar negationen av P” är alltså olika påståenden.