In first-order logic, there is normally a formal distinction between constants and variables. Namely:
-
A constant symbol is a $0$-ary function symbol in a language $\mathcal{L}$.
-
A variable is one of countably many special symbols used for first-order reasoning, and can be quantified over.
Instead, suppose we insist that there are no variables, but only constants. And specifically:
-
We may quantify over constant symbols, but not over general function or relation symbols.
-
There is an infinite supply of unused constant symbols available for use.
Question: can we develop first-order-logic this way? Has it been done, and if not, what goes wrong?
Why would you want to do that?
Both the syntax and the semantics of constants and variables suggest that they are more naturally understood as the same thing. Consider:
-
Logical implication for formulas Let $\varphi, \psi$ be any formulas. We say that $\varphi \vDash \psi$ if, under any model( interpretation of the function symbols and relation symbols), and any assignment of the variables to elements of our model, if $\varphi$ is true then $\psi$ is true.
If variables are just constant symbols, then this simply says that under any interpretation (which must automatically include interpreting the constant symbols), if $\varphi$ is true then $\psi$ is true.
-
Axioms with existential statements vs. axioms with constant symbols Consider the group axioms. There are two different formal presentations of the identity axiom, both commonly used: option (i) is to have a constant symbol $e$ in the language, and assert the axiom that $\forall x (x e = ex = x$). Option (ii) is to assert that $\exists y \forall x (xy = yx = x)$. If you do the first axiom, then your language of groups is $\mathcal{L} = \{*, e\}$; if you do the second axiom, your language is just $\{*\}$. (The unary function for inverse is also sometimes included, $^{-1}$.)
The two formulations give two different theories over two different languages, but they amount to the same thing. However, the equivalence is not immediate because while we can show the theory with the constant symbol $e$ in it can prove the other theory's axioms, going the other way requires "defining" a new symbol $e$ and adding it to the language, which has to be done on a meta level.
-
$\exists$ elimination The $\exists$ elimination rule tells us that from $\exists x \; \varphi(x)$, we may deduce that $\varphi(x)$, where $x$ is a new variable that does not occur free in the current scope. But informally, what is this saying? If we know that there exists an object satisfying a property, we may give it a name. And I think of the name as a constant symbol even though it's formally a variable.
Consider defining $i$ in the complex numbers given the axiom $\exists x \; : \; x^2 = -1$. We employ $\exists$ elimination to obtain $x^2 = -1$ for some variable $x$. But it would be helpful for this variable to then become part of our language, so that $i$ can be considered a constant instead of a variable.
-
$\forall$ introduction If $a$ is a constant symbol, it should be valid to conclude $\forall x \; \varphi(x)$ from $\varphi(a)$, if there are no formulas involving $a$ in scope. But, it isn't allowed. Because we insist on only generalizing from a variable which doesn't occur free in any other statement, we can't generalize from a constant even though it seems we should be able to.
Possible issues
-
How do we distinguish between sentences and formulas? For any language $\mathcal{L}$, we can define a sentence to be a formula where all the constant symbols are either bound, or elements of $\mathcal{L}$.
-
What about quantifying over an important constant? If we are in the langauge of fields, it does seem a bit odd to allow a sentences such as $\forall 0 \; \forall 1 \; (0 + 1 = 1 + 0)$. But this is more bad style than anything else, and doesn't strike me as a problem with the formal system. Bound variables are just dummy variables whose names don't matter; quantifying over constants that are mentioned in the axioms would be discouraged, but not disallowed formally. We would have to say that within the scope of the quantification the axioms about the constant will not apply.
Best Answer
On a fundamental level (not relative to the theory under consideration) Bourbaki does not define constants as separate from variables. To him, a constant in a theory is just a variable that does not occur (freely) in axioms of the theory. Clearly if you don't fundamentally distinguish constants from variables, then you need theories where a formula A can be a theorem without $\forall{x}A$ being a theorem; thus, the more fundamental question, perhaps, is whether such theories should be allowed. Indeed, it does seem slightly useful to define variables so that they can be the same in any language, reducing the bother of worrying about what the variables are, while it seems like $0$-ary functions (constant symbols) should depend on the language, but it doesn't feel fundamentally very useful, but just perhaps technically so.
Say you are trying to prove $A \rightarrow B$. Ideally you might want to assume $A$ by considering it an axiom temporarily, then prove $B$. But technically, without allowing axioms whose generalizations don't hold, one can't assume $A$. Instead, the modern way in practice is to temporarily pretend the free variables of $A$ are new constants and then use the theorem on constants at the end to replace the constants with variables. This is an inelegant nuisance which becomes unnecessary if one does things more like Bourbaki. True, you don't automatically get that $\forall{x}A$ is a theorem whenever $A$ is a theorem, but so what? Instead you have the equally useful rule that $\forall{x}A$ is a theorem whenever $A$ is a theorem and $x$ does not appear freely in an axiomatization of the theory (i.e., it is not a constant of the theory in Bourbaki terminology). True, when giving axioms, Bourbaki must be clear whether their generalizations or the statements themselves are intended as axioms, but that's just a mild nuisance.
Your first argument logical implication for formulas is spot on. Whether one feels it is more fundamental to interpret just the functions or the functions and their variables simultaneously, it is definitely convenient to be able to do the latter in one fell swoop, as one might by merely interpreting everything (say) into a complete Henkin extension of the theory, which one can't do if by complete one means a consistent theory generated by sentences in which every sentence or its negation is in the theory as opposed to a consistent theory not necessarily generated by sentences in which every statement or its negation is in the theory. True, the former standard notion of completeness may be more fundamental (or not!), but that's not the point--it's convenient to be able to have both concepts available with names for each.