Mixed consequence

A mixed consequence relation ([CERvR12], Definition 17) reads the premises of a sequent Γ ⇒ Δ by one notion of satisfaction and its conclusions by another: Γ ⇒ Δ is valid when every model that p-satisfies all of Γ q-satisfies some member of Δ. With p = q this is ordinary multiple-conclusion consequence. The strict, classical and tolerant satisfaction of [CERvR12] give nine such relations, among them the non-transitive st.

The structural behaviour of a mixed relation is fixed by how its two notions compare, in the pointwise order on satisfaction relations. The relation is reflexive iff p ≤ q, closed under cut when q ≤ p, and grows as p strengthens and q weakens (Lemma 7). Negation dualizes it (Lemma 6), and the deduction theorem holds when the conditional is read at q with its antecedent at p (Lemma 10).

Main definitions

• Consequence.Satisfies p q M Γ Δ: the model M satisfies the sequent Γ ⇒ Δ.
• Consequence.MixedConsequence p q Γ Δ: every model satisfies it (Definition 17).
• Consequence.IsDual neg p' p: p' is the dual of p along neg (Definition 20).

Main results

• MixedConsequence.comap: validity transfers along model correspondences (§2.2.2).
• MixedConsequence.mono: strength monotonicity (Lemma 7).
• stdRefl_mixedConsequence_iff: reflexivity holds iff p ≤ q.
• MixedConsequence.cut, isTrans_mixedConsequence: cut, and hence transitivity, when q ≤ p.
• mixedConsequence_iff_dual: Γ ⇒ Δ is valid iff ¬Δ ⇒ ¬Γ is valid for the dual standards (Lemma 6).
• mixedConsequence_cons_cons_iff: the deduction theorem in sequent form (Lemma 10).

Implementation notes

Satisfaction notions are relations Model → Formula → Prop, ordered pointwise, so p ≤ q says that whatever a model p-satisfies it also q-satisfies. A family of notions indexed by modes, like the three of [CERvR12], enters by fixing the mode. Premises and conclusions are lists: sequents are finite, as the deduction theorem requires.

References

• P. Cobreros, P. Égré, D. Ripley and R. van Rooij, Tolerant, Classical, Strict (2012)

def Consequence.Satisfies {Model : Type u_1} {Formula : Type u_2} (p q : Model → Formula → Prop) (M : Model) (Γ Δ : List Formula) : Prop

The model M satisfies the sequent Γ ⇒ Δ with premises read by p and conclusions by q: if it p-satisfies every premise, it q-satisfies some conclusion.

Equations

• Consequence.Satisfies p q M Γ Δ = ((∀ (γ : Formula), γ ∈ Γ → p M γ) → ∃ (δ : Formula), δ ∈ Δ ∧ q M δ)

def Consequence.MixedConsequence {Model : Type u_1} {Formula : Type u_2} (p q : Model → Formula → Prop) (Γ Δ : List Formula) : Prop

Mixed consequence ([CERvR12], Definition 17): every model that p-satisfies all the premises q-satisfies some conclusion.

Equations

• Consequence.MixedConsequence p q Γ Δ = ∀ (M : Model), Consequence.Satisfies p q M Γ Δ

def Consequence.IsDual {Model : Type u_1} {Formula : Type u_2} (neg : Formula → Formula) (p' p : Model → Formula → Prop) : Prop

p' is the dual of p along neg ([CERvR12], Definition 20): a model p'-satisfies neg φ exactly when it does not p-satisfy φ.

Equations

• Consequence.IsDual neg p' p = ∀ (M : Model) (φ : Formula), p' M (neg φ) ↔ ¬p M φ

theorem Consequence.Satisfies.cut {Model : Type u_1} {Formula : Type u_2} {p q : Model → Formula → Prop} {M : Model} {Γ Δ : List Formula} {φ : Formula} (hqp : q M φ → p M φ) (h₁ : Satisfies p q M (φ :: Γ) Δ) (h₂ : Satisfies p q M Γ (φ :: Δ)) : Satisfies p q M Γ Δ

Cut at a single model: if M satisfies φ, Γ ⇒ Δ and Γ ⇒ φ, Δ, it satisfies Γ ⇒ Δ, provided q-satisfying the cut formula implies p-satisfying it.

theorem Consequence.MixedConsequence.comap {Model : Type u_1} {Formula : Type u_2} {p q : Model → Formula → Prop} {Γ Δ : List Formula} {Model' : Type u_3} {p' q' : Model' → Formula → Prop} (f : Model' → Model) (hp : ∀ (M : Model') (γ : Formula), γ ∈ Γ → p' M γ → p (f M) γ) (hq : ∀ (M : Model') (δ : Formula), δ ∈ Δ → q (f M) δ → q' M δ) (h : MixedConsequence p q Γ Δ) : MixedConsequence p' q' Γ Δ

Validity transfers along a map of models that preserves the satisfaction of the premises and reflects that of the conclusions: the model correspondences of [CERvR12], §2.2.2.

