Similarity between "Exists" and "Sigma"

Stream: new members

[Vivek Rajesh Joshi]

In TPIL, chapter 7 (Inductive Types), there is a statement that says "∃ x : α, p is a Prop-valued variant of Σ x : α, p". A similar comparison is made between Prod and And, and Sum and Or, which I can understand, but I don't understand how "Exists" and "Sigma" are related in the same manner. Can anyone explain this connection to me?

[Yaël Dillies]

Can you describe in words what s : Σ x : α, p is? Now, can you do the same with h : ∃ x : α, p?

[Riccardo Brasca]

Be prepared that the next question usually is "why aren't they exactly the same thing?!"

[Yaël Dillies]

To be quite fair, I'm confused by the spelling. Let's assume it's s : Σ x : α, p x and h : ∃ x : α, p x instead.

[Vivek Rajesh Joshi]

s : Σ x : α, p x means that s is an element of the form (a,b) where the type of b depends on a as p a (not very sure, correct me if wrong)
h : ∃ x : α, p x means that h is a proof of there existing an element x that satisfies the property p x
Ah, now I see something: the type of a part of the proof h (the proof for p x) depends on x, similar to how the type of b depends on a. Is that enough to declare them as pretty much the same, apart from their output types?

[llllvvuu]

Riccardo Brasca said:

Be prepared that the next question usually is "why aren't they exactly the same thing?!"

Now I'm curious

[Riccardo Brasca]

It's just that it's an interesting subtlety why ∃ is not defined via Σ. Looking at docs#Sum, one sees that (β : Type v) cannot be a Prop, but the reason of this choice is proof irrelevance.

[Kyle Miller]

@Riccardo Brasca Was that supposed to be docs#Sigma ?

There's also docs#PSigma that allows both arguments to be props. The reason there's both Sigma and PSigma is that PSigma has a complicated universe level expression.

[Riccardo Brasca]

Ops sure, I meant that

[N Gelwan]

Riccardo Brasca said:

It's just that it's an interesting subtlety why ∃ is not defined via Σ. Looking at docs#Sum, one sees that (β : Type v) cannot be a Prop, but the reason of this choice is proof irrelevance.

What is proof irrelevance? Is that a formal term?

[N Gelwan]

Oh, found a reference to this term in docs#Exists:

Because Lean has proof irrelevance, any two proofs of an existential are definitionally equal.

[N Gelwan]

Ah, here's an answer from Andrej Bauer and Jacques Carette: https://cstheory.stackexchange.com/questions/48112/proof-relevance-vs-proof-irrelevance