# Formal proof : predicate logic

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 1: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 0:55

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
``````
• i don't think step 4 is right . – wenwen Nov 18 '16 at 0:08
• @wenwen fixed it. It's been a while since I used this syntax (See lagunita.stanford.edu/c4x/Philosophy/LPL-SP/asset/…) – virmaior Nov 18 '16 at 1: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 1: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 1:34
• still does't working :( – wenwen Nov 18 '16 at 1:45

``````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)]
``````
• what is rule for the step4 ? I have a little confuse – wenwen Nov 18 '16 at 1: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 2:08