The universal introduction rule
requires that x in the premise is a free variable. (In addition, it must not be free in any open assumption of P(x).) In your derivation, is a constant, so you can't apply this rule to derive .
On the other hand, and are inconsistent and therefore do imply any formula, including : one can conclude any formula directly from , which is obtained from and . However, that arbitrary conclusion would still have an open assumption . In contrast, the proof above takes care to close the temporary assumption .
Unfortunately, I don't have a copy of Copi's book. There are two options: either a is a object variable, or a is a constant. This is how first-order terms are built by definition.n my derivation a is any arbritary selected individual (Antony in my case).
If a is a variable, then your derivation in post #30 is correct. It derives ∀x P(x) from an open assumption ~∃x ~P(x), so this is not surprising.
We need to be clear about the assumptions of the derivation of ∀x P(x). It essentially uses the assumption ~∃x ~Px to derive a contradiction. On the other hand, it does not have ~Pa as an open assumption: it was closed when ~~P(a) was derived from a contradiction. The negation introduction rule, which is used at that point, takes a derivation of a contradiction from some open assumption A and derives ~A; in the process it closes A. Therefore, your derivation of ∀x P(x) in post #30 has a single open assumption: ~∃x ~Px, i.e., essentially, it is a derivation of (~∃x ~Px) -> ∀x P(x).In my post #30 i derived ∀x P(x) from ~Pa
It is somewhat misleading to interpret ~Pa as "Antony is not phony" when a is a free variable. When you say that a stands for a particular person Antony, you treat a as a constant that has a fixed meaning in your interpretation. Formulas with free variables in general cannot be interpreted as a propositions; their truth value depends on the value of the free variables.if Antony is not phonny ,then everybody is a phony ,which is not true
In page 56 line 13 from the top, of Angelo's Margaris FIRST ORDER MATHEMATICAL LOGIC we read and i quote:
"When an assumption is discharged (or closed to use your terminology)by the deduction theorem it does not disappear; it is transferred across |= (|= is a Logical symbol symbolizing conclusion) to become the antecedent of a conditional "
Hence in our case ~Pa ,when discharged ,it does not disappear , it is transferred further down the proof to become the antecedent of a conditional ,which is :