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:

VII.10 pts
Ax B(x) :PR B(c) Ay B(y)

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

VII.20 pts
Ax(H(x) -> A(x,g)) :PR Ax(A(x,g) -> C(x)) :PR ? Ax(H(x) -> C(x))
VII.30 pts

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:

VII.40 pts
Ex B(x) :PR B(c) :AS Ey B(y) Ey B(y)
VII.50 pts
Ex(H(x) /\ C(x)) :PR Ax(C(x) -> A(x,g)) :PR ? Ex(H(x) /\ A(x,g))
VII.60 pts

Practice problems without quantifier nesting

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

VII.70 pts
VII.80 pts

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

VII.90 pts
VII.100 pts

Here are exercises from Problem A from Chapter 33:

VII.110 pts
VII.120 pts
VII.130 pts
VII.140 pts
VII.150 pts

Problem C contains harder examples; they all require IP.

VII.160 pts
VII.170 pts

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

VII.160 pts
VII.170 pts

Proofs with quantifier nesting

VII.180 pts
VII.190 pts

Proofs with identity

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

VII.200 pts

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

VII.210 pts
VII.220 pts

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

VII.230 pts

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