Fitting (2021): The strict/tolerant idea and bilattices

This file formalizes [fitting-2021]'s generalization of the strict/tolerant logic ST of [cobreros-etal-2012] from three values to any logical bilattice: an interlaced bilattice with negation and conflation together with a prime bifilter of designated values ([arieli-avron-1996]). Over its exact values −a = a and anticonsistent values −a ≤ₖ a live two logics (Definition 8.7.1): ST⟨B, F⟩ reads premises strictly and conclusions tolerantly over anticonsistent valuations, C⟨B, F⟩ reads both strictly over exact valuations. They validate the same sequents (Proposition 8.7.2, stValid_iff_cValid), yet cut is locally valid only in the second (Proposition 8.7.3, cut_not_local_stValid).

The examples come from products L ⊙ L of De Morgan algebras: the exact values of L ⊙ L are L (Proposition 8.8.3, exactIso), D × L is a prime bifilter for every prime filter D (Lemma 8.9.2, PrimeFilter.prod), and C⟨L ⊙ L, D × L⟩ is the logic ⟨L, D⟩ itself (Proposition 8.9.3, cValid_prod_iff). Hence every logical De Morgan algebra has a strict/tolerant counterpart with the same consequence relation (Proposition 8.10.1, stValid_prod_iff): classical logic from Bool, K3 and LP from Trivalent, and FDE from FOUR (Examples 8.10.2–8.10.5).

Implementation notes

• Formulas have conjunction, disjunction and negation only (Definition 8.6.1); prime bifilters and prime filters carry the nonemptiness and properness that §8.2 requires of designated sets.
• Lemma 8.8.2, the general interlaced-bilattice route to Proposition 8.8.3, is not formalized; the proposition is proved in coordinates for the product.
• Locators use the chapter's numbering, 8.n for the preprint's §n.

References

• [fitting-2021]
• [cobreros-etal-2012]
• [arieli-avron-1996]
• [arieli-avron-1998]
• [belnap-1977]
• [priest-1979]

Formulas and valuations (§8.6)

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

