# Why a formula must be closed in order to prove decidability?

Based on this from http://www.encyclopediaofmath.org/index.php/Decidable_formula

A decidable formula is a formula A of a given formal system that is either provable in this system (that is, is a theorem) or refutable (that is, its negation ¬A is provable). If every closed formula of a given formal system is decidable, then such a system is said to be complete.

I'm wondering, why decidability is required for only the closed formulas (sentences)?

Second, my question arrises from Presburguer Arithmetic study. One of our goals is to compute truth value of presburguer formulas. For this, we proceed by first eliminating quantifiers (i.e., generating a logicaly equivalente closed formula).

Pedro

-
I am fairly certain that decision theory is the theory behind making decisions, and not behind decidability of formulas. –  Asaf Karagila Jan 7 '13 at 8:55
A formula with free variables cannot be a theorem. From the article you linked: "Note that it is impossible to require that all, and not just the closed, formulas be decidable in the system. Thus, the formula $x=0$, where $x$ runs over natural numbers, expresses neither a true nor a false proposition and therefore neither it nor its negation is a theorem of formal arithmetic." –  Dan Brumleve Jan 7 '13 at 8:55
@AsafKaragila: I believe so, was a mistake fulfilling the tags. –  Pedro Dusso Jan 7 '13 at 9:08
@DanBrumleve: yes, I read that line, but it isnt clear enought to me. –  Pedro Dusso Jan 7 '13 at 9:10
@Arthur: I always thought this was quantified, $\forall x.x=x$. –  Asaf Karagila Jan 7 '13 at 9:39

The basic idea comes from the definition of satisfaction of arbitrary formulae with a model $\mathcal{A}$. Suppose that $\varphi ( x_1 , \ldots , x_n )$ is a formula (with all free variables shown). We say that $\mathcal{A} \models \varphi ( x_1 , \ldots , x_n )$ iff $\mathcal{A} \models \varphi [ a_1 , \ldots , a_n ]$ for all choices of $a_1 , \ldots , a_n \in A$. The notation $\varphi [a_1 , \ldots , a_n]$ indicates that we are "replacing" the free occurrences of these variables with the indicated elements of the universe. We then ask whether the resulting "statement" is true in $\mathcal{A}$ about these elements.

It then follows quite easily that such formulae need not be either true or false in a given model.

Consider something nice and simple like the theory of the (additive) group $\mathbb{Z}/6 \mathbb{Z}$ under the language $\{ + , 0 \}$. This is clearly a complete theory, since it has (up to isomorphism) a unique (finite) model.

A perfectly good non-closed formula is $x + x = 0$.

* Is this formula true in $\mathbb{Z}/6 \mathbb{Z}$? Certainly not since $\mathbb{Z}/6 \mathbb{Z} \models 2 + 2 = 4 \neq 0$.
* Is its negation true in $\mathbb{Z}/6 \mathbb{Z}$? Again no, since $\mathbb{Z}/6 \mathbb{Z} \models 3 + 3 = 0$.

Since open formulae may fail to be either true or false in models, these formulae may also fail to be either formal theorems or negations of formal theorems. Since virtually all interesting theories have such formulae, it makes sense to only speak of sentences (closed formulae) when discussing decidability. (Otherwise models of decidable theories would have the property that their elements all satisfy the same formulae, which, as the above example indicates, is a very strong condition.)

-
thanks very much, really good answer. –  Pedro Dusso Jan 7 '13 at 10:27