Negation and conflation

A negation on a bilattice ([Avr96] Def 2.3) is an involution that reverses the truth order and preserves the knowledge order. Its first two conditions are an InvolutiveCompl on the truth order, which already supplies the De Morgan laws and the exchange of the truth bounds; Negation adds the third. A conflation ([Fit21] §8.4) is an involution that preserves the truth order and reverses the knowledge order. It splits the carrier into consistent values a ≤ₖ −a, anticonsistent values −a ≤ₖ a and exact values −a = a, the abstract forms of the value spaces of Kleene's, Priest's and classical logic ([Fit21] Def 8.5.1). The three classes are closed under the truth operations and, when negation and conflation commute, under negation.

Main definitions

• Bilattice.Negation: the truth-lattice involution preserves the knowledge order.
• Bilattice.Conflation: the knowledge-reversing involution conf.
• Bilattice.NegConfComm: negation and conflation commute.
• Bilattice.IsConsistent, Bilattice.IsAnticonsistent, Bilattice.IsExact: the three classes; the exact values are the fixed points of conf.

Main results

• Bilattice.compl_kInf, Bilattice.compl_kSup: negation commutes with the knowledge operations.
• Bilattice.IsConsistent.inf and its kin: the closure laws ([Fit21] Prop 8.5.2), and Bilattice.IsConsistent.kInf: consistency survives knowledge meets.
• Bilattice.IsConsistent.exists_exact_kLE, Bilattice.IsExact.eq_of_kLE: interpolation and the antichain law ([Fit21] Props 8.5.3 and 8.5.4).

References

• [Avr96]
• [Fit94]
• [Fit21]

Negation

class Bilattice.Negation (B : Type u) [Compl B] [Preorder (Know B)] : Prop

A negation ([Avr96] Def 2.3): the complement ᶜ, involutive (i) and reversing the truth order (ii) by InvolutiveCompl, also preserves the knowledge order (iii).

• compl_kLE_compl {a b : B} : kLE a b → kLE aᶜ bᶜ

  Negation preserves the knowledge order ([Avr96] Def 2.3(iii)).

theorem Bilattice.compl_kLE_compl_iff {B : Type u} [LE B] [InvolutiveCompl B] [Preorder (Know B)] [Negation B] {a b : B} : kLE aᶜ bᶜ ↔ kLE a b

def Bilattice.Negation.knowIso {B : Type u} [LE B] [InvolutiveCompl B] [Preorder (Know B)] [Negation B] : Know B ≃o Know B

Negation as an automorphism of the knowledge order.

Equations

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

theorem Bilattice.compl_kInf {B : Type u} [LE B] [InvolutiveCompl B] [Lattice (Know B)] [Negation B] (a b : B) : (kInf a b)ᶜ = kInf aᶜ bᶜ

Negation commutes with the knowledge meet, (a ⊓ₖ b)ᶜ = aᶜ ⊓ₖ bᶜ (note following [Avr96] Def 2.3).

theorem Bilattice.compl_kSup {B : Type u} [LE B] [InvolutiveCompl B] [Lattice (Know B)] [Negation B] (a b : B) : (kSup a b)ᶜ = kSup aᶜ bᶜ

Negation commutes with the knowledge join, (a ⊔ₖ b)ᶜ = aᶜ ⊔ₖ bᶜ (note following [Avr96] Def 2.3).

Conflation

The knowledge-order counterpart of negation, [Fit94]'s coinage with the axioms of [Fit21].

class Bilattice.Conflation (B : Type u) [Preorder B] [Preorder (Know B)] : Type u

A conflation ([Fit21] §8.4): an involution (Con-3) that preserves the truth order (Con-2) and reverses the knowledge order (Con-1).

• conf : B → B

  The conflation operation −.

• conf_conf (a : B) : conf (conf a) = a

  Conflation is an involution (Con-3).

• conf_le_conf {a b : B} : a ≤ b → conf a ≤ conf b

  Conflation preserves the truth order (Con-2).

• conf_kLE_conf {a b : B} : kLE a b → kLE (conf b) (conf a)

  Conflation reverses the knowledge order (Con-1).

class Bilattice.NegConfComm (B : Type u) [Preorder B] [Compl B] [Preorder (Know B)] [Conflation B] : Prop

