Examples

Easy semantic examples. Nothing here is about tableaux yet.

theorem mytaut1 (p : ℕ) : tautology (~·p⋀(~·p))

theorem mytaut2 (p : ℕ) : tautology (~(~~·p)⋀(~·p))

def myModel : KripkeModel ℕ

An infinite Kripke model with ℕ as the set of states. All atomic propositions alre true at all states, and all atomic programs lead from any state to state 1.

Equations

• myModel = { val := fun (x x : ℕ) => True, Rel := fun (x x v : ℕ) => HEq v 1 }

theorem mysat (p : ℕ) : HasSat.satisfiable (·p)

theorem A2 {a : Program} : tautology (⌈a⌉⊤)

theorem A3 {a : Program} {X Y : Formula} : tautology (~(⌈a⌉X⋀Y)⋀(~(⌈a⌉X)⋀⌈a⌉Y))

theorem A4 {a b : Program} {p : ℕ} : tautology ((~(⌈a;'b⌉·p)⋀(~⌈a⌉⌈b⌉·p))⋀(~(⌈a⌉⌈b⌉·p)⋀(~⌈a;'b⌉·p)))

theorem A5 {a b : Program} {X : Formula} : tautology ((~(⌈a⋓b⌉X)⋀(~(⌈a⌉X)⋀⌈b⌉X))⋀(~((⌈a⌉X)⋀⌈b⌉X)⋀(~⌈a⋓b⌉X)))

theorem A6 (a : Program) (φ : Formula) : tautology ((~(⌈∗a⌉φ)⋀(~φ⋀⌈a⌉⌈∗a⌉φ))⋀(~(φ⋀⌈a⌉⌈∗a⌉φ)⋀(~⌈∗a⌉φ)))

theorem inductionAxiom (a : Program) (φ : Formula) : tautology (~(φ⋀⌈∗a⌉~φ⋀(~⌈a⌉φ))⋀(~⌈∗a⌉φ))

The induction axiom is semantically valid. Example 1 in [Bor88].