Results 1 to 6 of 6

Thread: 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:

    $\displaystyle \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, $\displaystyle \forall vP\Rightarrow P[t/v]$ is an axiom iff no occurence of $\displaystyle v$ in $\displaystyle P$ lies within the scope of a quantifier binding a variable of $\displaystyle t$ (which is free since it's a term)

    This restriction is essential to avoid situations like:

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

    which would be an axiom without the restriction, with $\displaystyle P= \exists x(\neg x=v)$ and $\displaystyle 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 ) $\displaystyle \forall\beta\phi$ we may infer any wff of the form $\displaystyle \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 $\displaystyle \forall x_n...\forall x_1 F[x_n,...,x_1]$ be a universal formula, i.e. $\displaystyle F$ is quantifier free. We can assume $\displaystyle x_i\neq x_j if i\neq j$.

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

    Assume $\displaystyle \forall x_{n-1}...\forall x_1F\Rightarrow F[\beta_{n-1}/x_{n-1},...,\beta_1/x_1].$ Since $\displaystyle x_n$ has only free occurences in $\displaystyle \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 ) $\displaystyle \forall\beta\phi$ we may infer any wff of the form $\displaystyle \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 $\displaystyle \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 : $\displaystyle \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: Jun 25th 2010, 10:41 PM
  2. Replies: 1
    Last Post: Feb 11th 2010, 07:09 AM
  3. proof in pridicate calculus
    Posted in the Discrete Math Forum
    Replies: 5
    Last Post: Oct 14th 2008, 11:11 AM
  4. Replies: 1
    Last Post: Jun 23rd 2008, 09:17 AM
  5. Replies: 1
    Last Post: Jun 7th 2008, 11:47 AM

Search Tags


/mathhelpforum @mathhelpforum