Negation and conflation commute (Con-4).

• compl_conf (a : B) : (conf a)ᶜ = conf aᶜ

theorem Bilattice.conf_le_conf_iff {B : Type u} [Preorder B] [Preorder (Know B)] [Conflation B] {a b : B} : conf a ≤ conf b ↔ a ≤ b

theorem Bilattice.conf_kLE_conf_iff {B : Type u} [Preorder B] [Preorder (Know B)] [Conflation B] {a b : B} : kLE (conf b) (conf a) ↔ kLE a b

def Bilattice.Conflation.orderIso {B : Type u} [Preorder B] [Preorder (Know B)] [Conflation B] : B ≃o B

Conflation as an automorphism of the truth order.

Equations

• Bilattice.Conflation.orderIso = { toFun := Bilattice.conf, invFun := Bilattice.conf, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem Bilattice.conf_top {B : Type u} [PartialOrder B] [Preorder (Know B)] [BoundedOrder B] [Conflation B] : conf ⊤ = ⊤

Conflation fixes the truth top, −t = t (note following [Fit21] Def 8.5.1).

@[simp]

theorem Bilattice.conf_bot {B : Type u} [PartialOrder B] [Preorder (Know B)] [BoundedOrder B] [Conflation B] : conf ⊥ = ⊥

Conflation fixes the truth bottom, −f = f.

theorem Bilattice.conf_inf {B : Type u} [Lattice B] [Preorder (Know B)] [Conflation B] (a b : B) : conf (a ⊓ b) = conf a ⊓ conf b

Conflation commutes with truth meet (CDeM-1).

theorem Bilattice.conf_sup {B : Type u} [Lattice B] [Preorder (Know B)] [Conflation B] (a b : B) : conf (a ⊔ b) = conf a ⊔ conf b

Conflation commutes with truth join (CDeM-2).

The consistent / anticonsistent / exact classes

def Bilattice.IsConsistent {B : Type u} [Preorder B] [Preorder (Know B)] [Conflation B] (a : B) : Prop

Consistent values, a ≤ₖ −a ([Fit21] Def 8.5.1): the abstract form of the Kleene value space.

Equations

• Bilattice.IsConsistent a = Bilattice.kLE a (Bilattice.conf a)

def Bilattice.IsAnticonsistent {B : Type u} [Preorder B] [Preorder (Know B)] [Conflation B] (a : B) : Prop

Anticonsistent values, −a ≤ₖ a ([Fit21] Def 8.5.1): the abstract form of Priest's LP value space.

Equations

• Bilattice.IsAnticonsistent a = Bilattice.kLE (Bilattice.conf a) a

@[reducible, inline]

abbrev Bilattice.IsExact {B : Type u} [Preorder B] [Preorder (Know B)] [Conflation B] (a : B) : Prop

Exact values, −a = a ([Fit21] Def 8.5.1): the abstract classical value space, the fixed points of conflation.

Equations

• Bilattice.IsExact a = Function.IsFixedPt Bilattice.conf a

theorem Bilattice.IsExact.isConsistent {B : Type u} [Preorder B] [Preorder (Know B)] [Conflation B] {a : B} (h : IsExact a) : IsConsistent a

theorem Bilattice.IsExact.isAnticonsistent {B : Type u} [Preorder B] [Preorder (Know B)] [Conflation B] {a : B} (h : IsExact a) : IsAnticonsistent a

@[instance_reducible]

instance Bilattice.instDecidablePredIsConsistentOfDecidableRelKLE {B : Type u} [Preorder B] [Preorder (Know B)] [Conflation B] [DecidableRel kLE] : DecidablePred IsConsistent

Equations

• Bilattice.instDecidablePredIsConsistentOfDecidableRelKLE a = Bilattice.instDecidablePredIsConsistentOfDecidableRelKLE._aux_1 a

@[instance_reducible]

instance Bilattice.instDecidablePredIsAnticonsistentOfDecidableRelKLE {B : Type u} [Preorder B] [Preorder (Know B)] [Conflation B] [DecidableRel kLE] : DecidablePred IsAnticonsistent

Equations

• Bilattice.instDecidablePredIsAnticonsistentOfDecidableRelKLE a = Bilattice.instDecidablePredIsAnticonsistentOfDecidableRelKLE._aux_1 a

theorem Bilattice.IsConsistent.inf {B : Type u} [Lattice B] [Lattice (Know B)] [IsInterlaced B] [Conflation B] {a b : B} (ha : IsConsistent a) (hb : IsConsistent b) : IsConsistent (a ⊓ b)

The consistent values are closed under truth meet ([Fit21] Prop 8.5.2).

theorem Bilattice.IsConsistent.sup {B : Type u} [Lattice B] [Lattice (Know B)] [IsInterlaced B] [Conflation B] {a b : B} (ha : IsConsistent a) (hb : IsConsistent b) : IsConsistent (a ⊔ b)

The consistent values are closed under truth join.

theorem Bilattice.IsAnticonsistent.inf {B : Type u} [Lattice B] [Lattice (Know B)] [IsInterlaced B] [Conflation B] {a b : B} (ha : IsAnticonsistent a) (hb : IsAnticonsistent b) : IsAnticonsistent (a ⊓ b)

The anticonsistent values are closed under truth meet.

theorem Bilattice.IsAnticonsistent.sup {B : Type u} [Lattice B] [Lattice (Know B)] [IsInterlaced B] [Conflation B] {a b : B} (ha : IsAnticonsistent a) (hb : IsAnticonsistent b) : IsAnticonsistent (a ⊔ b)

The anticonsistent values are closed under truth join.

theorem Bilattice.IsExact.inf {B : Type u} [Lattice B] [Lattice (Know B)] [Conflation B] {a b : B} (ha : IsExact a) (hb : IsExact b) : IsExact (a ⊓ b)

The exact values are closed under truth meet.

theorem Bilattice.IsExact.sup {B : Type u} [Lattice B] [Lattice (Know B)] [Conflation B] {a b : B} (ha : IsExact a) (hb : IsExact b) : IsExact (a ⊔ b)

The exact values are closed under truth join.

theorem Bilattice.IsConsistent.compl {B : Type u} [Preorder B] [Compl B] [Preorder (Know B)] [Negation B] [Conflation B] [NegConfComm B] {a : B} (ha : IsConsistent a) : IsConsistent aᶜ

The consistent values are closed under negation ([Fit21] Prop 8.5.2; needs Con-4).

theorem Bilattice.IsAnticonsistent.compl {B : Type u} [Preorder B] [Compl B] [Preorder (Know B)] [Negation B] [Conflation B] [NegConfComm B] {a : B} (ha : IsAnticonsistent a) : IsAnticonsistent aᶜ

The anticonsistent values are closed under negation.

theorem Bilattice.IsExact.compl {B : Type u} [Preorder B] [Compl B] [Preorder (Know B)] [Conflation B] [NegConfComm B] {a : B} (ha : IsExact a) : IsExact aᶜ

The exact values are closed under negation.

theorem Bilattice.IsConsistent.kInf {B : Type u} [Preorder B] [Lattice (Know B)] [Conflation B] {a : B} (ha : IsConsistent a) (b : B) : IsConsistent (Bilattice.kInf a b)

The consensus of a consistent value with any value is consistent ([Fit94] Theorem 9.3, there for products).

theorem Bilattice.IsConsistent.exists_exact_kLE {B : Type u} [Lattice B] [Lattice (Know B)] [IsInterlaced B] [Conflation B] {a : B} (ha : IsConsistent a) : ∃ (b : B), IsExact b ∧ kLE a b

Every consistent value is knowledge-below an exact value ([Fit21] Prop 8.5.3): a ⊔ −a is exact.

theorem Bilattice.IsAnticonsistent.exists_exact_kLE {B : Type u} [Lattice B] [Lattice (Know B)] [IsInterlaced B] [Conflation B] {a : B} (ha : IsAnticonsistent a) : ∃ (b : B), IsExact b ∧ kLE b a

Every anticonsistent value is knowledge-above an exact value ([Fit21] Prop 8.5.3): a ⊓ −a is exact.

theorem Bilattice.IsExact.eq_of_kLE {B : Type u} [Preorder B] [PartialOrder (Know B)] [Conflation B] {a b : B} (ha : IsExact a) (hb : IsExact b) (h : kLE a b) : a = b

The exact values form a knowledge-order antichain ([Fit21] Prop 8.5.4).