Dismiss Notice
Join Physics Forums Today!
The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

Homework Help: 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.
     
Share this great discussion with others via Reddit, Google+, Twitter, or Facebook