Practice Problems: Proofs for FOL

The following are some practice problems on natural deduction proofs for FOL; i.e., they cover Part VII of forall x: Calgary.

When writing sentences of TFL, remember you can use the following ways to enter connectives that are easier to do with a keyboard:

not ¬ -, ~, not
and ∧ /\, &, and
or ∨ \/, |, or
if then → ->, >, only if
if and only if ↔ <->, <>, if and only if
contradiction ⊥ !?, _|_
universal quantifier ∀ A, @
existential quantifier ∃ E, 3

The rules for

To justify a sentence of the form ∀𝓍 𝒜(𝓍), you need 𝒜(𝒸), say with line number m. Then write as justification "AI m" (replacing m with the actual line number, of course). The name 𝒸 cannot occur in ∀𝓍 𝒜(𝓍) or in any premise or assumption open on line m.

You can use ∀𝓍 𝒜(𝓍) to justify 𝒜(𝒶) (for any name 𝒶, even if it appears in a premise or open assumption). If you have justified ∀𝓍 𝒜(𝓍) on line numer n, write "AE n" next to 𝒜(𝒶) as the justification.

Here's a simple proof that shows that you can rename variables. Fill in the missing justifications:

exercise VII.1
Ax B(x) :PR B(c) Ay B(y)

You can combine the rules for with the rules for the connectives of TFL.

exercise VII.2
Ax(H(x) -> A(x,g)) :PR Ax(A(x,g) -> C(x)) :PR ? Ax(H(x) -> C(x))
exercise VII.3

The rules for

To justify a sentence of the form ∃𝓍 𝒜(𝓍), you need 𝒜(𝒶), say with line number m. Then write as justification "EI m" (replacing m with the actual line number, of course). The name 𝒸 can ∃𝓍 𝒜(𝓍) and in any premise or assumption open on line m.

You can use ∃𝓍 𝒜(𝓍) to justify (for any sentence , if you can complete a subproof which:

  • ends with ,
  • starts with 𝒜(𝒸), and where
  • 𝒸 only occurs in that subproof, but not in .

If you have ∃𝓍 𝒜(𝓍) on line numer n, and your subproof is on lines k-l, write "EE n, k-l" next to (after the subproof) as the justification.

Here's a simple proof that shows that you can rename variables. Fill in the missing justifications:

exercise VII.4
Ex B(x) :PR B(c) :AS Ey B(y) Ey B(y)
exercise VII.5
Ex(H(x) /\ C(x)) :PR Ax(C(x) -> A(x,g)) :PR ? Ex(H(x) /\ A(x,g))
exercise VII.6

Practice problems without quantifier nesting

Here are the two examples from Chapter 33. Try to complete them without looking at the book:

exercise VII.7
exercise VII.8

Here are the two examples from Chapter 36. Again, try them before looking up the solution:

exercise VII.9
exercise VII.10

Here are exercises from Problem A from Chapter 33:

exercise VII.11
exercise VII.12
exercise VII.13
exercise VII.14
exercise VII.15

Problem C contains harder examples; they all require IP.

exercise VII.16
exercise VII.17

These are the two problems from Chapter 36. The first one's easy, the second one hard.

exercise VII.16
exercise VII.17

Proofs with quantifier nesting

exercise VII.18
exercise VII.19

Proofs with identity

"Everyone loves my baby, but my baby loves noone but me"

exercise VII.20

"There is exactly one hero" has two different symbolizations. Let's prove they are quivalent.

exercise VII.21
exercise VII.22

If there is at least one P, and no more than one, there is exactly one.

exercise VII.23

A proof box for you to play in!

Want to use Carnap to construct and check an arbitrary proof? You can do that in this "playground" proof editor. Use it for any of the exercises from Part VII in the book, for instance. (It should accept derived rules, too.)

Playground