Referential Fragment

A bounded referential fragment: a vocabulary and a theory over it.

Four conditions are required, so the result cannot be vacuous.

• The commitments lie in the vocabulary.
• The commitments are satisfiable.
• The commitments are nontrivial: some valuation violates them.
• The vocabulary is bounded: it lies inside a finite list of atoms.

This module says nothing about frameworks. Whether the commitments are justified as referential, that is, the referential fixing semantics of the fragment, is an obligation of the paper and of each realization. It is not proved here.

structure SE.CommonGround.Fragment.ReferentialFragment (Atom : Type u) : Type u

A bounded, satisfiable, nontrivial theory over a vocabulary.

• vocabulary : Logic.Vocabulary Atom

  The vocabulary the fragment speaks about.

• commitments : MathlibMini.Set (Logic.Formula Atom)

  The referential commitments of the fragment.

• commitments_in_vocabulary : Logic.TheoryIn self.vocabulary self.commitments

  Every commitment lies in the vocabulary.

• satisfiable : ∃ (v : Logic.Valuation Atom), Logic.Satisfies v self.commitments

  Some valuation satisfies the commitments.

• nontrivial : ∃ (v : Logic.Valuation Atom), ¬Logic.Satisfies v self.commitments

  Some valuation violates the commitments, so the fragment rules something out.

• bounded : ∃ (atoms : List Atom), ∀ (a : Atom), a ∈ self.vocabulary → a ∈ atoms

  The vocabulary lies inside a finite list of atoms.