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[1] 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

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:

[1] 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!)

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[1] 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`

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

And there’s our first solution:

`a = False`

,`b = True`

Example 2:Both of us are Knights or both of us are KnavesYou 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))`

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 KnaveThis 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 Mockingbirdin 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:

[1] 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

hadto scratch an itch. Weird itch, I know. (Disclaimer: It is a pet project – should not be relied on for anything approaching real work!)