Enrico Tassi has marked this topic as resolved.
This is also known as an "existential witness operator" or "constructive indefinite description" (when used as an axiom).
Last updated: Feb 08 2023 at 07:02 UTC