# The meaning of modulo in “formula modulo a background theory”

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.

• So it's just the same as in $\mathbb{Z}/2$ (read: the integers modulo (the ideal of) $2$)?
– Raphael
Sep 5 '12 at 19:40
• @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. 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.