1
$\begingroup$

I was following these notes and there was a section where they showed the following formula:

$$ \varphi(y) = \exists x (x \ne y)$$

and if one replaces the free variable $y$ with the variable $x$:

$$ \varphi(x/y) = \exists x (x \ne x)$$

then the above stops being true in every L-structure. In particular they say:

Thus, substituting x for the free occurences of y does not always preserve validity.

And thats why they go ahead and define

t is free in y in $\varphi$, if no variable in $t$ can become bounded upon replacing the free occurences of $y$ in $\varphi$ by t

for me it seems very weird that they go and define this notion of substitution or that they are disturbed that substituting x for y makes a formula invalid. Why is that disturbing or considered an anomaly? Of course that could happen depending what one substitutes!

I feel despite the extensive discussion, I fail to appreciate the need to define a new type of substitution that "preserves validity". Why does that matter? Things could change depending on what one substitutes.

Furthermore, as someone who like programming languages it seems to me is that we are in the face of an ambiguity, have to choose the semantics of what the ambiguous sentence:

$$ \varphi(x/y) = \exists x (x \ne x)$$

means. In one hand its bounded and controlled by a quantifier and on another its the input to a function. So if this were a programming language then if we consider the exists as a for loop, the input is always ignored. But we could have chosen the semantics to ignore the quantifiers for this specific formal language and listen to the input variable as the one holding the meaning (but obviously from the worry of this example it seems that quantifiers take precedence).

It just feels that I don't appreciate why they defined a way that preserves validity (plus I don't know why thats even true) and even if it were true, so what? I see more as an ambiguity as a designer of the language having the opportunity to choose a semantics. I don't care which semantics we choose, clearly from the way I'm talking about it, but the text clearly cares it seems. Any help? What am I missing?


For context here is the exact text from page 39.

Let x and y be distinct variables, and let ϕ(y) be the formula ∃x(x 6= y). Then ϕ(y) is valid in all A with |A| > 1, but ϕ(x/y) is invalid in all A. Thus substituting x for the free occurrences of y does not always preserve validity. To get rid of this anomaly, we introduce the following restriction on substitutions of a term t for free occurrences of y.

Definition. We say that t is free for y in ϕ, if no variable in t can become bound upon replacing the free occurrences of y in ϕ by t, more precisely: whenever x is a variable in t, then there are no occurrences of subformulas in ϕ of the form ∃xψ or ∀xψ that contain an occurrence of y that is free in ϕ.


The reason I am extra picky about this is because this notion seems important for understanding the quantifier axiom of L:

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

which builds up all predicate logic.

Though, my guess is the following. Consider the second axiom: $\forall y \varphi \to \varphi(t/y)$. My guess what the axiom is meant (semantically) to say is:

$$\forall y \in A, \varphi \to \varphi(t/y), \text{for any }t \in A$$

and the for all doesn't mean for all literally (i.e. allowing variables). If we didn't take this semantics approach, then the consequent of the above implication could be false despite $\varphi$ being true for all $y$ (meaning True implies False, which is bad!).

$\endgroup$
  • $\begingroup$ Substitution is defined at the bottom of page 29. Why do you think $\varphi(x/y)$ is ambiguous? $\endgroup$ – Fabio Somenzi Oct 2 '18 at 4:29
2
$\begingroup$

Substitution (page 29) is a syntactical operation defined on a formula $\varphi$ and is performed replacing free occurrences of a variable $x$ with a term $t$ : $\varphi(t/x)$.

Unfortunately, some substitution may cause troubles, because they change the "meaning" of the formula.

Consider the following example regarding first-order language of arithmetic : $\forall y \exists x (y < x)$.

Call it $\varphi$ and consider the substitution : $\varphi(x/y)$; it will be : $\exists x (x < x)$, which is clearly false.

This is why - in formulating axioms and rules - we have to apply suitable restrictions to the substitutions allowed : in order to preserve truth.

Regarding your "improved" version of the quantifier axiom, we have to note that the formula must be interpreted in a domain $A$ : but we want it to be valid, i.e. true in every interpretation.

Thus, when we interpret it in a domain $A$, the leading quantifier $∀y$ means exactly : "for every object in the domain $A$".

The "inference rule" formalized with the axiom says exactly: if the antecedent is true, the consequent is true also, whatever term $t$ we use to instantiate the universal quantifier, provided that the substitution is "sound" (see : the free for condition (page 39)).


Having said that, why "does it matter when we a substitution of a free variable into some $\mathcal L$-formulas preserve validity?"

Because we want that our proof system is sound, i.e. we want that it preserves truth (and validity).

Thus, the condition "free for" (necessary in order to avoid "unsound" substitutions) must be used in formulating quantifier axioms and rules.

The example above is quite clear; the formula $\forall y \exists x (y < x)$ is true in $\mathbb N$ (the structure with domain the set of natural numbers), while its (wrong) substitution instance : $\exists x (x < x)$, is false in $\mathbb N$.

$\endgroup$
0
$\begingroup$

I think the main idea is that when you have $\exists x (x \not = y)$ if you put $y=x$ you get: $\exists x (x \not = x)$. The issue is that the original statement "assumed" x and y were different variables. So by putting the $x=y$ we actually changed the meaning of the statement (L-sentence) in question. Thus, we care about not making variables collide because meanings for things change, which is simply reflected by truth values changing too. This is not what we want, its not what the creator of the sentences intended is my understanding of why we care about his.

$\endgroup$

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.