Is This Predicate Logic Proof Correct?

[lazycritic]

Hey,

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.

 

[lazycritic]

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?

 

[lazycritic]

Bump. Anyone mind checking these?

 

[honestrosewater]

[tex]\forall \exists \neg \vee \wedge \rightarrow \leftrightarrow \vdash[/tex]
Click the graphic to see the code; Follow the link for more.

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

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
Then
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

 

[honestrosewater]

how would I say I'm hypothesizing for a contradition?

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!

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

1. | ~[~Ex(Fx & ~Fx)] H(for con) - that

2. | Ex(Fx & ~Fx) 1, DN
3. | Fa & ~Fa 2, E Elim.(tex would be nice here)
4. ~Ex(Fx & ~Fx) 1-3 Con?

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?