Predicate vs Set

Stream: new members

[Ryan McCorvie]

My intuition is that a predicate is a denumerable sort of object, consisting of a finite number of terms. On the other hand, my intuition is that an arbitrary set comes from an enormous universe. However in lean, these are the same thing, a function P : α → Prop.

I'm not sure what my question is, I think I understand what is going on. I suppose it makes sense to think of membership in an arbitrary set as giving a predicate. How do other people think about this?

[Bulhwi Cha]

Ryan McCorvie said:

I suppose it makes sense to think of membership in an arbitrary set as giving a predicate.

I think you're right on this point.

[Kyle Miller]

Yes, sets and predicates are the same thing. It's just that sets use set notation.

Maybe what would unify the two ideas for you is that the only sets you can write down are finite terms.

My own understanding is that the blurring of predicates and functions is related to what happens when you move from first-order to second-order logic. In first-order logic, the native predicates are all actual formulae (and you can't quantify over them; instead you have schema), but in second-order logic you can quantify over all predicates (which might include ones you can't write down). In Lean, P : α → Prop lets you quantify over all predicates, including the ones you can't write down.

[Kyle Miller]

I'm a mathematician who only took a one-semester logic course taught by a mathematician, so I could be saying/thinking incorrectly about this.

[Martin Dvořák]

I really like Kyle Miller's comment, but I see a potential for confusion, so let me clarify stuff a bit.

Before I do so, please note that Lean doesn't use first-order logic, so this is just a tangential issue; I am not answering the original question.

In the first-order logic, the notions "relation" and "set" exist on completely different levels. First-order logic comes with relations and functions (technically speaking, relations would be enough, but working without function would make formulas very messy (remember Prolog?) so we use both). Relations and functions can have various arities. Any theory in the first-order logic is defined by axioms that speak about relations and functions. On the contrary, sets are non-logical notion related to some particular theories in the first-order logic. In the theory of sets, the universe consists of sets only. Since ∈ is a binary relation, we can view ∈ X as a unary relation.

[Martin Dvořák]

Ryan McCorvie said:

However in lean, these are the same thing, a function P : α → Prop.

Yes, they are the same thing in Lean. They are definitionally equivalent but I sometimes write setOf to make it explicit which of the equivalent types I am talking about. Sometimes I need to use Set.mem_setOf_eq to transition between them.

[Kyle Miller]

@Martin Dvořák That shouldn't be a "sometimes" thing :smile: They're defeq, but you're not supposed to treat them as being defeq -- that's breaking the Set API.

Here are the ways you're supposed to go back and forth. The primed versions are exactly the same as the non-primed versions:

def fromPredicateToSet (P : α → Prop) : Set α := setOf P
def fromPredicateToSet' (P : α → Prop) : Set α := {x | P x}

def fromSetToPredicate (s : Set α) : α → Prop := (· ∈ s)
def fromSetToPredicate' (s : Set α) : α → Prop := fun x => x ∈ s

[Kyle Miller]

I'm not sure what the status of it is, but the idea of wrapping Set as a structure to enforce this API has been thrown around:

structure Set (α : Type u) where
  mem : α → Prop

I remember one of the stumbling blocks was that Lean 3 didn't have eta reduction for structures, so you couldn't round-trip from Set to a predicate and back. Maybe the Lean 4 era will change this?

[Kyle Miller]

Eta for structures is what makes the first of these two theorems provable by rfl in Lean 4 but not in Lean 3:

theorem mk_mem (s : Set α) : Set.mk s.mem = s := rfl
theorem mem_mk (p : α → Prop) : (Set.mk p).mem = p := rfl