Fitting (1994): Kleene's three valued logics and their children

Fitting shows that Kleene's strong three-valued logic is the consistent part x ≤ₖ −x of Belnap's FOUR, and that the guard connective P : Q, which is Q if P is at least true and ⊥ otherwise, extends Belnap's logic so that Kleene's weak logic and the asymmetric Lisp logic become definable there (Definition 5.1). Both generalize to Ginsberg's product bilattices L ⊙ L, where the guard is ⟨a, b⟩ : ⟨c, d⟩ = ⟨a ∧ c, a ∧ d⟩ (Definition 9.4).

The main results are the identities of Figure 4 for the guard, the closure theorems for exact and consistent values (Theorems 9.2 and 9.3, not_isExact_kTop, isConsistent_kSup), the identification of the Lisp and weak connectives on Kleene's values with SignType.meetMiddle and SignType.meetWeak, and the collapse for bilinear bilattices: an equivalence of formulas holds in L ⊙ L for a linear L iff it holds in FOUR (Theorem 10.5, equivalent_iff_four).

Implementation notes

• The product, its negation and the conflation of §§6–7 are Bilattice.Product with its Compl and Conflation instances; a De Morgan lattice is a bounded distributive lattice with an InvolutiveCompl. §3's identification of Kleene's values with the consistent part of FOUR is Trivalent.orderIsoConsistent, and the closure clauses of Theorems 9.2 and 9.3 are IsExact.inf, IsConsistent.compl and their kin; the study keeps what the substrate lacks.
• The representation theorems of §8, with their negation- and conflation-preserving refinements (Theorems 8.2 and 8.3), and the tableau system of §4 are not formalized.
• Theorem 10.5 is stated for products of linear bounded lattices; ofFour embeds FOUR by sending the Boolean coordinates to the bounds, and θ_⊤ reads it back.

References

• [Fit94]
• [Kle52]
• [Bel77]
• [Gin88]
• [Avr96]
• [Pet79]

Formulas and the semantics behind the tableaux (§4)

inductive Fitting1994.Formula (Atom : Type u_1) : Type u_1

Formulas over the bilattice connectives, namely the truth connectives and negation, consensus ⊓ₖ, gullibility ⊔ₖ, and the guard P : Q of §5.

• atom {Atom : Type u_1} : Atom → Formula Atom
• inf {Atom : Type u_1} : Formula Atom → Formula Atom → Formula Atom
• sup {Atom : Type u_1} : Formula Atom → Formula Atom → Formula Atom
• neg {Atom : Type u_1} : Formula Atom → Formula Atom
• kInf {Atom : Type u_1} : Formula Atom → Formula Atom → Formula Atom
• kSup {Atom : Type u_1} : Formula Atom → Formula Atom → Formula Atom
• guard {Atom : Type u_1} : Formula Atom → Formula Atom → Formula Atom

def Fitting1994.Formula.eval {Atom : Type u_1} {L : Type u_2} [Lattice L] (v : Atom → Bilattice.Product L L) : Formula Atom → Bilattice.Product L L

Evaluation in L ⊙ L under a valuation of the atoms (Definition 4.1).

Equations

• Fitting1994.Formula.eval v (Fitting1994.Formula.atom a) = v a
• Fitting1994.Formula.eval v (φ.inf ψ) = Fitting1994.Formula.eval v φ ⊓ Fitting1994.Formula.eval v ψ
• Fitting1994.Formula.eval v (φ.sup ψ) = Fitting1994.Formula.eval v φ ⊔ Fitting1994.Formula.eval v ψ
• Fitting1994.Formula.eval v φ.neg = (Fitting1994.Formula.eval v φ)ᶜ
• Fitting1994.Formula.eval v (φ.kInf ψ) = Bilattice.kInf (Fitting1994.Formula.eval v φ) (Fitting1994.Formula.eval v ψ)
• Fitting1994.Formula.eval v (φ.kSup ψ) = Bilattice.kSup (Fitting1994.Formula.eval v φ) (Fitting1994.Formula.eval v ψ)
• Fitting1994.Formula.eval v (φ.guard ψ) = (Fitting1994.Formula.eval v φ).guard (Fitting1994.Formula.eval v ψ)

def Fitting1994.Formula.Restricts {Atom : Type u_1} (φ ψ : Formula Atom) : Prop

X restricts Y when, under every valuation in FOUR, Y is at most true (⊥ or true) whenever X is (Definition 4.2).

