4
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ It seems like you're just getting rid of constant symbols, not variables. In what sense do your "constant symbols" play any of the roles that constant symbols normally do? $\endgroup$ – Eric Wofsey Sep 15 '16 at 7:03
  • $\begingroup$ @EricWofsey they play all the roles of constant symbols, in addition to the roles of variables. Maybe my title was misleading though. I updated it. $\endgroup$ – 6005 Sep 15 '16 at 7:05
  • $\begingroup$ Maybe I will delete this question if it doesn't get much response. I am really only looking for a reference, but the post is too expository and maybe not a real question. $\endgroup$ – 6005 Sep 15 '16 at 7:11
  • $\begingroup$ I like the question! :P $\endgroup$ – Lorenzo Sep 15 '16 at 7:11
  • 1
    $\begingroup$ The distinction between variable and constant may be useful in informal comments to indicate how you intend to use a given symbol in a proof. For what is worth, however, in my own experience of writing formal proofs, I have never found it necessary to formally make the distinction. $\endgroup$ – Dan Christensen Sep 16 '16 at 15:31
2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ I think this basically settles the question, by giving the example of Bourbaki actually doing things this way. And I liked all of the relevant discussion. $\endgroup$ – 6005 Sep 16 '16 at 23:40
2
$\begingroup$

The obvious reason to distinguish constants from variables is that sometimes we really do want constants as a part of our structure, and not constants that can be uniquely determined from the other structure like the identity of a group. For instance, a perfectly natural sort of mathematical structure to study is a commutative ring with a distinguished element called $x$ (these are also known as commutative $\mathbb{Z}[x]$-algebras). If you don't distinguish between constants and variables, you can't distinguish between this structure and the structure of a commutative ring. The key reason that this distinguished constant $x$ is different from a variable is that to define a model of this theory, you need to define an interpretation for $x$, but you don't need to define an interpretation for all the infinitely many variables you have (or "unused constant symbols", as you call them).

It gets even worse if you try to add axioms. For instance, you might also study commutative rings with a distinguished element $x$ such that $x^2=0$ (these are also known as commutative $\mathbb{Z}[x]/(x^2)$-algebras). If you add an axiom $x^2=0$ to express this, then by your $\forall$ introduction rule, your structure would need to satisfy $(\forall x)x^2=0$, which actually together with the other ring axioms implies that your ring has only one element. (This was based on a misinterpretation of what you meant)

Your argument about "Axioms with existential statements vs. axioms with constant symbols" strikes me as kind of silly. Yes, sometimes the presence of constant symbols that aren't really necessary can make it slightly more complicated to compare two theories. But it is extremely common throughout logic for theories to have multiple different "equivalent" formulations which live over different languages, possibly in much more complicated ways than just inclusion of constant symbols. For instance, you can axiomatize groups using just a binary operation which sends $(x,y)$ to $xy^{-1}$. Eliminating the distinction between constants and variables is hardly going to eliminate the need to have a robust way of defining what this sort of "equivalence" really is.

It's also unclear to me what you're trying to do with $\exists$ elimination. Yes, you can go from $\exists x:x^2=-1$ to $x^2=-1$. But stating the axioms $\exists x:x^2=-1$ does not mean that $x^2=-1$ is true and you can refer to $x$ in other axioms as though this were true. It is only true in the context of an argument in which you have derived $x^2=-1$ as an instantiation of $\exists x:x^2=-1$, in which case I don't see what you have to gain by thinking of $x$ as a "constant" instead of a "variable". Note that including an axiom $x^2=-1$ where $x$ is a constant symbol actually gives you a genuinely different mathematical structure than including an axiom $\exists x:x^2=-1$ does: in the first case, complex conjugation is not an automorphism of $\mathbb{C}$ (since it doesn't fix the distinguished constant $x$), but in the second case it is. If you're trying to say that whenever you have an axiom $\exists x:x^2=-1$ you should also be able to get $x^2=-1$ for free, then it sounds like you're saying you don't want to allow $\mathbb{C}$ as a structure in which conjugation is an automorphism.

That said, the idea of treating certain free variables as though they are new constant symbols is a very natural one that is used all the time in model theory. For instance, it is convenient to think of a formula with $n$ free variables as really being a sentence over an enlarged language which has $n$ new constant symbols (this is basically the idea of "types" in model theory).

$\endgroup$
  • $\begingroup$ Thanks for this answer and the points you raised, especially the connection to types (I'll have to go back and review them). I am not sure about concluding that $\forall x \; x^2 = 0$ from $x^2 = 0$ if $x^2 = 0$ is one of the axioms of our theory, because then $x$ occurs in the scope so we cannot generalize. But maybe I am missing some more subtle argument? $\endgroup$ – 6005 Sep 15 '16 at 7:23
  • $\begingroup$ Well, if you're not going to allow generalizing like that, then how is what you're doing any different from the usual setup? There are some "constants" you aren't allowed to generalize over (namely the ones appearing in the axioms), and some you are (namely the ones not appearing in the axioms). This is just the usual distinction between constants and variables by another name, except that you've lost the flexibility to have constants you care about but impose no axioms on (like in the case of $\mathbb{Z}[x]$-modules). $\endgroup$ – Eric Wofsey Sep 15 '16 at 7:32
  • $\begingroup$ Hopefully, it is not any different than the usual setup, but more natural and elegant. I agree maybe the question is fairly trivial. My real motivation is, I'm hoping it leads to a form a second-order logic where the axiom of choice is a special case of $\exists$ elimination. $\endgroup$ – 6005 Sep 15 '16 at 7:36
  • $\begingroup$ It would be really silly to allow that kind of$\forall$ generalization -- in fact I think it makes the logic actually inconsistent, which is why I specified in my question that you can only generalize if a constant does not appear in scope, and which is why I'm not sure I see the weight of that particular objection in your answer. $\endgroup$ – 6005 Sep 15 '16 at 7:37
  • 2
    $\begingroup$ If you are still distinguishing between "constants in the language" and "constants not in the language", then I would agree that what you are doing is identical to ordinary first-order logic (you've just renamed variables to "constants not in the language"), except that you now allow yourself to generalize over constants if you happen to have no axioms involving them. $\endgroup$ – Eric Wofsey Sep 15 '16 at 7:47

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.