Is This Predicate Logic Proof Correct?

Click For Summary

Homework Help Overview

The discussion revolves around predicate logic proofs, specifically examining the correctness of logical arguments and the application of rules such as quantifier elimination and conditional proof. Participants are sharing their attempts at solving problems involving existential and universal quantifiers.

Discussion Character

  • Exploratory, Conceptual clarification, Mathematical reasoning

Approaches and Questions Raised

  • Participants are attempting to construct logical proofs and are questioning the validity of their steps, particularly in relation to rules of inference. There are discussions about how to express hypotheses for contradiction and the use of conditional proof.

Discussion Status

Some participants are providing guidance on logical rules and suggesting alternative approaches to the problems presented. There is an ongoing exploration of the implications of certain logical statements, but no consensus has been reached on the correctness of the proofs.

Contextual Notes

Participants are working under the constraints of homework assignments, which may limit the information available for their proofs. There is also a mention of a desire for LaTeX formatting assistance, indicating a focus on presenting logical arguments clearly.

lazycritic
Messages
15
Reaction score
0
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.
 
Last edited:
Physics news on Phys.org
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?
 
Bump. Anyone mind checking these?
 
[tex]\forall \exists \neg \vee \wedge \rightarrow \leftrightarrow \vdash[/tex]
Click the graphic to see the code; Follow the link for more.
lazycritic said:
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 :-p
 
lazycritic said:
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?