Equations

• φ.Restricts ψ = ∀ (v : Atom → Bilattice.FOUR), Bilattice.kLE (Fitting1994.Formula.eval v φ) Bilattice.FOUR.T → Bilattice.kLE (Fitting1994.Formula.eval v ψ) Bilattice.FOUR.T

def Fitting1994.Formula.Requires {Atom : Type u_1} (φ ψ : Formula Atom) : Prop

X requires Y when, under every valuation in FOUR, Y is at least true (true or ⊤) whenever X is (Definition 4.2).

Equations

• φ.Requires ψ = ∀ (v : Atom → Bilattice.FOUR), Bilattice.kLE Bilattice.FOUR.T (Fitting1994.Formula.eval v φ) → Bilattice.kLE Bilattice.FOUR.T (Fitting1994.Formula.eval v ψ)

def Fitting1994.Formula.Equivalent {Atom : Type u_1} (φ ψ : Formula Atom) : Prop

X ≡ Y when the two formulas take the same value in FOUR under every valuation.

Equations

• φ.Equivalent ψ = ∀ (v : Atom → Bilattice.FOUR), Fitting1994.Formula.eval v φ = Fitting1994.Formula.eval v ψ

theorem Fitting1994.Formula.restricts_iff_requires_neg {Atom : Type u_1} (φ ψ : Formula Atom) : φ.Restricts ψ ↔ ψ.neg.Requires φ.neg

X restricts Y iff ¬Y requires ¬X (§4).

theorem Fitting1994.Formula.equivalent_iff {Atom : Type u_1} (φ ψ : Formula Atom) : φ.Equivalent ψ ↔ φ.Restricts ψ ∧ φ.Requires ψ ∧ ψ.Restricts φ ∧ ψ.Requires φ

Two formulas are equivalent iff each restricts and requires the other (§4).

The guard connective (§5)

theorem Fitting1994.guard_four (x y : Bilattice.FOUR) : Bilattice.Product.guard x y = if Bilattice.kLE Bilattice.FOUR.T x then y else Bilattice.FOUR.U

On FOUR, P : Q is Q when P is at least true and ⊥ otherwise.

theorem Fitting1994.guard_kInf_left {L : Type u_1} [DistribLattice L] (x y z : Bilattice.Product L L) : (Bilattice.kInf x y).guard z = (x ⊓ y).guard z

The Figure 4 identity (P ⊓ₖ Q) : R = (P ∧ Q) : R.

theorem Fitting1994.guard_kInf_left_eq {L : Type u_1} [DistribLattice L] (x y z : Bilattice.Product L L) : (Bilattice.kInf x y).guard z = Bilattice.kInf (x.guard z) (y.guard z)

The Figure 4 identity (P ⊓ₖ Q) : R = (P : R) ⊓ₖ (Q : R).

theorem Fitting1994.guard_kInf_left_eq_guard_guard {L : Type u_1} [DistribLattice L] (x y z : Bilattice.Product L L) : (Bilattice.kInf x y).guard z = (x.guard y).guard z

The Figure 4 identity (P ⊓ₖ Q) : R = (P : Q) : R.

theorem Fitting1994.guard_kInf_left_eq_guard_guard' {L : Type u_1} [DistribLattice L] (x y z : Bilattice.Product L L) : (Bilattice.kInf x y).guard z = x.guard (y.guard z)

The Figure 4 identity (P ⊓ₖ Q) : R = P : (Q : R).

theorem Fitting1994.guard_kSup_left {L : Type u_1} [DistribLattice L] (x y z : Bilattice.Product L L) : (Bilattice.kSup x y).guard z = (x ⊔ y).guard z

The Figure 4 identity (P ⊔ₖ Q) : R = (P ∨ Q) : R.

theorem Fitting1994.guard_kSup_left_eq {L : Type u_1} [DistribLattice L] (x y z : Bilattice.Product L L) : (Bilattice.kSup x y).guard z = Bilattice.kSup (x.guard z) (y.guard z)

The Figure 4 identity (P ⊔ₖ Q) : R = (P : R) ⊔ₖ (Q : R).

theorem Fitting1994.guard_compl {L : Type u_1} [DistribLattice L] (x y : Bilattice.Product L L) : x.guard yᶜ = (x.guard y)ᶜ

The Figure 4 identity P : ¬Q = ¬(P : Q).

