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: More predicate logic problems

  1. May 10, 2005 #1

    If anyone here likes working on these problems, I'm working on a couple more. I finished the first two. These go:

    1. Vx Vy (Fxy ---> ~Fyx) |- -ExFxx
    (now my work - maybe wrong
    2. Vy (Fay ---> ~Fya) 1,VE
    3. (Faa ---> ~Faa) 2,VE
    4. | Faa H(for -->E)
    5. | ~Faa 3,4, CON
    6. Faa
    7. ~~Faa 3,6, MT
    (I find this hard to articulate in the logical format, but basically, if ~Faa is proved wrong by Faa in line six(~(~Faa)), then MT says that ~Faa can be infered...)
    8. ~Faa
    9. -ExFxx 8, EI(can I do this?)

    Actually ended up working it out as I posted it. Is it right, though? Btw, does anyone know the tex way to do this?

    Test: [tex]VxEy(Mxy -> Fxy) [/tex]

    Didn't work.
    Last edited: May 10, 2005
  2. jcsd
  3. May 10, 2005 #2
    I think I got the next problem, a theorom, but if anyone can look over it, I'd appreciate it.

    4) |- ~Ex(Fx & ~Fx)

    1. | ~[~Ex(Fx & ~Fx)] H(for con) - that how would I say I'm hypothesizing for a contradition?

    2. | Ex(Fx & ~Fx) 1, DN
    3. | Fa & ~Fa 2, E Elim.(tex would be nice here)
    4. ~Ex(Fx & ~Fx) 1-3 Con?
  4. May 10, 2005 #3
    Bump. Anyone mind checking these?
  5. May 10, 2005 #4


    User Avatar
    Gold Member

    [tex]\forall \exists \neg \vee \wedge \rightarrow \leftrightarrow \vdash[/tex]
    Click the graphic to see the code; Follow the link for more.
    From 4 and 5 you can infer Faa -> ~Faa (which you already have). Conditional proof gives you a conditional- a conditional which says that your hypothesis implies whatever you can derive while assuming it.
    Remember I don't know much about quantifier elimination and introduction. Maybe you could post your rules for these.
    If you can get
    3. Faa -> ~Faa
    4. ~Faa v ~Faa [3, Implication]
    5. ~Faa [4, Tautology]
    Of course, those are what my rules are called, you may use different names or different rules. But if you can see that (P -> Q) <=> (~P v Q) and (~P v ~P) <=> ~P, you can probably find the rules you need.

    Patience, grasshopper :tongue2:
  6. May 10, 2005 #5


    User Avatar
    Gold Member

    That seems fine. There are two rules that use provisional hypotheses: Conditional proof and Reductio ad absurdum. You can find both rules here. I highly recommend you read those rules!
    Not by any rules I know. However, you can do:
    1. | Fa & ~Fa [Reductio]
    2. | Fa [1, Simplification]
    3. | ~Fa [1, Simplification]
    Now what can you infer from that?
Share this great discussion with others via Reddit, Google+, Twitter, or Facebook