This question already has an answer here:

I still have doubts about the subject. I need help.

Are there really open axioms?

I do not think so. What exists, in fact, I think, are seemingly open axioms, with some implicit quantifier.

For example, when it is stated that x = x is an equality axiom, it seems to me that the following statement is implicit: for every x, x = x.

Am I right?


marked as duplicate by Carl Mummert logic Sep 12 '17 at 11:49

This question has been asked before and already has an answer. If those answers do not fully address your question, please ask a new question.

  • 5
    $\begingroup$ It is common to present the axioms for equational theories (e.g., the theory of groups) as a set of equations. These open formulas are intended to be read as universally quantified. $\endgroup$ – Rob Arthan Sep 11 '17 at 23:22
  • 4
    $\begingroup$ @Jim H . As for the open axioms, see, for example, Principles of Mathematical Logic, by Hilbert & Ackermann, pages 68, 69, 107, 108, etc. A link: academiaanalitica.files.wordpress.com/2016/10/… $\endgroup$ – Paulo Argolo Sep 11 '17 at 23:32
  • 4
    $\begingroup$ @RoddyMacPhee Godel isn't relevant here. $\endgroup$ – Noah Schweber Sep 12 '17 at 3:23
  • 1
    $\begingroup$ Yes; they are really open axioms. In the formula $(x=x)$ there is no quantifiers; thus, the variable $x$ is free. $\endgroup$ – Mauro ALLEGRANZA Sep 12 '17 at 5:59
  • 2
    $\begingroup$ @beroal - Every one... in different forms. It is "built in" in Natural Deduction (see $\forall$-intro) and it is provable in Hilbert -style proof systems. $\endgroup$ – Mauro ALLEGRANZA Sep 12 '17 at 7:08

Here’s where formal semantics really helps. I’ll assume we’re working in classical first-order logic with its standard model theory.

Assuming your axioms have a model, there is therefore an interpretation function in your model which among other things maps (or "assigns") each variable to a specific value. So let’s say the domain of your model is the natural numbers, and the interpretation function happens to map $x$ to the number $2$. So your open axiom really means $2 = 2$ in the semantics. So there’s no way to prove $3 = 3$ with that axiom. If you could, first-order logic would be unsound, which it isn’t, by the Soundness Theorem.

Here’s another way to go at it. Try using your axiom to prove $3 = 3$. You can’t apply your axiom because you can’t specialize $x$ to $3$ as you’d expect; only the universally quantified version of your axiom can do it: $\forall x(x = x)$.

So maybe you could write a theory with open axioms, but as you can see they aren't much use and don't capture what you're trying to capture.

  • $\begingroup$ But in every sound and complete proof system fo predicate logic with equality we can derive $\forall x (x=x)$ from $(x=x)$ (see e.g. Universal generalization). $\endgroup$ – Mauro ALLEGRANZA Sep 12 '17 at 7:27
  • $\begingroup$ @MauroALLEGRANZA Are you sure? The rule for $\forall$-intro is that the variable must not be present in an assumption, and axioms are about as assumptuous as it gets. Being able to derive $\forall x ~:~ x = x$ from $x=x$ would result in being unable to have a triple of axioms defining zero ($Z$) and one ($I$) like $\{\forall x ~:~ x \cdot Z = Z,~ \forall x ~:~ x \cdot I = x,~Z \ne I\}$ since the $Z$ variable (as well as the $I$ variable) would refer to a different variable in each axiom. $\endgroup$ – DanielV Sep 12 '17 at 12:24
  • $\begingroup$ @DanielV: this is one of the perpetually irritating issues. There are indeed systems in which $x = x \vdash (\forall x)[x = x]$, and others in which that logical implication does not hold. So different people learn different systems, and then they find the others surprising. Of course all the usual systems agree on when a set of sentences logically implies another sentence. But they differ for non-sentences. $\endgroup$ – Carl Mummert Sep 12 '17 at 13:33
  • $\begingroup$ Separately, in your set of axioms, the $Z$ is not a variable (as in $x = x$) but a constant (as in, part of the signature of the theory). In some systems, it is possible to generalize any variable, but not always possible to generalize a constant. $\endgroup$ – Carl Mummert Sep 12 '17 at 13:36
  • $\begingroup$ I think it is actually a bit more complicated than that even. For example, in a Hilbert System, it would be more correct to say $(\emptyset \vdash x = x) \vdash \forall x ~ (x = x)$, it is just happens that $(\emptyset \vdash x = x)$ doesn't hold since it isn't a FOL tautology. $\endgroup$ – DanielV Sep 12 '17 at 14:11

Not the answer you're looking for? Browse other questions tagged or ask your own question.