theorem Fitting1994.guard_inf {L : Type u_1} [DistribLattice L] (x y z : Bilattice.Product L L) : x.guard (y ⊓ z) = x.guard y ⊓ x.guard z

The Figure 4 identity P : (Q ∧ R) = (P : Q) ∧ (P : R).

theorem Fitting1994.guard_sup {L : Type u_1} [DistribLattice L] (x y z : Bilattice.Product L L) : x.guard (y ⊔ z) = x.guard y ⊔ x.guard z

The Figure 4 identity P : (Q ∨ R) = (P : Q) ∨ (P : R).

theorem Fitting1994.guard_kInf {L : Type u_1} [DistribLattice L] (x y z : Bilattice.Product L L) : x.guard (Bilattice.kInf y z) = Bilattice.kInf (x.guard y) (x.guard z)

The Figure 4 identity P : Q ⊓ₖ R = (P : Q) ⊓ₖ (P : R).

theorem Fitting1994.guard_kSup {L : Type u_1} [DistribLattice L] (x y z : Bilattice.Product L L) : x.guard (Bilattice.kSup y z) = Bilattice.kSup (x.guard y) (x.guard z)

The Figure 4 identity P : Q ⊔ₖ R = (P : Q) ⊔ₖ (P : R).

theorem Fitting1994.kSup_guard_self {L : Type u_1} [DistribLattice L] (x y : Bilattice.Product L L) : Bilattice.kSup x (y.guard x) = x

The Figure 4 identity P ⊔ₖ (Q : P) = P.

theorem Fitting1994.kInf_guard_self {L : Type u_1} [DistribLattice L] (x y : Bilattice.Product L L) : Bilattice.kInf x (y.guard x) = y.guard x

The Figure 4 identity P ⊓ₖ (Q : P) = Q : P.

theorem Fitting1994.guard_le_guard_right {L : Type u_1} [DistribLattice L] {x y z : Bilattice.Product L L} (h : y ≤ z) : x.guard y ≤ x.guard z

The guard is truth-monotone in its second input.

theorem Fitting1994.guard_kLE_guard_of_le {L : Type u_1} [DistribLattice L] {x y z : Bilattice.Product L L} (h : x ≤ y) : Bilattice.kLE (x.guard z) (y.guard z)

In the "curious property" of the guard, P₁ ≤ₜ P₂ gives (P₁ : Q) ≤ₖ (P₂ : Q).

theorem Fitting1994.not_guard_le_guard_left : ¬∀ (x y z : Bilattice.FOUR), x ≤ y → Bilattice.Product.guard x z ≤ Bilattice.Product.guard y z

The guard is not truth-monotone in its first input, since ⊥ ≤ₜ true in FOUR while ⊥ : false = ⊥ is not below true : false = false.

Lisp and weak Kleene connectives through the guard (§5)

def Fitting1994.landL {L : Type u_1} [DistribLattice L] (x y : Bilattice.Product L L) : Bilattice.Product L L

Lisp conjunction P ∧⃗ Q = P ∧ (P : Q) (Definition 5.1), which consults the second conjunct only past the guard of the first.

Equations

• Fitting1994.landL x y = x ⊓ x.guard y

def Fitting1994.lorL {L : Type u_1} [DistribLattice L] (x y : Bilattice.Product L L) : Bilattice.Product L L

Lisp disjunction P ∨⃗ Q = P ∨ (¬P : Q) (Definition 5.1).

Equations

• Fitting1994.lorL x y = x ⊔ xᶜ.guard y

def Fitting1994.landW {L : Type u_1} [DistribLattice L] (x y : Bilattice.Product L L) : Bilattice.Product L L

Weak Kleene conjunction P ∧ʷ Q = (P ∧⃗ Q) ⊓ₖ (Q ∧⃗ P) (Definition 5.1), the consensus of the two evaluation orders.

Equations

• Fitting1994.landW x y = Bilattice.kInf (Fitting1994.landL x y) (Fitting1994.landL y x)

def Fitting1994.lorW {L : Type u_1} [DistribLattice L] (x y : Bilattice.Product L L) : Bilattice.Product L L

Weak Kleene disjunction P ∨ʷ Q = (P ∨⃗ Q) ⊓ₖ (Q ∨⃗ P) (Definition 5.1).

Equations

• Fitting1994.lorW x y = Bilattice.kInf (Fitting1994.lorL x y) (Fitting1994.lorL y x)

