Suggestions for learning natural deductions in simple and ramified second order logic

Question

I am reading the book Natural Deductions: A proof-theoretic study by Dag Prawitz and stuck at the chapter V of this book, which is about natural deduction in second order logic. Before reading this chapter, I have read some expositions of second order logic by Dirk van Dalen’s Logic and Structure and Enderton’s A mathematical introduction to logic. Still, I couldn’t understand the motivations and related restrictions behind the inference rules in simple and ramified second order logic. Could anyone help me suggest further readings needed to understand that chapter or alternative texts explaining the same matter in more details? Thank you a lot!

Answer 1

For a detailed treatment of SOL, you can see:

• Stewart Shapiro, Foundations without Foundationalism: A Case for Second-order Logic (Clarendon, 1991), Ch.3, page 61-on.

We can consider the case of the universal quantifier.

In FOL we have the restriction on $(\forall \text I)$: $\dfrac {\varphi}{\forall x \varphi}$ that the bound variable $x$ in the conclusion of the inference must not be free in the open assumptions of the derivation.

Similarly, for $(\forall^2 \text I)$: $\dfrac {\varphi}{\forall X^n \varphi}$ we have that the predicate variable $X^n$ must not occur free in any open assumption.

Regarding $(\forall^2 \text E)$: $\dfrac {\forall X^n \varphi}{\varphi^*}$, we have that formula $\varphi^*$ is is obtained from $\varphi$ by replacing each occurrence of $X^n(t_1,\ldots, t_n)$ by $σ(t_1,\ldots, t_n)$ for a certain formula $σ$, such that no free variables among the $t_i$ become bound after the substitution.

Also in this case, we can compare the restriction with that of $(\forall \text E)$ : $\dfrac {\forall x \varphi}{\varphi [x \leftarrow t]}$, where $t$ must be free for $x$.

In this case, what we have to avoid is the following invalid inference: $\forall x \exists y [x < y] \vdash \exists y [y < y]$.

The move is forbidden by the restriction that term $t$ (in this case: variable $y$) must be free for $x$ in the formula.

What happens in SOL?

We have that the substitution operates with a predicate variable $X^n$, replacing it with a suitable formula: $\varphi^* := \varphi [X^n(t_1,\ldots, t_n) \leftarrow σ(t_1,\ldots, t_n)]$, provided that:

(i) formula $σ$ has no predicate variables that can be captured by some quantifier in $\varphi$.

This one is the second order version of the restriction above regarding $(\forall \text I)$.

But, in addition, we have that:

(ii) the terms $t_i$ have no individual variables that can be captured by some quantifier in $\varphi$ [see Prawitz, page 65], i.e.: after the substitution of $X^n$ with the formula $σ(t_1,\ldots, t_n)$, no occurrences of some variable in $σ$ is bound that was not already bound before the substitution.