theorem Consequence.MixedConsequence.mono {Model : Type u_1} {Formula : Type u_2} {p p' q q' : Model → Formula → Prop} {Γ Δ : List Formula} (hp : p' ≤ p) (hq : q ≤ q') (h : MixedConsequence p q Γ Δ) : MixedConsequence p' q' Γ Δ

Lemma 7 of [CERvR12]: holding premises to a stronger standard, or conclusions to a weaker one, preserves validity.

theorem Consequence.MixedConsequence.weaken {Model : Type u_1} {Formula : Type u_2} {p q : Model → Formula → Prop} {Γ Γ' Δ Δ' : List Formula} (hΓ : Γ ⊆ Γ') (hΔ : Δ ⊆ Δ') (h : MixedConsequence p q Γ Δ) : MixedConsequence p q Γ' Δ'

Weakening: adding premises or conclusions preserves validity.

theorem Consequence.MixedConsequence.of_mem {Model : Type u_1} {Formula : Type u_2} {p q : Model → Formula → Prop} {Γ Δ : List Formula} {φ : Formula} (hpq : p ≤ q) (hΓ : φ ∈ Γ) (hΔ : φ ∈ Δ) : MixedConsequence p q Γ Δ

A sequent sharing a formula between its sides is valid when p ≤ q.

theorem Consequence.MixedConsequence.cut {Model : Type u_1} {Formula : Type u_2} {p q : Model → Formula → Prop} {Γ Δ : List Formula} {φ : Formula} (hqp : q ≤ p) (h₁ : MixedConsequence p q (φ :: Γ) Δ) (h₂ : MixedConsequence p q Γ (φ :: Δ)) : MixedConsequence p q Γ Δ

Cut: from φ, Γ ⇒ Δ and Γ ⇒ φ, Δ infer Γ ⇒ Δ, when q ≤ p (the form of transitivity in [CERvR12], §3.3.2).

@[simp]

theorem Consequence.mixedConsequence_singleton_right {Model : Type u_1} {Formula : Type u_2} {p q : Model → Formula → Prop} {Γ : List Formula} {φ : Formula} : MixedConsequence p q Γ [φ] ↔ ∀ (M : Model), (∀ (γ : Formula), γ ∈ Γ → p M γ) → q M φ

With a single conclusion, mixed consequence is truth preservation from p to q.

theorem Consequence.mixedConsequence_nil_singleton {Model : Type u_1} {Formula : Type u_2} {p q : Model → Formula → Prop} {φ : Formula} : MixedConsequence p q [] [φ] ↔ ∀ (M : Model), q M φ

Definition 18 of [CERvR12]: validity with no premises is q-validity.

theorem Consequence.mixedConsequence_singleton_nil {Model : Type u_1} {Formula : Type u_2} {p q : Model → Formula → Prop} {φ : Formula} : MixedConsequence p q [φ] [] ↔ ∀ (M : Model), ¬p M φ

Definition 18 of [CERvR12]: validity with no conclusions is p-unsatisfiability.

theorem Consequence.stdRefl_mixedConsequence_iff {Model : Type u_1} {Formula : Type u_2} {p q : Model → Formula → Prop} : (Std.Refl fun (φ ψ : Formula) => MixedConsequence p q [φ] [ψ]) ↔ p ≤ q

The single-premise, single-conclusion relation is reflexive exactly when p ≤ q.

theorem Consequence.isTrans_mixedConsequence {Model : Type u_1} {Formula : Type u_2} {p q : Model → Formula → Prop} (hqp : q ≤ p) : IsTrans Formula fun (φ ψ : Formula) => MixedConsequence p q [φ] [ψ]

The single-premise, single-conclusion relation is transitive when q ≤ p.

theorem Consequence.mixedConsequence_iff_dual {Model : Type u_1} {Formula : Type u_2} {p p' q q' : Model → Formula → Prop} {Γ Δ : List Formula} {neg : Formula → Formula} (hp : IsDual neg p' p) (hq : IsDual neg q' q) : MixedConsequence p q Γ Δ ↔ MixedConsequence q' p' (List.map neg Δ) (List.map neg Γ)

Lemma 6 of [CERvR12]: Γ ⇒ Δ is valid for p, q iff the negated sequent ¬Δ ⇒ ¬Γ is valid for their duals q', p'.

theorem Consequence.mixedConsequence_cons_cons_iff {Model : Type u_1} {Formula : Type u_2} {p q : Model → Formula → Prop} {Γ Δ : List Formula} {φ ψ : Formula} {imp : Formula → Formula → Formula} (himp : ∀ (M : Model), q M (imp φ ψ) ↔ p M φ → q M ψ) : MixedConsequence p q (φ :: Γ) (ψ :: Δ) ↔ MixedConsequence p q Γ (imp φ ψ :: Δ)

Lemma 10 of [CERvR12] in sequent form: a premise moves into the antecedent of a conclusion when the conditional is q-satisfied just if its antecedent's p-satisfaction brings its consequent's q-satisfaction.