Three Logicians Walk into a Bar

"Three logicians walk into a bar. The bartender asks them, "do you all want a beer?". The first is unsure, and replies "I don't know". The second is likewise unsure, and replies "I don't know". The third confidently answers "yes!". The bartender serves them all beers."

-Anonymous

Here's a formalization of the proof that demonstrates the joke's consistency (i.e. lack of contradiction).
  1. Let ^ be the binary AND operator.
    1. Axiom: false ^ P is false for any proposition P.
    2. Axiom: true ^ true is true.
    3. Axiom: Associativity. P ^ Q implies Q ^ P for any propositions P and Q.
  2. Let == be the binary EQUALITY operator.
    1. Axiom: P == unsure and P == false implies a contradiction for any proposition P.
  3. Let L_n be the proposition that logician n wants a beer.
  4. Proposition Q == (L_1 ^ L_2) ^ L_3 (the bartender's question).
    1. Axiom: Q == true implies that the bartender serves all logicians beers.
  5. Let Q_n (logician n's answer) be the value of Q according to logician n. This evaluates to Q with L_n being appropriately substituted.
  6. Q_1 == unsure by joke.
    1. Suppose L_1 == false.
    2. Q_1 == (false ^ L_2) ^ L_3, by (5) and (6.1).
    3. Q_1 == (false ^ L_2) ^ L_3 implies Q_1 == false ^ L_3, by (1.1) and (6.2).
    4. Q_1 == false ^ L_3 implies Q_1 == false, by (1.1) and (6.3).
    5. L_1 == false implies a contradiction, by (2.1) and (6.4).
  7. Therefore L_1 is true, by (6.1) and (6.5).
  8. Q_2 == unsure by joke.
    1. Suppose L_2 == false.
    2. Q_2 == (L_1 ^ false) ^ L_3, by (5) and (8.1).
    3. Q_2 == (L_1 ^ false) ^ L_3 implies Q_2 == (true ^ false) ^ L_3, by (7) and (8.2).
    4. Q_2 == (true ^ false) ^ L_3 implies Q_2 == (false ^ true) ^ L_3, by (1.3) and (8.3).
    5. Q_2 == (false ^ true) ^ L_3 implies Q_2 == false ^ L_3, by (1.1) and (8.4).
    6. Q_2 == false ^ L_3 implies Q_2 == false, by (1.1) and (8.5).
    7. L_2 == false implies a contradiction, by (2.1) and (8.6).
  9. Therefore L_2 == true, by (8.1) and (8.7).
  10. Q_3 == true, by joke.
    1. Suppose L_3 == false.
    2. Q_3 == (L_1 ^ L_2) ^ false, by (5) and (10.1).
    3. Q_3 == (L_1 ^ L_2) ^ false implies Q_3 == (true ^ L_2) ^ false, by (7) and (10.2).
    4. Q_3 == (true ^ L_2) ^ false implies Q_3 == (true ^ true) ^ false, by (9) and (10.3).
    5. Q_3 == (true ^ true) ^ false implies Q_3 == true ^ false, by (1.2) and (10.4).
    6. Q_3 == true ^ false implies Q_3 == false ^ true, by (1.3) and (10.5).
    7. Q_3 == false ^ true implies Q_3 == false, by (1.1) and (10.6).
    8. L_3 == false implies a contradiction, by (2.1) and (10.7).
  11. Therefore L_3 == true, by (10.1) and (10.8).
  12. Q == (L_1 ^ L_2) ^ L_3 implies Q == (true ^ L_2) ^ L_3, by (4) and (7).
  13. Q == (true ^ L_2) ^ L_3 implies Q == (true ^ true) ^ L_3, by (9) and (12).
  14. Q == (true ^ true) ^ L_3 implies Q == (true ^ true) ^ true, by (11) and (13).
  15. Q == (true ^ true) ^ true implies Q == true ^ true, by (1.2) and (14).
  16. Q == true ^ true implies Q == true, by (1.2) and (15).
  17. Q == true implies that the bartender serves all logicians beers, by (4.1) and (16). QED.
As you can see, formalizations are often cumbersome, unwieldy, long, and difficult to follow. It's therefore no surprise that most analysis does not apply this level of rigor [1]!
[1]A more rigorous formalization would be a machine-readable one, but it is omitted on account that this essay is being read by humans.