In a predicate calculus book there is an axiom that states:
provided P admits t for v
in other words the implication holds if we can substitute v for t.
Can anybody give an explanation ,please, with an example??
If it's what I think, is an axiom iff no occurence of in lies within the scope of a quantifier binding a variable of (which is free since it's a term)
This restriction is essential to avoid situations like:
which would be an axiom without the restriction, with and , while you easily see it is wrong whenever you consider a model with at least two elements.
THANK you .
I agree with you.
But then how would you explain the following UNIVERSAL ELLIMINATION rule given in another logic book:
From a universally quantified wff (= well formed formula ) we may infer any wff of the form which results from replacing each occurrence of the variable β in φ by some name letter α
Ιs it right or wrong??
I guess you stay in the same formal system, so you can still use the axiom.
Let be a universal formula, i.e. is quantifier free. We can assume .
If then has only free occurences in therefore you can apply the axiom:
Assume Since has only free occurences in we can once again use the axiom, and get what we wanted.
The UNIVERSAL ELIMINATION in the 1st book appears as the following theorem :
From we can infer P(t/v) PROVIDED that P admits t for v ,using in the derivation of the theorem :
1) The axiom : ,provided P admits t for v.
The UNIVERSAL ELIMINATION in the 2nd book that appears in the post #3 ,
does not have the restriction that the 1st book has .
That is why i was wondering if the rule is right