From DRT to predicate logic

This file translates each DRS into a FirstOrder.Language.Formula and proves that the translation is realized exactly when the DRS is verified, Kamp and Reyle's reduction of the DRS language to first-order logic in §1.5, also given by Muskens. The universe of a sub-DRS is existentially closed (closeExists, via Formula.iExs), and the antecedent of a ⇒ universally (closeForall, via Formula.iAlls). The translation of a proper DRS realizes the same way under every assignment, as truth in the model (p. 138).

Main declarations

• DRS.toFormula, Condition.toFormula: the translation into L.Formula V.
• DRS.realize_toFormula: truth of a DRS matches its first-order translation's Realize.
• DRS.realize_toFormula_of_isProper: the translation of a proper DRS is realized iff some embedding verifies the DRS.

TODO

The translation of a proper DRS is closed (p. 138), so it is an L.Sentence and Def. 1.4.6's logical consequence is mathlib's ⊨ᵇ; this needs freeVarFinset lemmas for relabel, iExs and iAlls, which mathlib lacks.

References

• [KR93]
• [Mus96]

def DRT.splitOn {V : Type w} [DecidableEq V] (U : Finset V) : V → V ⊕ ↥U

Relabel the free referents V so that those in U move to the bound side {x // x ∈ U} (and the rest stay free) — the splitting iExs/iAlls quantify over. DecidableEq V is needed only for the x ∈ U test, not by iExs/iAlls.

Equations

• DRT.splitOn U x = if h : x ∈ U then Sum.inr ⟨x, h⟩ else Sum.inl x

noncomputable def DRT.closeExists {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (U : Finset V) (φ : L.Formula V) : L.Formula V

Existentially close the referents in U within a formula over free referents V (relabel via splitOn, then Formula.iExs).

Equations

• DRT.closeExists U φ = FirstOrder.Language.Formula.iExs (↥U) (FirstOrder.Language.Formula.relabel (DRT.splitOn U) φ)

noncomputable def DRT.closeForall {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (U : Finset V) (φ : L.Formula V) : L.Formula V

Universally close the referents in U (used for the antecedent of ⇒).

Equations

• DRT.closeForall U φ = FirstOrder.Language.Formula.iAlls (↥U) (FirstOrder.Language.Formula.relabel (DRT.splitOn U) φ)

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

The translation of a DRS existentially closes its universe over the conjunction of its translated conditions (§1.5).

Equations

• DRT.DRS.toFormula { referents := U, conditions := cs } = DRT.closeExists U (DRT.Condition.toFormulaAll cs)

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

The translation of a condition closes the universe of each sub-box existentially over the conjunction of its translated conditions, and that of the antecedent of a ⇒ universally (§1.5).

Equations

• (DRT.Condition.atom a).toFormula = a.toFormula
• (DRT.Condition.eq a b).toFormula = (FirstOrder.Language.var a).equal (FirstOrder.Language.var b)
• (DRT.Condition.neg K).toFormula = (DRT.DRS.toFormula K).not
• (DRT.Condition.imp { referents := Ua, conditions := ca } c).toFormula = DRT.closeForall Ua ((DRT.Condition.toFormulaAll ca).imp (DRT.DRS.toFormula c))
• (DRT.Condition.dis l r).toFormula = DRT.DRS.toFormula l ⊔ DRT.DRS.toFormula r

noncomputable def DRT.Condition.toFormulaAll {L : FirstOrder.Language} {V : Type w} [DecidableEq V] : List (Condition L V) → L.Formula V

The conjunction of a list of translated conditions.

Equations

• DRT.Condition.toFormulaAll [] = ⊤
• DRT.Condition.toFormulaAll (c :: cs) = c.toFormula ⊓ DRT.Condition.toFormulaAll cs

theorem DRT.DRS.toFormula_eq {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : K.toFormula = closeExists K.referents (Condition.toFormulaAll K.conditions)

theorem DRT.Condition.toFormulaAll_nil {L : FirstOrder.Language} {V : Type w} [DecidableEq V] : toFormulaAll [] = ⊤

theorem DRT.Condition.toFormulaAll_cons {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (c : Condition L V) (cs : List (Condition L V)) : toFormulaAll (c :: cs) = c.toFormula ⊓ toFormulaAll cs

theorem DRT.Condition.toFormula_neg {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : (neg K).toFormula = K.toFormula.not

theorem DRT.Condition.toFormula_imp {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (a c : DRS L V) : (imp a c).toFormula = closeForall a.referents ((toFormulaAll a.conditions).imp c.toFormula)

theorem DRT.Condition.toFormula_dis {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (l r : DRS L V) : (dis l r).toFormula = l.toFormula ⊔ r.toFormula

Agreement of the translation with the bespoke semantics

theorem DRT.realize_closeExists {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (U : Finset V) (φ : L.Formula V) (v : V → M) : (closeExists U φ).Realize v ↔ ∃ (v' : V → M), (∀ x ∉ U, v' x = v x) ∧ φ.Realize v'

closeExists realizes as existential quantification over embeddings that extend v on U.

theorem DRT.realize_closeForall {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (U : Finset V) (φ : L.Formula V) (v : V → M) : (closeForall U φ).Realize v ↔ ∀ (v' : V → M), (∀ x ∉ U, v' x = v x) → φ.Realize v'

closeForall realizes as universal quantification over embeddings that extend v on U.

theorem DRT.Condition.realize_toFormula {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (c : Condition L V) (v : V → M) : c.toFormula.Realize v ↔ VerifiesCondition v c

A single condition's translation realizes as VerifiesCondition.

theorem DRT.Condition.realize_toFormulaAll {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (cs : List (Condition L V)) (v : V → M) : (toFormulaAll cs).Realize v ↔ ∀ c ∈ cs, VerifiesCondition v c

A list of conditions' conjoined translation realizes as the conjunction of their realizations.

theorem DRT.DRS.realize_toFormula {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (K : DRS L V) (v : V → M) : K.toFormula.Realize v ↔ ∃ (v' : V → M), Box.Extends K v v' ∧ Verifies v' K

The translation's Realize coincides with verification (§1.5). As toFormula existentially closes the universe, the correspondence is with an embedding v' extending v over K.referents.

theorem DRT.DRS.realize_toFormula_of_isProper {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] {K : DRS L V} (hK : K.IsProper) (v : V → M) : K.toFormula.Realize v ↔ ∃ (f : V → M), Verifies f K

The translation of a proper DRS is realized under any assignment iff some embedding verifies the DRS (p. 138, Def. 1.4.5).