risk = nil;

最初は，操作（証明）を行う時に必要な公理である ¹．様相論理の場合は，少し複雑なので，「未来」における例を示す．

(0) □ φ → φ

(1) ○¬φ ⇔ ¬○φ

(2) ○(φ → ψ)  ⇔ (○φ → ○ψ)

(3) □(φ → ψ)  ⇔ (□φ → □ψ)

(4) □φ  → □○φ

(5) (φ ⇒ ○φ) → (φ ⇒ □φ)

(6) φWψ ⇔ [ψ  ∨ (φ ∧ ○(φWψ))]

(7) □φ ⇒ φWψ

ここで始めて出てきた φ ⇒ ψ は，□ (φ → ψ) である．また，φ ⇔ ψ は，□ (φ ↔ ψ) である．ほとんど，意味は明らかであろう．ちなみに□, ◇, U は，上記を用いて，次の様に代数的に書くことができる．

□φ⇔(φ∧○□φ)

◇φ ⇔ (φ ∧ ○◇φ)

φUψ ⇔ ( ψ  ∨  [φ ∧ ○ (φUψ)]

次は，いつもの（証明）規則である．典型的なものを示す．

特殊化

□ φ ⊢ φ

全ての φ が真であれば，ある φ も真である．これは，公理(0)でもある．

MP (Modus Ponens)

(φ１ ∧ … ∧ φn） ⇒ ψ, □p1, …, □ φn  ⊢ □ ψ

推移律

φ ⇒ ψ, ψ ⇒ ξ  ⊢  φ ⇒ ξ

単調性

φ ⇒ ψ ⊢  □φ ⇒ □ψ

(nil)