Question

College level mathematical logic question (first-order logic, proof with deduction, deduction theorem):

How to prove the following statement deductively of first-order logic? Y ⊢ (Z ∧ ¬Y) ⊃ X
Y is the premise and is the assumption. How can we prove this with deduction?

We got the hint, the we should use the deduction theorem. We also know, that the following axioms might be useful (these are just examples, schemes).
1 X⊃ (Y⊃ X)
2 (X⊃ (Y⊃ Z))→((X⊃ Y)⊃ (X⊃ Z))
3 (¬X⊃Y)⊃((¬X ⊃ ¬ Y)⊃X)
4 ¬ ¬ A ⊃ A
5 A ⊃ (B ⊃ A ∧ B)
6 A ∧ B ⊃ A
7 A ∧ B ⊃ B
8 (A ⊃ C) ⊃ ((B⊃C) ⊃(A v B ⊃ C))
9. A ⊃ A v B
10. B ⊃ A v B

Thanks for any help!

Answer 1

∀xA↔A if x is not free in A

∃xA↔A if x is not free in A

∀x(A(x)∧B(x))↔∀xA(x)∧∀xB(x)

∃x(A(x)∧B)↔∃xA(x)∧B if x is not free in B

∃x(A(x)∨B(x))↔∃xA(x)∨∃xB(x)

∀x(A(x)∨B)↔∀xA(x)∨B if x is not free in B

∀x(A(x)→B)↔(∃xA(x)→B) if x is not free in B

∃x(A(x)→B)↔(∀xA(x)→B) if x is not free in B

∀x(A→B(x))↔(A→∀xB(x)) if x is not free in A

∃x(A(x)→B)↔(A(x)→∃xB) if x is not free in B

∃xA(x)↔¬∀x¬A(x)

∀xA(x)↔¬∃x¬A(x)

¬∃xA(x)↔∀x¬A(x)

¬∀xA(x)↔∃x¬A(x)

All of these can be derived in natural deduction. The last two allow us to push negations inwards, so we can continue to put first-order formulas in negation normal form. Other rules allow us to bring quantifiers to the front of any formula, though, in general, there will be multiple ways of doing this. For example, the formula

∀xA(x)→∃y∀zB(y,z)

is equivalent to both

∃x,y∀z(A(x)→B(y,z))

and

∃y∀z∃x(A(x)→B(y,z)).

A formula with all the quantifiers in front is said to be in prenex form.

8.6. Exercises

Give a natural deduction proof of

∀x(A(x)→B(x))→(∀xA(x)→∀xB(x)).

Give a natural deduction proof of ∀xB(x) from hypotheses ∀x(A(x)∨B(x)) and ∀y¬A(y).

From hypotheses ∀x(even(x)∨odd(x)) and ∀x(odd(x)→even(s(x))) give a natural deduction proof ∀x(even(x)∨even(s(x))). (It might help to think of s(x) as the function defined by s(x)=x+1.)

Give a natural deduction proof of ∃xA(x)∨∃xB(x)→∃x(A(x)∨B(x)).

Give a natural deduction proof of ∃x(A(x)∧C(x)) from the assumptions ∃x(A(x)∧B(x)) and ∀x(A(x)∧B(x)→C(x)).

Prove some of the other equivalences in the last section.

Consider some of the various ways of expressing “nobody trusts a politician” in first-order logic:

∀x(politician(x)→∀y(¬trusts(y,x)))

∀x,y(politician(x)→¬trusts(y,x))

¬∃x,y(politician(x)∧trusts(y,x))

∀x,y(trusts(y,x)→¬politician(x))