In automata theory (finite automata, pushdown automata, ...) and in complexity, there is a notion of "ambiguity". An automaton is ambiguous if there is a word $w$ with at least two distinct accepting runs. A machine is $k$-ambiguous if for every word $w$ accepted by the machine there are at most $k$ distinct runs to accept $w$.
This notion is also defined over context-free grammars: a grammar is ambiguous if there exists a word that can be derived in two different ways.
It is also known that many languages have a nice logical characterization over finite models. (If a language $L$ is regular, there exists a monadic second-order formula $\phi$ over words such that every word $w$ of $L$ is a model of $\phi$, similarly NP if equivalent to the Second order formulae where every 2nd order quantifiers are existential.)
Hence, my question is at the edges of the two domains: is there any result, or even a canonical definition, of "ambiguity" of formulae of a given logic?
I can imagine a few definitions:
- $\exists x \phi(x)$ is non ambiguous if there exists at most one $x$ such that $\phi(x)$ holds and that $\phi(x)$ is non-ambiguous.
- $\phi_0\lor\phi_1$ would be ambiguous if there exists a model of both $\phi_0$ and $\phi_1$, or if $\phi_i$ is ambiguous.
- A SAT formula would be non-ambiguous iff there is at most one correct assignation.
Hence, I wonder if it is a well-known notion, else it may be interesting to try to do research on this topic. If the notion is known, could anyone give me keywords I could use to search for information on the matter (because "logic ambiguity" gives a lot of unrelated results), or a book/pdf/article references?