theorem Fitting1994.inf_eq_landL_kSup_landL {L : Type u_1} [DistribLattice L] (x y : Bilattice.Product L L) : x ⊓ y = Bilattice.kSup (landL x y) (landL y x)

Strong Kleene conjunction is the gullible combination of the two Lisp evaluations, P ∧ Q = (P ∧⃗ Q) ⊔ₖ (Q ∧⃗ P), in every product.

theorem Fitting1994.sup_eq_lorL_kSup_lorL {L : Type u_1} [DistribLattice L] (x y : Bilattice.Product L L) : x ⊔ y = Bilattice.kSup (lorL x y) (lorL y x)

Strong Kleene disjunction is the gullible combination of the two Lisp evaluations, P ∨ Q = (P ∨⃗ Q) ⊔ₖ (Q ∨⃗ P).

theorem Fitting1994.landL_toFour (a b : SignType) : landL a.toFour b.toFour = (a.meetMiddle b).toFour

On Kleene's values Lisp conjunction is the middle Kleene conjunction of [Pet79].

theorem Fitting1994.lorL_toFour (a b : SignType) : lorL a.toFour b.toFour = (a.joinMiddle b).toFour

On Kleene's values Lisp disjunction is middle Kleene disjunction.

theorem Fitting1994.landW_toFour (a b : SignType) : landW a.toFour b.toFour = (a.meetWeak b).toFour

On Kleene's values ∧ʷ is weak Kleene conjunction.

theorem Fitting1994.lorW_toFour (a b : SignType) : lorW a.toFour b.toFour = (a.joinWeak b).toFour

On Kleene's values ∨ʷ is weak Kleene disjunction.

theorem Fitting1994.meetMiddle_joinMiddle_distrib (a b c : SignType) : a.meetMiddle (b.joinMiddle c) = (a.meetMiddle b).joinMiddle (a.meetMiddle c)

Lisp conjunction distributes over Lisp disjunction on three values.

theorem Fitting1994.not_landL_lorL_distrib : ¬∀ (x y z : Bilattice.FOUR), landL x (lorL y z) = lorL (landL x y) (landL x z)

The distributivity law fails on four values, P = R = ⊤ and Q = ⊥ falsifying it.

Bilattices and the product construction (§§6–7)

theorem Fitting1994.extremal {L : Type u_1} [Lattice L] [BoundedOrder L] : Bilattice.kSup ⊤ ⊥ = Bilattice.Product.mk ⊤ ⊤ ∧ Bilattice.kInf ⊤ ⊥ = Bilattice.Product.mk ⊥ ⊥ ∧ Bilattice.Product.mk ⊤ ⊤ ⊓ Bilattice.Product.mk ⊥ ⊥ = ⊥ ∧ Bilattice.Product.mk ⊤ ⊤ ⊔ Bilattice.Product.mk ⊥ ⊥ = ⊤

The extremal identities (§6) true ⊔ₖ false = ⊤, true ⊓ₖ false = ⊥, ⊤ ∧ ⊥ = false and ⊤ ∨ ⊥ = true hold in L ⊙ L, with (⊤, ⊤) and (⊥, ⊥) the knowledge bounds.

Kleene's logics generalized (§9)

Definition 9.1's exact and consistent values are IsExact and IsConsistent, read off the coordinates by Product.isExact_iff and Product.isConsistent_iff; their closure under the truth connectives and negation (Theorems 9.2 and 9.3) is IsExact.inf, IsExact.sup, IsExact.compl, IsConsistent.inf, IsConsistent.sup and IsConsistent.compl. The guard of Definition 9.4 is guard, with its characterization in the bilattice operations guard_eq_kSup_compl.

theorem Fitting1994.not_isExact_kTop {L : Type u_1} [DistribLattice L] [BoundedOrder L] [InvolutiveCompl L] [Nontrivial L] : ¬Bilattice.IsExact (Bilattice.Product.mk ⊤ ⊤)

The knowledge top ⊤ = (⊤, ⊤) is not exact (Theorem 9.2).

theorem Fitting1994.not_isExact_kBot {L : Type u_1} [DistribLattice L] [BoundedOrder L] [InvolutiveCompl L] [Nontrivial L] : ¬Bilattice.IsExact (Bilattice.Product.mk ⊥ ⊥)

The knowledge bottom ⊥ = (⊥, ⊥) is not exact (Theorem 9.2).

