The meaning of a standalone predicate statement as an assumption or step in a formal proof

80 Views Asked by At

In Example 9 of section 17 of 'First Order Mathematical Logic' by Angelo Margaris, it is stated that:

In this example from number theory, we show what can happen if the restriction on gen ($v$ is not free in $\Delta$) is violated.

  1. $x < 2$ (as)
  2. $\forall x(x < 2)$ (gen)

... The error occurs at step 2. Since $x$ is free in the assumption $x < 2$, gen cannot be applied with $x$ until this assumption is discharged...

What does $x < 2$ mean as an assumption if it does not mean that for every $x$ in the domain of discourse $x < 2$ is true?

2

There are 2 best solutions below

10
On

In "gen" one can go from $\Delta$ to $\forall v \Delta,$ provided $v$ is not free in $\Delta,$ the latter meaning that $\Delta$ cannot contain $v$ as a free variable.

Ex: OK to say given $ \exists a (a>2)$ that it follows $\forall x \exists a (a>2).$ In this case the $x$ is not free in the $\exists a (a>2).$

The problem that can arise is when the variable generalized over is "free" in the statement over which generalization is to be done, since before the generalization the statement is only about one specific case, while after generalization it would be saying true for all cases of the generalizing variable.

You might want to look up the topic of "free and bound variables" which is a subtopic of quantifier theory.

5
On

Comment : in the calculus, on open formula is not "implicitly" universally quantified.

Consider :

1) $x=2$ (as)

2) $∀x(x=2)$ (gen) --- wrong !

3) $x=2 \to ∀x(x=2)$ --- from 1) and 2) by $\to$-intro (or Deduction Th, or Conditional Proof)

4) $∀x (x=2 \to ∀x(x=2))$ (gen) --- correct

5) $2=2 \to ∀x(x=2)$ --- from 4) instantiating the quantified variable $x$.