Quantified clauses

A quantified clause (Q R. S) is a quantifier on the tree of numbers with a restrictor and a nuclear scope, formulas of the propositional fragment whose atoms denote sets of world–individual pairs (Presupposition.QuantifiedClause). Its truth set is that of the nuclear scope's quantified sentence, with the restrictor and the scope read off the formulas' denotations (QuantifiedClause.truth).

A trigger of the clause sits in one argument of the quantifier, with the other argument given: in the restrictor before the scope, or in the scope after the restrictor (QuantifiedClause.Arg). Its environment is that argument together with the trigger's environment inside the argument's formula (QuantifiedClause.Env), and its meaning is the function from the gap's denotation to the clause's truth set. A good final of the clause may replace the scope after a restrictor and keeps the restrictor before a scope (QuantifiedClause.Env.SameInitialString). At a parsing point after the gap, the continuations are those of the argument's formula composed with what the good finals of the clause give the argument there: every scope at the first parsing point after a restrictor, the clause's own scope afterwards (QuantifiedClause.Env.continuations). The triggers of a clause are listed with their environments by QuantifiedClause.triggers, filling the gap of each gives back the clause (QuantifiedClause.fill_of_mem_triggers), and QuantifiedClause.occurrences lists them as occurrences with their parsing points.

Implementation notes

• A clause is the root of its sentence, so a sentence holds one quantifier, whose arguments are propositional.
• After a restrictor every predicate is a possible scope, not only those a formula denotes, as Expressivity has it.

References

• [Sch09a]
• [vB84]

structure Presupposition.QuantifiedClause (Atom : Type u_4) : Type u_4

A quantified clause (Q R. S): a quantifier with a restrictor and a nuclear scope, formulas whose atoms denote sets of world–individual pairs.

• quantifier : Quantifier.NumberTree

  The quantifier.

• restrictor : Formula Atom

  The restrictor.

• scope : Formula Atom

  The nuclear scope.

inductive Presupposition.QuantifiedClause.Arg (Atom : Type u_4) : Type u_4

The argument of a quantifier that holds a gap: the restrictor, followed by the scope S, or the scope, preceded by the restrictor R.

• restrictor {Atom : Type u_4} (S : Formula Atom) : Arg Atom
• scope {Atom : Type u_4} (R : Formula Atom) : Arg Atom

@[instance_reducible]

instance Presupposition.QuantifiedClause.instDecidableEqArg {Atom✝ : Type u_4} [DecidableEq Atom✝] : DecidableEq (Arg Atom✝)

Equations

• Presupposition.QuantifiedClause.instDecidableEqArg = Presupposition.QuantifiedClause.instDecidableEqArg.decEq

