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

    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:

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