Propositional Formulas

A concrete propositional object language over an arbitrary type of atoms.

The Common Ground library keeps its object language abstract. The Common Ground results need a concrete language so that joint consistency of theories over disjoint vocabularies can be proved and not assumed.

Connectives: atoms, the contradiction bot, negation neg, and conjunction conj. Other connectives are added when an example needs them.

This module gives syntax only. Meaning is given in SE.CommonGround.Logic.Semantics.

inductive SE.CommonGround.Logic.Formula (Atom : Type u) : Type u

Propositional formulas over the atoms Atom.

• atom {Atom : Type u} : Atom → Formula Atom

  An atomic proposition.

• bot {Atom : Type u} : Formula Atom

  The contradiction.

• neg {Atom : Type u} : Formula Atom → Formula Atom

  Negation.

• conj {Atom : Type u} : Formula Atom → Formula Atom → Formula Atom

  Conjunction.

def SE.CommonGround.Logic.language (Atom : Type u) : Logic.Language.PropositionalLanguage

The Common Ground PropositionalLanguage whose propositions are the formulas over Atom, whose negation is Formula.neg, and whose contradiction is Formula.bot.

Equations

• One or more equations did not get rendered due to their size.

theorem SE.CommonGround.Logic.language_neg {Atom : Type u} (p : Formula Atom) : (language Atom).neg p = p.neg

Negation in language Atom is Formula.neg.

theorem SE.CommonGround.Logic.language_bottom {Atom : Type u} : (language Atom).bottom = Formula.bot

The contradiction of language Atom is Formula.bot.