Universal Quantification proof

**chebyshev1** · August 13th 2010, 11:10 AM

x

**Ackbeet** · August 13th 2010, 11:20 AM

I am fairly familiar with LPL and natural deduction. As I recall, $\forall$ 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 $\forall$ 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, $\forall$ elimination seems intuitively obvious: if something is true for all objects, then it's true for a particular object.

**chebyshev1** · August 13th 2010, 02:02 PM

x

**Ackbeet** · August 13th 2010, 02:29 PM

What's the page number and problem number?

**emakarov** · August 14th 2010, 09:03 AM

I want to prove (using a formal proof) that ∀elim is sound.

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 am not sure if the book uses natural deduction, but the ND universal elimination rule is $\frac{\Gamma\vdash A[x]}{\Gamma\vdash\forall x\,A[x]}$ where $x$ is not free in the formulas in $\Gamma$ . (I write $A[x]$ to mean that $x$ may occur freely in the formula $A$ .)

Soundness theorem in general says the following: If $\Gamma\vdash A$ then $\Gamma\models A$ . Here $\Gamma\models A$ means that every model of all formulas in $\Gamma$ is also a model of $A$ . This is equivalent to $\models\bigwedge\Gamma\to A$ , i.e., the implication of the conjunction of formulas in $\Gamma$ and $A$ 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 $\Gamma\vdash A$ then the universal closure of $\bigwedge\Gamma\to A$ is valid, or, in symbolic form, $\models\forall(\bigwedge\Gamma\to A)$ . Here, for any formula $B[x_1,\dots,x_n]$ with free variables $x_1,\dots,x_n$ , the universal closure $\forall B$ of $B$ is $\forall x_1\dots\forall x_n\,B[x_1,\dots,x_n]$ .

What does this mean for universal elimination? For simplicity, assume that all formulas in $\Gamma$ are closed (i.e., no free variables) and $A[x]$ has a single free variable $x$ . Then to prove that the rule is sound means to show that the validity of $\forall x\,(\bigwedge\Gamma\to A[x])$ implies the validity of $\bigwedge\Gamma\to\forall x\,A[x]$ . 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?

**emakarov** · August 14th 2010, 09:08 AM

Oops, two seconds after posting I realized that I am talking about universal introduction. (Could not find a smiley for "ashamed".) Well, soundness of elimination is easier and is a good exercise.

**MoeBlee** · August 14th 2010, 11:06 AM

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.

**MoeBlee** · August 14th 2010, 11:24 AM

Originally Posted by chebyshev1

soundness(?)

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.

**undefined** · August 14th 2010, 11:29 AM

Originally Posted by emakarov

Oops, two seconds after posting I realized that I am talking about universal introduction. (Could not find a smiley for "ashamed".) Well, soundness of elimination is easier and is a good exercise.

Two possible smileys you can use are

(Blush)

(Itwasntme)

Thread: Universal Quantification proof

LinkBack

Thread Tools

Display

Universal Quantification proof

Similar Math Help Forum Discussions

Question about second-order quantification

[SOLVED] Universal and existential statements for prime and composite numbers(proof)

logical quantification

Logic: quantification

universal quantification over null set

Search Tags