def Presupposition.QuantifiedClause.instDecidableEqArg.decEq {Atom✝ : Type u_4} [DecidableEq Atom✝] (x✝ x✝¹ : Arg Atom✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Presupposition.QuantifiedClause.instDecidableEqArg.decEq (Presupposition.QuantifiedClause.Arg.restrictor S) (Presupposition.QuantifiedClause.Arg.scope R) = isFalse ⋯
• Presupposition.QuantifiedClause.instDecidableEqArg.decEq (Presupposition.QuantifiedClause.Arg.scope R) (Presupposition.QuantifiedClause.Arg.restrictor S) = isFalse ⋯

structure Presupposition.QuantifiedClause.Env (Atom : Type u_4) : Type u_4

A quantified clause with a gap: the environment of the gap inside one argument of the quantifier.

• quantifier : Quantifier.NumberTree

  The quantifier.

• arg : Arg Atom

  The argument that holds the gap, with the other argument.

• inner : SyntacticEnvironment Atom

  The environment of the gap inside the argument's formula.

def Presupposition.QuantifiedClause.truth {Atom : Type u_1} {W : Type u_2} {E : Type u_3} (I : Atom → Set (W × E)) (c : QuantifiedClause Atom) : Set W

The truth set of a clause.

Equations

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

def Presupposition.QuantifiedClause.Arg.fill {Atom : Type u_1} (q : Quantifier.NumberTree) : Arg Atom → Formula Atom → QuantifiedClause Atom

Fill the argument that holds the gap.

Equations

• Presupposition.QuantifiedClause.Arg.fill q (Presupposition.QuantifiedClause.Arg.restrictor S) x✝ = { quantifier := q, restrictor := x✝, scope := S }
• Presupposition.QuantifiedClause.Arg.fill q (Presupposition.QuantifiedClause.Arg.scope R) x✝ = { quantifier := q, restrictor := R, scope := x✝ }

def Presupposition.QuantifiedClause.Arg.truth {Atom : Type u_1} {W : Type u_2} {E : Type u_3} (I : Atom → Set (W × E)) (q : Quantifier.NumberTree) : Arg Atom → Set (W × E) → Set W

The truth set of the clause as a function of the denotation of the argument that holds the gap.

Equations

• Presupposition.QuantifiedClause.Arg.truth I q (Presupposition.QuantifiedClause.Arg.restrictor S) = Presupposition.restrictorTruth q fun (w : W) (e : E) => (w, e) ∈ Presupposition.Formula.truth I S
• Presupposition.QuantifiedClause.Arg.truth I q (Presupposition.QuantifiedClause.Arg.scope R) = Presupposition.scopeTruth q fun (w : W) (e : E) => (w, e) ∈ Presupposition.Formula.truth I R

def Presupposition.QuantifiedClause.Arg.continuations {Atom : Type u_1} {W : Type u_2} {E : Type u_3} (I : Atom → Set (W × E)) (q : Quantifier.NumberTree) : Arg Atom → ℕ∞ → Set (Set (W × E) → Set W)

The meanings that the good finals of the clause at parsing point n give the argument that holds the gap: at the first parsing point after a restrictor one for every scope, as Expressivity has it, and otherwise the clause's own.

Equations

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

theorem Presupposition.QuantifiedClause.Arg.truth_mem_continuations {Atom : Type u_1} {W : Type u_2} {E : Type u_3} (I : Atom → Set (W × E)) (q : Quantifier.NumberTree) (n : ℕ∞) (a : Arg Atom) : truth I q a ∈ continuations I q a n

theorem Presupposition.QuantifiedClause.Arg.antitone_continuations {Atom : Type u_1} {W : Type u_2} {E : Type u_3} (I : Atom → Set (W × E)) (q : Quantifier.NumberTree) (a : Arg Atom) : Antitone (continuations I q a)

theorem Presupposition.QuantifiedClause.Arg.continuations_top {Atom : Type u_1} {W : Type u_2} {E : Type u_3} (I : Atom → Set (W × E)) (q : Quantifier.NumberTree) (a : Arg Atom) : continuations I q a ⊤ = {truth I q a}

inductive Presupposition.QuantifiedClause.Arg.SameInitialString {Atom : Type u_1} : Arg Atom → Arg Atom → Prop

Two arguments have the same initial string when a good final may turn one into the other: it may replace the scope after a restrictor, and keeps the restrictor before a scope.

• restrictor {Atom : Type u_1} (S S' : Formula Atom) : (Arg.restrictor S).SameInitialString (Arg.restrictor S')
• scope {Atom : Type u_1} (R : Formula Atom) : (Arg.scope R).SameInitialString (Arg.scope R)

def Presupposition.QuantifiedClause.Env.fill {Atom : Type u_1} (k : Env Atom) (X : Formula Atom) : QuantifiedClause Atom

Fill the gap of a clause's environment.

Equations

• k.fill X = Presupposition.QuantifiedClause.Arg.fill k.quantifier k.arg (k.inner.fill X)

def Presupposition.QuantifiedClause.Env.truth {Atom : Type u_1} {W : Type u_2} {E : Type u_3} (I : Atom → Set (W × E)) (k : Env Atom) (d : Set (W × E)) : Set W

The meaning of a clause's environment as a function of the gap's denotation.

Equations

• Presupposition.QuantifiedClause.Env.truth I k d = Presupposition.QuantifiedClause.Arg.truth I k.quantifier k.arg (Presupposition.SyntacticEnvironment.truth I k.inner d)

theorem Presupposition.QuantifiedClause.Env.truth_fill {Atom : Type u_1} {W : Type u_2} {E : Type u_3} (I : Atom → Set (W × E)) (k : Env Atom) (X : Formula Atom) : QuantifiedClause.truth I (k.fill X) = truth I k (Formula.truth I X)

def Presupposition.QuantifiedClause.Env.continuations {Atom : Type u_1} {W : Type u_2} {E : Type u_3} (I : Atom → Set (W × E)) (k : Env Atom) (n : ℕ∞) : Set (Set (W × E) → Set W)

The continuations at parsing point n after the gap of a clause: the parsing point of the argument's formula inside the argument's good finals there, the argument coming after the items that follow the gap inside it.

Equations

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

theorem Presupposition.QuantifiedClause.Env.truth_mem_continuations {Atom : Type u_1} {W : Type u_2} {E : Type u_3} (I : Atom → Set (W × E)) (n : ℕ∞) (k : Env Atom) : truth I k ∈ continuations I k n

theorem Presupposition.QuantifiedClause.Env.antitone_continuations {Atom : Type u_1} {W : Type u_2} {E : Type u_3} (I : Atom → Set (W × E)) (k : Env Atom) : Antitone (continuations I k)

A later parsing point consults fewer continuations.

@[simp]

theorem Presupposition.QuantifiedClause.Env.continuations_top {Atom : Type u_1} {W : Type u_2} {E : Type u_3} (I : Atom → Set (W × E)) (k : Env Atom) : continuations I k ⊤ = {truth I k}

def Presupposition.QuantifiedClause.Env.occurrence {Atom : Type u_1} {W : Type u_2} {E : Type u_3} (I : Atom → Set (W × E)) (k : Env Atom) (p p' : Atom) : Occurrence W (Set (W × E))

The occurrence of the trigger trigger p p' at the gap of a clause, with the continuations of its parsing points.

Equations

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

def Presupposition.QuantifiedClause.Env.SameInitialString {Atom : Type u_1} (k k' : Env Atom) : Prop

SameInitialString k k' holds when k' keeps the material of k before the gap and replaces what follows it: the quantifier, a restrictor before the scope, and the material before the gap inside the argument stay.

Equations

• k.SameInitialString k' = (k.quantifier = k'.quantifier ∧ k.arg.SameInitialString k'.arg ∧ k.inner.SameInitialString k'.inner)

def Presupposition.QuantifiedClause.Env.TriggerFreeFinal {Atom : Type u_1} (k : Env Atom) : Prop

The material after the gap of a clause's environment contains no trigger: none after the gap inside the argument, and none in a scope after a restrictor.

Equations

• k.TriggerFreeFinal = (k.inner.TriggerFreeFinal ∧ ∀ (S : Presupposition.Formula Atom), k.arg = Presupposition.QuantifiedClause.Arg.restrictor S → S.triggers = [])

def Presupposition.QuantifiedClause.triggers {Atom : Type u_1} (c : QuantifiedClause Atom) : List (Env Atom × Atom × Atom)

The triggers of a clause, each with its environment and its presupposition and assertion.

Equations

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

theorem Presupposition.QuantifiedClause.fill_of_mem_triggers {Atom : Type u_1} {c : QuantifiedClause Atom} {o : Env Atom × Atom × Atom} (h : o ∈ c.triggers) : o.1.fill (Formula.trigger o.2.1 o.2.2) = c

def Presupposition.QuantifiedClause.occurrences {Atom : Type u_1} {W : Type u_2} {E : Type u_4} (I : Atom → Set (W × E)) (c : QuantifiedClause Atom) : List (Occurrence W (Set (W × E)))

The occurrences of the triggers of a quantified clause.

Equations

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

theorem Presupposition.QuantifiedClause.forall_mem_occurrences {Atom : Type u_1} {W : Type u_2} {E : Type u_4} {I : Atom → Set (W × E)} {c : QuantifiedClause Atom} {P : Occurrence W (Set (W × E)) → Prop} : (∀ o ∈ occurrences I c, P o) ↔ ∀ t ∈ c.triggers, P (Env.occurrence I t.1 t.2.1 t.2.2)