This is a sort of “theorem” that I made up in my mind has been itching me since my years in higher math education.
Context
Let a set and , such that forms a monoid.
We then define as the repeated variant of the binary operator :
using an infix notation for , defined as you would expect: .
This is why we need to be a monoid, instead of a unital magma: we need the operator to be associative, so that the repeated application of the operator is well-defined.
Note how repeated operators have their argument in a sequence space instead of a set. This is because:
- we need to iterate over the elements, which requires a well-defined order on the elements (otherwise, we would need to be commutative and therefore to be a group instead of just a monoid)
- We also want to be able to represent repeated operations on duplicates, which sets cannot represent.
Theorem
For any repeated operator :
where is the unit element of the monoid .
Application to ∀ and ∃
This looks really abstract right now, but consider the two statements that we (at least in France) are told to be “self-evident”:
- For any proposition , is true
- For any proposition , is false
But (resp. ) are just syntactic sugar for the repeated variants of the logical and (resp. logical or ) operators. So, in fact, the two statements are equivalent to:
- For any proposition , is true
- For any proposition , is false
Now, we can prove these statements with the preceding theorem:
- is the repeated variant of .
- is a monoid:
- is a binary operation on .
- is associative: .
- has a unit element (as for any ) and .
- .
Therefore, .
Adapting conventional set notation
You’ll have noticed how the previous statement is kind of akwardly written: we say instead of the much more usual notations, or .
This is because we decided to model the repeated operators as functions over sequences, instead of sets.
But, as long as the set is ordered, we can trivially adapt the notation:
Let an ordered set and a binary operator such that forms a monoid.
We define the set-to-sequence function as:
You’ll notice that is basically a quicksort algorithm.
The interesting thing to note though, is that the function is not bijective, as converting a sequence back to a set would require dropping duplicates. But most usages of repeated operators don’t operate on duplicate elements anyways.
With that said, we can overload the notation of to accept sets:
Then, we can finally state:
Proof
The proof is actually reaaaally trivial, that’s why I put “theorem” in quotes in the introduction. It’s more of a way to have fun with (excessive?) formalization of simple things haha
Anyway, here is the proof.
Let a set and such that is a monoid. Let be the repeated variant of and the unit element of .
Proof by contradiction.
Assume that .
Then:
But we also have, by definition: .
We thus have , which is a contradiction.
So, .
Applications
Operation | Application | |
---|---|---|
where is the universe set |