TeXipedia

Diamond

Represents a diamond-shaped operator commonly used in modal logic and mathematical proofs.

Overview

Serves as a fundamental symbol in modal logic, temporal logic, and formal reasoning systems where it typically denotes possibility or future-tense operators.

  • Essential in formal specifications and verification of computer programs
  • Frequently appears in philosophical logic and mathematical discourse
  • Often paired with its dual operator (box) in modal logical expressions
  • Used in formal proofs to indicate potentially true statements or future states

Examples

Modal logic operator expressing 'it is possible that'

◊p→¬□¬p\Diamond p \rightarrow \neg\Box\neg p 
\Diamond p \rightarrow \neg\Box\neg p

Expressing possibility in temporal logic

◊(x>0)∧◊(x<0)\Diamond(x > 0) \land \Diamond(x < 0) 
\Diamond(x > 0) \land \Diamond(x < 0)

Formal specification with eventually operator

p→◊qp \rightarrow \Diamond q 
p \rightarrow \Diamond q