Scope and Substitution

To use Natural Deduction for Predicate Logic we need to upgrade our ideas of judgement to track which variables are in scope during a proof. We also need to be able to correctly substitute terms into formulas with free variables.

Slides for the videos (PDF)

Managing which variables are in scope

The key difference between Propositional Logic and Predicate Logic is that the latter allows us to name individuals x, y and so on. To upgrade Natural Deduction to handle Predicate Logic, we need to make sure that we keep track of the names that we are using in our proofs, making sure that our terms and formulas are well-scoped.

Well-scopedness of terms and formulas means that all the variables mentioned in a term or formula are already declared to the left of them in a judgement. This is explained in the following video:

Enter any notes to yourself here.

Exercises

Are these judgements well scoped?

```
P(a()) |- Q
```
(config (options ("Well Scoped" "Not Well Scoped")))
Answer...
Well Scoped. The a() names an individual from the vocabulary, and is not a variable.
```
Q(z,s(z())) |- P
```
(config (options ("Well Scoped" "Not Well Scoped")))
Answer...
Not Well Scoped. The variable “z” has not been declared to the left of where it is used.
```
x, y, P(x,y), Q(x) |- R
```
(config (options ("Well Scoped" "Not Well Scoped")))
Answer...
Well Scoped. The variables “x” and “y” have both been declared to the left of where they are used, and there are no other variables.
```
x, y, P(x,y), Q(x), R(z) |- S
```
(config (options ("Well Scoped" "Not Well Scoped")))
Answer...
Not Well Scoped. The variables “x” and “y” have been properly declared, but “z” has not.
```
x, y, P(x,y), ∀z. Q(z), R(z) |- S
```
(config (options ("Well Scoped" "Not Well Scoped")))
Answer...
Not Well Scoped. The “z” in “∀z. Q(z)” is bound by the quantifier, but the “z” in “R(z)” has not been declared.
```
x, y, P(x,y), Q(x), ∀z. R(z) |- S
```
(config (options ("Well Scoped" "Not Well Scoped")))
Answer...
Well Scoped. The “z” in “∀z. R(z)” is bound by the quantifier. The “x” and the “y” have been declared before (i.e., to the left of) use.
```
x, P(x,y), y, Q(x) | -R
```
(config (options ("Well Scoped" "Not Well Scoped")))
Answer...
Not Well Scoped. The “y” in “P(x,y)” is not in scope.
```
|- P(x)
```
(config (options ("Well Scoped" "Not Well Scoped")))
Answer...
Not Well Scoped. The variable “x” has not been declared.
```
|- ∀x. P(x)
```
(config (options ("Well Scoped" "Not Well Scoped")))
Answer...
Well Scoped. The quantifier “∀x.” binds the use of “x” in “P(x)”.
```
x, y |- P(x)
```
(config (options ("Well Scoped" "Not Well Scoped")))
Answer...
Well Scoped. The variable “x” is used in the conclusion, and has been declared in the context.
```
x [Q(y)] |- ∀y. P(y)
```
(config (options ("Well Scoped" "Not Well Scoped")))
Answer...
Not Well Scoped. The formula in focus “Q(y)” uses the variable “y” which has not been declared.
```
x, P(y) [Q(y)] |- ∀y. P(y)
```
(config (options ("Well Scoped" "Not Well Scoped")))
Answer...
Not Well Scoped. The assumption “P(y)” uses the variable “y” which has not been declared.
```
x, y, P(y) [Q(y)] |- ∀y. P(y)
```
(config (options ("Well Scoped" "Not Well Scoped")))
Answer...
Well Scoped. The assumption “P(y)” uses the variable “y” which has not been declared.

Substitution

Next is the important concept of subsitution. Substitution is how we go from a general statement like “for all x, if x is human, then x is mortal” to a specific statement "if socrates is human, then socrates is mortal": we substitute the specific individual “socrates” for the general variable “x”.

Substitution is not much more than simply “plugging in values”, like you may be used to in formulas in mathematics, but gets a little more subtle when we have formulas that bind variables in them, as we see in this video:

Enter any notes to yourself here.

Exercises

Compute the results of the following substitutions, being careful with renaming to avoid variable capture.

```
(∀x. P(x) -> Q(x,y))[x := f(x)]
```
Enter your formula here
```
(∀x. P(x) -> Q(x,y))[y := f(x)]
```
Enter your formula here
```
(P(x) -> (∃x. q(x,y)))[x := g(y)]
```
Enter your formula here
```
(p(x) -> (∃y. q(x,y)))[x := g(y)]
```
Enter your formula here