Quantifier for "there is at most one"?

Question

As "there is at least one" and "there is exactly one" both have their symbols, I wonder what is the common notation for "there is at most one"? By "common" I mean the desired notation can be used without re-defining it.

Answer 1

$\exists_{\leq 1}$

$(\nexists\vee\exists!)$

Warning: to my knowledge, neither notation is a well-established standard. I think, at any rate, that the first one has the advantage of being quite intuitive, while the second one consists of a combination of already familiar symbols.

Answer 2

The quantifier you are looking for is a special case of a counting quantifier. Wikipedia's link Counting quantifier only mentions quantifiers of the form "there exists at least k elements that satisfy property X", but a more general definition can be given, see for instance Majority logic, p. 60.

These quantifiers are used in various domains of theoretical computer science (circuit complexity [3,4], constraint satisfaction problems [2], complexity [1], etc.). There is no agreement on notation yet, but $\exists^{\leqslant 1}$ seems to be a reasonable suggestion.

[1] K. Etessami, Counting Quantifiers, Successor Relations, and Logarithmic Space, Journal of Computer and System Sciences 54, (1997) 400–411.

[2] F. Madelaine, B. Martin, J. Stacho, Constraint Satisfaction with Counting Quantifiers, LNCS 7353, 2012, pp 253-265.

[3] N. Schweikardt Arithmetic, First-Order Logic, and Counting Quantifiers, ACM Transactions on Computational Logic (2002)

[4] H. Straubing, Finite automata, formal logic, and circuit complexity. Progress in Theoretical Computer Science. Birkhäuser Boston Inc., Boston, MA, 1994.