Fitting 2021: strict/tolerant logics from logical bilattices

[Fit21]

[Fit21] generalizes the strict/tolerant phenomenon of [CERvR12] — ST has exactly classical logic's consequence relation yet differs at the metaconsequence level — from three truth values to any logical bilattice: an interlaced bilattice with negation and conflation together with a prime bifilter F of designated values (the designated-value theory of [AA96], [AA98]). From such a pair, two logics arise ([Fit21] Def 8.7.1): ST⟨B,F⟩ runs valuations over the anticonsistent values with strict (exact designated) premises and tolerant (anticonsistent designated) conclusions; C⟨B,F⟩ — the classical-like logic — runs valuations over the exact values.

The chapter's central results, formalized here over the Core.Logic.Bilattice substrate:

• stValid_iff_cValid ([Fit21] Prop 8.7.2): ST⟨B,F⟩ and C⟨B,F⟩ validate exactly the same sequents. (Both directions are proved directly: right-to-left builds an exact valuation knowledge-below the given anticonsistent one by the interpolation lemma and transports along knowledge-monotonicity, rather than contraposing as in the chapter.)
• cut_cSatisfies / cut_not_local_stValid ([Fit21] Prop 8.7.3): the cut scheme is locally valid in C⟨B,F⟩ but fails in ST⟨B,F⟩ — the two logics differ at the metaconsequence level. The countermodel sends a letter to the knowledge top: designated and anticonsistent but not exact.
• the FOUR instance ([Fit21] Example 8.7.4): FOUR's exact values are {F, T}, its anticonsistent values {F, T, I}, and {T, I} is a prime bifilter; the resulting pair is the original [CERvR12] ST alongside classical logic, so the collapse and the cut failure specialize to the classic case.

The §8.8–8.10 extension — every non-distributive logical De Morgan algebra generates a strict/tolerant counterpart via the product L ⊙ L — remains TODO; its bilattice ingredients (Product, the diagonal Negation instance, factor recovery) are already in the substrate.

inductive Fitting2021.Fml (α : Type u_3) : Type u_3

Formulas over propositional letters ([Fit21] Def 8.6.1): conjunction, disjunction, negation — no implication.

• atom {α : Type u_3} (p : α) : Fml α
• and {α : Type u_3} (φ ψ : Fml α) : Fml α
• or {α : Type u_3} (φ ψ : Fml α) : Fml α
• not {α : Type u_3} (φ : Fml α) : Fml α

def Fitting2021.Fml.eval {B : Type u_1} {α : Type u_2} [Lattice B] [Lattice (Bilattice.Know B)] [Bilattice.Negation B] (v : α → B) : Fml α → B

Valuation extension ([Fit21] Def 8.6.2).

Equations

• Fitting2021.Fml.eval v (Fitting2021.Fml.atom p) = v p
• Fitting2021.Fml.eval v (φ.and ψ) = Fitting2021.Fml.eval v φ ⊓ Fitting2021.Fml.eval v ψ
• Fitting2021.Fml.eval v (φ.or ψ) = Fitting2021.Fml.eval v φ ⊔ Fitting2021.Fml.eval v ψ
• Fitting2021.Fml.eval v φ.not = Bilattice.neg (Fitting2021.Fml.eval v φ)

theorem Fitting2021.eval_isExact {B : Type u_1} {α : Type u_2} [Lattice B] [Lattice (Bilattice.Know B)] [Bilattice.Negation B] [Bilattice.Conflation B] [Bilattice.NegConfComm B] {v : α → B} (hv : ∀ (p : α), Bilattice.IsExact (v p)) (φ : Fml α) : Bilattice.IsExact (Fml.eval v φ)

Exact valuations evaluate to exact values ([Fit21] Prop 8.6.3).