theorem Fitting1994.not_isExact_kInf {L : Type u_1} [DistribLattice L] [BoundedOrder L] [InvolutiveCompl L] [Nontrivial L] : ¬Bilattice.IsExact (Bilattice.kInf ⊤ ⊥)

The exact values are not closed under ⊓ₖ, since true ⊓ₖ false = ⊥ (Theorem 9.2).

theorem Fitting1994.not_isExact_kSup {L : Type u_1} [DistribLattice L] [BoundedOrder L] [InvolutiveCompl L] [Nontrivial L] : ¬Bilattice.IsExact (Bilattice.kSup ⊤ ⊥)

The exact values are not closed under ⊔ₖ, since true ⊔ₖ false = ⊤ (Theorem 9.2).

theorem Fitting1994.isConsistent_kSup {L : Type u_1} [DistribLattice L] {x y z : Bilattice.Product L L} [InvolutiveCompl L] (hx : Bilattice.IsConsistent x) (hy : Bilattice.IsConsistent y) (hz : Bilattice.IsConsistent z) (hxz : Bilattice.kLE x z) (hyz : Bilattice.kLE y z) : Bilattice.IsConsistent (Bilattice.kSup x y)

The consistent values are closed under gullibility ⊔ₖ below a common consistent upper bound (Theorem 9.3).

theorem Fitting1994.isConsistent_guard {L : Type u_1} [DistribLattice L] {y : Bilattice.Product L L} [InvolutiveCompl L] (hy : Bilattice.IsConsistent y) (x : Bilattice.Product L L) : Bilattice.IsConsistent (x.guard y)

The guard of a consistent value is consistent (§9).

theorem Fitting1994.landL_kLE_landL {L : Type u_1} [DistribLattice L] {x y x' y' : Bilattice.Product L L} (hx : Bilattice.kLE x x') (hy : Bilattice.kLE y y') : Bilattice.kLE (landL x y) (landL x' y')

Lisp conjunction is knowledge-monotone (§9).

theorem Fitting1994.lorL_kLE_lorL {L : Type u_1} [DistribLattice L] {x y x' y' : Bilattice.Product L L} (hx : Bilattice.kLE x x') (hy : Bilattice.kLE y y') : Bilattice.kLE (lorL x y) (lorL x' y')

Lisp disjunction is knowledge-monotone (§9).

theorem Fitting1994.landW_kLE_landW {L : Type u_1} [DistribLattice L] {x y x' y' : Bilattice.Product L L} (hx : Bilattice.kLE x x') (hy : Bilattice.kLE y y') : Bilattice.kLE (landW x y) (landW x' y')

Weak conjunction is knowledge-monotone (§9).

theorem Fitting1994.lorW_kLE_lorW {L : Type u_1} [DistribLattice L] {x y x' y' : Bilattice.Product L L} (hx : Bilattice.kLE x x') (hy : Bilattice.kLE y y') : Bilattice.kLE (lorW x y) (lorW x' y')

Weak disjunction is knowledge-monotone (§9).

theorem Fitting1994.isConsistent_landL {L : Type u_1} [DistribLattice L] {x y : Bilattice.Product L L} [InvolutiveCompl L] (hx : Bilattice.IsConsistent x) (hy : Bilattice.IsConsistent y) : Bilattice.IsConsistent (landL x y)

The consistent values are closed under the four Kleene connectives (§9).

theorem Fitting1994.isConsistent_lorL {L : Type u_1} [DistribLattice L] {x y : Bilattice.Product L L} [InvolutiveCompl L] (hx : Bilattice.IsConsistent x) (hy : Bilattice.IsConsistent y) : Bilattice.IsConsistent (lorL x y)

theorem Fitting1994.isConsistent_landW {L : Type u_1} [DistribLattice L] {x y : Bilattice.Product L L} [InvolutiveCompl L] (hx : Bilattice.IsConsistent x) (hy : Bilattice.IsConsistent y) : Bilattice.IsConsistent (landW x y)

theorem Fitting1994.isConsistent_lorW {L : Type u_1} [DistribLattice L] {x y : Bilattice.Product L L} [InvolutiveCompl L] (hx : Bilattice.IsConsistent x) (hy : Bilattice.IsConsistent y) : Bilattice.IsConsistent (lorW x y)

Bilinear bilattices (§10)

def Fitting1994.Bilinear (B : Type u_1) [Preorder B] [Preorder (Bilattice.Know B)] : Prop

