The syntax of dynamic predicate logic

The formulas of [GS91a]'s dynamic predicate logic over a first-order language L and a type V of variables. The syntax is that of ordinary predicate logic with named variables; what is dynamic is its interpretation (DPL/Semantics.lean), under which an existential quantifier binds occurrences of its variable outside its syntactic scope. The binding theory of the paper is therefore not the usual one: a formula has a set of free variables and a set of active quantifier variables, those whose existential quantifier can still bind to the right, and a quantifier's binding exceeds its scope exactly where an active quantifier variable of a left conjunct or an antecedent is free in what follows.

Main definitions

• DPL.Formula L V: the formulas, with scoped notation ¬ᵈ, ⋏, ⋎, ⟿, ∃[x], ∀[x], ≐; DPL.Formula.exs and DPL.Formula.conjs close over a list of variables and conjoin a list.
• DPL.Formula.toFormula: the same formula as a first-order formula L.Formula V.
• DPL.Formula.aqv: the active quantifier variables.
• DPL.Formula.fv: the free variables.
• DPL.Formula.IsScopeBound: every variable a quantifier binds is in its scope.

Implementation notes

Mathlib's FirstOrder.Language.BoundedFormula binds de Bruijn indices and so identifies alphabetic variants by construction. Dynamic binding links a quantifier to a named occurrence outside its scope, which that syntax cannot express, and alphabetic variants are not equivalent under the dynamic interpretation; hence the named-variable syntax here. Read statically, a formula is a mathlib formula over the same variables (toFormula), each quantifier closing its named variable through Formula.ex₁ or Formula.all₁.

All the connectives and both quantifiers of the paper's syntax are primitive, as in the paper, so that their interdefinability is a theorem about the interpretation: conjunction and the existential are not definable from the rest. top is the one addition, [Vis98]'s ⊤: the translation of an empty discourse representation structure and the scope of a bare reset need it, and x ≐ x is no substitute, since it reads x. Terms are mathlib's, so function symbols come along; the paper has variables and constants only.

The paper defines binding pairs, active quantifier occurrences, free occurrences and scope pairs as sets of occurrences, and passes to sets of variables for every fact that uses them; aqv and fv are those sets of variables. The paper gives the identity statement no clause; it is treated as an atom. IsScopeBound renders the paper's condition that the binding pairs are the scope pairs: the two differ exactly by the pairs the clauses for conjunction and implication add, an active quantifier of the left part with a free occurrence in the right. fv is a syntactic notion and overapproximates the variables the interpretation depends on, as x ≐ x shows.

References

• [GS91a]
• [Vis98]

inductive DPL.Formula (L : FirstOrder.Language) (V : Type w) : Type (max u v w)

The formulas of dynamic predicate logic over the language L with variables V.

• top {L : FirstOrder.Language} {V : Type w} : Formula L V

  The formula that is always true and changes nothing.

• rel {L : FirstOrder.Language} {V : Type w} {n : ℕ} (R : L.Relations n) (ts : Fin n → L.Term V) : Formula L V

  A relation symbol applied to terms.

• equal {L : FirstOrder.Language} {V : Type w} (t₁ t₂ : L.Term V) : Formula L V

  An identity statement.

• neg {L : FirstOrder.Language} {V : Type w} (φ : Formula L V) : Formula L V

  Negation.

• conj {L : FirstOrder.Language} {V : Type w} (φ ψ : Formula L V) : Formula L V

  Conjunction.

• disj {L : FirstOrder.Language} {V : Type w} (φ ψ : Formula L V) : Formula L V

  Disjunction.

• imp {L : FirstOrder.Language} {V : Type w} (φ ψ : Formula L V) : Formula L V

  Implication.

• ex {L : FirstOrder.Language} {V : Type w} (x : V) (φ : Formula L V) : Formula L V

  Existential quantification.

• all {L : FirstOrder.Language} {V : Type w} (x : V) (φ : Formula L V) : Formula L V

  Universal quantification.

def DPL.«term¬ᵈ_» : Lean.ParserDescr

Negation.

Equations

• DPL.«term¬ᵈ_» = Lean.ParserDescr.node `DPL.«term¬ᵈ_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "¬ᵈ") (Lean.ParserDescr.cat `term 1024))

def DPL.«term_⋏_» : Lean.TrailingParserDescr

Conjunction.

Equations

• DPL.«term_⋏_» = Lean.ParserDescr.trailingNode `DPL.«term_⋏_» 69 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋏ ") (Lean.ParserDescr.cat `term 69))

