# Thread: Universal Quantifier Introduction Rule

1. ## Universal Quantifier Introduction Rule

Anyone can advise if line (6) is correct?
Restriction for UI is that the x variable must not occur free in any of the assumptions. From line (2), it is clear that -ϕ is bounded, and from line (1), θ is bounded, but how about -θ?

1 (1) ∀x (θ ↔ Ψ) Ass
2 (2) ∀x (-Ψ ∨ -ϕ) Ass
1 (3) (θ ↔ Ψ) UE, (1)
2 (4) (-Ψ ∨ -ϕ) UE, (2)
1,2 (5) (-ϕ ∨ -θ) Taut, (3), (4)
1,2 (6) ∀x (-ϕ ∨ -θ) UI, (5)

These formal proof questions are drowning me...

2. Originally Posted by tottijohn
Anyone can advise if line (6) is correct?
Restriction for UI is that the x variable must not occur free in any of the assumptions. From line (2), it is clear that -ϕ is bounded, and from line (1), θ is bounded, but how about -θ?

1 (1) ∀x (θ ↔ Ψ) Ass
2 (2) ∀x (-Ψ ∨ -ϕ) Ass
1 (3) (θ ↔ Ψ) UE, (1)
2 (4) (-Ψ ∨ -ϕ) UE, (2)
1,2 (5) (-ϕ ∨ -θ) Taut, (3), (4)
1,2 (6) ∀x (-ϕ ∨ -θ) UI, (5)

These formal proof questions are drowning me...
You seem to be using the word,"bounded", in a rather strange way. At least it looks strange to me.
After dropping the quantifiers, what has 'x' been replaced by?

3. From line (2), it is clear that -ϕ is bounded, and from line (1), θ is bounded, but how about -θ?
You seem to be using the word,"bounded", in a rather strange way.
Yes, "bounded" is not used in this sense, especially when talking about subformulas. The standard terminology is, "(An occurrence of) a variable x is free/bound in a formula θ" and "A (sub)formula θ is closed" (when all variables are bound in θ).

In this derivation, the application of UI is correct because in the only two assumptions (1) and (2), x is not free. It does not matter that x may be free in the intermediate formulas (3)--(5) because they are not assumptions.

After dropping the quantifiers, what has 'x' been replaced by?
It isn't replaced, or, rather, it is replaced by itself. Presumably, x is free in θ, Ψ, and ϕ, but it does not have to be. E.g., using Universal Elimination, one gets $x\ge 0$ from $\forall x.\,x\ge 0$, as well as $y\ge 0$ from $\forall x.\,y\ge 0$ (in the latter two formulas, y is free).

So, it is not true that θ is closed; most likely, it has a free occurrence of x.