Results 1 to 9 of 9

Math Help - Universal Quantification proof

  1. #1
    Newbie
    Joined
    Aug 2010
    Posts
    6

    Universal Quantification proof

    x
    Last edited by chebyshev1; August 17th 2010 at 11:59 PM.
    Follow Math Help Forum on Facebook and Google+

  2. #2
    A Plied Mathematician
    Joined
    Jun 2010
    From
    CT, USA
    Posts
    6,318
    Thanks
    4
    Awards
    2
    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.
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Newbie
    Joined
    Aug 2010
    Posts
    6
    x
    Last edited by chebyshev1; August 17th 2010 at 11:59 PM.
    Follow Math Help Forum on Facebook and Google+

  4. #4
    A Plied Mathematician
    Joined
    Jun 2010
    From
    CT, USA
    Posts
    6,318
    Thanks
    4
    Awards
    2
    What's the page number and problem number?
    Follow Math Help Forum on Facebook and Google+

  5. #5
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,502
    Thanks
    765
    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?
    Follow Math Help Forum on Facebook and Google+

  6. #6
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,502
    Thanks
    765
    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.
    Follow Math Help Forum on Facebook and Google+

  7. #7
    Senior Member
    Joined
    Feb 2010
    Posts
    466
    Thanks
    4
    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.
    Last edited by MoeBlee; August 14th 2010 at 11:18 AM.
    Follow Math Help Forum on Facebook and Google+

  8. #8
    Senior Member
    Joined
    Feb 2010
    Posts
    466
    Thanks
    4
    Quote Originally Posted by chebyshev1 View Post
    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.
    Follow Math Help Forum on Facebook and Google+

  9. #9
    MHF Contributor undefined's Avatar
    Joined
    Mar 2010
    From
    Chicago
    Posts
    2,340
    Awards
    1
    Quote Originally Posted by emakarov View Post
    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)
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Question about second-order quantification
    Posted in the Discrete Math Forum
    Replies: 4
    Last Post: July 7th 2011, 07:20 AM
  2. Replies: 7
    Last Post: January 6th 2011, 07:23 PM
  3. logical quantification
    Posted in the Discrete Math Forum
    Replies: 12
    Last Post: November 25th 2009, 10:47 AM
  4. Logic: quantification
    Posted in the Discrete Math Forum
    Replies: 0
    Last Post: February 1st 2009, 06:18 AM
  5. universal quantification over null set
    Posted in the Discrete Math Forum
    Replies: 3
    Last Post: July 18th 2007, 03:07 PM

Search Tags


/mathhelpforum @mathhelpforum