0

I'm wondering what the following statement is equivalent to in an intuitionistic framework.

For a union of sets $C = \bigcup\limits_{i \in I} X_i,$ if $S \in C,$ there exists $s \in I$ such that $S \in X_s.$

In classical logic, the proof just relies on ZF and the law of the excluded middle. Indeed, if there does not exist $s$ such that $S \in X_s,$ then $S \not\in X_s$ for all $s \in I,$ hence $S \not\in C$ by the definition of union, contradiction.

Display name
  • 5,144
  • The very same strengthening of the meaning of the existential quantifier that pervades intuitionistic logic comes into play in the definition of union. – Ian Jan 30 '20 at 19:36

1 Answers1

2

As best I can tell, it's not so much an important axiom or theorem as the definition of $\bigcup$ (or rather it would be, if you changed the if to iff). As it stands, it follows from the iff version of the definition.

J.G.
  • 115,835