@hollyr.eth
Framedl 2026-10-10 1/6*
A vacuous truth is a statement that holds because there's nothing inside it to make it false. Ex falso is the underlying principle for this lean proof:
-- "Every unicorn in this room is purple."
example (Unicorn : Type) [IsEmpty Unicorn] (Purple : Unicorn → Prop) :
∀ u : Unicorn, Purple u :=
fun u => isEmptyElim u
Robert Rauschenberg's White Paintings, 1951: panels rolled flat with white house paint. Critics called them empty. John Cage called them 'airports for the lights, shadows and particles' and wrote 4′33″, his silent piece, partly in response.
Nod: @ogerpon.eth
1 reply
0 recast
4 reactions