A bilattice is bilinear when any two members are comparable in at least one of the two orders (Definition 10.1).

Equations

• Fitting1994.Bilinear B = ∀ (x y : B), x ≤ y ∨ y ≤ x ∨ Bilattice.kLE x y ∨ Bilattice.kLE y x

theorem Fitting1994.bilinear_iff {L : Type u_1} {R : Type u_2} [PartialOrder L] [PartialOrder R] [BoundedOrder L] [BoundedOrder R] : Bilinear (Bilattice.Product L R) ↔ (∀ (a b : L), a ≤ b ∨ b ≤ a) ∧ ∀ (a b : R), a ≤ b ∨ b ≤ a

A product is bilinear iff each factor is linearly ordered (Proposition 10.2).

def Fitting1994.theta {L : Type u_1} [LinearOrder L] (a : L) (x : Bilattice.Product L L) : Bilattice.FOUR

θ_a reads a member of L ⊙ L into FOUR coordinatewise by a → x, which is true iff a ≤ x (Definition 10.3).

Equations

• Fitting1994.theta a x = Bilattice.Product.mk (decide (a ≤ x.pro)) (decide (a ≤ x.con))

theorem Fitting1994.theta_compl {L : Type u_1} [LinearOrder L] (a : L) (x : Bilattice.Product L L) : theta a xᶜ = (theta a x)ᶜ

theorem Fitting1994.theta_inf {L : Type u_1} [LinearOrder L] (a : L) (x y : Bilattice.Product L L) : theta a (x ⊓ y) = theta a x ⊓ theta a y

θ_a preserves ∧ when L is linear (Lemma 10.4).

theorem Fitting1994.theta_sup {L : Type u_1} [LinearOrder L] (a : L) (x y : Bilattice.Product L L) : theta a (x ⊔ y) = theta a x ⊔ theta a y

theorem Fitting1994.theta_kInf {L : Type u_1} [LinearOrder L] (a : L) (x y : Bilattice.Product L L) : theta a (Bilattice.kInf x y) = Bilattice.kInf (theta a x) (theta a y)

theorem Fitting1994.theta_kSup {L : Type u_1} [LinearOrder L] (a : L) (x y : Bilattice.Product L L) : theta a (Bilattice.kSup x y) = Bilattice.kSup (theta a x) (theta a y)

theorem Fitting1994.theta_guard {L : Type u_1} [LinearOrder L] (a : L) (x y : Bilattice.Product L L) : theta a (x.guard y) = Bilattice.Product.guard (theta a x) (theta a y)

theorem Fitting1994.eval_theta {L : Type u_1} [LinearOrder L] (a : L) {Atom : Type u_2} (v : Atom → Bilattice.Product L L) (φ : Formula Atom) : Formula.eval (theta a ∘ v) φ = theta a (Formula.eval v φ)

θ_a is a homomorphism for every connective, so it commutes with evaluation (Lemma 10.4).

theorem Fitting1994.exists_theta_ne {L : Type u_1} [LinearOrder L] {x y : Bilattice.Product L L} (h : x ≠ y) : ∃ (a : L), theta a x ≠ theta a y

Distinct members of L ⊙ L are separated by some θ_a (the proof of Theorem 10.5).

def Fitting1994.ofFour {L : Type u_1} [LinearOrder L] [BoundedOrder L] (z : Bilattice.FOUR) : Bilattice.Product L L

The embedding of FOUR into L ⊙ L sends the Boolean coordinates to the bounds.

Equations

• Fitting1994.ofFour z = Bilattice.Product.mk (if Bilattice.Product.pro z = true then ⊤ else ⊥) (if Bilattice.Product.con z = true then ⊤ else ⊥)

theorem Fitting1994.theta_top_ofFour {L : Type u_1} [LinearOrder L] [BoundedOrder L] [Nontrivial L] (z : Bilattice.FOUR) : theta ⊤ (ofFour z) = z

θ_⊤ reads ofFour back.

theorem Fitting1994.equivalent_iff_four {L : Type u_1} [LinearOrder L] {Atom : Type u_2} [BoundedOrder L] [Nontrivial L] (φ ψ : Formula Atom) : (∀ (v : Atom → Bilattice.Product L L), Formula.eval v φ = Formula.eval v ψ) ↔ φ.Equivalent ψ

An equivalence is valid in the bilinear product L ⊙ L iff it is valid in FOUR (Theorem 10.5).