Formal proof : predicate logic

Question

This is what I need to prove formally:

1.∃x Cube(x) ∧ Small(d)
.
.
.
.
Goal :∃x (Cube(x) ∧ Small(d))

I have already tried different ways, but I still can't prove the goal.

1. ∃x Cube(x) ∧ Small(d)
2. ∃x Cube(x)         ∧Eilm1
3.Small(d)            ∧Eilm1    
4.∃x Small(x)         ∃intro

...

Could you provide some suggestions for how I might prove that?

I'm a little bit confused what you're trying to prove is identical to your premise... since Small(d) is bound, ∃x only ranges over ∃x Cube(x) part even if it is ^ to something else. Did you miswrite what you need to prove? — virmaior, Nov 16 '16 at 23:03
My premise is ∃x Cube(x) ∧ Small(d). And my goal is ∃x (Cube(x) ∧ Small(d)) — wenwen, Nov 16 '16 at 23:42
This is an example where adding extra parenthesis is useful. I presume what you mean is that your premise is ∃x[Cube(x)] ∧ Small(d) and your desired conclusion is ∃x [Cube(x) ∧ Small(d)]? — Cort Ammon, Nov 17 '16 at 01:06
yes.my premise is ∃x[Cube(x)] ∧ Small(d) and my desired conclusion is ∃x [Cube(x) ∧ Small(d)] — wenwen, Nov 18 '16 at 00:55

virmaior · Answer 1 · 2016-11-18T01:04:49.897

3

I would do the following:

1. ∃x Cube(x) ∧ Small(d)
2. ∃x Cube(x)      ∧Elim1
3. Small(d)        ∧Elim1    
4. | Cube(z)         A
5. | Cube(z) ^ Small(d) ^Intr 3,4
6. | ∃x(Cube(x) ^ Small(d)) ∃Intr 5
7. ∃x(Cube(x) ^ Small(d)) ∃Elim 2,4-6

edited Nov 18 '16 at 01:04

answered Nov 17 '16 at 00:00

virmaior

24,518
3
48
105

i don't think step 4 is right . – wenwen Nov 18 '16 at 00:08
@wenwen fixed it. It's been a while since I used this syntax (See https://lagunita.stanford.edu/c4x/Philosophy/LPL-SP/asset/Chapter_13_of_LPL_textbook.pdf) – virmaior Nov 18 '16 at 01:05
But when I type step 5 "Cube(z) ^ Small(d) ^Intr 3,4", the fitch tell me it is not a sentence. How can I do that – wenwen Nov 18 '16 at 01:12
To a large extent, that's fitch being fidly, but you may need to repeat 3 after 4 to be able to ^Intr – virmaior Nov 18 '16 at 01:34
still does't working :( – wenwen Nov 18 '16 at 01:45
@wenwen For what it's worth, I get a correct result with a proof checker using the steps provided in this answer. – Frank Hubeny Aug 06 '18 at 19:34
1

@wenwen I think in Fitch, *z* is a constant, so that 'Cube(z)' is an open sentence. If you use *a* and 'Cube(a)', it should work (even without repeating 3). – MarkOxford Aug 06 '18 at 21:00
@MarkOxford good to know... – virmaior Aug 07 '18 at 00:55

score 1 · Answer 2 · answered Nov 18 '16 at 01:31

1

I would start with

1. ∃x Cube(x) ∧ Small(d)
2. Small(d)
3. ∃x Cube(x)

Which is true because both sides of a true ∧ expression must also be true.

I'd then modify 3 to :

4. ∃x [Cube(x)∧T]

Because you can always intersect something with True without changing its value. I can then substitute one true expression(2) for another true expression (T) because they both have the same truth value

5. ∃x [Cube(x)∧Small(d)]

answered Nov 18 '16 at 01:31

Cort Ammon

17,336
23
59

what is rule for the step4 ? I have a little confuse – wenwen Nov 18 '16 at 01:34
I don't know what name it would be given, but it's easy to prove with a basic truth table. For any P and Q, `Q→(P↔P∧Q) `. As long as Q is true, you can add conjunctions (and) with it as much as you like without changing the truth value of the expression. In my case, Q is the very trivial `T`, which leads to `P↔P∧T`. It's like adding 0 or multiplying by 1. – Cort Ammon Nov 18 '16 at 02:08

Formal proof : predicate logic

2 Answers2