Extensional Equality for Recursively Defined Fuzzy Sets

Stream: maths

[Hunches Freeze]

Hi all,

I'm working on formalizing a theory of fuzzy sets in Lean where elements can be other fuzzy sets, and my ultimate goal is to have extensionality as the fundamental notion of equality. That is, for fuzzy sets X and Y, their equality $X = Y$ should be equivalent to $\forall Z, Z \in\sim X = Z \in\sim Y$ (where $Z \in\sim X$ is the membership degree of $Z$ in $X$).

My base type for constructing these is an inductive type:
inductive PreFuzzySet : Type (u + 1) | mk (α : Type u) (A : α → PreFuzzySet) (f : α → R01)
(where R01 is the type for truth values in $[0,1]$).

Initial Attempt (Structural Equivalence - from my project's InfiniteCore.lean):

My first approach was:

1. Define a structural, bisimilarity-like equivalence PreFuzzySet.Equiv ($E_S$):
   $E_S(\text{mk } \alpha A f, \text{mk } \beta B g) \iff (\forall a, \exists b, E_S(A a, B b) \land f a = g b) \land (\forall b, \exists a, E_S(A a, B b) \land f a = g b)$.

2. Define membership PreFuzzySet.Mem ($M_S$) based on this structural equivalence:
   $M_S(Z_{rep}, X_{rep}) := \bigvee_{i} (\text{if } E_S(Z_{rep}, X_{rep}.A_i) \text{ then } X_{rep}.f_i \text{ else } 0)$.

3. Define FuzzySet := Quotient (PreFuzzySet.setoid_of_relation E_S). So, $X=Y$ in this system meant their representatives were $E_S$-equivalent.

4. Lift $M_S$ to FuzzySet.Mem (Z,X).

Outcome: With this setup, the desired extensionality principle ($X=Y \iff (\forall Z', \text{FuzzySet.Mem } Z' X = \text{FuzzySet.Mem } Z' Y)$) turned out to be false.
Specifically, the $(\Leftarrow)$ direction failed. For example, a pre-fuzzy set representing $\{ (S_0, 0.5), (S_0, 0.4) \}$ and another representing $\{ (S_0, 0.5) \}$ are not $E_S$-equivalent (so their FuzzySet quotients are not equal). However, they yield the same membership degrees for all test sets $Z'$ using $M_S$, because $M_S$ involves a supremum (⨆), which effectively only "sees" the highest degree ($0.5$) for $S_0$-equivalent elements.

This led me to realize that if extensionality is primary, it must be baked into the definition of equality itself.

Target: Co-recursive Definition of Extensional Equality and Membership

I now want to define extensional equality E(X,Y) (a Prop) and membership M(Z,X) : R01 that satisfy the mutually recursive fixed-point equations:

1. $E(X,Y) \iff (\forall (Z : \text{PreFuzzySet}), M(Z,X) = M(Z,Y))$
2. $M(Z,X) \iff \bigvee_{i} (\text{if } E(Z, X.A_i) \text{ then } X.f_i \text{ else } 0)$ (where $X.A_i, X.f_i$ are from $X$'s mk constructor)

Challenges in Realizing This in Lean:

• Direct mutual def block: An attempt to define E and M directly using a mutual block in Lean fails termination checking, primarily due to the ∀ Z in the definition of E. When M(Z,X) recursively calls E(Z, X.Aᵢ), the argument Z is not necessarily structurally smaller than X or Y from an initial E(X,Y) definition, breaking Lean's default structural recursion checker.

• Iterative Approach (Approximating $E$ as $\forall k, E_k(X,Y)$):
  I then tried defining $E$ as the limit of approximations $E_k$:

  * $E_0(X,Y) := \text{True}$ (the universal relation).
  * $E_{k+1}(X,Y) := \forall (Z : \text{PreFuzzySet}), M(E_k, Z, X) = M(E_k, Z, Y)$,
  where $$M(R, Z, X) := \text{Mem_step } R Z X = \bigvee_{i} (\text{if } R(Z, X.A_i) \text{ then } X.f_i \text{ else } 0)$$

  * And finally, $E(X,Y) := \forall k, E_k(X,Y)$.

  The problem here is that for $E = \bigcap E_k$ to be the greatest fixed point (gfp) of the operator $\Phi(R)(X,Y) := (\forall Z, M(R, Z, X) = M(R, Z, Y))$, such that $E = \Phi(E)$, the sequence $(E_k)_k$ must be decreasing ($E_k \supseteq E_{k+1}$, i.e., $E_{k+1}(X,Y) \implies E_k(X,Y)$). This typically requires $\Phi$ to be $\supseteq$-monotonic (if $R_1 \supseteq R_2$, then $\Phi(R_1) \supseteq \Phi(R_2)$). My analysis suggests this specific $\Phi$ is not $\supseteq$-monotonic. If this is correct, the sequence $E_k = \Phi^k(\top)$ is not guaranteed to be decreasing, and therefore $E = \bigcap E_k$ might not be the desired gfp satisfying $E = \Phi(E)$. This makes proving essential properties like $E(X,Y) \implies \Phi(E)(X,Y)$ (which is extensionalEquiv_unfolds in my code) problematic from this construction.

My Core Question:

What is the standard or recommended "Lean-idiomatic" and mathematically rigorous way to define such an extensional equivalence E (which should effectively be the gfp of the operator $\Phi$ described above) and the corresponding membership function M for an inductive type like PreFuzzySet?
Specifically, I'm looking for an approach that:

• Is provably terminating / well-defined in Lean.
• Avoids "approximations" (like fuel parameters) in the final definitions of E and M.
• Allows establishing the fixed-point property $E(X,Y) \iff (\forall Z, M(E, Z, X) = M(E, Z, Y))$.

Is there a standard technique in Mathlib or a common pattern for these types of coinductive definitions over inductive structures, especially when a universal quantifier (∀ Z) is involved in the defining equation and the "observation" (M) returns a value from a lattice like R01 rather than just a Prop?

Thanks for any guidance or pointers to relevant Mathlib theories or techniques!

[Aaron Liu]

I am thinking it should suffice to modify the definition of PreFuzzySet.Equiv to $E_S(\text{mk } \alpha A f, \text{mk } \beta B g) \iff (\forall a, \exists b, E_S(A a, B b) \land f a \le g b) \land (\forall b, \exists a, E_S(A a, B b) \land f a \ge g b)$ (note I have only checked this for R01 a linear order) EDIT: failed on an edge case

[Hunches Freeze]

The problem is that ANY structural equivalence will be too fine-grained. When membership is defined as ⨆{f_i : A_i ≡ Z}, sets like {(S₀, 0.5), (S₀, 0.4)} and {(S₀, 0.5)} give the same membership values but aren't structurally equivalent. The issue is circular: we need extensional equivalence to define membership, but need membership to define extensional equivalence. The iterative approximation approach tries to solve this but requires complex convergence proofs that may not hold

[Kenny Lau]

sounds like forcing to me

[Aaron Liu]

Does this count as extensional?

import Mathlib

-- Since `Rpt` is opaque, this should work for any complete lattice.
private opaque Rpt : (R01 : Type) × CompleteLattice R01 := ⟨Unit, inferInstance⟩
def R01 := Rpt.fst
instance : CompleteLattice R01 := Rpt.snd

inductive PreFuzzySet : Type (u + 1)
  | mk (α : Type u) (A : α → PreFuzzySet) (f : α → R01)

def PreFuzzySet.α : PreFuzzySet.{u} → Type u
  | mk α _ _ => α

def PreFuzzySet.A : (x : PreFuzzySet) → x.α → PreFuzzySet
  | mk _ A _ => A

def PreFuzzySet.f : (x : PreFuzzySet) → x.α → R01
  | mk _ _ f => f

def PreFuzzySet.Equiv : PreFuzzySet → PreFuzzySet → Prop
  | .mk α A f, .mk β B g =>
    (∀ a, f a ≤ ⨆ (i : β) (_ : (A a).Equiv (B i)), g i) ∧
    (∀ b, g b ≤ ⨆ (i : α) (_ : (A i).Equiv (B b)), f i)

-- Should this be `Mem` or `mem`?
def PreFuzzySet.Mem (z x : PreFuzzySet) : R01 :=
  ⨆ (i : x.α) (_ : z.Equiv (x.A i)), x.f i

@[refl, simp]
theorem PreFuzzySet.Equiv.refl (x : PreFuzzySet) : x.Equiv x := by
  induction x with | mk α A f ih
  unfold PreFuzzySet.Equiv
  constructor
  · intro i
    exact @le_iSup₂ R01 α ((A i).Equiv <| A ·) _ (fun j _ => f j) i (ih i)
  · intro i
    exact @le_iSup₂ R01 α (A · |>.Equiv (A i)) _ (fun j _ => f j) i (ih i)

theorem PreFuzzySet.Equiv.rfl {x : PreFuzzySet} : x.Equiv x := .refl x

@[symm]
theorem PreFuzzySet.Equiv.symm {x y : PreFuzzySet} (hxy : x.Equiv y) : y.Equiv x := by
  induction x generalizing y with | mk α A f ih
  cases y with | mk β B g
  unfold PreFuzzySet.Equiv at hxy ⊢
  constructor
  · intro a
    apply (hxy.right a).trans
    apply iSup₂_mono'
    intro i hi
    exact ⟨i, ih i hi, le_rfl⟩
  · intro b
    apply (hxy.left b).trans
    apply iSup₂_mono'
    intro i hi
    exact ⟨i, ih b hi, le_rfl⟩

theorem PreFuzzySet.equiv_comm {x y : PreFuzzySet} : x.Equiv y ↔ y.Equiv x :=
  ⟨.symm, .symm⟩

@[trans]
theorem PreFuzzySet.Equiv.trans {x y z : PreFuzzySet} (hxy : x.Equiv y) (hyz : y.Equiv z) :
    x.Equiv z := by
  induction x generalizing y z with | mk α A f ih
  cases y with | mk β B g
  cases z with | mk γ C h
  unfold PreFuzzySet.Equiv at hxy hyz ⊢
  constructor
  · intro a
    apply (hxy.left a).trans
    apply iSup₂_le
    intro i hi
    apply (hyz.left i).trans
    apply iSup₂_mono'
    intro j hj
    exact ⟨j, ih a hi hj, le_rfl⟩
  · intro b
    apply (hyz.right b).trans
    apply iSup₂_le
    intro i hi
    apply (hxy.right i).trans
    apply iSup₂_mono'
    intro j hj
    exact ⟨j, ih j hj hi, le_rfl⟩

theorem PreFuzzySet.mem_congr {x y z w : PreFuzzySet}
    (hxy : x.Equiv y) (hzw : z.Equiv w) : x.Mem z = y.Mem w := by
  cases x with | mk α A f
  cases y with | mk β B g
  cases z with | mk γ C h
  cases w with | mk δ D k
  unfold PreFuzzySet.Mem
  apply le_antisymm
  · apply iSup₂_le
    intro i hi
    apply (hzw.left i).trans
    apply iSup₂_mono'
    intro j hj
    exact ⟨j, hxy.symm.trans (hi.trans hj), le_rfl⟩
  · apply iSup₂_le
    intro i hi
    apply (hzw.right i).trans
    apply iSup₂_mono'
    intro j hj
    exact ⟨j, hxy.trans (hi.trans hj.symm), le_rfl⟩

-- I was going to make this universe polymorphic but it was too much of a hassle so I didn't.
theorem PreFuzzySet.ext {x y : PreFuzzySet.{u}}
    (h : ∀ (z : PreFuzzySet.{u}), z.Mem x = z.Mem y) : x.Equiv y := by
  cases x with | mk α A f
  cases y with | mk β B g
  constructor
  · intro a
    apply le_of_eq_of_le' (h (A a))
    exact @le_iSup₂ R01 α ((A a).Equiv <| A ·) _ (fun j _ => f j) a .rfl
  · intro b
    conv =>
      enter [2, 1, i]
      rw [PreFuzzySet.equiv_comm]
    apply le_of_eq_of_le' (h (B b)).symm
    exact @le_iSup₂ R01 β ((B b).Equiv <| B ·) _ (fun j _ => g j) b .rfl

theorem PreFuzzySet.ext_iff {x y : PreFuzzySet.{u}} :
    x.Equiv y ↔ ∀ (z : PreFuzzySet.{u}), z.Mem x = z.Mem y :=
  ⟨fun h z => PreFuzzySet.mem_congr (.refl z) h, PreFuzzySet.ext⟩

-- bonus
theorem PreFuzzySet.mem_self_eq_bot {x : PreFuzzySet} : x.Mem x = ⊥ := by
  induction x with | mk α A f ih
  unfold PreFuzzySet.Mem
  rw [iSup₂_eq_bot]
  intro i hi
  rw [← le_bot_iff, ← (PreFuzzySet.mem_congr hi hi).trans (ih i)]
  unfold PreFuzzySet.Mem
  exact @le_iSup₂ R01 α ((PreFuzzySet.mk α A f).Equiv <| A ·) _ (fun j _ => f j) i hi

[Hunches Freeze]

Thank you for this solution! After analyzing it more carefully, I think this might actually work for my purposes. The ext_iff theorem achieves extensionality, and the mem_self_eq_bot theorem aligns perfectly with ZFC's foundation axiom.

My ultimate goal is to show that ZFC is an edge case of a Fuzzy ZFC (FZFC) theory. The idea is that when membership degrees are restricted to {0,1}, we recover classical ZFC exactly, which would then give us all of mathematics built on ZFC "for free" in the fuzzy setting.

What I need to verify is that I can:

1. Define fuzzy versions of all ZFC operations (pairing, union, powerset, infinity, etc.)
2. Prove these operations reduce to their classical counterparts when membership ∈ {0,1}
3. Show all ZFC axioms hold in the restricted case

Your construction seems to provide the right foundation for this - it has extensionality, respects well-foundedness, and the membership relation behaves correctly. I'll need to work through defining the other operations and checking that everything aligns properly when restricted to classical membership values.

Thanks again for this elegant approach! I'll experiment with it and see if I can build the full FZFC theory on top.

[Hunches Freeze]

I've been building on your approach and it's looking quite promising. The construction now includes:

Core pieces:

• Proper Truth type for [0,1] with complete lattice structure
• Your ext_iff: x.Equiv y ↔ ∀ z, z.Mem x = z.Mem y
• Foundation analog: mem_self_eq_bot gives x.Mem x = ⊥
• New: IsCrisp predicate for sets with only {0,1} degrees
• New: crisp_ext showing that for crisp sets, fuzzy extensionality reduces exactly to classical extensionality

The crisp_ext result is the key piece - it confirms that when restricted to crisp sets, we get exactly ZFC's extensionality axiom:

x.Equiv y ↔ ∀ z, z.CrispMem x ↔ z.CrispMem y

So the "classical limit" seems to be working as intended. I'll need to polish this up and build a proper FSet quotient type to get a higher-level API, but the foundational pieces look solid.

Next is defining fuzzy union, pairing, powerset etc. and proving they reduce to classical operations on crisp sets. But this gives me confidence the approach will work. Aaron, I owe you a coffee (or several)! This is brilliant.

[Adam Topaz]

Mathematical question: what's the relationship between fuzzy sets and continuous logic?

[Hunches Freeze]

The connection is that fuzzy set membership is essentially a continuous logic predicate. When I write "x ∈ A = 0.7" in fuzzy set theory, I'm really saying the predicate "x belongs to A" has truth value 0.7 in continuous logic.

So fuzzy set theory can be seen as continuous logic applied to membership relations. The logical connectives in continuous logic (like Godel t-norms for conjunction) correspond exactly to operations on fuzzy sets (like intersection).

In my FZFC project, I'm basically doing continuous logic for set theory - instead of "x ∈ y" being true or false, it's a degree in [0,1]. When I restrict back to {0,1}, I recover classical ZFC.

The neat thing is that continuous logic has nice model-theoretic properties that classical logic has, just generalized. So fuzzy set theory inherits a lot of that structure (like compactness - you can still have "if every finite subset of formulas is satisfiable, then the whole set is satisfiable", just with degrees instead of boolean satisfaction).

[Adam Topaz]

Ok, thanks. That essentially agrees with my (naive) understanding of fuzzy set theory. It would be an interesting project to formalize continuous logic analogously to how we have formalized first order logic in mathlib!

[Hunches Freeze]

Absolutely! That's exactly right - I'll need to formalize at least the relevant parts of continuous logic for FZFC. The membership relation z.Mem x : R01 is already a continuous logic predicate, and I'll need the logical connectives (which I'm starting to build with the Gödel t-norms).

Philosophically I think FZFC → ZFC is much more natural than trying to force fuzzy concepts into classical foundations. The idea is that "crisp" sets are just a special case where membership happens to be {0,1}, rather than the fundamental building blocks.

The quantum mechanics angle is what I'm thinking about long-term. QM with its superpositions, entanglement, and probabilistic measurements feels like it wants fuzzy/continuous foundations. Right now we're essentially forcing quantum phenomena through a classical set-theoretic lens, which always felt awkward to me.

I see it like ZFC gives us a "black and white" model of reality - which works brilliantly for many phenomena! But FZFC could unlock a "colorful" model, revealing new dimensions that were simply impossible to conceive within the crisp framework. General Relativity works fine in ZFC, but "pulling it down" to the FZFC layer might illuminate what pieces we're missing or help us see the connections between quantum and classical in ways that weren't visible before.

If we can show that all of classical mathematics emerges naturally when FZFC restricts to crisp sets, then we get the best of both worlds - full compatibility with existing math, but with this new colorful dimension available when reality demands it.

It's wildly ambitious, but the clean extensionality and foundation axioms make me optimistic this could actually work!

[Hunches Freeze]

What if we don't just stop at fuzzy sets, but extend the fuzziness to logic itself?

Imagine a formal system where the truth of any proposition isn't binary (True/False), but a continuously evolving value in [0,1]. This isn't just about handling uncertainty in set membership; it's about a "Calculus of Truth" where:

• Proofs are Truth-Increasing Functions: A proof isn't a single "True/False" deduction, but an operator that incrementally increases a statement's truth value.
• Conjectures Converge to 1: Problems like the Riemann Hypothesis could be "solved" by showing their truth value converges to 1 via an iterative process (e.g., 0.9 → 0.99 → 0.999...). This offers a "continuous" path to formal proof.
• Truth Sensitivity Analysis: We could precisely measure which parts of a proof are most critical to its overall truth. This would reveal the "drivers" and "bottlenecks" in a complex argument.
• The Geometry of Proofs: We could analyze different "proof shapes" – the shortest path to truth, the most intuitive, or the most convoluted. This might even expose "unnatural glue" in classical proofs – auxiliary lemmas that are only needed to bridge binary gaps, but are irrelevant if we allow for limits. We could prove a theorem without this "glue" by showing its truth value converges to 1 anyway!

This would transform theorem proving into a dynamic field of Truth Analysis, offering unparalleled insight into the structure of mathematical knowledge itself, potentially revealing new ways to prove theorems and simplify existing ones by understanding the very "topology of truth."

This is just off the top of my head but I think it could be a very interesting avenue to pursue. I am aware that it would require implementing basically a fuzzy mathlib from scratch. But still, I am putting it out there; I may try after FZFC is done.

[Hunches Freeze]

Just wanted to give you a quick update and see if you might have any insights.

I've successfully implemented:

• Membership (Mem)
• Equivalence (Equiv)
• Equality (eq)
• Subset (subset)
• Union (union)
• And I'm currently working on Intersection (inter), and its properties, which seems to be coming along.

I'm now looking ahead to implementing complementation (compl). I'm running into a conceptual block on how to define compl given the inductive PreFuzzySet.mk α A f structure, such that the expected membership property z.Mem (xᶜ) = ¬(z.Mem x) holds.

It seems like my current PreFuzzySet.mk pattern, while great for union and intersection, might not directly support this kind of pointwise complement without some deeper considerations.

Any guidance on how to approach defining compl (or other operations that require a more general PreFuzzySet construction from a membership function) within this inductive framework would be incredibly helpful!

Thanks so much for your time and expertise.

[Aaron Liu]

I don't quite understand your z.Mem (xᶜ) = ¬(z.Mem x), what's ¬ in fuzzy logic?

[Hunches Freeze]

When I wrote z.Mem (xᶜ) = ¬(z.Mem x), the ¬ refers to the fuzzy negation operator (Truth.neg) I'm planning to use. Based on the Truth.imp definition currently in Core/Truth.lean, the most natural fuzzy negation derived from it is Gödel negation (i.e., ¬p would be p.imp 0).

-- Core/Truth.lean
universe u

/-- Closed unit interval with range witnesses. -/
@[ext]
structure Truth where
  val  : ℝ
  range : 0 ≤ val ∧ val ≤ 1
-- Notation for Truth values
notation "R01" => Truth

namespace Truth
-- Instances for 0 and 1
instance : Zero R01 := ⟨⟨0, by simp⟩⟩
instance : One  R01 := ⟨⟨1, by simp⟩⟩
@[simp] lemma val_zero : (0 : R01).val = 0 := rfl
@[simp] lemma val_one  : (1 : R01).val = 1 := rfl
-- Instances for order relations
instance : LE R01 where
  le a b := a.val ≤ b.val

instance : LT R01 where
  lt a b := a.val < b.val
-- Gödel implication
noncomputable def imp (a b : R01) : R01 :=
  ⟨if h_condition : a.val ≤ b.val then (1 : ℝ) else b.val,
   -- (original proof here, omitted for brevity)
   by exact And.intro (by split_ifs <;> simp [*]) (by split_ifs <;> simp [*])
  ⟩

end Truth

In standard fuzzy set theory, the complement of a fuzzy set X is defined pointwise: μ_{Xᶜ}(z) = ¬(μ_X(z)). This z.Mem (xᶜ) = ¬(z.Mem x) is the intuitive property I'm aiming for, ensuring ZFC behavior in the crisp edge case.

However, with the PreFuzzySet.mk α A f inductive structure you suggested, I've encountered a "short blanket" dilemma. This structure is powerful for building nested fuzzy sets, but it appears to clash with achieving perfectly pointwise complementation.

If I define compl x in the most direct way (e.g., PreFuzzySet.mk x.α x.A (fun a => ¬(x.f a))), the resulting z.Mem (xᶜ) becomes ⨆ (i : x.α) (_ : z.Equiv (x.A i)), ¬(x.f i). The core problem is that ⨆ (negated values) is generally not equal to negated (⨆ original values) when using Gödel negation (or even Łukasiewicz negation), because fuzzy negation doesn't commute with the iSup operation.

This mismatch becomes evident even for crisp sets:
Assume x is crisp. Suppose z is equivalent to multiple constituents of x, say x.A₁ with x.f₁ = 1 and x.A₂ with x.f₂ = 0.

1. z.Mem x (actual membership): max(x.f₁, x.f₂, ...) = max(1, 0, ...) = 1. (z is in x).
2. Desired ZFC complement (¬ is Gödel negation): ¬(z.Mem x) = ¬1 = 0. (z is not in xᶜ).
3. z.Mem (xᶜ) (with proposed compl): max(¬x.f₁, ¬x.f₂, ...) = max(¬1, ¬0, ...) = max(0, 1, ...) = 1. (z is in xᶜ).

Since 0 ≠ 1, z.Mem (xᶜ) does not match ¬(z.Mem x) for a crisp set, breaking the ZFC edge case.

Given this, I'm wondering if a fundamental choice about PreFuzzySet's core structure, or perhaps a redesign, is necessary to fully capture both the nested set capability and the desired pointwise ZFC behavior for all operations. Any further insights you might have on this specific challenge with the PreFuzzySet.mk design would be greatly appreciated!

[Aaron Liu]

Now what stops you from constructing the fuzzy set of all fuzzy sets that do not contain themselves (assuming you get comprehension/specification)?

[Aaron Liu]

Building off what I wrote earlier,

def PreFuzzySet.empty : PreFuzzySet := .mk PEmpty PEmpty.elim PEmpty.elim

theorem PreFuzzySet.mem_empty_eq_bot (x : PreFuzzySet) :
    x.Mem PreFuzzySet.empty = ⊥ := by
  unfold PreFuzzySet.Mem PreFuzzySet.empty PreFuzzySet.α
  simp

-- presumably you would want these properties
axiom R01.neg : R01 → R01
axiom R01.neg_bot : R01.neg ⊥ = ⊤
axiom R01.bot_ne_top : (⊥ : R01) ≠ ⊤
axiom PreFuzzySet.compl : PreFuzzySet.{u} → PreFuzzySet.{u}
axiom PreFuzzySet.mem_compl (x y : PreFuzzySet) : x.Mem y.compl = R01.neg (x.Mem y)

-- but this leads to a contradiction since
theorem uhoh : False := by
  apply R01.bot_ne_top
  rw [← R01.neg_bot, ← PreFuzzySet.mem_empty_eq_bot.{0} (PreFuzzySet.empty.compl),
    ← PreFuzzySet.mem_compl, PreFuzzySet.mem_self_eq_bot, PreFuzzySet.mem_empty_eq_bot]

Full Code

import Mathlib

-- Since `Rpt` is opaque, this should work for any complete lattice.
private opaque Rpt : (R01 : Type) × CompleteLattice R01 := ⟨Unit, inferInstance⟩
def R01 := Rpt.fst
instance : CompleteLattice R01 := Rpt.snd

inductive PreFuzzySet : Type (u + 1)
  | mk (α : Type u) (A : α → PreFuzzySet) (f : α → R01)

def PreFuzzySet.α : PreFuzzySet.{u} → Type u
  | mk α _ _ => α

def PreFuzzySet.A : (x : PreFuzzySet) → x.α → PreFuzzySet
  | mk _ A _ => A

def PreFuzzySet.f : (x : PreFuzzySet) → x.α → R01
  | mk _ _ f => f

def PreFuzzySet.Equiv : PreFuzzySet → PreFuzzySet → Prop
  | .mk α A f, .mk β B g =>
    (∀ a, f a ≤ ⨆ (i : β) (_ : (A a).Equiv (B i)), g i) ∧
    (∀ b, g b ≤ ⨆ (i : α) (_ : (A i).Equiv (B b)), f i)

-- Should this be `Mem` or `mem`?
def PreFuzzySet.Mem (z x : PreFuzzySet) : R01 :=
  ⨆ (i : x.α) (_ : z.Equiv (x.A i)), x.f i

@[refl, simp]
theorem PreFuzzySet.Equiv.refl (x : PreFuzzySet) : x.Equiv x := by
  induction x with | mk α A f ih
  unfold PreFuzzySet.Equiv
  constructor
  · intro i
    exact @le_iSup₂ R01 α ((A i).Equiv <| A ·) _ (fun j _ => f j) i (ih i)
  · intro i
    exact @le_iSup₂ R01 α (A · |>.Equiv (A i)) _ (fun j _ => f j) i (ih i)

theorem PreFuzzySet.Equiv.rfl {x : PreFuzzySet} : x.Equiv x := .refl x

@[symm]
theorem PreFuzzySet.Equiv.symm {x y : PreFuzzySet} (hxy : x.Equiv y) : y.Equiv x := by
  induction x generalizing y with | mk α A f ih
  cases y with | mk β B g
  unfold PreFuzzySet.Equiv at hxy ⊢
  constructor
  · intro a
    apply (hxy.right a).trans
    apply iSup₂_mono'
    intro i hi
    exact ⟨i, ih i hi, le_rfl⟩
  · intro b
    apply (hxy.left b).trans
    apply iSup₂_mono'
    intro i hi
    exact ⟨i, ih b hi, le_rfl⟩

theorem PreFuzzySet.equiv_comm {x y : PreFuzzySet} : x.Equiv y ↔ y.Equiv x :=
  ⟨.symm, .symm⟩

@[trans]
theorem PreFuzzySet.Equiv.trans {x y z : PreFuzzySet} (hxy : x.Equiv y) (hyz : y.Equiv z) :
    x.Equiv z := by
  induction x generalizing y z with | mk α A f ih
  cases y with | mk β B g
  cases z with | mk γ C h
  unfold PreFuzzySet.Equiv at hxy hyz ⊢
  constructor
  · intro a
    apply (hxy.left a).trans
    apply iSup₂_le
    intro i hi
    apply (hyz.left i).trans
    apply iSup₂_mono'
    intro j hj
    exact ⟨j, ih a hi hj, le_rfl⟩
  · intro b
    apply (hyz.right b).trans
    apply iSup₂_le
    intro i hi
    apply (hxy.right i).trans
    apply iSup₂_mono'
    intro j hj
    exact ⟨j, ih j hj hi, le_rfl⟩

theorem PreFuzzySet.mem_congr {x y z w : PreFuzzySet}
    (hxy : x.Equiv y) (hzw : z.Equiv w) : x.Mem z = y.Mem w := by
  cases x with | mk α A f
  cases y with | mk β B g
  cases z with | mk γ C h
  cases w with | mk δ D k
  unfold PreFuzzySet.Mem
  apply le_antisymm
  · apply iSup₂_le
    intro i hi
    apply (hzw.left i).trans
    apply iSup₂_mono'
    intro j hj
    exact ⟨j, hxy.symm.trans (hi.trans hj), le_rfl⟩
  · apply iSup₂_le
    intro i hi
    apply (hzw.right i).trans
    apply iSup₂_mono'
    intro j hj
    exact ⟨j, hxy.trans (hi.trans hj.symm), le_rfl⟩

-- I was going to make this universe polymorphic but it was too much of a hassle so I didn't.
theorem PreFuzzySet.ext {x y : PreFuzzySet.{u}}
    (h : ∀ (z : PreFuzzySet.{u}), z.Mem x = z.Mem y) : x.Equiv y := by
  cases x with | mk α A f
  cases y with | mk β B g
  constructor
  · intro a
    apply le_of_eq_of_le' (h (A a))
    exact @le_iSup₂ R01 α ((A a).Equiv <| A ·) _ (fun j _ => f j) a .rfl
  · intro b
    conv =>
      enter [2, 1, i]
      rw [PreFuzzySet.equiv_comm]
    apply le_of_eq_of_le' (h (B b)).symm
    exact @le_iSup₂ R01 β ((B b).Equiv <| B ·) _ (fun j _ => g j) b .rfl

theorem PreFuzzySet.ext_iff {x y : PreFuzzySet.{u}} :
    x.Equiv y ↔ ∀ (z : PreFuzzySet.{u}), z.Mem x = z.Mem y :=
  ⟨fun h z => PreFuzzySet.mem_congr (.refl z) h, PreFuzzySet.ext⟩

-- bonus
theorem PreFuzzySet.mem_self_eq_bot {x : PreFuzzySet} : x.Mem x = ⊥ := by
  induction x with | mk α A f ih
  unfold PreFuzzySet.Mem
  rw [iSup₂_eq_bot]
  intro i hi
  rw [← le_bot_iff, ← (PreFuzzySet.mem_congr hi hi).trans (ih i)]
  unfold PreFuzzySet.Mem
  exact @le_iSup₂ R01 α ((PreFuzzySet.mk α A f).Equiv <| A ·) _ (fun j _ => f j) i hi

def PreFuzzySet.empty : PreFuzzySet := .mk PEmpty PEmpty.elim PEmpty.elim

theorem PreFuzzySet.mem_empty_eq_bot (x : PreFuzzySet) :
    x.Mem PreFuzzySet.empty = ⊥ := by
  unfold PreFuzzySet.Mem PreFuzzySet.empty PreFuzzySet.α
  simp

-- presumably you would want these properties
axiom R01.neg : R01 → R01
axiom R01.neg_bot : R01.neg ⊥ = ⊤
axiom R01.bot_ne_top : (⊥ : R01) ≠ ⊤
axiom PreFuzzySet.compl : PreFuzzySet.{u} → PreFuzzySet.{u}
axiom PreFuzzySet.mem_compl (x y : PreFuzzySet) : x.Mem y.compl = R01.neg (x.Mem y)

-- but this leads to a contradiction since
theorem uhoh : False := by
  apply R01.bot_ne_top
  rw [← R01.neg_bot, ← PreFuzzySet.mem_empty_eq_bot.{0} (PreFuzzySet.empty.compl),
    ← PreFuzzySet.mem_compl, PreFuzzySet.mem_self_eq_bot, PreFuzzySet.mem_empty_eq_bot]

[Hunches Freeze]

Yes, uhoh goes right to the core of the issue.

My understanding is now:

1. The ZFC-compatible complement should probably be complement_in U X, with z.Mem (complement_in U X) = (z.Mem U) ⊓ (¬(z.Mem X)). This is because in ZFC, the complement of a set X is always defined relative to a universe/context set U as Xᶜ = {z ∈ U | z ∉ X}. Translating this directly to fuzzy logic yields (z.Mem U) ⊓ (¬(z.Mem X)).
2. However, constructing this using PreFuzzySet.mk is still problematic due to the iSup aggregation in Mem not commuting with negation.
3. More fundamentally, the uhoh paradox suggests that even the existence of a universal function complement_in : PreFuzzySet → PreFuzzySet → PreFuzzySet is likely inconsistent with the current PreFuzzySet structure (which allows self-reference) and the x.Mem x = ⊥ property.

It seems the current PreFuzzySet design, while excellent for nesting, fundamentally clashes with consistently defining a universal pointwise complement that ensures strict ZFC behavior for the crisp edge case.

I believe it might be possible to fix this by fundamentally redefining FuzzySet as a function U → R01, allowing nesting through type parameterization. This approach should hopefully resolve the paradox and ensure exact ZFC behavior in the crisp edge case.

[Paul Reichert]

I have no business in fuzzy set theory and am not sure whether it helps in your case, but you mentioned that you are trying to define a coinductive predicate. Fresh from the oven, corecursive predicates have landed as a language feature.

Here's a silly example how they can be defined:

def eq (f : Nat → Nat) (g : Nat → Nat) : Prop :=
  f 0 = g 0 ∧ eq (f ∘ Nat.succ) (g ∘ Nat.succ)
greatest_fixpoint -- use `monotonicity by` if you need to prove monotonicity manually

Just a heads up, feel free to ignore this if it doesn't help.

[Hunches Freeze]

Thanks for the suggestion! Corecursive predicates are really cool. However, I don't think they directly resolve the current paradox. The issue seems to stem from the consistency of having a universal complement function on a self-referential type, rather than how a specific predicate itself is defined.

[Aaron Liu]

Hunches Freeze said:

1. The ZFC-compatible complement should probably be complement_in U X, with z.Mem (complement_in U X) = (z.Mem U) ⊓ (¬(z.Mem X)). This is because in ZFC, the complement of a set X is always defined relative to a universe/context set U as Xᶜ = {z ∈ U | z ∉ X}. Translating this directly to fuzzy logic yields (z.Mem U) ⊓ (¬(z.Mem X)).

This seems correct to me. Instead of calling it "complement", I think it would be better to call it "set difference", since this matches with what we use already (the notation typeclass is docs#SDiff).

2. However, constructing this using PreFuzzySet.mk is still problematic due to the iSup aggregation in Mem not commuting with negation.

I think this isn't a problem that can't be solved with a little folding.

3. More fundamentally, the uhoh paradox suggests that even the existence of a universal function complement_in : PreFuzzySet → PreFuzzySet → PreFuzzySet is likely inconsistent with the current PreFuzzySet structure (which allows self-reference) and the x.Mem x = ⊥ property.

I don't think the uhoh paradox doesn't extend to this since you can't actually create a set that contains itself with just set difference, since taking the set difference will only shrink your sets.

[Hunches Freeze]

That's a very interesting and crucial distinction regarding set difference (SDiff) inherently shrinking sets and how that avoids the paradox. If SDiff indeed bypasses the inconsistency that uhoh demonstrated for a universal compl, then that simplifies the foundational issue considerably!

This would mean the primary remaining challenge is the construction problem: how to define difference U X using PreFuzzySet.mk such that z.Mem (U \ X) = (z.Mem U) ⊓ (¬(z.Mem X)) holds, given the iSup aggregation in Mem and its non-commutativity with negation. You mentioned this might be solvable with "a little folding."

If both the paradox and the construction problem can be overcome for SDiff with the current PreFuzzySet.mk structure, then it seems it might be possible to achieve ZFC compatibility in the crisp edge case without a fundamental redesign of PreFuzzySet.

[Aaron Liu]

I think to define set difference you need a docs#Order.Frame

[Hunches Freeze]

How would Order.Frame and/or folding specifically address the fundamental non-commutativity of iSup and negation (¬(⨆ f) ≠ ⨆ (¬f)) in the construction of set difference?

[Aaron Liu]

You get that inf distributes over iSup

[Aaron Liu]

Here we are, note the the ᶜ is the pseudo-negation you get from being a heyting algebra

def PreFuzzySet.filter (x : PreFuzzySet) (p : PreFuzzySet → R01) : PreFuzzySet :=
  .mk x.α x.A fun u => x.f u ⊓ p (x.A u)

theorem PreFuzzySet.mem_filter {p : PreFuzzySet → R01} (hp : ∀ a b, a.Equiv b → p a = p b) (x y : PreFuzzySet) :
    x.Mem (y.filter p) = x.Mem y ⊓ p x := by
  unfold Mem PreFuzzySet.filter
  simp_rw [iSup_inf_eq]
  conv =>
    enter [2, 1, i, 1, h, 2]
    rw [hp x (y.A i) h]
  rfl

def PreFuzzySet.sdiff (x y : PreFuzzySet) : PreFuzzySet := x.filter (fun i => (i.Mem y)ᶜ)

-- once again too lazy to make this universe polymorphic
theorem PreFuzzySet.mem_sdiff (x y z : PreFuzzySet.{u}) :
    z.Mem (x.sdiff y) = z.Mem x ⊓ (z.Mem y)ᶜ := by
  unfold PreFuzzySet.sdiff
  rw [PreFuzzySet.mem_filter fun a b h => congrArg compl (PreFuzzySet.mem_congr h .rfl)]

Full Code

import Mathlib

-- Since `Rpt` is opaque, this should work for any complete heyting algebra.
private opaque Rpt : (R01 : Type) × Order.Frame R01 := ⟨Unit, inferInstance⟩
def R01 := Rpt.fst
instance : Order.Frame R01 := Rpt.snd

@[pp_with_univ]
inductive PreFuzzySet : Type (u + 1)
  | mk (α : Type u) (A : α → PreFuzzySet) (f : α → R01)

def PreFuzzySet.α : PreFuzzySet.{u} → Type u
  | mk α _ _ => α

def PreFuzzySet.A : (x : PreFuzzySet) → x.α → PreFuzzySet
  | mk _ A _ => A

def PreFuzzySet.f : (x : PreFuzzySet) → x.α → R01
  | mk _ _ f => f

def PreFuzzySet.Equiv : PreFuzzySet → PreFuzzySet → Prop
  | .mk α A f, .mk β B g =>
    (∀ a, f a ≤ ⨆ (i : β) (_ : (A a).Equiv (B i)), g i) ∧
    (∀ b, g b ≤ ⨆ (i : α) (_ : (A i).Equiv (B b)), f i)

-- Should this be `Mem` or `mem`?
def PreFuzzySet.Mem (z x : PreFuzzySet) : R01 :=
  ⨆ (i : x.α) (_ : z.Equiv (x.A i)), x.f i

@[refl, simp]
theorem PreFuzzySet.Equiv.refl (x : PreFuzzySet) : x.Equiv x := by
  induction x with | mk α A f ih
  unfold PreFuzzySet.Equiv
  constructor
  · intro i
    exact @le_iSup₂ R01 α ((A i).Equiv <| A ·) _ (fun j _ => f j) i (ih i)
  · intro i
    exact @le_iSup₂ R01 α (A · |>.Equiv (A i)) _ (fun j _ => f j) i (ih i)

theorem PreFuzzySet.Equiv.rfl {x : PreFuzzySet} : x.Equiv x := .refl x

@[symm]
theorem PreFuzzySet.Equiv.symm {x y : PreFuzzySet} (hxy : x.Equiv y) : y.Equiv x := by
  induction x generalizing y with | mk α A f ih
  cases y with | mk β B g
  unfold PreFuzzySet.Equiv at hxy ⊢
  constructor
  · intro a
    apply (hxy.right a).trans
    apply iSup₂_mono'
    intro i hi
    exact ⟨i, ih i hi, le_rfl⟩
  · intro b
    apply (hxy.left b).trans
    apply iSup₂_mono'
    intro i hi
    exact ⟨i, ih b hi, le_rfl⟩

theorem PreFuzzySet.equiv_comm {x y : PreFuzzySet} : x.Equiv y ↔ y.Equiv x :=
  ⟨.symm, .symm⟩

@[trans]
theorem PreFuzzySet.Equiv.trans {x y z : PreFuzzySet} (hxy : x.Equiv y) (hyz : y.Equiv z) :
    x.Equiv z := by
  induction x generalizing y z with | mk α A f ih
  cases y with | mk β B g
  cases z with | mk γ C h
  unfold PreFuzzySet.Equiv at hxy hyz ⊢
  constructor
  · intro a
    apply (hxy.left a).trans
    apply iSup₂_le
    intro i hi
    apply (hyz.left i).trans
    apply iSup₂_mono'
    intro j hj
    exact ⟨j, ih a hi hj, le_rfl⟩
  · intro b
    apply (hyz.right b).trans
    apply iSup₂_le
    intro i hi
    apply (hxy.right i).trans
    apply iSup₂_mono'
    intro j hj
    exact ⟨j, ih j hj hi, le_rfl⟩

theorem PreFuzzySet.mem_congr {x y z w : PreFuzzySet}
    (hxy : x.Equiv y) (hzw : z.Equiv w) : x.Mem z = y.Mem w := by
  cases x with | mk α A f
  cases y with | mk β B g
  cases z with | mk γ C h
  cases w with | mk δ D k
  unfold PreFuzzySet.Mem
  apply le_antisymm
  · apply iSup₂_le
    intro i hi
    apply (hzw.left i).trans
    apply iSup₂_mono'
    intro j hj
    exact ⟨j, hxy.symm.trans (hi.trans hj), le_rfl⟩
  · apply iSup₂_le
    intro i hi
    apply (hzw.right i).trans
    apply iSup₂_mono'
    intro j hj
    exact ⟨j, hxy.trans (hi.trans hj.symm), le_rfl⟩

-- I was going to make this universe polymorphic but it was too much of a hassle so I didn't.
theorem PreFuzzySet.ext {x y : PreFuzzySet.{u}}
    (h : ∀ (z : PreFuzzySet.{u}), z.Mem x = z.Mem y) : x.Equiv y := by
  cases x with | mk α A f
  cases y with | mk β B g
  constructor
  · intro a
    apply le_of_eq_of_le' (h (A a))
    exact @le_iSup₂ R01 α ((A a).Equiv <| A ·) _ (fun j _ => f j) a .rfl
  · intro b
    conv =>
      enter [2, 1, i]
      rw [PreFuzzySet.equiv_comm]
    apply le_of_eq_of_le' (h (B b)).symm
    exact @le_iSup₂ R01 β ((B b).Equiv <| B ·) _ (fun j _ => g j) b .rfl

theorem PreFuzzySet.ext_iff {x y : PreFuzzySet.{u}} :
    x.Equiv y ↔ ∀ (z : PreFuzzySet.{u}), z.Mem x = z.Mem y :=
  ⟨fun h z => PreFuzzySet.mem_congr (.refl z) h, PreFuzzySet.ext⟩

-- bonus
theorem PreFuzzySet.mem_self_eq_bot {x : PreFuzzySet} : x.Mem x = ⊥ := by
  induction x with | mk α A f ih
  unfold PreFuzzySet.Mem
  rw [iSup₂_eq_bot]
  intro i hi
  rw [← le_bot_iff, ← (PreFuzzySet.mem_congr hi hi).trans (ih i)]
  unfold PreFuzzySet.Mem
  exact @le_iSup₂ R01 α ((PreFuzzySet.mk α A f).Equiv <| A ·) _ (fun j _ => f j) i hi

def PreFuzzySet.empty : PreFuzzySet := .mk PEmpty PEmpty.elim PEmpty.elim

theorem PreFuzzySet.mem_empty_eq_bot (x : PreFuzzySet) :
    x.Mem PreFuzzySet.empty = ⊥ := by
  unfold PreFuzzySet.Mem PreFuzzySet.empty PreFuzzySet.α
  simp

def PreFuzzySet.filter (x : PreFuzzySet) (p : PreFuzzySet → R01) : PreFuzzySet :=
  .mk x.α x.A fun u => x.f u ⊓ p (x.A u)

theorem PreFuzzySet.mem_filter {p : PreFuzzySet → R01} (hp : ∀ a b, a.Equiv b → p a = p b) (x y : PreFuzzySet) :
    x.Mem (y.filter p) = x.Mem y ⊓ p x := by
  unfold Mem PreFuzzySet.filter
  simp_rw [iSup_inf_eq]
  conv =>
    enter [2, 1, i, 1, h, 2]
    rw [hp x (y.A i) h]
  rfl

def PreFuzzySet.sdiff (x y : PreFuzzySet) : PreFuzzySet := x.filter (fun i => (i.Mem y)ᶜ)

-- once again too lazy to make this universe polymorphic
theorem PreFuzzySet.mem_sdiff (x y z : PreFuzzySet.{u}) :
    z.Mem (x.sdiff y) = z.Mem x ⊓ (z.Mem y)ᶜ := by
  unfold PreFuzzySet.sdiff
  rw [PreFuzzySet.mem_filter fun a b h => congrArg compl (PreFuzzySet.mem_congr h .rfl)]

[Hunches Freeze]

Thank you so much for your absolutely invaluable guidance over the past few days! Your insights have been truly instrumental in moving this fuzzy set theory project forward.

I've now implemented the Truth machinery to get Order.Frame and the sdiff solution you suggested, and it all seems to be working very well. Your expertise really helped clarify the path forward and overcome those tricky foundational issues.

Thanks again for everything!

[Hunches Freeze]

Quick update, I fully implemented Intersection and all of the relevant properties, all of these compile

theorem mem_inter (x y z : PreFuzzySet.{u}) : z.mem (x ∩ y) = (z.mem x) ⊓ (z.mem y)
theorem inter_comm (x y : PreFuzzySet.{u}) : (x ∩ y).Equiv (y ∩ x)
theorem inter_assoc (x y z : PreFuzzySet.{u}) : ((x ∩ y) ∩ z).Equiv (x ∩ (y ∩ z))
theorem inter_empty_left (x : PreFuzzySet) : (emptyPre ∩ x).Equiv emptyPre
theorem inter_self (x : PreFuzzySet) : (x ∩ x).Equiv x
theorem union_inter_distrib (x y z : PreFuzzySet.{u}) : ((x ∪ y) ∩ z).Equiv ((x ∩ z) ∪ (y ∩ z))
theorem inter_subset_left (x y : PreFuzzySet.{u}) : subset (x ∩ y) x = ⊤
theorem inter_subset_right (x y : PreFuzzySet.{u}) : subset (x ∩ y) y = ⊤
lemma imp_monotone_right (a b c : R01) (h : b ≤ c) : a.imp b ≤ a.imp c
lemma imp_inf_le_left_case_le (a b c : R01) (hab : a.val ≤ b.val) (hac : a.val ≤ c.val) : (a.imp b) ⊓ (a.imp c) ≤ a.imp (b ⊓ c)
lemma imp_inf_le_left_case_gt (a b c : R01) (hab : a.val ≤ b.val) (hac_not : ¬(a.val ≤ c.val)) : (a.imp b) ⊓ (a.imp c) ≤ a.imp (b ⊓ c)
lemma imp_inf_le_left (a b c : R01) (hab : a.val ≤ b.val) : (a.imp b) ⊓ (a.imp c) ≤ a.imp (b ⊓ c)
lemma imp_inf_le_right (a b c : R01) (hab : ¬(a.val ≤ b.val)) : (a.imp b) ⊓ (a.imp c) ≤ a.imp (b ⊓ c)
lemma imp_inf_le (a b c : R01) : (a.imp b) ⊓ (a.imp c) ≤ a.imp (b ⊓ c)
theorem subset_inter_iff (x y z : PreFuzzySet) : subset z (x ∩ y) = subset z x ⊓ subset z y

I also had this sketched out but I dont think this is provable. It might not be needed at all anyway.

/- Universe is identity for intersection -/
theorem inter_univ_left (x : PreFuzzySet.{u}) : (univPre ∩ x).Equiv x := by
  sorry

Now I am in the process of sketching out the properties for SDiff, and this is what I came up with (none of these were actually implemented yet)

theorem mem_sdiff (x y z : PreFuzzySet.{u}) : z.mem (x.sdiff y) = z.mem x ⊓ (z.mem y)ᶜ
theorem sdiff_eq_inter_sdiff_univ (x y : PreFuzzySet.{u}) : (x.sdiff y).Equiv (x ∩ (univPre.sdiff y))
theorem sdiff_empty (x : PreFuzzySet.{u}) : (x.sdiff emptyPre).Equiv x
theorem empty_sdiff (x : PreFuzzySet.{u}) : (emptyPre.sdiff x).Equiv emptyPre
theorem sdiff_self_eq_empty (x : PreFuzzySet.{u}) : (x.sdiff x).Equiv emptyPre
theorem sdiff_subset_self (x y : PreFuzzySet.{u}) : subset (x.sdiff y) x = ⊤
theorem inter_sdiff_eq_empty (x y : PreFuzzySet.{u}) : ((x ∩ y).sdiff y).Equiv emptyPre
theorem sdiff_inter_distrib (x y z_set : PreFuzzySet.{u}) : (x.sdiff (y ∩ z_set)).Equiv ((x.sdiff y) ∪ (x.sdiff z_set))
theorem union_sdiff_distrib (x y z_set : PreFuzzySet.{u}) : ((x ∪ y).sdiff z_set).Equiv ((x.sdiff z_set) ∪ (y.sdiff z_set))
theorem sdiff_mono_left (x y z_set : PreFuzzySet.{u}) (hxy : subset x y = ⊤) : subset (x.sdiff z_set) (y.sdiff z_set) = ⊤
theorem sdiff_antimono_right (x y z_set : PreFuzzySet.{u}) (hyz : subset y z_set = ⊤) : subset (x.sdiff z_set) (x.sdiff y) = ⊤
theorem sdiff_inter_assoc_like (x y z_set : PreFuzzySet.{u}) : ((x.sdiff y) ∩ z_set).Equiv ((x ∩ z_set).sdiff y)
theorem sdiff_sdiff_eq_sdiff_union (x y z_set : PreFuzzySet.{u}) : ((x.sdiff y).sdiff z_set).Equiv (x.sdiff (y ∪ z_set))
theorem sdiff_eq_self_iff_inter_empty (x y : PreFuzzySet.{u}) : (x.sdiff y).Equiv x ↔ (x ∩ y).Equiv emptyPre

Are those all right? Am I missing anything? Note that most of the signatures don't even compile yet.. just wanted to know if I am on the right track.

[Aaron Liu]

What is univPre?

[Aaron Liu]

After looking over these, inter_univ_left seems unprovable (or you need more universe parameter annotations), and sdiff_inter_distrib also seems unprovable (due to a lack of excluded middle), but you can prove one direction of subset. EDIT: it seems you don't need full excluded middle but only demorgans which R01 as a biheyting algebra does have.

[Hunches Freeze]

I actually got it working! There is a small issue however, I have emptyPre defined as

def emptyPre : PreFuzzySet :=
  PreFuzzySet.mk Empty (fun e => Empty.elim e) (fun e => Empty.elim e)

Which then constrains sdiff_empty

theorem sdiff_empty (x : PreFuzzySet.{0}) : -- x \ ∅ = x
    (x.sdiff emptyPre).Equiv x := by
  apply PreFuzzySet.ext
  intro z
  -- Goal: z.mem (x.sdiff emptyPre) = z.mem x
  rw [mem_sdiff x emptyPre z] -- Explicitly state arguments for mem_sdiff
  -- Goal: z.mem x ⊓ (z.mem emptyPre)ᶜ = z.mem x
  rw [mem_emptyPre_eq_bot]    -- Requires this lemma: z.mem emptyPre = ⊥
  -- Goal: z.mem x ⊓ (⊥ : R01)ᶜ = z.mem x
  rw [Truth.compl_bot]        -- Requires this lemma: ⊥ᶜ = ⊤
  -- Goal: z.mem x ⊓ (⊤ : R01) = z.mem x
  simp_all only [le_top, inf_of_le_left]

And thus all the following theorems

theorem empty_sdiff (x : PreFuzzySet.{0}) :
    (emptyPre.sdiff x).Equiv emptyPre

theorem sdiff_self_eq_empty (x : PreFuzzySet.{0}) : -- x \ x = ∅
    (x.sdiff x).Equiv emptyPre

theorem inter_sdiff_eq_empty (x y : PreFuzzySet.{0}) : -- (x ∩ y) \ y = ∅
    ((x ∩ y).sdiff y).Equiv emptyPre

theorem sdiff_eq_self_iff_inter_empty (x y : PreFuzzySet.{0}) :
    (x.sdiff y).Equiv x ↔ (x ∩ y).Equiv emptyPre

And here is sdiff_inter_distrib

theorem sdiff_inter_distrib (x y z_set : PreFuzzySet.{u}) :
    (x.sdiff (y ∩ z_set)).Equiv ((x.sdiff y) ∪ (x.sdiff z_set)) := by
  apply PreFuzzySet.ext
  intro w
  rw [mem_sdiff, mem_inter, mem_union, mem_sdiff, mem_sdiff]
  -- Goal: Px ⊓ (Py ⊓ Pz)ᶜ = (Px ⊓ Pyᶜ) ⊔ (Px ⊓ Pzᶜ)
  -- Requires (Py ⊓ Pz)ᶜ = Pyᶜ ⊔ Pzᶜ (De Morgan for ᶜ over ⊓ for R01 truth values)
  -- And Px ⊓ (Pyᶜ ⊔ Pzᶜ) = (Px ⊓ Pyᶜ) ⊔ (Px ⊓ Pzᶜ) (Distributivity of ⊓ over ⊔ for R01)

  rw [Truth.compl_inf_distrib] -- Assuming De Morgan: (A ⊓ B)ᶜ = Aᶜ ⊔ Bᶜ
  rw [inf_sup_left] -- Distributivity: A ⊓ (B ⊔ C) = (A ⊓ B) ⊔ (A ⊓ C)

I am a bit afraid that while all of this compiles the universe constraint will force all lemmas downstream to adapt which might not be optimal.

I tried

def emptyPre : PreFuzzySet.{u} :=
  PreFuzzySet.mk Empty (fun e => Empty.elim e) (fun e => Empty.elim e)

But then it throws this which I am not quite sure how to resolve

application type mismatch
  mk Empty
argument
  Empty
has type
  Type : Type 1
but is expected to have type
  Type u : Type (u + 1)

[Aaron Liu]

You can use PEmpty

[Hunches Freeze]

Thank you, this did indeed fix the issue!

[Hunches Freeze]

I've wrapped up lifting all the basic PreFuzzySet operations to FSet, so that foundational layer is solid. I'm now starting to think on how to best handle the powerset axiom, and since a direct construction seems impossible, I'm leaning towards postulating it with something like axiom powerset_exists (x) : ∃ p, ∀ y, y ∈~ p = subset y x.

My main worry with the other approach I thought of—adding a powerset constructor directly to the PreFuzzySet definition—is how it scales over time. The union function is currently defined by pattern matching on the mk constructor. If powerset was added as a new constructor, and then later an infinity constructor for that axiom, union definition would be forced by the compiler to handle every possible combination.

For example, its definition would look like def union (x y) := match x, y with ..., and the compiler would give an error until a case is explicitly written for | .powerset _, .infinity => ???. We would literally be forced to invent a mathematical meaning for powerset ∪ infinity just to get the code to build. It feels wrong to have the structure of the proofs dictated by these kinds of nonsensical, hybrid cases.

I feel like using the axiom is cleaner by avoiding this (and also the huge effort of rewriting all downstream code), but I'm not sure, it does feel a bit like cheating. What are your thoughts on this?

[Aaron Liu]

Why is a direct construction difficult?

[Hunches Freeze]

I think the difficulty is fundamental to the type system itself.

Our PreFuzzySet constructor requires an indexing set α from a smaller universe (Type u) to build the set in a larger universe (Type u+1). But to construct a powerset, the indexing set would need to represent all possible subsets, which are PreFuzzySets themselves and thus live in the larger universe already. The constructor just can't accept an index set that's as complex as the object it's trying to build; the type system forbids it to prevent paradoxes, if I understand correctly.

[Aaron Liu]

When building the powerset of x you can index over Set x.α. The whole point of the universes is that they represent inaccessible cardinals so you can build a whole model of ZFC with just one universe bump.

[Aaron Liu]

Hmmm but this still doesn't quite capture all the subsets. This is trickier than I thought! I feel like this should still be doable with a clever indexing set though.

[Hunches Freeze]

The problem is that our goal for FZFC is to construct the fuzzy powerset, where membership is graded. We need to build a set P(x) such that for any set y:

y ∈~ P(x) = FSet.subset y x

The value of FSet.subset y x is a fuzzy truth value in [0, 1], not just 0 or 1.

[Aaron Liu]

This time I had to upgrade to a complete linear order. It seems that the more you want the more you need to assume.

-- too lazy to make this universe polymorphic
def PreFuzzySet.Subset (x y : PreFuzzySet.{u}) : R01 :=
  ⨅ i : PreFuzzySet.{u}, i.Mem x ⇨ i.Mem y

-- too lazy to make this one universe polymorphic
theorem PreFuzzySet.subset_congr {x y z w : PreFuzzySet.{u}} (hxy : x.Equiv y) (hzw : z.Equiv w) :
    x.Subset z = y.Subset w := by
  unfold PreFuzzySet.Subset
  simp_rw [PreFuzzySet.mem_congr .rfl hxy, PreFuzzySet.mem_congr .rfl hzw]

def PreFuzzySet.powerset (x : PreFuzzySet) : PreFuzzySet :=
  .mk (x.α → R01) (fun c => .mk x.α x.A c) (fun v => (PreFuzzySet.mk x.α x.A v).Subset x)

theorem PreFuzzySet.mem_powerset (x y : PreFuzzySet.{u}) : x.Mem y.powerset = x.Subset y := by
  unfold PreFuzzySet.powerset PreFuzzySet.Mem
  conv =>
    enter [1, 1, i, 1, h]
    exact PreFuzzySet.subset_congr h.symm .rfl
  rw [iSup_subtype']
  apply iSup_const_le.antisymm
  by_cases hc : ∀ c : PreFuzzySet, c.Mem x ≠ ⊥ → ∃ d, c.Equiv (y.A d)
  · refine le_iSup (fun _ => x.Subset y) ⟨fun k => (y.A k).Mem x, (PreFuzzySet.ext fun c => ?_).symm⟩
    change c.Mem (mk y.α y.A fun k => (y.A k).Mem x) = c.Mem x
    rw [PreFuzzySet.Mem]
    conv =>
      enter [1, 1, i, 1, h]
      exact PreFuzzySet.mem_congr h.symm .rfl
    rw [iSup_subtype']
    apply iSup_const_le.antisymm
    by_cases hx : c.Mem x = ⊥
    · exact hx.trans_le bot_le
    · obtain ⟨d, hd⟩ := hc c hx
      exact le_iSup (fun _ => c.Mem x) ⟨d, hd⟩
  · simp_rw [not_forall, not_exists] at hc
    obtain ⟨c, hc, hd⟩ := hc
    apply bot_le.trans'
    unfold PreFuzzySet.Subset
    apply iInf_le_of_le c
    have hcy : c.Mem y = ⊥ := by
      rw [← le_bot_iff]
      unfold PreFuzzySet.Mem
      apply iSup₂_le
      intro i hi
      exact (hd i hi).elim
    rw [hcy, himp_eq_sSup, le_bot_iff, sSup_eq_bot]
    intro a ha
    rw [Set.mem_setOf, le_bot_iff, min_eq_bot] at ha
    exact ha.resolve_right hc

Full Code

import Mathlib

-- Since `Rpt` is opaque, this should work for any complete linear order.
private opaque Rpt : (R01 : Type) × CompleteLinearOrder R01 := ⟨Unit, inferInstance⟩
def R01 := Rpt.fst
instance : CompleteLinearOrder R01 := Rpt.snd

@[pp_with_univ]
inductive PreFuzzySet : Type (u + 1)
  | mk (α : Type u) (A : α → PreFuzzySet) (f : α → R01)

def PreFuzzySet.α : PreFuzzySet.{u} → Type u
  | mk α _ _ => α

def PreFuzzySet.A : (x : PreFuzzySet) → x.α → PreFuzzySet
  | mk _ A _ => A

def PreFuzzySet.f : (x : PreFuzzySet) → x.α → R01
  | mk _ _ f => f

def PreFuzzySet.Equiv : PreFuzzySet → PreFuzzySet → Prop
  | .mk α A f, .mk β B g =>
    (∀ a, f a ≤ ⨆ (i : β) (_ : (A a).Equiv (B i)), g i) ∧
    (∀ b, g b ≤ ⨆ (i : α) (_ : (A i).Equiv (B b)), f i)

-- Should this be `Mem` or `mem`?
def PreFuzzySet.Mem (z x : PreFuzzySet) : R01 :=
  ⨆ (i : x.α) (_ : z.Equiv (x.A i)), x.f i

@[refl, simp]
theorem PreFuzzySet.Equiv.refl (x : PreFuzzySet) : x.Equiv x := by
  induction x with | mk α A f ih
  unfold PreFuzzySet.Equiv
  constructor
  · intro i
    exact @le_iSup₂ R01 α ((A i).Equiv <| A ·) _ (fun j _ => f j) i (ih i)
  · intro i
    exact @le_iSup₂ R01 α (A · |>.Equiv (A i)) _ (fun j _ => f j) i (ih i)

theorem PreFuzzySet.Equiv.rfl {x : PreFuzzySet} : x.Equiv x := .refl x

@[symm]
theorem PreFuzzySet.Equiv.symm {x y : PreFuzzySet} (hxy : x.Equiv y) : y.Equiv x := by
  induction x generalizing y with | mk α A f ih
  cases y with | mk β B g
  unfold PreFuzzySet.Equiv at hxy ⊢
  constructor
  · intro a
    apply (hxy.right a).trans
    apply iSup₂_mono'
    intro i hi
    exact ⟨i, ih i hi, le_rfl⟩
  · intro b
    apply (hxy.left b).trans
    apply iSup₂_mono'
    intro i hi
    exact ⟨i, ih b hi, le_rfl⟩

theorem PreFuzzySet.equiv_comm {x y : PreFuzzySet} : x.Equiv y ↔ y.Equiv x :=
  ⟨.symm, .symm⟩

@[trans]
theorem PreFuzzySet.Equiv.trans {x y z : PreFuzzySet} (hxy : x.Equiv y) (hyz : y.Equiv z) :
    x.Equiv z := by
  induction x generalizing y z with | mk α A f ih
  cases y with | mk β B g
  cases z with | mk γ C h
  unfold PreFuzzySet.Equiv at hxy hyz ⊢
  constructor
  · intro a
    apply (hxy.left a).trans
    apply iSup₂_le
    intro i hi
    apply (hyz.left i).trans
    apply iSup₂_mono'
    intro j hj
    exact ⟨j, ih a hi hj, le_rfl⟩
  · intro b
    apply (hyz.right b).trans
    apply iSup₂_le
    intro i hi
    apply (hxy.right i).trans
    apply iSup₂_mono'
    intro j hj
    exact ⟨j, ih j hj hi, le_rfl⟩

theorem PreFuzzySet.mem_congr {x y z w : PreFuzzySet}
    (hxy : x.Equiv y) (hzw : z.Equiv w) : x.Mem z = y.Mem w := by
  cases x with | mk α A f
  cases y with | mk β B g
  cases z with | mk γ C h
  cases w with | mk δ D k
  unfold PreFuzzySet.Mem
  apply le_antisymm
  · apply iSup₂_le
    intro i hi
    apply (hzw.left i).trans
    apply iSup₂_mono'
    intro j hj
    exact ⟨j, hxy.symm.trans (hi.trans hj), le_rfl⟩
  · apply iSup₂_le
    intro i hi
    apply (hzw.right i).trans
    apply iSup₂_mono'
    intro j hj
    exact ⟨j, hxy.trans (hi.trans hj.symm), le_rfl⟩

-- I was going to make this universe polymorphic but it was too much of a hassle so I didn't.
theorem PreFuzzySet.ext {x y : PreFuzzySet.{u}}
    (h : ∀ (z : PreFuzzySet.{u}), z.Mem x = z.Mem y) : x.Equiv y := by
  cases x with | mk α A f
  cases y with | mk β B g
  constructor
  · intro a
    apply le_of_eq_of_le' (h (A a))
    exact @le_iSup₂ R01 α ((A a).Equiv <| A ·) _ (fun j _ => f j) a .rfl
  · intro b
    conv =>
      enter [2, 1, i]
      rw [PreFuzzySet.equiv_comm]
    apply le_of_eq_of_le' (h (B b)).symm
    exact @le_iSup₂ R01 β ((B b).Equiv <| B ·) _ (fun j _ => g j) b .rfl

theorem PreFuzzySet.ext_iff {x y : PreFuzzySet.{u}} :
    x.Equiv y ↔ ∀ (z : PreFuzzySet.{u}), z.Mem x = z.Mem y :=
  ⟨fun h z => PreFuzzySet.mem_congr (.refl z) h, PreFuzzySet.ext⟩

-- bonus
theorem PreFuzzySet.mem_self_eq_bot {x : PreFuzzySet} : x.Mem x = ⊥ := by
  induction x with | mk α A f ih
  unfold PreFuzzySet.Mem
  rw [iSup₂_eq_bot]
  intro i hi
  rw [← le_bot_iff, ← (PreFuzzySet.mem_congr hi hi).trans (ih i)]
  unfold PreFuzzySet.Mem
  exact @le_iSup₂ R01 α ((PreFuzzySet.mk α A f).Equiv <| A ·) _ (fun j _ => f j) i hi

def PreFuzzySet.empty : PreFuzzySet := .mk PEmpty PEmpty.elim PEmpty.elim

theorem PreFuzzySet.mem_empty_eq_bot (x : PreFuzzySet) :
    x.Mem PreFuzzySet.empty = ⊥ := by
  unfold PreFuzzySet.Mem PreFuzzySet.empty PreFuzzySet.α
  simp

def PreFuzzySet.filter (x : PreFuzzySet) (p : PreFuzzySet → R01) : PreFuzzySet :=
  .mk x.α x.A fun u => x.f u ⊓ p (x.A u)

theorem PreFuzzySet.mem_filter {p : PreFuzzySet → R01} (hp : ∀ a b, a.Equiv b → p a = p b) (x y : PreFuzzySet) :
    x.Mem (y.filter p) = x.Mem y ⊓ p x := by
  unfold Mem PreFuzzySet.filter
  simp_rw [iSup_inf_eq]
  conv =>
    enter [2, 1, i, 1, h, 2]
    rw [hp x (y.A i) h]
  rfl

def PreFuzzySet.sdiff (x y : PreFuzzySet) : PreFuzzySet := x.filter (fun i => (i.Mem y)ᶜ)

-- once again too lazy to make this universe polymorphic
theorem PreFuzzySet.mem_sdiff (x y z : PreFuzzySet.{u}) :
    z.Mem (x.sdiff y) = z.Mem x ⊓ (z.Mem y)ᶜ := by
  unfold PreFuzzySet.sdiff
  rw [PreFuzzySet.mem_filter fun a b h => congrArg compl (PreFuzzySet.mem_congr h .rfl)]

-- too lazy to make this universe polymorphic
def PreFuzzySet.Subset (x y : PreFuzzySet.{u}) : R01 :=
  ⨅ i : PreFuzzySet.{u}, i.Mem x ⇨ i.Mem y

-- too lazy to make this one universe polymorphic
theorem PreFuzzySet.subset_congr {x y z w : PreFuzzySet.{u}} (hxy : x.Equiv y) (hzw : z.Equiv w) :
    x.Subset z = y.Subset w := by
  unfold PreFuzzySet.Subset
  simp_rw [PreFuzzySet.mem_congr .rfl hxy, PreFuzzySet.mem_congr .rfl hzw]

def PreFuzzySet.powerset (x : PreFuzzySet) : PreFuzzySet :=
  .mk (x.α → R01) (fun c => .mk x.α x.A c) (fun v => (PreFuzzySet.mk x.α x.A v).Subset x)

theorem PreFuzzySet.mem_powerset (x y : PreFuzzySet.{u}) : x.Mem y.powerset = x.Subset y := by
  unfold PreFuzzySet.powerset PreFuzzySet.Mem
  conv =>
    enter [1, 1, i, 1, h]
    exact PreFuzzySet.subset_congr h.symm .rfl
  rw [iSup_subtype']
  apply iSup_const_le.antisymm
  by_cases hc : ∀ c : PreFuzzySet, c.Mem x ≠ ⊥ → ∃ d, c.Equiv (y.A d)
  · refine le_iSup (fun _ => x.Subset y) ⟨fun k => (y.A k).Mem x, (PreFuzzySet.ext fun c => ?_).symm⟩
    change c.Mem (mk y.α y.A fun k => (y.A k).Mem x) = c.Mem x
    rw [PreFuzzySet.Mem]
    conv =>
      enter [1, 1, i, 1, h]
      exact PreFuzzySet.mem_congr h.symm .rfl
    rw [iSup_subtype']
    apply iSup_const_le.antisymm
    by_cases hx : c.Mem x = ⊥
    · exact hx.trans_le bot_le
    · obtain ⟨d, hd⟩ := hc c hx
      exact le_iSup (fun _ => c.Mem x) ⟨d, hd⟩
  · simp_rw [not_forall, not_exists] at hc
    obtain ⟨c, hc, hd⟩ := hc
    apply bot_le.trans'
    unfold PreFuzzySet.Subset
    apply iInf_le_of_le c
    have hcy : c.Mem y = ⊥ := by
      rw [← le_bot_iff]
      unfold PreFuzzySet.Mem
      apply iSup₂_le
      intro i hi
      exact (hd i hi).elim
    rw [hcy, himp_eq_sSup, le_bot_iff, sSup_eq_bot]
    intro a ha
    rw [Set.mem_setOf, le_bot_iff, min_eq_bot] at ha
    exact ha.resolve_right hc

[Hunches Freeze]

Whoa, okay, that's a very elegant idea. I have absolutely not tried to run this, and I'm probably completely wrong because this stuff is way over my head, but I've been trying to trace it with an edge case in my head.

My first thought was, "what about the empty set?" Like, if we take powerset(x) for some non-empty x, then emptyPre should be a member with degree 1, right? But for that to happen, emptyPre would have to be Equiv to one of those generated sets A(c) = .mk x.α x.A c.

And this is where I get lost. All those A(c) sets have the same "shape" as x, but emptyPre has a different shape (its kernel type is PEmpty). I thought that meant they could never be equivalent, so the membership for emptyPre would come out as 0, which would be wrong.

But I'm almost certainly missing something obvious about how Equiv works between sets with different kernel types. The proof is really dense, and I'm still just trying to get my head around it; maybe that hc case handles exactly this kind of problem.

Honestly, this is way trickier than I thought! I have no idea if my concern about the edge case is valid at all.

[Aaron Liu]

I'm sure this proof could be shortened too, I was stuck for a long time until I decided to upgrade to linear order, and the proof probably accumulated some junk during that time.

[Aaron Liu]

Hunches Freeze said:

My first thought was, "what about the empty set?" Like, if we take powerset(x) for some non-empty x, then emptyPre should be a member with degree 1, right? But for that to happen, emptyPre would have to be Equiv to one of those generated sets A(c) = .mk x.α x.A c.

And this is where I get lost. All those A(c) sets have the same "shape" as x, but emptyPre has a different shape (its kernel type is PEmpty). I thought that meant they could never be equivalent, so the membership for emptyPre would come out as 0, which would be wrong.

For empty, set c := fun _ => 0, and then all the sets in your "shape" are still in there, just with degree 0, so what you get is equivalent to the empty set.

[Hunches Freeze]

I was fixated on the idea that Equiv had to preserve the underlying type α of the kernel, thinking of it as a "shape." I completely missed the fact that a set with a non-empty kernel can still be equivalent to the empty set if all its internal membership degrees are zero. That is an incredibly elegant way to solve the problem.

So the powerset construction isn't just indexing over subsets that share x's shape; it's indexing over a family of sets rich enough to contain equivalents to all the structurally different subsets. That's a much deeper idea than I was grasping.

It seems the construction is sound then, at least for the edge cases I was worried about, hopefully I am not missing anything.

[Hunches Freeze]

Right so I am having a small issue, I tried to get CompleteLinearOrder working for R01 like this

-- Helper lemma for sdiff_le_iff
lemma sdiff_le_iff_aux (a b c : R01) :
    (if a ≤ b then ⊥ else a) ≤ c ↔ a ≤ b ⊔ c := by
  constructor
  · intro h
    split_ifs at h with hab
    · -- a ≤ b, so a \ b = ⊥, and we have ⊥ ≤ c
      exact le_sup_of_le_left hab
    · -- ¬(a ≤ b), so a \ b = a, and we have a ≤ c
      exact le_sup_of_le_right h
  · intro h
    split_ifs with hab
    · -- a ≤ b, so a \ b = ⊥
      exact bot_le
    · -- ¬(a ≤ b), so a \ b = a, need to prove a ≤ c
      push_neg at hab
      -- hab : b < a and h : a ≤ b ⊔ c
      -- We need to show a ≤ c
      by_contra hac
      push_neg at hac
      -- We have b < a and c < a, so b ⊔ c < a
      have : b ⊔ c < a := by
        rw [Truth.lt_val_iff, show (b ⊔ c).val = max b.val c.val from rfl]
        rw [Truth.lt_val_iff] at hab hac
        exact max_lt hab hac
      -- But this contradicts h : a ≤ b ⊔ c
      exact not_le.mpr this h
-- Helper lemma for top_sdiff
lemma top_sdiff_aux (a : R01) :
    (if ⊤ ≤ a then ⊥ else ⊤) = aᶜ := by
  ext
  -- We need to show (if ⊤ ≤ a then ⊥ else ⊤).val = aᶜ.val
  split_ifs with h
  · -- ⊤ ≤ a, which means a = ⊤
    have : a = ⊤ := le_antisymm le_top h
    subst this
    simp_all only [le_refl, compl_top]
  · sorry -- ⊤.val = aᶜ.val

noncomputable instance : CompleteLinearOrder R01 := {
  (by infer_instance : CompleteLattice R01),
  (by infer_instance : LinearOrder R01),
  (by infer_instance : Order.Frame R01) with
  sdiff := fun a b => if a ≤ b then ⊥ else a
  hnot := fun a => aᶜ
  sdiff_le_iff := sdiff_le_iff_aux
  top_sdiff := top_sdiff_aux
}

But it seems that top_sdiff_aux cannot be proven.

The R01 type, representing the unit interval with Gödel logic operations, is a CompleteLattice and a HeytingAlgebra. However, it is not a CoheytingAlgebra because the critical axiom ⊤ \ a = ¬a does not hold for the operations defined (where \ is the Coheyting difference and ¬ is the Gödel negation).

Therefore, R01 cannot be an instance of BiheytingAlgebra with its current operational definitions, and consequently, it cannot be an instance of CompleteLinearOrder

This is the full code. Sorry for the huge mess. Also not sure how to do that 'full code' button you have in your messages.

Truth.lean

[Aaron Liu]

It is not a coheyting algebra if you use the heyting negation

[Aaron Liu]

You need to use

noncomputable def coneg (p : R01) : R01 :=
  ⟨if p.val = 1 then 0 else 1,
   by
    split_ifs with h
    · exact ⟨le_refl 0, zero_le_one⟩
    · exact ⟨zero_le_one, le_refl 1⟩⟩

[Hunches Freeze]

And can I just add it and use it for this even if for the other stuff i use godel negation? Would this cause issues downstream? To be fair, I got powerset and powerset_mem to work without a CompleteLinearOrder instance like below. But I also got the CompleteLinearOrder to compile with your coneg suggestion. Not sure at this point if I should just leave it be or remove everything related to it.

noncomputable def powerset (x : PreFuzzySet) : PreFuzzySet :=
  .mk (x.α → R01) (fun c => .mk x.α x.A c) (fun v => (PreFuzzySet.mk x.α x.A v).subset x)

theorem mem_powerset (x y : PreFuzzySet.{u}) : x.mem y.powerset = x.subset y := by
  unfold PreFuzzySet.powerset PreFuzzySet.mem
  conv =>
    enter [1, 1, i, 1, h]
    exact PreFuzzySet.subset_congr h.symm .rfl
  rw [iSup_subtype']
  apply iSup_const_le.antisymm
  by_cases hc : ∀ c : PreFuzzySet, c.mem x ≠ ⊥ → ∃ d, c.Equiv (y.A d)
  · refine le_iSup (fun _ => x.subset y) ⟨fun k => (y.A k).mem x, (PreFuzzySet.ext fun c => ?_).symm⟩
    change c.mem (mk y.α y.A fun k => (y.A k).mem x) = c.mem x
    rw [PreFuzzySet.mem]
    conv =>
      enter [1, 1, i, 1, h]
      exact PreFuzzySet.mem_congr h.symm .rfl
    rw [iSup_subtype']
    apply iSup_const_le.antisymm
    by_cases hx : c.mem x = ⊥
    · exact hx.trans_le bot_le
    · obtain ⟨d, hd⟩ := hc c hx
      exact le_iSup (fun _ => c.mem x) ⟨d, hd⟩
  · simp_rw [not_forall, not_exists] at hc
    obtain ⟨c, hc, hd⟩ := hc
    apply bot_le.trans'
    unfold subset
    apply iInf_le_of_le c
    have hcy : c.mem y = ⊥ := by
      rw [← le_bot_iff]
      unfold PreFuzzySet.mem
      apply iSup₂_le
      intro i hi
      exact (hd i hi).elim
    rw [hcy, Truth.himp_bot]
    rw [le_bot_iff]
    ext
    change ((c.mem x)ᶜ).val = (⊥:R01).val
    rw [Truth.val_compl]
    rw [if_neg]
    simp_all only [ne_eq]
    rfl
    exact (Truth.val_ne_zero_iff (c.mem x)).mpr hc

[Aaron Liu]

Hunches Freeze said:

And can I just add it and use it for this even if for the other stuff i use godel negation? Would this cause issues downstream?

Every complete linear order is a biheyting algebra in exactly one way, and it turns out the coheyting complement on R01 is given by coneg. This is formally dual to neg, and is the least element such that a ⊔ coneg a = ⊤, where Godel negation is the greatest element such that a ⊓ neg a = ⊥. The notation in mathlib for this kind of negation is ￢. In a boolean algebra these coincide, but for R01 they do not. I could maybe see this causing issues downstream if you try to use x \ y = x ⊓ neg y, since this is not true for R01.

See also ncatlab page I found

[Hunches Freeze]

So one more reason to get rid of coneg and the CompleteLinearOrder instance I guess? But I am incredibly excited about Powerset actually compiling, I believe this is a strong sign that the foundations are sound. The rest of the ZFC axioms should be achievable with some effort, but I feel like Powerset was the hardest. I can start to see the finish line to a full Fuzzy ZFC, proved constructively without any axioms apart from the inductive PreFuzzySet. Thank you Aaron, I couldn't have done it without you!

[Kevin Buzzard]

Wait -- you have an axiom? Is it consistent? Or are you not talking about axiom?

[Hunches Freeze]

To clarify: I have not used the axiom keyword anywhere. My entire development is constructive, flowing from a single inductive definition for PreFuzzySet. When I said "without any axioms apart from...", I meant that I haven't introduced any new, unproven postulates on top of Lean's foundational type theory. I'm building everything from the ground up rather than, for example, axiomatically asserting the existence of a powerset.

And as a quick progress update, this constructive approach is proving to be very successful. I've now managed to prove the fuzzy analogues for the axioms of Infinity, Pairing, and Replacement at the PreFuzzySet level. I'm currently working on finishing the proofs for BigUnion. Since the congruence theorems are in place for each operation, lifting them all to the final FSet quotient type is indeed a straightforward and repeatable process.

So, to answer your questions directly:

1. Do I have an axiom? No, not in the sense of the Lean keyword. My foundation is the inductive type PreFuzzySet, which is a definition justified by Lean's logic.
2. Is it consistent? Yes. Its consistency is guaranteed by the consistency of Lean's underlying type theory.

I'm excited because having Powerset, Infinity, Pairing, and Replacement all compile in this constructive framework feels like a strong validation that the foundation is sound and that a complete, contradiction-free FZFC is within reach.

[Mario Carneiro]

Hunches Freeze said:

1. Do I have an axiom? No, not in the sense of the Lean keyword. My foundation is the inductive type PreFuzzySet, which is a definition justified by Lean's logic.
2. Is it consistent? Yes. Its consistency is guaranteed by the consistency of Lean's underlying type theory.

I don't think it's quite that simple. If you are using a definition which bundles all your "axioms", like mathlib does for its algebraic structures, then the question shifts a bit, and rather than asking "is it consistent" we should ask "is the type inhabited". You can equally well work with inconsistent theories using "axioms" bundled in a structure, you are still unprotected unless you prove that it's possible to construct a PreFuzzySet.

[Mario Carneiro]

@Kevin Buzzard told me a story of an instance of this once, I forget the details but it was some complicated construction proving facts about prime numbers and at the end someone discovered that the definition of prime was wrong and there were in fact no prime numbers according to the definition

[Hunches Freeze]

That's a fantastic point, thank you, Mario. You're absolutely right that logical consistency isn't enough, and that the key question is whether the type is inhabited.

I think I have proven that it is. The proof is the construction of the empty set, emptyPre, which is a well-defined term of type PreFuzzySet:
def emptyPre := PreFuzzySet.mk PEmpty (fun e => PEmpty.elim e) (fun e => PEmpty.elim e)

This serves as the base case for the universe, demonstrating that the definition isn't vacuous (I hope!).

[Mario Carneiro]

where is the powerset axiom coming from then?

[Mario Carneiro]

I meant the axiomatization of fuzzy sets

[Mario Carneiro]

Is PreFuzzySet parameterized over a FuzzySetStructure giving you all the axioms? If not, where are the axioms coming from?

[Hunches Freeze]

I'm not using a structure or typeclass that bundles the axioms. Instead, each "axiom" of my Fuzzy ZFC is implemented as a direct, constructive def that builds a new PreFuzzySet from existing ones. The axioms are then proven as theorems about these concrete definitions.

For example, the Powerset Axiom isn't an axiom at all. It's this function:

noncomputable def powerset (x : PreFuzzySet.{u}) : PreFuzzySet :=
.mk (x.α → R01) (fun c => .mk x.α x.A c) (fun v => (PreFuzzySet.mk x.α x.A v).subset x)

And the "axiom" itself is then a theorem I prove about this specific construction:

theorem mem_powerset (x y : PreFuzzySet.{u}) : x.mem (powerset y) = x.subset y

So, the power to create these sets comes directly from the richness of Lean's underlying type theory—specifically, the ability to form new types to serve as indices (like dependent sums for union or function types for powerset). My approach is to build a concrete model of FZFC from the ground up, rather than axiomatizing the theory in a structure first.

[Mario Carneiro]

reread the OP, looks like the powerset axiom is really a theorem about a specific defined model, in which case there should not be any problems about consistency

[Mario Carneiro]

I guess this is just a generalization of what is being done in Mathlib.SetTheory.ZFC.PSet?

[Hunches Freeze]

Yes, I think that's a great way to put it.

I believe the PreFuzzySet model I'm using is a fuzzy generalization of what is being done with PSet. The definition seems very analogous:

inductive PreFuzzySet | mk (α : Type u) (A : α → PreFuzzySet) (f : α → R01)

The main difference, I think, is the addition of the membership grade function f : α → R01. This function seems to be what introduces the fuzziness. My understanding is that if R01 were replaced by a two-point {0, 1} type, the model should essentially collapse back to the classical PSet model.

[Mario Carneiro]

I guess you can probably do this over any complete lattice?

[Mario Carneiro]

unclear if linear ordering is needed for some things but I would assume not

[Hunches Freeze]

I think you're probably right.

My implementation is concrete over R01, but I believe the core machinery relies on it being a CompleteLattice. More specifically, since my definitions of subset and eq use Godel implication, I think the most important structure is that R01 is an Order.Frame. I would think the whole construction could be generalized to work over any L : Type* with an [Order.Frame L] instance.

Regarding the linear ordering, I also suspect it might not be essential for the main theorems to hold, but I have to admit that some of my current proofs do take advantage of it. For example, some proofs about the properties of implication use by_cases on a.val ≤ b.val, which relies on le_total.

So, my feeling is that the framework should be generalizable to any Order.Frame, but the specific proofs I have at the moment are written for the simpler, linearly-ordered case of R01.

[Hunches Freeze]

Alright, so BigUnion is at a good stage now. I need to prove some additional basic properties but mem_big_union and big_union_congr compile just fine. I gave a shot to the foundation axiom, but it's proving to be quite tricky. Not sure if I need more machinery, or this is just highly non trivial. But this is my current attempt. Apart from the defs, nothing compiles just yet. Ran out of time for today unfortunately.

import FZFC.PreFuzzySet.Basic
import FZFC.PreFuzzySet.Equality
import FZFC.PreFuzzySet.Ops.Intersection

universe u

namespace PreFuzzySet

/--
The truth value of a set `x` being non-empty.
It is defined as the complement of `x` being equal to the empty set.
In the crisp case, this corresponds to `x ≠ ∅`.
-/
noncomputable def is_nonempty (x : PreFuzzySet.{u}) : R01 :=
  (eq x emptyPre)ᶜ

/--
The Axiom of Foundation (or Regularity).

This is the fuzzy analogue of the classical ZFC axiom. It is formulated as:
"For all sets x, if x is non-empty, then there exists a y such that y is a
member of x and y is disjoint from x."

This axiom rules out paradoxical sets, such as sets that contain themselves or
infinite descending chains of membership. When truth values are crisp ({⊥, ⊤}),
this definition collapses to the standard ZFC axiom.
-/
noncomputable def AxiomOfFoundation : R01 :=
  ⨅ (x : PreFuzzySet.{u}),
    (is_nonempty.{u} x).imp (⨆ (y : PreFuzzySet.{u}), (y.mem x) ⊓ (eq (x ∩ y) emptyPre.{u}))


/--
A helper lemma stating that if Foundation fails for a set `x`, it must
also fail for one of `x`'s constituents. This is the core inductive step.
-/
private theorem foundation_descent (x : PreFuzzySet.{u}) :
  (is_nonempty x = ⊤ ∧ (⨆ y, y.mem x ⊓ eq (x ∩ y) emptyPre) < ⊤) →
  (∃ i : x.α, is_nonempty (x.A i) = ⊤ ∧ (⨆ y, y.mem (x.A i) ⊓ eq ((x.A i) ∩ y) emptyPre) < ⊤) := by
  sorry

/-- The `val` homomorphism preserves arbitrary infima. -/
private theorem val_iInf_comm {ι : Type u} (f : ι → R01) : (iInf f).val = iInf (fun i => (f i).val) := by
  sorry

theorem axiom_of_foundation_holds : AxiomOfFoundation = ⊤ := by
  have imp_eq_top_iff_le (a b : R01) : a.imp b = ⊤ ↔ a ≤ b := by
    constructor
    · intro h; rw [Truth.le_val_iff]; have hv : (a.imp b).val = 1 := by simp_all only; rfl
      rw [Truth.val_imp] at hv; split_ifs at hv with h_le; · exact h_le
      exact le_trans a.range.2 (le_of_eq hv.symm)
    · intro h; ext;  simp_all only [Truth.le_val_iff, Truth.val_imp, ↓reduceIte]; rfl
  have val_eq_one_iff (a : R01) : a.val = 1 ↔ a = ⊤ := by
    constructor; · intro h; exact Truth.ext (by simp_all only [Truth.le_val_iff]; rfl)
    · intro h
      simp [h];
      subst h
      simp_all only [Truth.le_val_iff]
      rfl
  have val_lt_one_iff (a : R01) : a.val < 1 ↔ a < ⊤ := by
    simp [Truth.lt_val_iff]
    simp_all only [Truth.le_val_iff]
    rfl
  rw [AxiomOfFoundation, iInf_eq_top]
  intro x
  induction x using PreFuzzySet.rec with | mk α A f ih =>
    rw [imp_eq_top_iff_le]
    by_contra h_not_le
    let S_x := ⨆ y, y.mem (mk α A f) ⊓ eq ((mk α A f) ∩ y) emptyPre
    have h_val_gt : S_x.val < (is_nonempty (mk α A f)).val := not_le.mp h_not_le
    have h_is_crisp : (is_nonempty (mk α A f)).val = 1 ∨ (is_nonempty (mk α A f)).val = 0 := by
      have h_base_crisp : (eq (mk α A f) emptyPre).val = 1 ∨ (eq (mk α A f) emptyPre).val = 0 := by
        by_cases h_equiv : (mk α A f).Equiv emptyPre
        · left; simp [eq_equiv_iff_eq_top.mp h_equiv]
        · right
          apply le_antisymm
          · have h_not_ext : ¬ ∀ (z : PreFuzzySet), z.mem (mk α A f) = z.mem emptyPre :=
              mt (ext_iff _ _).mpr h_equiv
            rw [not_forall] at h_not_ext
            rcases h_not_ext with ⟨z, hz⟩
            have h_mem_ne_bot : z.mem (mk α A f) ≠ ⊥ := by
              intro h_mem_bot; apply hz; rw [h_mem_bot, mem_emptyPre_eq_bot]
            calc (eq (mk α A f) emptyPre).val
              _ = (iInf (fun z' => (z'.mem (mk α A f))ᶜ)).val := by simp [eq, himp_bot]
              _ = iInf (fun z' => ((z'.mem (mk α A f))ᶜ).val) := val_iInf_comm _
              _ ≤ ((z.mem (mk α A f))ᶜ).val := iInf_le _ z
              _ = if (z.mem (mk α A f)).val = 0 then 1 else 0 := by rfl
              _ = 0 := if_neg ((Truth.val_ne_zero_iff _).mpr h_mem_ne_bot)
          · exact (eq (mk α A f) emptyPre).range.1
      rw [is_nonempty]
      cases h_base_crisp with | inl h => right; rw [Truth.val_compl, h]; simp | inr h => left; rw [Truth.val_compl, h]; simp
    have h_nonempty_val_one : (is_nonempty (mk α A f)).val = 1 := by
      cases h_is_crisp with | inl h => exact h | inr h => linarith [S_x.range.1, h, h_val_gt]
    have h_nonempty : is_nonempty (mk α A f) = ⊤ := by simp_all only [Truth.le_val_iff, Truth.lt_val_iff, not_le, one_ne_zero, or_false, S_x]
    have h_S_x_lt_top : S_x < ⊤ := by
      simp_all only [Truth.le_val_iff, Truth.lt_val_iff, top_le_iff, true_or, S_x]
    rcases foundation_descent (mk α A f) ⟨h_nonempty, h_S_x_lt_top⟩ with ⟨i, h_Ai_nonempty, h_S_Ai_lt_top⟩
    specialize ih i
    rw [imp_eq_top_iff_le] at ih
    have h_S_Ai_ge_nonempty : (⨆ y, y.mem (A i) ⊓ eq ((A i) ∩ y) emptyPre).val ≥ (is_nonempty (A i)).val := ih
    rw [h_Ai_nonempty, Truth.val_one] at h_S_Ai_ge_nonempty
    have h_S_Ai_lt_one : (⨆ y, y.mem (A i) ⊓ eq ((A i) ∩ y) emptyPre).val < 1 :=
      val_lt_one_iff.mpr h_S_Ai_lt_top
    linarith
-- Useful Consequences of Foundation
-- The following theorems would be derived from `axiom_of_foundation_holds`.

/--
A key consistency check: the general Axiom of Foundation should imply the
specific result we already proved, that no set can contain itself.
-/
theorem foundation_imp_mem_self_eq_bot (x : PreFuzzySet.{u}) :
    AxiomOfFoundation = ⊤ → x.mem x = ⊥ := by
  sorry

/--
The Axiom of Foundation prohibits cycles of membership. This theorem states that
it's impossible for `a` to be a member of `b` and `b` to be a member of `a`
simultaneously with non-zero truth.
This is the fuzzy analogue of `∀a,b, ¬(a ∈ b ∧ b ∈ a)`.
-/
theorem no_two_cycles (a b : PreFuzzySet.{u}) :
    AxiomOfFoundation = ⊤ → (a.mem b ⊓ b.mem a) = ⊥ := by
  sorry
-- We could generalize to `no_n_cycles`, but the 2-cycle case is the most illustrative.

end PreFuzzySet

[Aaron Liu]

Mario Carneiro said:

I guess you can probably do this over any complete lattice?

Take a look at my code snippets: at the start it worked for any complete lattice but then for comprehension/specification it got upgraded to a complete heyting algebra and for powerset it was again upgraded to a complete linear order.

[Hunches Freeze]

I had a bit of a wild thought, what if instead of trying to prove the axiom of foundation like this, we built a "NonWFPreFuzzySet" and show that it is impossible to construct a "NonWFPreFuzzySet" with a PreFuzzySet, since PreFuzzySet IS well founded by definition, and thus we get the axiom of foundation for free?

[Aaron Liu]

I have no idea what you mean by that.

[Hunches Freeze]

Yeah sorry I realize now that what I wrote makes very little sense. I am just trying to figure out a way to exploit the inductive nature of PreFuzzySet to prove the foundation axiom. Maybe something like this would be better than the approach I attempted above?

/-- A witness that x violates foundation: y ∈ x but x ∩ y ≠ ∅ -/
structure FoundationViolation (x : PreFuzzySet) where
  y : PreFuzzySet
  y_mem_x : y.mem x ≠ ⊥
  intersection_nonempty : eq (x ∩ y) emptyPre ≠ ⊤

/-- The key theorem: no such violation can exist -/
theorem no_foundation_violation (x : PreFuzzySet) :
    is_nonempty x = ⊤ → ¬∃ v : FoundationViolation x := by
  intro h_nonempty
  intro ⟨v⟩
  -- This is impossible because elements of x come from x.A
  -- and the inductive construction prevents cycles
  sorry

theorem axiom_of_foundation_holds : AxiomOfFoundation = ⊤ := by
  -- From no_foundation_violation, we get that every non-empty set
  -- has a disjoint member
  sorry

[Mario Carneiro]

yes you can prove foundation by induction

[Mario Carneiro]

I don't think you need to negate it, that mostly just makes things more complicated

[Hunches Freeze]

I got this to work, ideally I would just need a full proof for exists_foundation_witness. But I am fairly sure it's not possible to prove that, a non-empty fuzzy set doesn't necessarily have any element with full membership! So this might be a dead end.

import FZFC.PreFuzzySet.Basic
import FZFC.PreFuzzySet.Equality
import FZFC.PreFuzzySet.Ops.Intersection

universe u

namespace PreFuzzySet

noncomputable def is_nonempty (x : PreFuzzySet.{u}) : R01 :=
  (eq x emptyPre)ᶜ

noncomputable def AxiomOfFoundation : R01 :=
  ⨅ (x : PreFuzzySet.{u}),
    (is_nonempty.{u} x).imp (⨆ (y : PreFuzzySet.{u}), (y.mem x) ⊓ (eq (x ∩ y) emptyPre.{u}))

/-- When x is empty, the foundation axiom holds trivially -/
lemma foundation_holds_for_empty (x : PreFuzzySet) (h_empty : eq x emptyPre = ⊤) :
    (x.eq emptyPre)ᶜ.imp (⨆ y, y.mem x ⊓ (x ∩ y).eq emptyPre) = ⊤ := by
  rw [h_empty, Truth.compl_top]
  exact Truth.bot_imp_eq _

/-- For any non-empty set, we can find an element that witnesses foundation -/
lemma exists_foundation_witness (x : PreFuzzySet) (h_nonempty : eq x emptyPre ≠ ⊤) :
    ∃ i : x.α, x.f i = ⊤ ∧ eq (x ∩ (x.A i)) emptyPre = ⊤ := by
  -- In a well-founded structure, we can pick a "minimal" element
  -- Since x ≠ ∅, there must be at least one i with x.f i > ⊥
  -- Among all such i, pick one where x.f i = ⊤ (if it exists)
  -- If no such i exists with x.f i = ⊤, we need a different approach
  sorry

/-- The supremum is high enough to make the implication work -/
lemma foundation_sup_sufficient (x : PreFuzzySet)
    (h_witness : ∃ i : x.α, x.f i = ⊤ ∧ eq (x ∩ (x.A i)) emptyPre = ⊤) :
    ⨆ y, y.mem x ⊓ (x ∩ y).eq emptyPre = ⊤ := by
  obtain ⟨i, h_mem_top, h_disjoint⟩ := h_witness
  apply le_antisymm le_top

  apply le_trans _ (le_iSup (fun y => y.mem x ⊓ (x ∩ y).eq emptyPre) (x.A i))

  rw [h_disjoint, inf_top_eq]

  have h_mem_eq_top : (x.A i).mem x = ⊤ := by
    apply le_antisymm le_top
    unfold mem
    apply le_trans _ (le_iSup₂_of_le i (Equiv.refl (x.A i)) (le_refl _))
    rw [h_mem_top]

  rw [h_mem_eq_top]

/-- When x is non-empty, we can find a disjoint element -/
lemma foundation_holds_for_nonempty (x : PreFuzzySet) (h_nonempty : eq x emptyPre ≠ ⊤) :
    (x.eq emptyPre)ᶜ.imp (⨆ y, y.mem x ⊓ (x ∩ y).eq emptyPre) = ⊤ := by
  -- Get a witness with full membership
  have h_witness := exists_foundation_witness x h_nonempty

  -- Show the supremum equals ⊤
  have h_sup := foundation_sup_sufficient x h_witness

  -- When the consequent is ⊤, the implication is ⊤ regardless of antecedent
  rw [h_sup]
  ext
  simp only [Truth.val_imp, Truth.val_one]
  simp_all only [ne_eq, Truth.val_compl, ite_eq_right_iff]
  intro a
  obtain ⟨w, h⟩ := h_witness
  obtain ⟨left, right⟩ := h
  rfl

theorem axiom_of_foundation_holds : AxiomOfFoundation.{u} = ⊤ := by
  unfold AxiomOfFoundation is_nonempty
  rw [iInf_eq_top]
  intro x

  by_cases h : eq x emptyPre = ⊤
  · exact foundation_holds_for_empty x h
  · exact foundation_holds_for_nonempty x h

end PreFuzzySet

[Hunches Freeze]

Quick update: Foundation and Choice are now done! The PreFuzzySet layer is fully complete. The FSet quotient is ~70% done. Next up is proving the ZFC crisp edge case, but that should be fairly straightforward.

[James E Hanson]

@Adam Topaz Generally speaking the formalism of continuous logic in the Ben Yaacov–Berenstein–Henson–Usvyatsov sense is very closely related to real-valued Łukasiewicz logic. There are some significant but arguably cosmetic differences in the setup of the formalism and some meaningful differences in the intended semantics, but they are in a strong sense equivalent.

There's also a pretty big philosophical difference between work in the two fields. People who do continuous logic (i.e., the model theory of metric structures) generally see real-valued logic as a technical device to extend modern model theory to more classes of structures. On the other hand I think it's fair to say that a lot of people working in Łukasiewicz, fuzzy, and other real-valued logics tend to see it as having a least a bit of philosophical motivation (such as wanting to formalize reasoning about vague concepts).

That said, not everything called 'fuzzy logic' in the literature reduces to real-valued Łukasiewicz logic. For example, $t$-norm fuzzy logic allows certain discontinuous connectives.

[James E Hanson]

@Hunches Freeze Is the axiomatization of FZFC you're working with written up somewhere?

[Hunches Freeze]

Apologies for the slow reply, I've been out sick all week.

To answer your question, no, it's not written up anywhere yet. And to be honest, I'm not entirely satisfied with the current result. The main reason is that some of the axioms aren't fully fuzzy. While some of these are solvable with a bit of work, others seem to be fundamentally blocked until the logical foundation of Lean itself can handle fuzzy propositions, which is well beyond the scope of this project.

The issue splits into two categories:

1. Workable Problems: The axioms of Pairing and Infinity are currently crisp (e.g., membership in a singleton is 0 or 1). This can be fixed by redefining them within the existing framework. For instance, a fuzzy singleton {a} could have its membership defined by the fuzzy equality eq z a, and a fuzzy omega could be constructed from a universal property as the intersection of all inductive sets. It would be a fair bit of work, but it's conceptually straightforward.
2. Blocked Problems: The real roadblock is with axioms of principle like Regularity and Choice. These are formulated as classical propositions (Prop) that are either true or false. Making the axioms themselves fuzzy-valued statements would require fuzzy quantifiers and proof machinery that just doesn't exist in Lean. They rely on classical tools like WellFounded.induction and Classical.epsilon, so they are stuck in their current form for now.

For completeness, here is a brief rundown of the current axiomatization in FZFC. The logic is Gödel-T an its residuum over the real unit interval .

• Extensionality: Two sets are equivalent if they have the same members to the same degree.
• Empty Set: There exists a set with no members.
• Pairing: For any sets , the set exists (currently a crisp container).
• Union: For any set , the union exists.
• Powerset: For any set , the powerset exists, where membership is given by the degree of subsetness.
• Replacement: The image of a set under a function exists.
• Infinity: The set of von Neumann numerals, , exists (currently as a crisp collection).
• Regularity: Every non-empty set has an -minimal element (formulated as a classical Prop).
• Choice: Every non-empty set has a member (based on Hilbert's -operator, a classical principle).

[James E Hanson]

@Hunches Freeze Ah okay, so I think you should probably know that there's fundamental issues with formalizing induction principles like the axiom of regularity and the version of infinity you're suggesting in real-valued logics. I talk about this a bit in the intro of one of my papers. That's in the context of different kinds of set theories, but the fundamental issue is that it's not always possible to talk about implication in a way that avoids Sorites-like issues.

What kind of fuzzy logic do you want to be using specifically?

[James E Hanson]

Another thing you should probably know (since you're talking about defining fuzzy singletons in terms of fuzzy equality) is that generally speaking fuzzy comprehension together with reasonable forms of extensionality are often enough to imply that equality is crisp.