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”?
$\begingroup$
$\endgroup$
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
2
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.
answered Sep 5, 2012 at 13:02
Gilles 'SO- stop being evil'Gilles 'SO- stop being evil'
44k8 gold badges118 silver badges184 bronze badges
-
$\begingroup$ So it's just the same as in $\mathbb{Z}/2$ (read: the integers modulo (the ideal of) $2$)? $\endgroup$– RaphaelCommented Sep 5, 2012 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$ Commented Sep 5, 2012 at 19:42
$\begingroup$
$\endgroup$
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.