def DPL.«term_⋎_» : Lean.TrailingParserDescr

Disjunction.

Equations

• DPL.«term_⋎_» = Lean.ParserDescr.trailingNode `DPL.«term_⋎_» 68 69 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋎ ") (Lean.ParserDescr.cat `term 68))

def DPL.«term_⟿_» : Lean.TrailingParserDescr

Implication.

Equations

• DPL.«term_⟿_» = Lean.ParserDescr.trailingNode `DPL.«term_⟿_» 62 63 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟿ ") (Lean.ParserDescr.cat `term 62))

def DPL.«term∃[_]_» : Lean.ParserDescr

Existential quantification.

Equations

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

def DPL.«term∀[_]_» : Lean.ParserDescr

Universal quantification.

Equations

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

def DPL.«term_≐_» : Lean.TrailingParserDescr

An identity statement.

Equations

• DPL.«term_≐_» = Lean.ParserDescr.trailingNode `DPL.«term_≐_» 88 89 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≐ ") (Lean.ParserDescr.cat `term 89))

def DPL.Formula.exs {L : FirstOrder.Language} {V : Type w} (xs : List V) (φ : Formula L V) : Formula L V

The existential closure of a formula over a list of variables.

Equations

• DPL.Formula.exs xs φ = List.foldr DPL.Formula.ex φ xs

def DPL.Formula.conjs {L : FirstOrder.Language} {V : Type w} (φs : List (Formula L V)) : Formula L V

The conjunction of a list of formulas, top for the empty list.

Equations

• DPL.Formula.conjs φs = List.foldr DPL.Formula.conj DPL.Formula.top φs

@[simp]

theorem DPL.Formula.exs_nil {L : FirstOrder.Language} {V : Type w} (φ : Formula L V) : exs [] φ = φ

@[simp]

theorem DPL.Formula.exs_cons {L : FirstOrder.Language} {V : Type w} (x : V) (xs : List V) (φ : Formula L V) : exs (x :: xs) φ = ex x (exs xs φ)

@[simp]

theorem DPL.Formula.conjs_nil {L : FirstOrder.Language} {V : Type w} : conjs [] = top

@[simp]

theorem DPL.Formula.conjs_cons {L : FirstOrder.Language} {V : Type w} (φ : Formula L V) (φs : List (Formula L V)) : conjs (φ :: φs) = φ.conj (conjs φs)

def DPL.Formula.toFormula {L : FirstOrder.Language} {V : Type w} [DecidableEq V] : Formula L V → L.Formula V

The first-order formula with the same connectives, a quantifier binding its named variable.

Equations

• DPL.Formula.top.toFormula = ⊤
• (DPL.Formula.rel R ts).toFormula = R.formula ts
• (DPL.Formula.equal t₁ t₂).toFormula = t₁.equal t₂
• φ.neg.toFormula = φ.toFormula.not
• (φ.conj ψ).toFormula = φ.toFormula ⊓ ψ.toFormula
• (φ.disj ψ).toFormula = φ.toFormula ⊔ ψ.toFormula
• (φ.imp ψ).toFormula = φ.toFormula.imp ψ.toFormula
• (DPL.Formula.ex x_1 φ).toFormula = FirstOrder.Language.Formula.ex₁ x_1 φ.toFormula
• (DPL.Formula.all x_1 φ).toFormula = FirstOrder.Language.Formula.all₁ x_1 φ.toFormula

def DPL.Formula.aqv {L : FirstOrder.Language} {V : Type w} [DecidableEq V] : Formula L V → Finset V

The active quantifier variables are those x with an occurrence of ∃x that can still bind to the right. Only an existential contributes one, and only conjunction passes them on.

Equations

• (φ.conj ψ).aqv = φ.aqv ∪ ψ.aqv
• (DPL.Formula.ex x_1 φ).aqv = insert x_1 φ.aqv
• x✝.aqv = ∅

def DPL.Formula.fv {L : FirstOrder.Language} {V : Type w} [DecidableEq V] : Formula L V → Finset V

The free variables. In a conjunction or an implication the active quantifier variables of the left part bind into the right part.

Equations

