Ambiguity and Logic

Question

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?

Answer 1

Rules in a grammar and inference rules in logic can both be thought of as production rules which gives us "new stuff" from "known stuff". Just as there may be many ways to produce (or parse) a word with respect to a grammar, so may there be many ways to produce (or prove) a logical formula. This analogy can be drawn further. For example, certain logical systems admit normal forms of proofs. Likewise, certain grammars admit canonical parse trees.

So I'd say your examples from logic are going in the wrong direction. The correct analogy is

"parse tree" : "word" = "proof" : "logical formula"

In fact, a sufficiently general kind of grammar will be able to express typical inference rules of logic, so that the grammatically correct words will be precisely the provable formulas. In this case the parse trees will actually be the proofs.

In the opposite direction, if we are willing to think of very general inference rules (which do not necessarily have a traditional logical flavor), then every grammar will be expressible as a system of axioms (terminals) and inference rules (productions). And once again we will see that a proof is the same thing as a parse tree.

Answer 2

Just two remarks. I hope they help.

The standard definitions of semantics of a logic and of truth follow Tarski's presentation, proceeding by induction on formula structure. Another possibility is to give game-based semantics as suggested by Hintikka. Truth and satisfiability are all defined in terms of strategies in a game. For first order formulae, one can prove that a formula is true under Tarski's notion if and only if there exists a winning strategy in the Hintikka game.

Towards formalising your question, one can ask if the game admits multiple strategies. There is also the interesting question about whether the strategies should be deterministic. Hintikka required them to be deterministic. The proof that Hintikka's original and Tarski's semantics are equivalent requires the Axiom of Choice. One can also formalise truth in terms of games with non-deterministic strategies with fewer complications.

Your language theory example brought to mind determinism, simulation relations and language acceptance. A simulation relation between automata implies language inclusion between their languages though the converse is not true. For deterministic automata the two notions coincide. One can ask if it is possible to extend simulation relations in a 'smooth' manner to capture language equivalence for non-deterministic automata. Kousha Etessami has a really nice paper showing how to do this using k-simulations (A Hierarchy of Polynomial-Time Computable Simulations for Automata). Intuitively, the 'k' reflects the degree of non-determinism the simulation relation can capture. When 'k' equals the level of non-determinism in the automaton, simulation and language equivalence coincide. That paper also gives a logical characterisation of k-simulations in terms of polyadic modal logic and a bounded variable fragment of first-order logic. You get language inclusion, determinism, games, modal logic and first order logic, all in one bumper package.

Answer 3

This started as a comment under Andrej Bauer's answer, but it got too big.

I think an obvious definition of ambiguity from a Finite Model Theory point of view would be: $ambiguous(\phi) \implies \exists M_1,M_2 | M_1 \vDash \phi \wedge M_2 \vDash \phi \wedge M_1 \vDash \psi \wedge M_2 \nvDash \psi$

In words, there exist distinct models of your grammar encoded as a formula $\phi$ that can be distinguished by some formula $\psi$, perhaps a sub-formula of $\phi$.

You can connect this to Andrej's response about proofs through Descriptive Complexity. The combination of the existence of an encoding of a particular model plus its acceptance by an appropriate TM as a model of a given formula IS a proof that the axioms and inferences (and hence an equivalent grammar) encoded in that formula are consistent.

To make this fully compatible with Andrej's answer, you would have to say that the model is "generated" by the formula acting as a filter on the space of all possible finite models (or something like that), with the encoding and action of filtering on the input model as the "proof". The distinct proofs then witness the ambiguity.

This may not be a popular sentiment, but I tend to think of finite model theory and proof theory as the same thing seen from different angles. ;-)

Answer 4

Not sure about the question applied to CS, but try searching for the term Vagueness and logic. In philosophy of logic, ambiguity is usually made distinct from vagueness (see here for instance), and I think what you are after is vagueness (as vagueness is defined as terms where there are borderline cases). The major book in this area is Timothy Williamson's Vagueness (but also see the bibliography on the Stanford site above).

Answer 5

I (also) agree with Anrej.

I think descriptive complexity is a computation-less characterization (which makes it interesting in its own way) and therefore the computational ambiguity examples from formal languages theory (automata/grammars/...) that you gave look to be in a quite different domain. In descriptive complexity languages correspond to complexity classes and queries (in a language) correspond to computational problems (not algorithms). There is no intended way of checking/computing a query AFAIK, so if you are not looking for computational ambiguity IMHO those examples are misleading.