| model | Definition. A MODEL for a set of sentences is an interpretation in which all the sentences in the set are true. |
| countermodel | Definition. A COUNTERMODEL for a given argument is a model for the premises in which the conclusion is false. |
| Comment. The idea behind a countermodel is the same as that behind using a truth table to demon- strate that an argument is invalid. The point is to demonstrate that it is possible for all the premises of an ar-gument to be true and still have the conclusion turn out false. Thus, a countermodel is the predicate-logic analogue of an invalidating assignment (introduced in chapter 2). | |
| Comment. Given an invalid sequent with one-place predicates and no many-place predicates, it is always possible to find a finite countermodel. Indeed, if the sequent contains n predicates, the universe of a countermodel need not have more than 2n elements, and will often have fewer. | |
| Comment. Expansions provide a convenient way of demonstrating that a given interpretation is a countermodel for an argument. | |
|
Examples. (a) Give a countermodel and an expansion to show this sequent invalid: $xGx |- P -> @xGx Model: U: {a,b} G: {a} P is True Expansions: The premise $xGx expands to Ga v Gb with these truth assignments: T v F T The conclusion P -> @xGx expands to P -> (Ga & Gb) with these truth assignments: T -> (T & F) T -> F F The premise is true and the conclusion is false in this interpretation, so the argument is invalid. |
|
|
(b) Give a countermodel and an expansion to show this sequent invalid: @xFx -> @xGx |- Fm -> $xGx Model: U: {m,a} F: {m} G: { } Expansion: The premise (@xFx -> @xGx) expands to
Fm & Fa -> Gm & Ga
T F F T
The conclusion (Fm -> $xGx) expands to
Fm -> Gm v Ga
T F F F F
The conclusion is false in this interpretation and the premise is true; hence, this interpretation is a countermodel for the given sequent. |
|
| Exercise 4.3 | Construct countermodels and expansions to show the following sequents invalid. |
| i* | @xFx -> @xGx |- @x(Fx -> Gx) |
| ii* | $xFx -> $xGx |- @x(Fx -> Gx) |
| iii* | $xFx & $xGx |- $x(Fx & Gx) |
| iv* | $x(Fx v Gx) |- @xFx v @xGx |
| v* | $x(Fx -> Gx) |- $xFx -> $xGx |
| vi* | $x(Fx -> Gx) |- @xFx -> @xGx |
| vii* | @xFx <-> @xGx |- @x(Fx <-> Gx) |
| viii* | $xFx <-> $xGx |- @x(Fx <-> Gx) |
| ix* | @xFx <-> P |- @x(Fx <-> P) |
| x* | $xFx <-> P |- @x(Fx <-> P) |
| xi* | $x(Fx <-> P) |- $xFx <-> P |
| xii* | $x(Fx <-> P) |- @xFx <-> P |
| xiii* | @x(Fx -> Gx), @x(Gx -> Hx) |- @x(Hx -> Fx) |
| xiv* | @x(Fx -> ~Hx), @x(Hx -> ~Gx) |- $x(Fx & Gx) |
| xv* | $xFx <-> @xGx, ~@x(Fx -> Hx) |- $xHx -> $x~Gx |
| xvi* | @x(Gx v ~Hx), $x(Gx & Fx) |- $x~Hx |
| xvii* | @x(Fx & Gx -> Hx), $x(Fx & Hx) |- $xGx |
| xviii* | $xFx, $xGx, $xHx |- @x(Fx v Gx -> Hx) |
| xix* | ~@xFx |- @x~Fx |
| xx* | $x(Fx -> $yGy) |- $xFx -> $yGy |