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

This file formalizes Fitting's generalization of the strict/tolerant logic ST of Cobreros, Égré, Ripley and van Rooij from three values to any logical bilattice: an interlaced bilattice with negation and conflation together with a prime bifilter of designated values, after Arieli and Avron. 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 SignType, 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.
• Sequent satisfaction is Consequence.Satisfies, with strict and tolerant designation as the premise and conclusion standards, so local cut in C⟨B, F⟩ is Consequence.Satisfies.cut. STValid and CValid are Consequence.MixedConsequence over the anticonsistent and exact valuations and LValid over all valuations into L, so Propositions 8.7.2 and 8.9.3 are pairs of model correspondences (Consequence.MixedConsequence.comap).
• 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

• [Fit21]
• [CERvR12]
• [AA96]
• [AA98]
• [Bel77]
• [Pri79]

Formulas and valuations (§8.6)

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

Formulas over propositional letters built by conjunction, disjunction and negation, with no implication ([Fit21] Def 8.6.1).

• 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] [InvolutiveCompl B] (v : α → B) : Fml α → B

The extension of a valuation to formulas ([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 = (Fitting2021.Fml.eval v φ)ᶜ

theorem Fitting2021.eval_isExact {B : Type u_1} {α : Type u_2} [Lattice B] [InvolutiveCompl B] [Lattice (Bilattice.Know 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] [InvolutiveCompl B] [Lattice (Bilattice.Know B)] [Bilattice.Conflation B] [Bilattice.NegConfComm B] [Bilattice.Negation B] [Bilattice.IsInterlaced 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] [InvolutiveCompl B] [Lattice (Bilattice.Know B)] [Bilattice.Negation B] [Bilattice.IsInterlaced 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 is a proper nonempty subset that is a prime filter for both the truth and the knowledge lattice operations ([Fit21] Def 8.6.5). It generalizes the designated values {t, ⊤} of FOUR ([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

@[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 ([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 (§8.7)

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

A value is strictly designated when it is 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

A value is tolerantly designated when it is 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] [InvolutiveCompl B] [Lattice (Bilattice.Know B)] [Bilattice.Conflation B] (F : PrimeBifilter B) (v : α → B) (Γ Δ : List (Fml α)) : Prop

A valuation satisfies a sequent strict-to-tolerantly when some conclusion is tolerantly designated whenever every premise is strictly designated.

Equations

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

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

A valuation satisfies a sequent strictly on both sides.

Equations

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

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

ST⟨B, F⟩ validity is the mixed consequence of strict premises and tolerant conclusions over the valuations into the anticonsistent values ([Fit21] Def 8.7.1).

Equations

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

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

C⟨B, F⟩ validity is the consequence of strict premises and strict conclusions over the valuations into the exact values ([Fit21] Def 8.7.1).

Equations

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

@[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 = { decide := decide (a ∈ F) && decide (Bilattice.IsExact a), reflects_decide := ⋯ }

@[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

• Fitting2021.instDecidableTolerantlyDesignatedOfMemPrimeBifilterOfDecidablePredIsAnticonsistent a = { decide := decide (a ∈ F) && decide (Bilattice.IsAnticonsistent a), reflects_decide := ⋯ }

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

The strict/tolerant and classical logics of a logical bilattice validate exactly the same sequents ([Fit21] Prop 8.7.2). Both directions are model correspondences (Consequence.MixedConsequence.comap). Every exact valuation is anticonsistent, and below every anticonsistent valuation lies an exact one on which strict premises agree, whose strict conclusions lift along knowledge-monotonicity and bifilter closure. This replaces the chapter's contraposition.

theorem Fitting2021.cut_cSatisfies {B : Type u_1} {α : Type u_2} [Lattice B] [InvolutiveCompl B] [Lattice (Bilattice.Know 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⟩, so a valuation satisfying both premises of a cut instance satisfies its conclusion ([Fit21] Prop 8.7.3).

theorem Fitting2021.cut_not_local_stValid {B : Type u_1} {α : Type u_2} [Lattice B] [InvolutiveCompl B] [Lattice (Bilattice.Know 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 [] []

The cut scheme fails locally in ST⟨B, F⟩ when the knowledge order is nontrivial, the ST half of [Fit21] Prop 8.7.3. 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} [Lattice L] [InvolutiveCompl L] : { x : Bilattice.Product L L // Bilattice.IsExact x } ≃o L

The exact members of L ⊙ L are the pairs ⟨a, aᶜ⟩, and under the truth order they are L ([Fit21] Prop 8.8.3).

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 holds the designated values of a logical De Morgan algebra ⟨L, D⟩, nonempty and proper as §8.2 requires ([Fit21] Def 8.9.1).

• 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} [Lattice 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} [Lattice L] [BoundedOrder L] (D : PrimeFilter L) : PrimeBifilter (Bilattice.Product L L)

D × L is a prime bifilter of L ⊙ L ([Fit21] Lemma 8.9.2).

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} [Lattice L] [BoundedOrder L] (D : PrimeFilter L) (x : Bilattice.Product L L) : x ∈ D.prod ↔ x.pro ∈ D

@[instance_reducible]

instance Fitting2021.instDecidablePredProductMemPrimeBifilterProdOfPrimeFilter {L : Type u_3} [Lattice L] [BoundedOrder 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} [Lattice L] [BoundedOrder L] [InvolutiveCompl 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} [Lattice L] [BoundedOrder L] [InvolutiveCompl 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} [Lattice L] [InvolutiveCompl L] (v : α → L) : Fml α → L

The logic ⟨L, D⟩ evaluates formulas 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} [Lattice L] [InvolutiveCompl L] (D : PrimeFilter L) (Γ Δ : List (Fml α)) : Prop

A sequent is valid in the logic ⟨L, D⟩ when designated premises entail a designated conclusion (§8.2).

Equations

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

def Fitting2021.exactVal {α : Type u_2} {L : Type u_3} [Lattice L] [InvolutiveCompl 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} [Lattice L] [InvolutiveCompl L] (v : α → L) (p : α) : Bilattice.IsExact (exactVal v p)

theorem Fitting2021.eq_exactVal_of_isExact {α : Type u_2} {L : Type u_3} [Lattice L] [InvolutiveCompl 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} [Lattice L] [InvolutiveCompl 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} [Lattice L] [InvolutiveCompl L] [BoundedOrder L] (D : PrimeFilter L) (Γ Δ : List (Fml α)) : CValid D.prod Γ Δ ↔ LValid D Γ Δ

C⟨L ⊙ L, D × L⟩ is the logic ⟨L, D⟩ ([Fit21] Prop 8.9.3). 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} [Lattice L] [InvolutiveCompl L] [BoundedOrder L] (D : PrimeFilter L) (Γ Δ : List (Fml α)) : STValid D.prod Γ Δ ↔ LValid D Γ Δ

The strict/tolerant counterpart ST⟨L ⊙ L, D × L⟩ of a logical De Morgan algebra ⟨L, D⟩ has the same consequence relation ([Fit21] Prop 8.10.1).

theorem Fitting2021.cut_not_local_prod {α : Type u_2} {L : Type u_3} [Lattice L] [InvolutiveCompl L] [BoundedOrder 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 [] []

The strict/tolerant counterpart differs at the metaconsequence level, since cut fails locally in it ([Fit21] Prop 8.10.1).

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

def Fitting2021.classicalFilter : PrimeFilter Bool

Classical logic is the 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 ([Fit21] Example 8.7.4) are {true} × Bool ([Fit21] 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} ([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}, the value space of LP ([Fit21] Example 8.7.4).

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

ST and classical logic validate the same sequents, the original collapse of [CERvR12] (via [Fit21] Example 8.7.4).

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 SignType

K3, Kleene's strong three-valued logic, is SignType with {1} designated ([Fit21] Example 8.10.3).

Equations

• Fitting2021.k3Filter = { carrier := {a : SignType | a = 1}, nonempty := Fitting2021.k3Filter._proof_4, ne_univ := Fitting2021.k3Filter._proof_5, inf_mem_iff := ⋯, sup_mem_iff := ⋯ }

@[instance_reducible]

instance Fitting2021.instDecidablePredSignTypeMemPrimeFilterK3Filter : DecidablePred fun (x : SignType) => x ∈ k3Filter

Equations

• Fitting2021.instDecidablePredSignTypeMemPrimeFilterK3Filter a = Fitting2021.instDecidablePredSignTypeMemPrimeFilterK3Filter._aux_1 a

def Fitting2021.lpFilter : PrimeFilter SignType

LP, the logic of paradox of [Pri79], is SignType with {0, 1} (Fitting's {½, 1}) designated ([Fit21] Example 8.10.4).

Equations

• Fitting2021.lpFilter = { carrier := {a : SignType | a ≠ -1}, nonempty := Fitting2021.lpFilter._proof_5, ne_univ := Fitting2021.lpFilter._proof_6, inf_mem_iff := ⋯, sup_mem_iff := ⋯ }

@[instance_reducible]

instance Fitting2021.instDecidablePredSignTypeMemPrimeFilterLpFilter : DecidablePred fun (x : SignType) => x ∈ lpFilter

Equations

• Fitting2021.instDecidablePredSignTypeMemPrimeFilterLpFilter a = { decide := !decide (a = -1), reflects_decide := ⋯ }

@[reducible, inline]

abbrev Fitting2021.NINE : Type

The bilattice NINE = SignType ⊙ SignType of Figure 4 ([Fit21] Example 8.10.3).

Equations

• Fitting2021.NINE = Bilattice.Product SignType SignType

theorem Fitting2021.nine_isExact_iff (x : NINE) : Bilattice.IsExact x ↔ x = Bilattice.Product.mk (-1) 1 ∨ x = Bilattice.Product.mk 0 0 ∨ x = Bilattice.Product.mk 1 (-1)

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

theorem Fitting2021.nine_isConsistent_iff (x : NINE) : Bilattice.IsConsistent x ↔ Bilattice.IsExact x ∨ x = Bilattice.Product.mk (-1) 0 ∨ x = Bilattice.Product.mk (-1) (-1) ∨ x = Bilattice.Product.mk 0 (-1)

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

theorem Fitting2021.nine_isAnticonsistent_iff (x : NINE) : Bilattice.IsAnticonsistent x ↔ Bilattice.IsExact x ∨ x = Bilattice.Product.mk 0 1 ∨ x = Bilattice.Product.mk 1 1 ∨ x = Bilattice.Product.mk 1 0

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

theorem Fitting2021.nine_bifilters : (∀ (x : NINE), x ∈ k3Filter.prod ↔ x = Bilattice.Product.mk 1 (-1) ∨ x = Bilattice.Product.mk 1 0 ∨ x = Bilattice.Product.mk 1 1) ∧ ∀ (x : NINE), x ∈ lpFilter.prod ↔ x = Bilattice.Product.mk 0 (-1) ∨ x = Bilattice.Product.mk 1 (-1) ∨ x = Bilattice.Product.mk 0 0 ∨ x = Bilattice.Product.mk 1 0 ∨ x = Bilattice.Product.mk 0 1 ∨ x = Bilattice.Product.mk 1 1

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

theorem Fitting2021.k3_strict_iff (x : NINE) : StrictlyDesignated k3Filter.prod x ↔ x = Bilattice.Product.mk 1 (-1)

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

theorem Fitting2021.lp_designated : (∀ (x : NINE), StrictlyDesignated lpFilter.prod x ↔ x = Bilattice.Product.mk 0 0 ∨ x = Bilattice.Product.mk 1 (-1)) ∧ ∀ (x : NINE), TolerantlyDesignated lpFilter.prod x ↔ x = Bilattice.Product.mk 1 (-1) ∨ x = Bilattice.Product.mk 0 0 ∨ x = Bilattice.Product.mk 1 0 ∨ x = Bilattice.Product.mk 0 1 ∨ x = Bilattice.Product.mk 1 1

With LP the strictly designated values are {d⊤, t} and the tolerantly designated ones {t, d⊤, ot, of, ⊤} ([Fit21] 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, with countermodel v(P) = d⊤ and v(Q) = f ([Fit21] Example 8.10.4).

def Fitting2021.fdeFilter : PrimeFilter Bilattice.FOUR

FDE is the logical De Morgan algebra FOUR under the truth order with {t, ⊤} designated ([Fit21] 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 = { decide := decide (x = Bilattice.FOUR.T) || decide (x = Bilattice.FOUR.I), reflects_decide := ⋯ }

@[reducible, inline]

abbrev Fitting2021.SIXTEEN : Type

The bilattice SIXTEEN = FOUR ⊙ FOUR of Figure 6 ([Fit21] 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 ([Fit21] 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, since ⟨⊥, ⊤⟩ and ⟨⊤, ⊥⟩ of SIXTEEN are neither consistent nor anticonsistent ([Fit21] §8.5, Example 8.10.5).