A modal logic operator representing necessity or provability in formal logic and mathematical proofs.
