Ambiguity and Logic

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?

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.

• I did not really thought about proofs. I am more used to (finite) model theory. We care about figuring out which sets are models of a formula, and which set are not. (Especially, for a formula, what is the complexity of finding if a set is a model or not, and for provable formula, hence tautologies, the complexity is O(1) since every sets are models). But thank you a lot for your answer. Mar 31, 2011 at 14:46
• Well, to add analogy: model theory is to logic what semantics is to languages. Model theory assigns meaning to logical theories, while semantics assigns meaning to languages. Sometimes it is best not to mix apples and oranges, even if you're used to it. Mar 31, 2011 at 21:43

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.

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. ;-)

• "Of your grammar encoded a formula $\phi$", I beg your pardon, I do not understand. Do you mean "as a formula". As far as I can tell, you can always distinguish two different finite models. Mar 31, 2011 at 21:18
• Yes, that should have been "as a formula". I've fixed it. As for distinguishing finite models, the other situation is that there is only one accepted finite model for your language (possibly up to some notion of isomorphism). That is the opposite of ambiguity. Apr 1, 2011 at 1:04
• I guess that would indeed be "ambiguity". I just did not thought about it like this. Mostly because as far as language are concerned this would not really be interesting. But from a logical point-of-vue if makes sens Apr 1, 2011 at 18:10
• I'm not sure that the language part has to be be boring. I have more ideas about this, but I think it would takes us beyond the scope of this forum. ;-) Apr 1, 2011 at 19:06

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).

• Thank you for your answer. But as you tell, I do not really see relation with computer science. Especially, an universe is or is not a model of a formula, there are not really any vagueness here. Instead, over automata, ambiguity is something that is well-defined, and there are known algorithm to decide if an automaton is abiguous, k-ambiguous or unambiguous. (only over some kind of automaton) Mar 31, 2011 at 21:12
• You are quite right, I probably shouldn't have jumped in on this question and stuck to lurking. I'm only a noob at CS (about to finish my undergrad in logic/philosophy of science and pure math). Thanks for the information though. Apr 2, 2011 at 4:05

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.

• Kaveh, I'm not sure that I agree that the computation-less characterization of descriptive complexity is 100% right. The computational details are very important to understanding how a particular logic captures a complexity class. The advantage is that, once you have done your proofs and understand how it works, you can set the computation aside, and focus on the logical details using standard logical methods. Apr 1, 2011 at 14:56
• Same remark à Mark. Descriptive complexity is also known as database theory, a vocabulary beeing a structure of a database, and the models of the theory beeing the content of the database. Hence it's happy that we can compute and figure out if a database respect a formula. Apr 1, 2011 at 18:09
• @Marc, but there is no intended way of computation, it is a purely descriptive characterization. Of course you can connect it to algorithms (and their computations) in other settings, but that is secondary to its nature. As I said, complexity classes (e.g. $\mathbf{AC^0}$) correspond to descriptive languages (e.g. $\mathbf{FO}$), computational problems correspond to queries, but AFAIK there is not anything corresponding to algorithms or computations in descriptive complexity (which is not surprising considering it is also part of model theory). Apr 1, 2011 at 20:35
• @Kaveh, I'm making a slightly subtle point, but one that I think is important, since it seems to be frequently misunderstood (for example by failed P=NP? attempts). There is an underlying, fairly brute-force algorithm that underlies the correspondence of a logical language and a complexity class. Working with the logic allows you not to have to think about the details of this algorithm every second, but the beauty and genius of the proofs by Fagin, Immerman, Vardi and others lies exactly in describing these algorithms. People who lose sight of them completely generally end up in trouble. Apr 1, 2011 at 21:05
• @Kaveh, I think we understand each other, and share our respect for the field. "Brute-force" was not intended as a slight on the underlying algorithms, just making clear that we are talking about something slightly more abstract than what someone who does, say, algorithmic optimization work might think of as an algorithm. Apr 1, 2011 at 22:32