x
I am fairly familiar with LPL and natural deduction. As I recall, elimination is regarded as one of the rules of inference. Aren't those regarded as axioms or axiom schemas? If so, those are assumptions. You're probably not going to be able to prove they are true within first order logic. However, it may have been proven that elimination is consistent with the other axioms/axiom schemas. I don't know all that's involved with that other than metalogic theorems. To me, elimination seems intuitively obvious: if something is true for all objects, then it's true for a particular object.
I am not familiar with the book, but I think this question make sense. The universal elimination rule is about syntax, while the question asks to prove that this inference rule is matches the semantics.I want to prove (using a formal proof) that ∀elim is sound.
I am not sure if the book uses natural deduction, but the ND universal elimination rule is where is not free in the formulas in . (I write to mean that may occur freely in the formula .)
Soundness theorem in general says the following: If then . Here means that every model of all formulas in is also a model of . This is equivalent to , i.e., the implication of the conjunction of formulas in and is valid. It is proved by induction on derivation. In order for the induction to go through for first-order logic, it has to be formulated more precisely: if then the universal closure of is valid, or, in symbolic form, . Here, for any formula with free variables , the universal closure of is .
What does this mean for universal elimination? For simplicity, assume that all formulas in are closed (i.e., no free variables) and has a single free variable . Then to prove that the rule is sound means to show that the validity of implies the validity of . This is proved using the definitions, especially those of validity and when a universal formula is true in a particular interpretation.
Does this mesh with what the book says, or do I use completely different concepts?
Some notation (if it doesn't match your book, then you can make any needed adjustments, since the basic concepts are pretty standard):
I'll use 'A' to stand for the universal quantifer.
'P[t|x]' stands for the result of replacing, in the formula P, all free occurrences of x with the term t.
't is free for x in P' means that no occurrences of variables are bound in P[t|x] that weren't already bound in P.
'v is a variable assignment per M' stands for 'v is function from the set of variables into the universe for the structure M'.
'|=_M P [[v]]' stands for 'the formula P is satisfied in the structure M with v (where v is a variable assignment per M).
universal-elim is the rule:
If t is free for x in P, then from AxP we may infer P[t|x].
/
To prove the soundness of universal-elim is to prove:
If t is free for x in P, and |=_M AxP [[v]], then
|=_M P[t|x] [[v]]
So v is a function that maps each variable to a member of the universe (by 'universe' I mean 'universe for the structure').
So, intuitively, |=_M P [[v]] says 'the formula P is satisfied (like 'true' except also covers the case where there are free variables in P) by M with v'.
So, intuitively, universal-elim is sound. That is, if P holds for every x in the universe, then P holds in particular for whatever object is named by t.
Let me know whether you think you can now prove this formally or whether you'd like further help.
But at least now you have an exact specification of the problem.
Roughly put, an inference rule is sound iff the rule never leads from true premises to a false conclusion.
But sometimes we have open formulas (formulas with occurrences of free variables), so we need to consider the more general notion of satisfaction as opposed to the more speical notion of truth.
So an inference rule is sound iff whenever the premises of are satisfied in a model with an assignment for the variables, then the conclusion is satisfied by that model with assignment for the variables.