Let me first transcript his math. He's giving a judgement for regex semantics `s matches r`. - [for all r] <empty> matches r [unconditionally] - [for

Let me first transcript his math. He's giving a judgement for regex semantics `s matches r`. - [for all r] <empty> matches r [unconditionally] - [for all c] c matches c - [for all w, r1, r2] IF w matches r1 AND w matches r2 THEN w matches (r1 \/ r2) - (no rule for "w matches bottom") - [for all w, r1, r2] IF there exists w1, w2 such that w = w1 . w2 AND w1 matches r1 AND w2 matches r2 THEN w matches r1 . r2 - [for all w, r] IF there exists w1, w2 such that w = w1 . w2 AND w1 matches r AND w2 matches r* THEN w matches r* So he notes that in the semantics of regex we have non-trivial "there exists" quantification expressing the "search" over possible breaks in the target string. This need for an existential to give semantics to a language is his focus. Perhaps the most obvious example then is Hilbert's epsilon, such as what appears in TLA+ (section 6.6) http://lamport.azurewebsites.net/tla/xmxx00-02-09.pdf http://lamport.azurewebsites.net/tla/xmxx00-02-09.pdf This is called CHOOSE in TLA+ and it's a constructive existential quantifier in that a / b === CHOOSE c in REAL : a = b * c results in evaluating a / b to "some" real value c such that the multiplicative condition holds (or some arbitrary value if no such value exists, fwiw). This shows up in SQL as being essentially exactly what SELECT is doing: `SELECT * FROM Table WHERE Cond` is CHOOSE row in Table : Cond(row) except now CHOOSE returns all matching values as opposed to just "some" matching value.