# What is "the quantifier axioms of L" and why are they true in all L-structures?

I was going through these notes for logic. They started describing the axioms for predicate logic and said the following:

The quantifer axioms of L are the formulas $$\varphi(t/y) \to \exists y \varphi$$ and $$\forall y \varphi \to \varphi(t/y)$$ where $$t$$ is free for $$y$$ in $$\varphi$$.

This axiom is what doesn't make sense. I just don't know what its saying.

I tried figuring out what it means by parsing its parts. I know earlier in the book he said that $$p \to q$$ was just short hand for $$\neg p \lor q$$ (i.e. implication in propositional logic, which I assume still is the short hand for the same thing in predicate logic since we included the same symbols when defining L-formulas in previous sections). That didn't help much. Also note the notation $$\varphi(t/y)$$ means that if we substitute $$y$$ for $$t$$ or $$\varphi(t/y) = \varphi(t)$$.

I am assuming that what it means is implicitly somehow is that if $$\varphi(t/y)$$ is True in an L-structure, then $$\exists y \varphi$$ is true. In other words if $$\varphi(y)$$ is True, then we have $$\mathcal A \models \exists y \varphi$$. Basically that implication as a whole is always true and thus if we have the first part in isolation to be true then by MP we have the consequent $$\mathcal \models \exists x \varphi$$. Is this more or less what it means? It means that the statement as a whole is always true?

How do you actually show this is true, i.e. that statement is indeed an axiom. If we plug in something to a formula then it implies there exists an element that makes the formula True in some L-structure. Is that what we are trying to show?

note there is a universal axiom too:

$$\forall y \varphi -\to \varphi(t/y)$$

where $$t$$ is free for y in $$\varphi$$

I think I understand that "y is free for x". My confusion stems from the fact that $$\varphi(t/y)$$ is considered true at all. If $$y$$ is not only free from $$x$$ but completely free, in principle, it might not be always be true because it would depend what concrete values of the underlying set $$A$$ in the L structure $$\mathcal A$$ we substitute in for $$y$$.

my confusion stems because on page 37 they define $$\varphi$$ is valid in the L-structure $$\mathcal A$$ if $$\mathcal A \models \varphi \iff \mathcal A \models \forall x_1 \dots x_m \varphi$$, which seems to be opposite of what the existential quantifier is trying to say. Specifically, thats the definition I would plug in to find out what the LHS of the implication means in the existential quantifier axiom. i.e. in $$\varphi (t / y )$$ if I wanted to know if it where true or not.

• I am not sure what you think the term "axiom" means but it seems to have little relation to the actual meaning here. Sep 28, 2018 at 5:04
• @EricWofsey usually axiom means to me a statement that is true by "definition". Sort of the starting rules to play the game of maths or even better metaphor, common ground rules that we agree as true so that we can talk about the same thing. The notes say the the logical axioms (=propositional, equality and quantifier axioms) have been chosen to be true in every L-structure. So I'd guess those particular axioms are always true regardless of "maths world we are" (which is sort of what L-structure means to me). Sep 28, 2018 at 14:10
• @EricWofsey is what I said not correct? What do you mean little relation, to what exactly are you referring to? Sep 30, 2018 at 3:11

Axiom :

$$φ(t/y) → ∃yφ$$

is a version of Existential introduction.

It formalizes the rule (or law) that if we know that $$\varphi$$ is true of some object (or individual) $$t$$, it is true also that there is something that is $$\varphi$$.

Axiom :

$$∀yφ → φ(t/y)$$

is a version of Universal elimination.

It formalizes the rule (or law) that if we know that $$\varphi$$ is true of every object (or individual), it is true also that an object $$t$$ whatever will satisfies $$\varphi$$.

Both are axioms of predicate calculus (Hilbert-style) and thus they are valid, i.e. true in every interpretation ("always true").

To check it, we have to apply the formal semantical specifications for language $$\mathcal L$$, like e.g. :

formula $$∀x \varphi$$ is satisfied in the structure $$\mathfrak A$$ (in symbols : $$\mathfrak A \vDash \varphi$$) iff we have $$\mathfrak A \vDash \varphi(\underline a/x)$$ for every $$a \in A$$, where $$A$$ is the domain of the structure $$\mathfrak A$$, where $$\underline a$$ is the name for the object $$a$$ [see page 32 and Definition page 33 of van den Dries' Lecture Notes].

• what I find confusing with this notaiton is that $y$ could be variable free. So I'm not sure what it would mean for it to be true. The way they define being true formula's in a previous page is that they satisfy the formula for ALL values of y. But in this case its just 1 value of y, which is confusing me. Sep 28, 2018 at 14:35
• "free for" is : consider $\exists y (x \ne y)$ and consider $y$ as $t$. Then $y$ is not free for $x$ in the formula because if we perform the subst we get : $\exists y (y \ne y)$, which is wrong. "free for" means : acoiding "capturing" of free occurrences of variable by existing (into the formula) quantifiers. Sep 28, 2018 at 14:47
• yes I think I understand that "y is free for x". My confusion stems from the fact that $\varphi(t/y)$ is considered true at all. If $y$ is not only free from $x$ but completely free, in principle, it might not be always be true because it would depend what concrete values of the underlying set $A$ in the L structure $\mathcal A$ we substitute in for $y$. Sep 28, 2018 at 14:53
• Consider for simplicity $\varphi(y) \to \exists x \varphi$. Why it is true in every int ? The def says: consider $\forall y (\varphi(y) \to \exists x \varphi$. We have to "check it" for every $a \in A$. Sep 28, 2018 at 15:03
• Two cases : (i) $\varphi(\underline a /y)$ is FALSE. Then the conditional is TRUE. (ii) (i) $\varphi(\underline a /y)$ is TRUE; then (see semantical spec page 33) $\exists x \varphi$ is TRUE, and the conditional is again TRUE. Sep 28, 2018 at 15:05