I have been reading some papers where I keep reading stuff like “first-order formula modulo a background theory”. Does anyone know what modulo means in this case ? Is it something like “with respect to”?


A theory, in this sense, is an equivalence relation on the formula, which states when these formula are equivalent (as in: $F$ is equivalent to $G$ iff $F$ implies $G$ and $G$ implies $F$). The theory is usually presented by a set of deduction rules, though this is not an obligation.

The word theory is often used in the context of rewriting systems: if you have rules to rewrite terms (which may be formulas, but the concept is more general) of the form $t \rightarrow t'$, then the induced equivalence relation $t_1 (\leftarrow \cup \rightarrow)^* t_2$ (any number of rewriting steps, alternating directions as often as desired) is the equational theory of this rewriting system.

Technically, “first-order formula modulo a theory $T$” means that you are manipulating equivalence classes which are sets of formulas. Intuitively and practically, this is saying that we are manipulating formulas, but we may replace a formula by some other equivalent formula at any time.

  • $\begingroup$ So it's just the same as in $\mathbb{Z}/2$ (read: the integers modulo (the ideal of) $2$)? $\endgroup$ – Raphael Sep 5 '12 at 19:40
  • 1
    $\begingroup$ @Raphael Yes, it's the same mathematical definition of “modulo”. The intuitions are more or less the same: in $\mathbb{Z}/n$, you can add or subtract $n$ as many times as you like; in reasoning modulo a theory, you can replace a formula by an equivalent formula as many times as you like. $\endgroup$ – Gilles 'SO- stop being evil' Sep 5 '12 at 19:42

In first order logic there are formulae that are not necessarily valid. The equality

$x + y = y + x$

does not hold for arbitrary interpretations of equality and the addition symbol. It does hold for the interpretation of $+$ and $=$ in standard arithmetic. So if we assume the theory of Peano arithmetic (or first order arithmetic, or even Presburger arithmetic), then, the first order formula is said to be true "modulo a background theory".

More generally, if you assume you are working with a specific theory such as a fragment of arithmetic, or a theory of strings, or lists, or any of the many logical theories that exist, the phrase "true modulo a background theory" means, you are assuming first order logic with some axioms which will not be repeated explicitly every time.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.