The quantified modal language

ModalFormula L α: modal formulas over L with named free variables α, in mathlib's BoundedFormula basis — atomic equal/rel, falsum, imp — plus □ and named universal quantification, with ∼, ⊤, ⊓, ⊔, ex, and diamond derived exactly as for BoundedFormula. [UPSTREAM] candidate for Mathlib/ModelTheory.

inductive FirstOrder.Language.ModalFormula (L : Language) (α : Type u_2) : Type (max (max u_2 u_3) u_4)

Modal formulas over L with named free variables α: mathlib's BoundedFormula basis — atomic equal/rel, falsum, imp — plus □ and named quantification; ∼, ⊤, ⊓, ⊔, ex, and diamond are derived exactly as for BoundedFormula.

• equal {L : Language} {α : Type u_2} (t₁ t₂ : L.Term α) : L.ModalFormula α

  The proposition that two terms are equal.

• rel {L : Language} {α : Type u_2} {n : ℕ} (R : L.Relations n) (ts : Fin n → L.Term α) : L.ModalFormula α

  A relation symbol applied to terms.

• falsum {L : Language} {α : Type u_2} : L.ModalFormula α

  The contradiction.

• imp {L : Language} {α : Type u_2} (φ ψ : L.ModalFormula α) : L.ModalFormula α

  Implication.

• box {L : Language} {α : Type u_2} (φ : L.ModalFormula α) : L.ModalFormula α

  Necessity.

• all {L : Language} {α : Type u_2} (x : α) (φ : L.ModalFormula α) : L.ModalFormula α

  Universal quantification of a named variable.

@[instance_reducible]

instance FirstOrder.Language.ModalFormula.instInhabited {L : Language} {α : Type u_1} : Inhabited (L.ModalFormula α)

Equations

• FirstOrder.Language.ModalFormula.instInhabited = { default := FirstOrder.Language.ModalFormula.falsum }

@[instance_reducible]

instance FirstOrder.Language.ModalFormula.instBot {L : Language} {α : Type u_1} : Bot (L.ModalFormula α)

Equations

• FirstOrder.Language.ModalFormula.instBot = { bot := FirstOrder.Language.ModalFormula.falsum }

@[match_pattern]

def FirstOrder.Language.ModalFormula.not {L : Language} {α : Type u_1} (φ : L.ModalFormula α) : L.ModalFormula α

The negation of a modal formula.

Equations

• φ.not = φ.imp ⊥

@[instance_reducible]

instance FirstOrder.Language.ModalFormula.instTop {L : Language} {α : Type u_1} : Top (L.ModalFormula α)

Equations

• FirstOrder.Language.ModalFormula.instTop = { top := ⊥.not }

@[instance_reducible]

instance FirstOrder.Language.ModalFormula.instMin {L : Language} {α : Type u_1} : Min (L.ModalFormula α)

Equations

• FirstOrder.Language.ModalFormula.instMin = { min := fun (φ ψ : L.ModalFormula α) => (φ.imp ψ.not).not }

@[instance_reducible]

instance FirstOrder.Language.ModalFormula.instMax {L : Language} {α : Type u_1} : Max (L.ModalFormula α)

Equations

• FirstOrder.Language.ModalFormula.instMax = { max := fun (φ ψ : L.ModalFormula α) => φ.not.imp ψ }

@[match_pattern]

def FirstOrder.Language.ModalFormula.ex {L : Language} {α : Type u_1} (x : α) (φ : L.ModalFormula α) : L.ModalFormula α

Existential quantification of a named variable, derived: ∃x := ∼∀x∼.

Equations

• FirstOrder.Language.ModalFormula.ex x φ = (FirstOrder.Language.ModalFormula.all x φ.not).not

@[match_pattern]

def FirstOrder.Language.ModalFormula.diamond {L : Language} {α : Type u_1} (φ : L.ModalFormula α) : L.ModalFormula α

Possibility, derived: ◇φ := ∼□∼φ — to box what ex is to all.

Equations

• φ.diamond = φ.not.box.not

@[reducible, inline]

abbrev FirstOrder.Language.Relations.modalFormula {L : Language} {α : Type u_1} {n : ℕ} (R : L.Relations n) (ts : Fin n → L.Term α) : L.ModalFormula α

Applies a relation symbol to terms as a modal formula.

Equations

• R.modalFormula ts = FirstOrder.Language.ModalFormula.rel R ts

@[reducible, inline]

abbrev FirstOrder.Language.Relations.modalFormula₁ {L : Language} {α : Type u_1} (R : L.Relations 1) (t : L.Term α) : L.ModalFormula α

Applies a unary relation symbol to a term as a modal formula.

Equations

• R.modalFormula₁ t = FirstOrder.Language.ModalFormula.rel R ![t]