• DPL.Formula.top.fv = ∅
• (DPL.Formula.rel R ts).fv = Finset.univ.biUnion fun (i : Fin n) => (ts i).varFinset
• (DPL.Formula.equal t₁ t₂).fv = t₁.varFinset ∪ t₂.varFinset
• φ.neg.fv = φ.fv
• (φ.conj ψ).fv = φ.fv ∪ ψ.fv \ φ.aqv
• (φ.imp ψ).fv = φ.fv ∪ ψ.fv \ φ.aqv
• (φ.disj ψ).fv = φ.fv ∪ ψ.fv
• (DPL.Formula.ex x_1 φ).fv = φ.fv.erase x_1
• (DPL.Formula.all x_1 φ).fv = φ.fv.erase x_1

def DPL.Formula.IsScopeBound {L : FirstOrder.Language} {V : Type w} [DecidableEq V] : Formula L V → Prop

A formula is scope-bound when no active quantifier variable of a left conjunct or an antecedent is free in what follows, so that every variable a quantifier binds is in its scope.

Equations

• (φ.conj ψ).IsScopeBound = (φ.IsScopeBound ∧ ψ.IsScopeBound ∧ Disjoint φ.aqv ψ.fv)
• (φ.imp ψ).IsScopeBound = (φ.IsScopeBound ∧ ψ.IsScopeBound ∧ Disjoint φ.aqv ψ.fv)
• (φ.disj ψ).IsScopeBound = (φ.IsScopeBound ∧ ψ.IsScopeBound)
• φ.neg.IsScopeBound = φ.IsScopeBound
• (DPL.Formula.ex x_1 φ).IsScopeBound = φ.IsScopeBound
• (DPL.Formula.all x_1 φ).IsScopeBound = φ.IsScopeBound
• x✝.IsScopeBound = True

@[instance_reducible]

instance DPL.Formula.decidableIsScopeBound {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (φ : Formula L V) : Decidable φ.IsScopeBound

Equations

• DPL.Formula.top.decidableIsScopeBound = isTrue trivial
• (DPL.Formula.rel R ts).decidableIsScopeBound = isTrue trivial
• (DPL.Formula.equal t₁ t₂).decidableIsScopeBound = isTrue trivial
• φ.neg.decidableIsScopeBound = φ.decidableIsScopeBound
• (DPL.Formula.ex x_1 φ).decidableIsScopeBound = φ.decidableIsScopeBound
• (DPL.Formula.all x_1 φ).decidableIsScopeBound = φ.decidableIsScopeBound
• (φ.conj ψ).decidableIsScopeBound = { decide := decide φ.IsScopeBound && decide (ψ.IsScopeBound ∧ Disjoint φ.aqv ψ.fv), reflects_decide := ⋯ }
• (φ.imp ψ).decidableIsScopeBound = { decide := decide φ.IsScopeBound && decide (ψ.IsScopeBound ∧ Disjoint φ.aqv ψ.fv), reflects_decide := ⋯ }
• (φ.disj ψ).decidableIsScopeBound = { decide := decide φ.IsScopeBound && decide ψ.IsScopeBound, reflects_decide := ⋯ }

@[simp]

theorem DPL.Formula.aqv_conj {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (φ ψ : Formula L V) : (φ.conj ψ).aqv = φ.aqv ∪ ψ.aqv

@[simp]

theorem DPL.Formula.aqv_ex {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (x : V) (φ : Formula L V) : (ex x φ).aqv = insert x φ.aqv

@[simp]

theorem DPL.Formula.fv_conj {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (φ ψ : Formula L V) : (φ.conj ψ).fv = φ.fv ∪ ψ.fv \ φ.aqv

@[simp]

theorem DPL.Formula.fv_imp {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (φ ψ : Formula L V) : (φ.imp ψ).fv = φ.fv ∪ ψ.fv \ φ.aqv

@[simp]

theorem DPL.Formula.fv_ex {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (x : V) (φ : Formula L V) : (ex x φ).fv = φ.fv.erase x

@[simp]

theorem DPL.Formula.fv_all {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (x : V) (φ : Formula L V) : (all x φ).fv = φ.fv.erase x

theorem DPL.Formula.isScopeBound_conj {L : FirstOrder.Language} {V : Type w} [DecidableEq V] {φ ψ : Formula L V} : (φ.conj ψ).IsScopeBound ↔ φ.IsScopeBound ∧ ψ.IsScopeBound ∧ Disjoint φ.aqv ψ.fv

theorem DPL.Formula.isScopeBound_imp {L : FirstOrder.Language} {V : Type w} [DecidableEq V] {φ ψ : Formula L V} : (φ.imp ψ).IsScopeBound ↔ φ.IsScopeBound ∧ ψ.IsScopeBound ∧ Disjoint φ.aqv ψ.fv