Formulas over propositional letters ([fitting-2021] 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

The extension of a valuation to formulas ([fitting-2021] 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 ([fitting-2021] 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 ([fitting-2021] 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 ([fitting-2021] Prop 8.6.4).

Prime bifilters ([fitting-2021] Def 8.6.5, after [arieli-avron-1998])

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 ([fitting-2021] Def 8.6.5), generalizing the designated values {t, ⊤} of FOUR ([arieli-avron-1996], [arieli-avron-1998]).

• 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

@[instance_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 ([fitting-2021] 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 ([fitting-2021] Prop 8.6.6).

The strict/tolerant and classical logics of a logical bilattice (§8.7)

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 ([fitting-2021] 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 ([fitting-2021] 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 ([fitting-2021] 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 ([fitting-2021] 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 Γ Δ

@[instance_reducible]

instance Fitting2021.instDecidableStrictlyDesignatedOfMemPrimeBifilterOfDecidablePredIsExact {B : Type u_1} [Lattice B] [Lattice (Bilattice.Know B)] [Bilattice.Conflation B] {F : PrimeBifilter B} [DecidablePred fun (x : B) => x ∈ F] [DecidablePred Bilattice.IsExact] (a : B) : Decidable (StrictlyDesignated F a)

Equations

• Fitting2021.instDecidableStrictlyDesignatedOfMemPrimeBifilterOfDecidablePredIsExact a = Fitting2021.instDecidableStrictlyDesignatedOfMemPrimeBifilterOfDecidablePredIsExact._aux_1 a

@[instance_reducible]

instance Fitting2021.instDecidableTolerantlyDesignatedOfMemPrimeBifilterOfDecidablePredIsAnticonsistent {B : Type u_1} [Lattice B] [Lattice (Bilattice.Know B)] [Bilattice.Conflation B] {F : PrimeBifilter B} [DecidablePred fun (x : B) => x ∈ F] [DecidablePred Bilattice.IsAnticonsistent] (a : B) : Decidable (TolerantlyDesignated F a)

Equations

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

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 Γ Δ

[fitting-2021] 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, 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⟩ ([fitting-2021] Prop 8.7.3): a 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 [] []

[fitting-2021] Prop 8.7.3, the ST half: the cut scheme fails locally in ST⟨B, F⟩ when the knowledge order is nontrivial. 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.

Products of De Morgan algebras (§§8.8–8.9)

def Fitting2021.exactIso {L : Type u_3} [LatticeWithInvolution L] : { x : Bilattice.Product L L // Bilattice.IsExact x } ≃o L

[fitting-2021] Prop 8.8.3: the exact members of L ⊙ L are the pairs ⟨a, aᶜ⟩, and under the truth order they are L.

Equations

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

structure Fitting2021.PrimeFilter (L : Type u_4) [Lattice L] : Type u_4

A prime filter of L ([fitting-2021] Def 8.9.1): the designated values of a logical De Morgan algebra ⟨L, D⟩, nonempty and proper as §8.2 requires.

• carrier : Set L

  The designated values.

• nonempty : self.carrier.Nonempty
• ne_univ : self.carrier ≠ Set.univ
• inf_mem_iff {a b : L} : a ⊓ b ∈ self.carrier ↔ a ∈ self.carrier ∧ b ∈ self.carrier
• sup_mem_iff {a b : L} : a ⊔ b ∈ self.carrier ↔ a ∈ self.carrier ∨ b ∈ self.carrier

@[instance_reducible]

instance Fitting2021.instMembershipPrimeFilter {L : Type u_3} [LatticeWithInvolution L] : Membership L (PrimeFilter L)

Equations

• Fitting2021.instMembershipPrimeFilter = { mem := fun (D : Fitting2021.PrimeFilter L) (a : L) => a ∈ D.carrier }

def Fitting2021.PrimeFilter.prod {L : Type u_3} [LatticeWithInvolution L] (D : PrimeFilter L) : PrimeBifilter (Bilattice.Product L L)

[fitting-2021] Lemma 8.9.2: D × L is a prime bifilter of L ⊙ L.

Equations

• D.prod = { carrier := {x : Bilattice.Product L L | x.pro ∈ D}, nonempty := ⋯, ne_univ := ⋯, inf_mem_iff := ⋯, kInf_mem_iff := ⋯, sup_mem_iff := ⋯, kSup_mem_iff := ⋯ }

theorem Fitting2021.PrimeFilter.mem_prod_iff {L : Type u_3} [LatticeWithInvolution L] (D : PrimeFilter L) (x : Bilattice.Product L L) : x ∈ D.prod ↔ x.pro ∈ D

@[instance_reducible]

instance Fitting2021.instDecidablePredProductMemPrimeBifilterProdOfPrimeFilter {L : Type u_3} [LatticeWithInvolution L] (D : PrimeFilter L) [DecidablePred fun (x : L) => x ∈ D] : DecidablePred fun (x : Bilattice.Product L L) => x ∈ D.prod

Equations

• Fitting2021.instDecidablePredProductMemPrimeBifilterProdOfPrimeFilter D x = Fitting2021.instDecidablePredProductMemPrimeBifilterProdOfPrimeFilter._aux_1 D x

theorem Fitting2021.strictlyDesignated_prod_iff {L : Type u_3} [LatticeWithInvolution L] (D : PrimeFilter L) (x : Bilattice.Product L L) : StrictlyDesignated D.prod x ↔ x.pro ∈ D ∧ x.con = x.proᶜ

In D × L the strictly designated values are the exact pairs ⟨a, aᶜ⟩ with a ∈ D.

theorem Fitting2021.tolerantlyDesignated_prod_iff {L : Type u_3} [LatticeWithInvolution L] (D : PrimeFilter L) (x : Bilattice.Product L L) : TolerantlyDesignated D.prod x ↔ x.pro ∈ D ∧ x.proᶜ ≤ x.con

In D × L the tolerantly designated values are the anticonsistent pairs with a ∈ D.

def Fitting2021.Fml.evalL {α : Type u_2} {L : Type u_3} [LatticeWithInvolution L] (v : α → L) : Fml α → L

The logic ⟨L, D⟩: formulas evaluated in L by meet, join and the De Morgan complement.

Equations

• Fitting2021.Fml.evalL v (Fitting2021.Fml.atom p) = v p
• Fitting2021.Fml.evalL v (φ.and ψ) = Fitting2021.Fml.evalL v φ ⊓ Fitting2021.Fml.evalL v ψ
• Fitting2021.Fml.evalL v (φ.or ψ) = Fitting2021.Fml.evalL v φ ⊔ Fitting2021.Fml.evalL v ψ
• Fitting2021.Fml.evalL v φ.not = (Fitting2021.Fml.evalL v φ)ᶜ

def Fitting2021.LValid {α : Type u_2} {L : Type u_3} [LatticeWithInvolution L] (D : PrimeFilter L) (Γ Δ : List (Fml α)) : Prop

Validity in the logic ⟨L, D⟩ (§8.2): designated premises entail a designated conclusion.

Equations

• Fitting2021.LValid D Γ Δ = ∀ (v : α → L), (∀ φ ∈ Γ, Fitting2021.Fml.evalL v φ ∈ D) → ∃ ψ ∈ Δ, Fitting2021.Fml.evalL v ψ ∈ D

def Fitting2021.exactVal {α : Type u_2} {L : Type u_3} [LatticeWithInvolution L] (v : α → L) (p : α) : Bilattice.Product L L

The exact valuation of L ⊙ L a valuation in L determines, p ↦ ⟨v p, (v p)ᶜ⟩.

Equations

• Fitting2021.exactVal v p = Bilattice.Product.mk (v p) (v p)ᶜ

theorem Fitting2021.exactVal_isExact {α : Type u_2} {L : Type u_3} [LatticeWithInvolution L] (v : α → L) (p : α) : Bilattice.IsExact (exactVal v p)

theorem Fitting2021.eq_exactVal_of_isExact {α : Type u_2} {L : Type u_3} [LatticeWithInvolution L] {v : α → Bilattice.Product L L} (hv : ∀ (p : α), Bilattice.IsExact (v p)) : v = exactVal fun (p : α) => (v p).pro

Exact valuations are exactly the exactVals.

theorem Fitting2021.eval_exactVal {α : Type u_2} {L : Type u_3} [LatticeWithInvolution L] (v : α → L) (φ : Fml α) : Fml.eval (exactVal v) φ = Bilattice.Product.mk (Fml.evalL v φ) (Fml.evalL v φ)ᶜ

Evaluation in L ⊙ L along an exact valuation is evaluation in L.

theorem Fitting2021.cValid_prod_iff {α : Type u_2} {L : Type u_3} [LatticeWithInvolution L] (D : PrimeFilter L) (Γ Δ : List (Fml α)) : CValid D.prod Γ Δ ↔ LValid D Γ Δ

[fitting-2021] Prop 8.9.3: C⟨L ⊙ L, D × L⟩ is the logic ⟨L, D⟩ — the two validate the same sequents, the exact values of the product corresponding to L and (D × L) ∩ E to D.

Generating strict/tolerant examples (§8.10)

theorem Fitting2021.stValid_prod_iff {α : Type u_2} {L : Type u_3} [LatticeWithInvolution L] (D : PrimeFilter L) (Γ Δ : List (Fml α)) : STValid D.prod Γ Δ ↔ LValid D Γ Δ

[fitting-2021] Prop 8.10.1: the strict/tolerant counterpart ST⟨L ⊙ L, D × L⟩ of a logical De Morgan algebra ⟨L, D⟩ has the same consequence relation.

theorem Fitting2021.cut_not_local_prod {α : Type u_2} {L : Type u_3} [LatticeWithInvolution L] [Nontrivial L] (D : PrimeFilter L) (p : α) : ¬∀ (v : α → Bilattice.Product L L), (∀ (q : α), Bilattice.IsAnticonsistent (v q)) → STSatisfies D.prod v [Fml.atom p] [] → STSatisfies D.prod v [] [Fml.atom p] → STSatisfies D.prod v [] []

[fitting-2021] Prop 8.10.1: and it differs at the metaconsequence level — cut fails locally in the counterpart.

Examples 8.10.2–8.10.5: classical logic, K3, LP and FDE

def Fitting2021.classicalFilter : PrimeFilter Bool

Classical logic as a logical De Morgan algebra: Bool with {true} designated.

Equations

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

@[instance_reducible]

instance Fitting2021.instDecidablePredBoolMemPrimeFilterClassicalFilter : DecidablePred fun (x : Bool) => x ∈ classicalFilter

Equations

• Fitting2021.instDecidablePredBoolMemPrimeFilterClassicalFilter b = Fitting2021.instDecidablePredBoolMemPrimeFilterClassicalFilter._aux_1 b

@[reducible, inline]

abbrev Fitting2021.fourBifilter : PrimeBifilter Bilattice.FOUR

The designated values {t, ⊤} of FOUR ([fitting-2021] Example 8.7.4) are {true} × Bool ([fitting-2021] Example 8.10.2).

Equations

• Fitting2021.fourBifilter = Fitting2021.classicalFilter.prod

theorem Fitting2021.mem_fourBifilter_iff (x : Bilattice.FOUR) : x ∈ fourBifilter ↔ x = Bilattice.FOUR.T ∨ x = Bilattice.FOUR.I

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} ([fitting-2021] 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}, the value space of LP ([fitting-2021] Example 8.7.4).

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

The original collapse ([cobreros-etal-2012], via [fitting-2021] Example 8.7.4): ST and classical logic validate 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 cut fails locally in ST over FOUR.

def Fitting2021.k3Filter : PrimeFilter Trivalent

K3, Kleene's strong three-valued logic: Trivalent with {true} designated ([fitting-2021] Example 8.10.3).

Equations

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

@[instance_reducible]

instance Fitting2021.instDecidablePredTrivalentMemPrimeFilterK3Filter : DecidablePred fun (x : Trivalent) => x ∈ k3Filter

Equations

• Fitting2021.instDecidablePredTrivalentMemPrimeFilterK3Filter a = Fitting2021.instDecidablePredTrivalentMemPrimeFilterK3Filter._aux_1 a

def Fitting2021.lpFilter : PrimeFilter Trivalent

LP, Priest's logic of paradox ([priest-1979]): the same values with {½, 1} designated ([fitting-2021] Example 8.10.4).

Equations

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

@[instance_reducible]

instance Fitting2021.instDecidablePredTrivalentMemPrimeFilterLpFilter : DecidablePred fun (x : Trivalent) => x ∈ lpFilter

Equations

• Fitting2021.instDecidablePredTrivalentMemPrimeFilterLpFilter a = Fitting2021.instDecidablePredTrivalentMemPrimeFilterLpFilter._aux_1 a

@[reducible, inline]

abbrev Fitting2021.NINE : Type

The bilattice NINE = Trivalent ⊙ Trivalent of Figure 4 ([fitting-2021] Example 8.10.3).

Equations

• Fitting2021.NINE = Bilattice.Product Trivalent Trivalent

theorem Fitting2021.nine_isExact_iff (x : NINE) : Bilattice.IsExact x ↔ x = Bilattice.Product.mk Trivalent.false Trivalent.true ∨ x = Bilattice.Product.mk Trivalent.indet Trivalent.indet ∨ x = Bilattice.Product.mk Trivalent.true Trivalent.false

NINE's exact values are {f, d⊤, t} ([fitting-2021] §8.5).

theorem Fitting2021.nine_isConsistent_iff (x : NINE) : Bilattice.IsConsistent x ↔ Bilattice.IsExact x ∨ x = Bilattice.Product.mk Trivalent.false Trivalent.indet ∨ x = Bilattice.Product.mk Trivalent.false Trivalent.false ∨ x = Bilattice.Product.mk Trivalent.indet Trivalent.false

NINE's consistent values are the exact ones with {df, ⊥, dt} ([fitting-2021] §8.5).

theorem Fitting2021.nine_isAnticonsistent_iff (x : NINE) : Bilattice.IsAnticonsistent x ↔ Bilattice.IsExact x ∨ x = Bilattice.Product.mk Trivalent.indet Trivalent.true ∨ x = Bilattice.Product.mk Trivalent.true Trivalent.true ∨ x = Bilattice.Product.mk Trivalent.true Trivalent.indet

NINE's anticonsistent values are the exact ones with {of, ⊤, ot} ([fitting-2021] §8.5).

theorem Fitting2021.nine_bifilters : (∀ (x : NINE), x ∈ k3Filter.prod ↔ x = Bilattice.Product.mk Trivalent.true Trivalent.false ∨ x = Bilattice.Product.mk Trivalent.true Trivalent.indet ∨ x = Bilattice.Product.mk Trivalent.true Trivalent.true) ∧ ∀ (x : NINE), x ∈ lpFilter.prod ↔ x = Bilattice.Product.mk Trivalent.indet Trivalent.false ∨ x = Bilattice.Product.mk Trivalent.true Trivalent.false ∨ x = Bilattice.Product.mk Trivalent.indet Trivalent.indet ∨ x = Bilattice.Product.mk Trivalent.true Trivalent.indet ∨ x = Bilattice.Product.mk Trivalent.indet Trivalent.true ∨ x = Bilattice.Product.mk Trivalent.true Trivalent.true

The two prime bifilters of NINE ([fitting-2021] Examples 8.7.5 and 8.10.4): {t, ot, ⊤} from K3 and the six-element {dt, t, d⊤, ot, of, ⊤} from LP.

theorem Fitting2021.k3_strict_iff (x : NINE) : StrictlyDesignated k3Filter.prod x ↔ x = Bilattice.Product.mk Trivalent.true Trivalent.false

With K3 the strictly designated values reduce to {t}, so C⟨NINE, {1} × K3⟩ is K3 ([fitting-2021] Example 8.7.5).

theorem Fitting2021.lp_designated : (∀ (x : NINE), StrictlyDesignated lpFilter.prod x ↔ x = Bilattice.Product.mk Trivalent.indet Trivalent.indet ∨ x = Bilattice.Product.mk Trivalent.true Trivalent.false) ∧ ∀ (x : NINE), TolerantlyDesignated lpFilter.prod x ↔ x = Bilattice.Product.mk Trivalent.true Trivalent.false ∨ x = Bilattice.Product.mk Trivalent.indet Trivalent.indet ∨ x = Bilattice.Product.mk Trivalent.true Trivalent.indet ∨ x = Bilattice.Product.mk Trivalent.indet Trivalent.true ∨ x = Bilattice.Product.mk Trivalent.true Trivalent.true

With LP the strictly designated values are {d⊤, t} and the tolerantly designated ones {t, d⊤, ot, of, ⊤} ([fitting-2021] Example 8.10.4).

theorem Fitting2021.lp_explosion_fails : ¬STValid lpFilter.prod [Fml.atom true, (Fml.atom true).not] [Fml.atom false]

P, ¬P ⇒ Q fails in strict/tolerant LP as in LP: v(P) = d⊤, v(Q) = f ([fitting-2021] Example 8.10.4).

def Fitting2021.fdeFilter : PrimeFilter Bilattice.FOUR

FDE as a logical De Morgan algebra: FOUR under the truth order with {t, ⊤} designated ([fitting-2021] Example 8.10.5).

Equations

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

@[instance_reducible]

instance Fitting2021.instDecidablePredFOURMemPrimeFilterFdeFilter : DecidablePred fun (x : Bilattice.FOUR) => x ∈ fdeFilter

Equations

• Fitting2021.instDecidablePredFOURMemPrimeFilterFdeFilter x = Fitting2021.instDecidablePredFOURMemPrimeFilterFdeFilter._aux_1 x

@[reducible, inline]

abbrev Fitting2021.SIXTEEN : Type

The bilattice SIXTEEN = FOUR ⊙ FOUR of Figure 6 ([fitting-2021] Example 8.10.5).

Equations

• Fitting2021.SIXTEEN = Bilattice.Product Bilattice.FOUR Bilattice.FOUR

theorem Fitting2021.fde_stValid_iff {α : Type u_3} (Γ Δ : List (Fml α)) : STValid fdeFilter.prod Γ Δ ↔ LValid fdeFilter Γ Δ

FDE's strict/tolerant counterpart validates exactly the sequents of FDE ([fitting-2021] Example 8.10.5).

theorem Fitting2021.sixteen_neither : ¬Bilattice.IsConsistent (Bilattice.Product.mk Bilattice.FOUR.U Bilattice.FOUR.I) ∧ ¬Bilattice.IsAnticonsistent (Bilattice.Product.mk Bilattice.FOUR.U Bilattice.FOUR.I) ∧ ¬Bilattice.IsConsistent (Bilattice.Product.mk Bilattice.FOUR.I Bilattice.FOUR.U) ∧ ¬Bilattice.IsAnticonsistent (Bilattice.Product.mk Bilattice.FOUR.I Bilattice.FOUR.U)

Not every value is exact, consistent or anticonsistent: ⟨⊥, ⊤⟩ and ⟨⊤, ⊥⟩ of SIXTEEN are none ([fitting-2021] §8.5, Example 8.10.5).