1. Limited time only! Sign up for a free 30min personal 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!

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