Suppose you have a proof along the lines of

$$\begin{array} {rc} \text{Assume:} & x > 2 \\ & \vdots \\ & \text{Some logic stuff} \\ & \vdots \\ \text{Conclude:} & x > 1 \\ \end{array}$$

Two common ways for this to be interpreted are (1) $(\forall x~.~x > 2) \to (\forall x~.~x > 1)$ and (2) $\forall x~.~(x > 2 \to x > 1)$. Logics that intend the first way include PRA and Hilbert style FOL. Logics that intend the second way include Fitch style Natural Deduction.

Is there common terminology to distinguish the two approaches to interpreting how the free variables are shared between propositions in a proof? Or if you have reason to think there are no such common terms, what would you suggest?

  • $\begingroup$ There is a termonolgu used by Kleene into his Intro to metamath (1952), page 95 : a variable is varied in a given deduction vs held costant. Absolutely not "standard"... $\endgroup$ – Mauro ALLEGRANZA Nov 13 '18 at 10:56
  • $\begingroup$ @MauroALLEGRANZA Thanks for that reference. I'm also interested in recommendations if you have any. $\endgroup$ – DanielV Nov 13 '18 at 12:28
  • $\begingroup$ Maybe something like global vs local ? In your first example the free var $x$ is implicitly universally quantified "locally", i.e. in the context of the single assumption, while in case (2) above it is quantified "globally", i.e. in the context of the entire derivation. $\endgroup$ – Mauro ALLEGRANZA Nov 13 '18 at 12:32
  • $\begingroup$ Interesting, I was actually thinking the exact same thing. Thanks~ $\endgroup$ – DanielV Nov 13 '18 at 13:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.