Results 1 to 6 of 6

Math Help - pridicate calculus

  1. #1
    Banned
    Joined
    Mar 2009
    Posts
    256
    Thanks
    1

    pridicate calculus

    In a predicate calculus book there is an axiom that states:

    \forall vP\Longrightarrow P(t/v) 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??

    Thank you
    Follow Math Help Forum on Facebook and Google+

  2. #2
    Senior Member
    Joined
    Nov 2008
    From
    Paris
    Posts
    354
    Hi

    If it's what I think, \forall vP\Rightarrow P[t/v] is an axiom iff no occurence of v in P lies within the scope of a quantifier binding a variable of t (which is free since it's a term)

    This restriction is essential to avoid situations like:

    \forall v\exists x(\neg x=v)\Rightarrow \exists x(\neg x=x)

    which would be an axiom without the restriction, with P= \exists x(\neg x=v) and t=x, while you easily see it is wrong whenever you consider a model with at least two elements.
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Banned
    Joined
    Mar 2009
    Posts
    256
    Thanks
    1
    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 ) \forall\beta\phi we may infer any wff of the form \phi\alpha/\beta which results from replacing each occurrence of the variable β in φ by some name letter α

    Ιs it right or wrong??
    Follow Math Help Forum on Facebook and Google+

  4. #4
    Senior Member
    Joined
    Nov 2008
    From
    Paris
    Posts
    354
    I guess you stay in the same formal system, so you can still use the axiom.

    Let \forall x_n...\forall x_1 F[x_n,...,x_1] be a universal formula, i.e. F is quantifier free. We can assume x_i\neq x_j if i\neq j.

    If n=1, then x_1 has only free occurences in F[x_1], therefore you can apply the axiom: \forall x_1F\Rightarrow F[\beta_1 /x_1].

    Assume \forall x_{n-1}...\forall x_1F\Rightarrow F[\beta_{n-1}/x_{n-1},...,\beta_1/x_1]. Since x_n has only free occurences in \forall x_{n-1}...\forall x_1F, we can once again use the axiom, and get what we wanted.
    Follow Math Help Forum on Facebook and Google+

  5. #5
    Junior Member
    Joined
    Oct 2006
    Posts
    71
    Quote Originally Posted by xalk View Post
    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 ) \forall\beta\phi we may infer any wff of the form \phi\alpha/\beta which results from replacing each occurrence of the variable β in φ by some name letter α

    Ιs it right or wrong??
    It's somewhat restrictive, but certainly not wrong.
    Note, the author refers specifically to "name letter".
    By name, she surely means designator. That's a closed term.
    The so-called "non-capture" restriction applies only to open terms.
    Follow Math Help Forum on Facebook and Google+

  6. #6
    Banned
    Joined
    Mar 2009
    Posts
    256
    Thanks
    1
    The UNIVERSAL ELIMINATION in the 1st book appears as the following theorem :

    From \forall v.P we can infer P(t/v) PROVIDED that P admits t for v ,using in the derivation of the theorem :

    1) The axiom : \forall vP\Longrightarrow P(t/v),provided P admits t for v.
    2) M.Ponens.

    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
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Replies: 2
    Last Post: June 25th 2010, 11:41 PM
  2. Replies: 1
    Last Post: February 11th 2010, 08:09 AM
  3. proof in pridicate calculus
    Posted in the Discrete Math Forum
    Replies: 5
    Last Post: October 14th 2008, 12:11 PM
  4. Replies: 1
    Last Post: June 23rd 2008, 10:17 AM
  5. Replies: 1
    Last Post: June 7th 2008, 12:47 PM

Search Tags


/mathhelpforum @mathhelpforum