theorem Fitting2021.eval_isAnticonsistent {B : Type u_1} {α : Type u_2} [Lattice B] [Lattice (Bilattice.Know B)] [Bilattice.Negation B] [Bilattice.Conflation B] [Bilattice.NegConfComm B] [Bilattice.Interlaced B] {v : α → B} (hv : ∀ (p : α), Bilattice.IsAnticonsistent (v p)) (φ : Fml α) : Bilattice.IsAnticonsistent (Fml.eval v φ)

Anticonsistent valuations evaluate to anticonsistent values ([Fit21] Prop 8.6.3).

theorem Fitting2021.eval_kLE_eval {B : Type u_1} {α : Type u_2} [Lattice B] [Lattice (Bilattice.Know B)] [Bilattice.Negation B] [Bilattice.Interlaced B] {v w : α → B} (h : ∀ (p : α), Bilattice.kLE (v p) (w p)) (φ : Fml α) : Bilattice.kLE (Fml.eval v φ) (Fml.eval w φ)

Evaluation is knowledge-monotone in the valuation ([Fit21] Prop 8.6.4).

Prime bifilters ([Fit21] Def 8.6.5, after [AA98])

structure Fitting2021.PrimeBifilter (B : Type u_3) [Lattice B] [Lattice (Bilattice.Know B)] : Type u_3

A prime bifilter: a proper nonempty subset that is a prime filter for both the truth and the knowledge lattice operations ([Fit21] Def 8.6.5, generalizing the designated values {t, ⊤} of FOUR per [AA96], [AA98]).

• carrier : Set B

  The designated values.

• nonempty : self.carrier.Nonempty
• ne_univ : self.carrier ≠ Set.univ
• inf_mem_iff {a b : B} : a ⊓ b ∈ self.carrier ↔ a ∈ self.carrier ∧ b ∈ self.carrier
• kInf_mem_iff {a b : B} : Bilattice.kInf a b ∈ self.carrier ↔ a ∈ self.carrier ∧ b ∈ self.carrier
• sup_mem_iff {a b : B} : a ⊔ b ∈ self.carrier ↔ a ∈ self.carrier ∨ b ∈ self.carrier
• kSup_mem_iff {a b : B} : Bilattice.kSup a b ∈ self.carrier ↔ a ∈ self.carrier ∨ b ∈ self.carrier

@[implicit_reducible]

instance Fitting2021.instMembershipPrimeBifilter {B : Type u_1} [Lattice B] [Lattice (Bilattice.Know B)] : Membership B (PrimeBifilter B)

Equations

• Fitting2021.instMembershipPrimeBifilter = { mem := fun (F : Fitting2021.PrimeBifilter B) (a : B) => a ∈ F.carrier }

theorem Fitting2021.PrimeBifilter.mem_of_kLE {B : Type u_1} [Lattice B] [Lattice (Bilattice.Know B)] (F : PrimeBifilter B) {a b : B} (ha : a ∈ F) (h : Bilattice.kLE a b) : b ∈ F

Prime bifilters are upward closed in the knowledge order ([Fit21] Prop 8.6.6).

theorem Fitting2021.PrimeBifilter.mem_of_le {B : Type u_1} [Lattice B] [Lattice (Bilattice.Know B)] (F : PrimeBifilter B) {a b : B} (ha : a ∈ F) (h : a ≤ b) : b ∈ F

Prime bifilters are upward closed in the truth order ([Fit21] Prop 8.6.6).

The strict/tolerant and classical logics of a logical bilattice

def Fitting2021.StrictlyDesignated {B : Type u_1} [Lattice B] [Lattice (Bilattice.Know B)] [Bilattice.Conflation B] (F : PrimeBifilter B) (a : B) : Prop

Strictly designated: designated and exact ([Fit21] Def 8.7.1).

Equations

• Fitting2021.StrictlyDesignated F a = (a ∈ F ∧ Bilattice.IsExact a)

def Fitting2021.TolerantlyDesignated {B : Type u_1} [Lattice B] [Lattice (Bilattice.Know B)] [Bilattice.Conflation B] (F : PrimeBifilter B) (a : B) : Prop

