# Ghilbert Pax
# Interface file for propositional calculus

kind (wff)
var (wff ph ps ch)

term (wff (-. wff))
term (wff (-> wff wff))
stmt (ax-1 () () (-> ph (-> ps ph)))
stmt (ax-2 () () (-> (-> ph (-> ps ch)) (-> (-> ph ps) (-> ph ch))))
stmt (ax-3 () () (-> (-> (-. ph) (-. ps)) (-> ps ph)))
stmt (ax-mp () (ph (-> ph ps)) ps)

# Definitions, which could be split into a separate module

term (wff (<-> wff wff))
term (wff (\/ wff wff))
term (wff (/\ wff wff))
term (wff (\/\/ wff wff wff))
term (wff (/\/\ wff wff wff))
stmt (df-bi () ()
  (-. (-> (-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph)))))
          (-. (-> (-. (-> (-> ph ps) (-. (-> ps ph)))) (<-> ph ps))))))
stmt (df-or () () (<-> (\/ ph ps) (-> (-. ph) ps)))
stmt (df-an () () (<-> (/\ ph ps) (-. (-> ph (-. ps)))))
stmt (df-3or () () (<-> (\/\/ ph ps ch) (\/ (\/ ph ps) ch)))
stmt (df-3an () () (<-> (/\/\ ph ps ch) (/\ (/\ ph ps) ch)))