MHB Determine if a Term is Free: Logic for Mathematicians

[Barioth]

Hi everyone,

I'm reading Logic for mathematician form A.G. Hamilton, at some point the book explain what a free term is, but I'm not sure how to determine if t is free or not.

I was wondering if one of you may have a link where I could read more about it.

(I have find some info on wikipedia, but I would like to have some more if possible.)

Thanks!

 

[Evgeny.Makarov]

Do you mean a free variable?

 

[Barioth]

Hi,

The definitions given by the book is:

Let A be any wf (well formed formula) of L (the formal system of statement calculus). A term t is "free" for xi (a variable) in A if xi does not occur free in A within the scope of $$\forall$$ xi, where xi is any variable occurring in t.

Yeah I should have written variable.

I'll write an exemple of question given:

Given the well formed formula A:

$$(\forall x_1) A^3_1(f^2_1(x_1,x_2),x_2,f^1_1(x_2))\rightarrow (\forall x_2)A^2_1(x_1,x_3)$$

and the term $$t=f^2_2(x_1,x_3)$$

A) is t free for x1
B) is t free for x2
C) is t free for x3

note: $$f^i_j$$ are function letters.

I would guess that for A and B t is free, but not for C. But that's just a guts feeling...

 

[Evgeny.Makarov]

The definitions given by the book is:

Let A be any wf (well formed formula) of L (the formal system of statement calculus). A term t is "free" for xi (a variable) in A if xi does not occur free in A within the scope of $$\forall$$ xi, where xi is any variable occurring in t.

First, the defined concept is a "term free for a variable", not just a "free term". It's an ideomatic expression. Admittedly, it is rather obtuse and cannot be deciphered without knowing the definition. Second, I believe this definition uses two variable names and not one $x_i$. That is, a term $t$ is called free for $x$ in $A$ if $x$ does not occur free in $A$ within the scope of $$\forall y$$ where $y$ is any variable occurring in $t$.

The idea is quite simple and relates to "variable capture", which happens when a free variable (and all variables are free in a term) becomes bound when a term is plugged inside a formula. The formerly free variable becomes "captured". Suppose a formula $A$ has the form
\[
\dots(\forall y.\ \dots x\dots)\dots
\]
the indicated occurrence of $x$ is free (that is, it is "visible" from outside of $A$) and $t$ contains $y$. If we substitute $t$ for $x$ (which only makes sense if that occurrence of $x$ is free in $A$), then $y$ finds itself within the scope of $\forall y$ and thus becomes bound.

This situation violates our intuition about a legal substitution. Formally, it turns true formulas (or rather formulas whose universal closure is true) into false ones. For example, the universal closure of $\exists y\,x=y$ is $\forall x\exists y\,x=y$, and it is true in every model. But if we substitute $y+1$ for $x$, the result is $\exists y\,y+1=y$, which is false on numbers. The rule of universal elimination, or instantiation, turns $\forall x\,A[x]$ into $A[t]$, and thus it requires that the substitution is capture-free for its soundness. For another perspective, if we consider terms and formulas as functions that turn values of their free variables into (truth) values, then we view substitution as composition. For example, if the semantics of $A[x]$ is $f:\mathbb{N}\to\{\text{true},\text{false}\}$ and the semantics of $t[y]$ is $g:\mathbb{N}\to\mathbb{N}$, then the semantics of $A[t[y]]$ should be $f\circ g$. This does not happen if $y$ is captured and $A[t[y]]$ is closed, in which case its semantics is a constant.

Perhaps it is better to call a substitution of $t$ for $x$ in $A$ capture-free if free occurrences of $x$ in $A$ do not occur within the scope of quantifiers with variables from $t$. You may find more information if you search for "substitution" and "variable capture". Perhaps you can also redo the exercise if you understand the issue better now. Does the scope of $\forall x_1$ include the whole formula or just the premise of the implication?

By the way, I like my former advisor's convention of using square brackets to indicate that a variable occurs somewhere in a term or formula, such as $A[x]$, and using parentheses when a propositional or functional symbol is applied to a variable, as in $P(x)$ and $f(x)$.

 

[Barioth]

1) Thanks for tacking the time to write such a complete answer.

2)

By the way, I like my former advisor's convention of using square brackets to indicate that a variable occurs somewhere in a term or formula, such as $A[x]$, and using parentheses when a propositional or functional symbol is applied to a variable, as in $P(x)$ and $f(x)$.

$$(\forall x_1) A^3_1(f^2_1(x_1,x_2),x_2,f^1_1(x_2))\rightarrow (\forall x_2)A^2_1(x_1,x_3)$$

Would became, following your advisor's convention:

$$(\forall x_1) A^3_1[f^2_1[x_1,x_2],x_2,f^1_1[x_2]]\rightarrow (\forall x_2)A^2_1[x_1,x_3]$$ ?

3) Using the keyword you gave me, I found some documentation, which (I think) helped me understand more.

I found another definition, which (I think) is more "intuitive" to me, I'll write it down here

"A term t is free for (substitution for) a variable x in a formula A, if no variable in t is captured by a quantifier when t is substituted for
x in A. "
(which seem to be the same as yours, if I have understand correctly)

Link:

http://www2.imm.dtu.dk/~vfgo/02286/2013/Slides/FirstOrderLogicSyntaxFreeBoundVarsQuantScopeCaptureSubstRenamingTrans.pdfNow I'll try to redo the exemple I posted.

