1. 8
1.

2. 2

These types of posts are great! Logic has a special place in my heart. I studied it several years prior to getting into programming so I really enjoy when it all comes full circle.

The first three examples can also be analyzed and solved with a good old truth table. I wrote a little sentential logic “prover” project that I’ll use to demonstrate. It’s a Python library called sentential.

Example 1: Both of us are Knaves.

The author writes: “A and B are both False, if and only if A is True.”

This can be translated into sentential logic as: `a <-> (¬a & ¬b)`. Alternatively: `(¬a & ¬b) <-> a`

``````from sentential import Proposition

both_are_knaves = Proposition('''a <-> (¬a & ¬b)''')
both_are_knaves.pretty_truth_table()
+-------+-------+-----------------+
| a     | b     | a <-> (¬a & ¬b) |
+-------+-------+-----------------+
| True  | True  | False           |
| True  | False | False           |
| False | True  | True            |
| False | False | False           |
+-------+-------+-----------------+
``````

In order to find our satisfying condition(s), we inspect the table for rows where the whole expression evaluates to True.

``````# Filter rows to find only cases where the whole expression is True
both_are_knaves.pretty_truth_table(cond=lambda row: row['expr_truth_value'] == True)
+-------+------+-----------------+
| a     | b    | a <-> (¬a & ¬b) |
+-------+------+-----------------+
| False | True | True            |
+-------+------+-----------------+
``````

And there’s our first solution: `a = False`, `b = True`

Example 2: Both of us are Knights or both of us are Knaves

You can build these up piecewise as well – it need not all be done in one shot.

“both of us are knights”: `(a and b)`

“both of us are knaves”: `(¬a and ¬b)`

A is making this claim, so we use the biconditional (`<->`) again: `a <-> ((a and b) or (¬a and ¬b))`

``````both_are_knaves_OR_both_are_knights = Proposition("""a <-> ((a and b) or (¬a and ¬b))""")

both_are_knaves_OR_both_are_knights.pretty_truth_table(cond=lambda row: row['expr_truth_value'] == True)
+-------+------+----------------------------------+
| a     | b    | a <-> ((a and b) or (¬a and ¬b)) |
+-------+------+----------------------------------+
| True  | True | True                             |
| False | True | True                             |
+-------+------+----------------------------------+
``````

Two possible solutions this time: [`a = True`, `b = True`], [`a = False`, `b = True`].

Example 3: A claims to be a Knave, then claims B is a Knave

This example can be expressed as: `(a and ¬a) and (a and b)`.

As the author notes, the initial contradiction prevents this proposition from being satisfiable, so there are no rows of the truth table where the expression = True.

I actually picked up Smullyan’s To Mock a Mockingbird in the past year or so hoping I could tackle some of the problems with provers. Perhaps I should take a look at that again…

Notes:

 I suppose one may say it is an “interpreter” (it computes truth tables and understands how to interpret logical expressions in a sense) or a “prover” (it implements resolution using the set of support of strategy). I wrote it a few years ago for personal edification and because I just had to scratch an itch. Weird itch, I know. (Disclaimer: It is a pet project – should not be relied on for anything approaching real work!)