1. Not finding help here? Sign up for a free 30min tutor trial with Chegg Tutors
    Dismiss Notice
Dismiss Notice
Join Physics Forums Today!
The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

Predicate logic proof

  1. Jun 20, 2006 #1
    Hello,

    I don't know how to prove this:

    [tex]
    \vdash (A \rightarrow B) \rightarrow (\exists x)(A \rightarrow B)
    [/tex]

    First I thought it is just an instantiation of the dual form of the axiom of specification, which says

    [tex]
    \vdash A_{x}[t] \rightarrow (\exists x) A
    [/tex]

    but it probably shouldn't be so easy...

    Would someone give me any hints?

    Thank you.
     
  2. jcsd
  3. Jun 20, 2006 #2

    AKG

    User Avatar
    Science Advisor
    Homework Helper

    Your notation and terminology is different from mine, but yes, it is that easy.
     
  4. Jun 21, 2006 #3
    Thank you. Could you tell me the name you use for the axiom I used here? I often don't know how to translate these things from Czech to English when I want to find something on Google.
     
  5. Jun 21, 2006 #4

    AKG

    User Avatar
    Science Advisor
    Homework Helper

    Different books call it different things. The book I used called it "existential introduction", and in fact it was given in my book as a rule of inference (from [itex]A_x[t][/itex] you may infer [itex](\exists x)(A)[/itex]).
     
  6. Jun 21, 2006 #5
    So I suppose there's no problem having unbound x in [itex]A -> B[/itex]?

    It would be strange if it was problem, but to be sure...
     
  7. Jun 21, 2006 #6

    AKG

    User Avatar
    Science Advisor
    Homework Helper

    Well, what exactly does your book say? You have the scheme [itex]\vdash A_x[t] \rightarrow (\exists x)A[/tex], but like I said, your notation is different from mine. How exactly is Ax[t] defined? I assume it means that every free occurence of x in A is replaced with t? Does it require that there actually is a free occurence of x in A? For example, if A is y=y, then can Ax[t] be defined, and is it just y=y?

    If there are free x in [itex]A \rightarrow B[/itex], then you cannot use the axioms you're given, since if Ax[t] is defined such that EVERY free occurence of x is replaced by t, then if A -> B has free occurences of x in it, it doesn't fit the right format to be used in the "axioms of specificatino" scheme. So if there are free x in [itex]A \rightarrow B[/itex], then I would use the following facts:

    [itex]\phi \vdash (\forall x)(\phi )[/itex] for any formula [itex]\phi[/itex]

    [itex](\forall x)(\phi ) \vdash \phi _x[t][/itex] for any term t, and any formula [itex]\phi[/itex].

    [itex]\vdash (\phi _x[t] \rightarrow (\exists x)(\phi ))[/itex], the axioms you've given.
     
  8. Jun 21, 2006 #7
    We say that term [itex]t[/itex] is substituable for variable [itex]x[/itex] in formula [itex]A[/itex] if for each variable [itex]y[/itex] from [itex]t[/itex] no subformula of [itex]A[/itex] of form [itex](\forall x) B[/itex], [itex](\exists x) B[/itex] contains free occurence of [itex]x[/itex].

    And if this condition is satisfied, then

    [tex]
    A_{x}[t]
    [/tex]

    means formula [itex]A[/itex] with ALL occurrences of [itex]x[/itex] substituted with [itex]t[/itex].

    Given the definition above, I would say, NO, it doesn't require any occurrence of the variable being substitued and YES, the result of what you wrote is just [itex]y = y[/itex].

    I don't get this...if I have let's say formula A

    [tex]
    (x.x = z.x) \rightarrow (z > 0)
    [/tex]

    then if I write [itex]A_{x}[t][/itex], where [itex]t = \sin z[/itex], it is

    [tex]
    (\sin z. \sin z = z.\sin z) \rightarrow (z > 0)
    [/tex]

    and I think it's perfectly ok even though [itex]x[/itex] is of free occurrence in [itex]A[/itex].
     
    Last edited: Jun 21, 2006
  9. Jun 21, 2006 #8

    AKG

    User Avatar
    Science Advisor
    Homework Helper

    Something is wrong here. You mean that subformulas of the form [itex](\forall y)B[/itex] and [itex](\exists y)B[/itex] contain no free occurence of x.
    I was thinking, for some reason, that t had to be a constant symbol. Since t can be any term, Ax[x] is the same as A, and so the "axiom of specification" does apply.
     
  10. Jun 21, 2006 #9
    I think we're both saying the same, I wrote ...no subformula of form....

    So the result is that I should know something more about the variables in [tex]A \rightarrow B[/itex] to know if I can directly use the axiom of specification ( = if term [itex]t[/itex] can be substituted for [itex]x[/itex])?

    Or that I can prove it that way?
     
  11. Jun 22, 2006 #10

    AKG

    User Avatar
    Science Advisor
    Homework Helper

    ... of the form [itex](\forall \mathbf{x})[/itex]..." but it should be [itex](\forall \mathbf{y})[/itex].
    No, I mean you can use the axiom of specification. I assume that the scheme:

    [tex]\vdash A_x[t] \rightarrow (\exists x) A[/tex]

    holds for any formula A, and any term t. Then, in particular its true that:

    [tex]\vdash (A \rightarrow B)_x[x] \rightarrow (\exists x)(A \rightarrow B)[/tex]

    But [itex](A \rightarrow B)_x[x][/itex] is just [itex](A \rightarrow B)[/itex] so indeed

    [tex]\vdash (A \rightarrow B) \rightarrow (\exists x)(A \rightarrow B)[/tex]
     
  12. Jun 23, 2006 #11
    You're right, it's my typo.

    Thank you for help.
     
Know someone interested in this topic? Share this thread via Reddit, Google+, Twitter, or Facebook

Have something to add?



Similar Discussions: Predicate logic proof
  1. Predicate logic (Replies: 2)

Loading...