Tolerantly designated: designated and anticonsistent ([Fit21] Def 8.7.1).

Equations

• Fitting2021.TolerantlyDesignated F a = (a ∈ F ∧ Bilattice.IsAnticonsistent a)

def Fitting2021.STSatisfies {B : Type u_1} {α : Type u_2} [Lattice B] [Lattice (Bilattice.Know B)] [Bilattice.Negation B] [Bilattice.Conflation B] (F : PrimeBifilter B) (v : α → B) (Γ Δ : List (Fml α)) : Prop

A valuation satisfies a sequent strict-to-tolerantly: if every premise is strictly designated, some conclusion is tolerantly designated.

Equations

• Fitting2021.STSatisfies F v Γ Δ = ((∀ φ ∈ Γ, Fitting2021.StrictlyDesignated F (Fitting2021.Fml.eval v φ)) → ∃ ψ ∈ Δ, Fitting2021.TolerantlyDesignated F (Fitting2021.Fml.eval v ψ))

def Fitting2021.CSatisfies {B : Type u_1} {α : Type u_2} [Lattice B] [Lattice (Bilattice.Know B)] [Bilattice.Negation B] [Bilattice.Conflation B] (F : PrimeBifilter B) (v : α → B) (Γ Δ : List (Fml α)) : Prop

A valuation satisfies a sequent strictly on both sides.

Equations

• Fitting2021.CSatisfies F v Γ Δ = ((∀ φ ∈ Γ, Fitting2021.StrictlyDesignated F (Fitting2021.Fml.eval v φ)) → ∃ ψ ∈ Δ, Fitting2021.StrictlyDesignated F (Fitting2021.Fml.eval v ψ))

def Fitting2021.STValid {B : Type u_1} {α : Type u_2} [Lattice B] [Lattice (Bilattice.Know B)] [Bilattice.Negation B] [Bilattice.Conflation B] (F : PrimeBifilter B) (Γ Δ : List (Fml α)) : Prop

ST⟨B,F⟩ validity ([Fit21] Def 8.7.1): over valuations into the anticonsistent values, strict premises entail a tolerant conclusion.

Equations

• Fitting2021.STValid F Γ Δ = ∀ (v : α → B), (∀ (p : α), Bilattice.IsAnticonsistent (v p)) → Fitting2021.STSatisfies F v Γ Δ

def Fitting2021.CValid {B : Type u_1} {α : Type u_2} [Lattice B] [Lattice (Bilattice.Know B)] [Bilattice.Negation B] [Bilattice.Conflation B] (F : PrimeBifilter B) (Γ Δ : List (Fml α)) : Prop

C⟨B,F⟩ validity ([Fit21] Def 8.7.1): over valuations into the exact values, strict premises entail a strict conclusion.

Equations

• Fitting2021.CValid F Γ Δ = ∀ (v : α → B), (∀ (p : α), Bilattice.IsExact (v p)) → Fitting2021.CSatisfies F v Γ Δ

theorem Fitting2021.stValid_iff_cValid {B : Type u_1} {α : Type u_2} [Lattice B] [Lattice (Bilattice.Know B)] [Bilattice.Negation B] [Bilattice.Conflation B] [Bilattice.Interlaced B] [Bilattice.NegConfComm B] (F : PrimeBifilter B) (Γ Δ : List (Fml α)) : STValid F Γ Δ ↔ CValid F Γ Δ

[Fit21] Prop 8.7.2: the strict/tolerant and classical logics of a logical bilattice validate exactly the same sequents. Right-to-left replaces the chapter's contraposition: given an anticonsistent valuation, choose an exact valuation knowledge-below it (interpolation), win there classically, and transport the witness up along knowledge-monotonicity and bifilter closure.

theorem Fitting2021.cut_cSatisfies {B : Type u_1} {α : Type u_2} [Lattice B] [Lattice (Bilattice.Know B)] [Bilattice.Negation B] [Bilattice.Conflation B] (F : PrimeBifilter B) {Γ Δ : List (Fml α)} {A : Fml α} {v : α → B} (h₁ : CSatisfies F v (A :: Γ) Δ) (h₂ : CSatisfies F v Γ (A :: Δ)) : CSatisfies F v Γ Δ

