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...
From line (2), it is clear that -ϕ is bounded, and from line (1), θ is bounded, but how about -θ?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 θ).You seem to be using the word,"bounded", in a rather strange way.
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.
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 from , as well as from (in the latter two formulas, y is free).After dropping the quantifiers, what has 'x' been replaced by?
So, it is not true that θ is closed; most likely, it has a free occurrence of x.