Quantifier for "there is at most one"? 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.
 A: 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.
A: $\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.