Cut is locally valid in C⟨B,F⟩ ([Fit21] Prop 8.7.3): any valuation satisfying both premises of a cut instance satisfies its conclusion.

theorem Fitting2021.cut_not_local_stValid {B : Type u_1} {α : Type u_2} [Lattice B] [Lattice (Bilattice.Know B)] [Bilattice.Negation B] [Bilattice.Conflation B] [BoundedOrder (Bilattice.Know B)] (F : PrimeBifilter B) (p : α) (hbt : ⊥ ≠ ⊤) : ¬∀ (v : α → B), (∀ (q : α), Bilattice.IsAnticonsistent (v q)) → STSatisfies F v [Fml.atom p] [] → STSatisfies F v [] [Fml.atom p] → STSatisfies F v [] []

[Fit21] Prop 8.7.3, ST half: the cut scheme fails locally in ST⟨B,F⟩ (for a nontrivial knowledge order). The countermodel sends a letter to the knowledge top — designated and anticonsistent, but not exact — so both cut premises hold while the empty conclusion fails.

The FOUR instance ([Fit21] Example 8.7.4)

Belnap's FOUR with the designated values {t, ⊤} is the paradigm logical bilattice: its exact values are the classical {F, T}, its anticonsistent values {F, T, I} (Priest's LP space), and the resulting logic pair is the original strict/tolerant logic of [CERvR12] alongside classical logic.

@[implicit_reducible]

instance Fitting2021.instConflationFOUR : Bilattice.Conflation Bilattice.FOUR

Boolean-complement conflation makes FOUR a bilattice with conflation.

Equations

• Fitting2021.instConflationFOUR = { conf := Bilattice.FOUR.conf, conf_conf := Fitting2021.four_conf_conf✝, conf_le_conf := ⋯, conf_kLE_conf := ⋯ }

instance Fitting2021.instNegConfCommFOUR : Bilattice.NegConfComm Bilattice.FOUR

Negation and conflation commute on FOUR.

theorem Fitting2021.four_isExact_iff (x : Bilattice.FOUR) : Bilattice.IsExact x ↔ x = Bilattice.FOUR.F ∨ x = Bilattice.FOUR.T

FOUR's exact values are the classical {F, T} ([Fit21] Example 8.7.4).

theorem Fitting2021.four_isAnticonsistent_iff (x : Bilattice.FOUR) : Bilattice.IsAnticonsistent x ↔ x = Bilattice.FOUR.F ∨ x = Bilattice.FOUR.T ∨ x = Bilattice.FOUR.I

FOUR's anticonsistent values are {F, T, I} — Priest's LP value space ([Fit21] Example 8.7.4).

def Fitting2021.fourBifilter : PrimeBifilter Bilattice.FOUR

The designated values {t, ⊤} of FOUR form a prime bifilter ([Fit21] Example 8.7.4; the designated-value choice of [AA96]).

Equations

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

theorem Fitting2021.four_stValid_iff_cValid {α : Type u_3} (Γ Δ : List (Fml α)) : STValid fourBifilter Γ Δ ↔ CValid fourBifilter Γ Δ

The original strict/tolerant collapse ([CERvR12], via [Fit21] Example 8.7.4): over FOUR with designated {t, ⊤}, ST and classical logic validate exactly the same sequents.

theorem Fitting2021.four_cut_not_local {α : Type u_3} (p : α) : ¬∀ (v : α → Bilattice.FOUR), (∀ (q : α), Bilattice.IsAnticonsistent (v q)) → STSatisfies fourBifilter v [Fml.atom p] [] → STSatisfies fourBifilter v [] [Fml.atom p] → STSatisfies fourBifilter v [] []

And the pair separates at the metaconsequence level: cut fails locally in ST over FOUR.