starting with
A) is t free for $$x_1$$doing the substitution of $$x_1$$ by t (t given in the first post) we get
The well formed formula A':

$$[\forall x_1) A^3_1[f^2_1[f^2_2[x_1,x_3],x_2],x_2,f^1_1[x_2]]\rightarrow (\forall x_2)A^2_1[f^2_2[x_1,x_3],x_3]$$

Now since the Quantifier $$\forall x_1$$ at the begining, we have that $$x_1$$ in bound within A', so we can conclude that t is bound for $$x_1$$

Doing the same for B) we get the term t is free for $$x_2$$ in A
and for C) t is free for $$x_3$$ in A
Doing some exercice in my book, will write them down here with, what I think, is the solution, if you could tell me if I'm right:

Which occurence of $$x_1$$ in the following well formed formula are free and which are bound:
A)$$(\forall x_2)[A^2_1[x_1,x_2]\rightarrow A^2_1[x_2,a_1]]$$ where $$a_1$$ is an individual constant, I would say that $$x_1$$ is free in this one. Since there is no quantifier that apply to $x_1$

 

[Evgeny.Makarov]

Sorry for the delay. I also realized that the notation $A[x]$, which I introduced, is not essential to the topic, though it is convenient. But since it came up, I could as well clarify what I meant, especially since thinking about it made it clearer for me as well.

$$(\forall x_1) A^3_1(f^2_1(x_1,x_2),x_2,f^1_1(x_2))\rightarrow (\forall x_2)A^2_1(x_1,x_3)$$

Would became, following your advisor's convention:

$$(\forall x_1) A^3_1[f^2_1[x_1,x_2],x_2,f^1_1[x_2]]\rightarrow (\forall x_2)A^2_1[x_1,x_3]$$ ?

No. I am pretty sure that $A^3_1$ and $f^2_1$ are propositional and functional symbols, respectively, so you should use parentheses. Parentheses are elements of the formal language, along with commas, propositional connectives and variable names. In contrast, square brackets are elements of the metalanguage, which is used to talk about formulas and their properties.

Square brackets is another way of writing substitutions, which are functions that map formulas to formulas and thus are defined in the metalanguage, after the definition of formulas is completed. There are many different notations for substitutions, and I'll write $A[t/x]$ for the result of substituting $t$ for $x$ (i.e., replacing $x$ with $t$) in $A$. So, $A[t/x]$ is a phrase of the metalanguage. As a sequence of characters, the word $A[t/x]$ is not a well-formed formula and is not part of the object language of first-order logic. (There are, in fact, formalism where substitution is a part of the object language.)

Instead of writing substitutions explicitly, one can use notations $A[x]$ and $A[t]$. Here $A[x]$ means that $x$ is a free variable that may occur in $A$, and $A[t]$ is the result of replacing that variable with $t$. This resembles application of functions to arguments. Here is how van Dalen puts it in Logic and Structure.

"In order to simplify the substitution notation and to conform to an ancient suggestive tradition we will write down (meta-) expressions like φ(x, y, z), ψ(x, x), etc. This neither means that the listed variables occur free nor that no other ones occur free. It is merely a convenient way to handle substitution informally: φ(t) is the result of replacing x by t in φ(x); φ(t) is called a substitution instance of φ(x)."

My advisor preferred to use square brackets here to clearly indicate that this is a metalanguage operation and to distinguish it from application of a propositional symbol to its arguments. Many books don't use this notation at all and always write substitutions in the form $A[t/x]$.

 

[Evgeny.Makarov]

Now I'll try to redo the exemple I posted.

starting with
A) is t free for $$x_1$$doing the substitution of $$x_1$$ by t (t given in the first post) we get
The well formed formula A':

$$[\forall x_1) A^3_1[f^2_1[f^2_2[x_1,x_3],x_2],x_2,f^1_1[x_2]]\rightarrow (\forall x_2)A^2_1[f^2_2[x_1,x_3],x_3]$$

Now since the Quantifier $$\forall x_1$$ at the begining, we have that $$x_1$$ in bound within A', so we can conclude that t is bound for $$x_1$$

You should not replace the first occurrence of $x_1$ in $A$ with $t$ because that occurrence is not free; it is invisible from outside. Concerning the second occurrence, you have not said whether the scope of $\forall x_1$ extends to the conclusion of the implication.

In general, substituting a term $t$ with a single free variable $x$ for the same variable never results in variable capture: we can only substitute for free occurrences of $x$, and therefore $t$ will not be in the scope of $\forall x$.

Doing the same for B) we get the term t is free for $$x_2$$ in A
and for C) t is free for $$x_3$$ in A

The first occurrence of $x_2$ is free and is within the scope of $\forall x_1$. Therefore, replacing $x_2$ with $t$ results in the capture of $x_1$. The answer to C) depends on the scope of $\forall x_1$.

 

[Barioth]

Sorry for the delay.

Don't be, you're giving me some of your free time, I can only thanks you!

As for the scope of $\forall x_1$ from it should only be on $A^3_1(...)$

So doing the substition:

$$A[t/x]:= (\forall x_1) A^3_1(f^2_1(x_1,x_2),x_2,f^1_1(x_2))\rightarrow (\forall x_2)A^2_1(t,x_3)$$

and then since the $\forall x_1$ doesn't apply to $A^2_1$ I can conclude that t is free for x1 in A?

 

[Evgeny.Makarov]

and then since the $\forall x_1$ doesn't apply to $A^2_1$ I can conclude that t is free for x1 in A?

Yes.