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$
Additional comments:
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$.
Additional comments:
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.
Best Answer
Axiom :
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 :
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. :
You can see also : Classical Quantificational Logic.