More predicate logic problems

  • Thread starter lazycritic
  • Start date
  • #1
15
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:

Answers and Replies

  • #2
15
0
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?
 
  • #3
15
0
Bump. Anyone mind checking these?
 
  • #4
honestrosewater
Gold Member
2,105
5
[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 :tongue2:
 
  • #5
honestrosewater
Gold Member
2,105
5
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?
 

Related Threads on More predicate logic problems

  • Last Post
Replies
7
Views
3K
  • Last Post
Replies
10
Views
4K
Replies
5
Views
3K
  • Last Post
Replies
2
Views
1K
  • Last Post
Replies
10
Views
2K
  • Last Post
Replies
5
Views
3K
  • Last Post
Replies
1
Views
7K
  • Last Post
Replies
4
Views
1K
  • Last Post
Replies
16
Views
5K
  • Last Post
Replies
1
Views
1K
Top