Countermodels
The CounterModeler
class indicates that a code block will contain
countermodel construction exercises.
Simple Countermodels
You can create simple countermodel problems, checking to see if one or more formulas are true in a constructed model like this:
```{.CounterModeler .Simple}
1.1 AxF(x), ExG(x)
```
The result will be:
Here is an example with some more interesting vocabulary:
```{.CounterModeler .Simple}
1.2 AxAy(f(x,y) = f(y,x))
```
Producing:
The domain of the model must consist of one or more natural numbers. The tuples
making up the extensions of predicate and relation symbols are comma-separated
and enclosed in brackets, parentheses, or <>
pairs, like this: [0,0]
or
this <1,1>
. The tuples themselves should be separated by commas, like this:
[0,0],[1,0]
.
The extension of each constant must be a natural number. The extension of a
given function symbol will be a comma-separated list of tuples as above but
with the arguments separated from the value by a semicolon, thus: [0,0;1]
.
Formulas containing free variables are treated as equivalent to their universal closures.
Validity Countermodels
You can create a countermodel problem for showing invalidity like this:
```{.CounterModeler .Validity}
1.3 AxEyF(x,y) :|-: ExAyF(y,x)
```
Creating:
Validity countermodel problems can include comma-separated lists of formulas to both the left and right of the turnstile. A countermodel is successful if it makes all the formulas to the left of the turnstile true and all the formulas to the right of the turnstile false.
Constraint Countermodels
You can create a countermodel with some implicit constraints on the allowable models like this:
```{.CounterModeler .Constraint }
1.4 ExEy(not x = y) : AxAyF(x,y)
```
Resulting in:
A countermodel with implicit constraints is successful if it makes all the
formulas to the right and the left of the :
true.
Advanced Usage
Options
In addition to setting a custom point value or turning off submission by adding
points=VALUE
and submission="none"
, several other options are available for
countermodels:
Name | Effect |
---|---|
nocheck |
Disables the "check" button |
exam |
Allows for submission of work which is incomplete or incorrect |
strictGivens |
Makes givens immutable (see below) |
double-turnstile |
Displays a double turnstile (like so ⊨) rather than the single turnstile |
negated-double-turnstile |
Displays a negated double turnstile (like so ⊭) rather than the single turnstile |
Counterexamples
There are also a number of options that affect what counts as a successful
countermodel. these are set using the counterexample-to
attribute. The
options are:
Name | Counterexample is |
---|---|
validity |
a situation in which all formulas are false |
tautology |
Same as validity |
equivalence |
a situation in which two formulas have different truth values |
inconsistency |
a situation in which all formulas are true |
In the case of simple countermodels, these apply to all formulas. In the case of validity countermodels, a successful countermodel is a situation in which the formulas to the left of the turnstile are all true, and the ones to the right of the turnstile have the counterexample property. Similarly in the case of a constraint countermodel problem---all the constraints must be true, and the other formulas must have the counterexample property.
Systems
The way that formulas are parsed and displayed can also be customized. This is
done by setting the system
attribute to indicate which formal system you are
drawing your syntax from. So for example,
~~~{.CounterModeler .Simple system="LogicBookPD"}
1.5 (Ax)(Ax->Bx)
~~~
will generate:
The available systems are firstOrder
montagueQC
magnusQL
thomasBolducAndZachFOL
thomasBolducAndZachFOL2019
thomasBolducAndZachFOLPlus
LogicBookPD
LogicBookPDPlus
hausmanPL
howardSnyderPL
ichikawaJenkinsQL
hardegreePL
goldfarbAltND
goldfarbNDPlus
and goldfarbAltNDPlus
.
Givens
It is also possible to give a "partial solution" to a countermodeling problem,
in which the model is partly filled in, and the student needs either to
complete it or correct it. To pre-populate models with "givens" in this way,
write each field you want filled in, preceded by the bar character |
and
followed by a colon and what you want it filled in with, like this:
```{.CounterModeler .Simple}
1.1 AxF(x), ExG(x)
| Domain : 0,1,2
| F(_) : 1,2
| a : 1
```
Which will produce:
The field-names for the givens should match how the field-names would be displayed in the exercise.
Ordinarily, givens function as hints. However, you can make it
impossible for students to change them (thereby turning them into
requirements) by adding the strictGivens
option to your problem. Use
this, for instance, to require students to use a specific domain, or
to prevent them from making universal sentences vacuously true.