Use of unconditional probability

Filed under: math — jlm @ 21:06

Recently I had a discussion with some friends about the probability that a certain card was among the first n cards dealt from a shuffled deck of m cards. Here I’m going to only cover the specific case of a deck consisting of the 13 spades, and the chance that the ace is one of the first two cards dealt — n=2 and m=13. We came up with four ways to perform this elementary probability calculation.

Combinatorics: There are 12C1 ways to have the ace and one other spade, without regard to order. There are 13C2 ways to deal two spades. So the probability is 12C1/13C2 = 12/78 = 2/13.

Trickery: The chance the first card isn’t the ace is 12/13. The chance that the second card, dealt from the remaining 12 cards, also isn’t the ace is 11/12. So the chance that neither is the ace is (12/13)⋅(11/12) = 11/13. Thus the chance that one of the first two cards is the ace is 1 − 11/13 = 2/13.

Conditional probability: The chance that the first card is the ace is 1/13 and the chance it isn’t is 12/13. If we represent the event of the first card being the ace as 1 and the event the second card is the ace as 2, then that is P(1) = 1/13 and P(~1) = 12/13. Now, P(2|~1) = 1/12. ∴ P(1 or 2) = P(1) + P(2|~1)⋅P(~1) = 1/13 + (1/12)⋅(12/13) = 1/13 + 1/13 = 2/13.

Unconditional probability: P(1 or 2) = P(1) + P(2) − P(1 and 2) = 1/13 + 1/13 − 0 = 2/13.

They all generalize into dealing n cards out of m, but the one using unconditional probability not only is the simplest, it generalizes the most cleanly. But most of us found it the least satisfying solution. Maybe because it was too simple?


Ouroboros in Std.Logic

Filed under: math — jlm @ 18:14

This post dissects a very short yet fascinating and enigmatic proof that can be found in the Logic module of the standard library of the Lean proof verifier:

theorem iff_not_self : ¬(a ↔ ¬a)
  | H => let f h := H.1 h h
         f (H.2 f)

OK, the fact being proved isn’t enigmatic — it’s stating that a proposition’s truth value is never the same as its own negation’s — but the proof thereof sure is. If that looks to you like some incomprehensible formal logic circling to eat its own tail, that’s because it kinda is.

However, it’s written extremely densely, which inhibits comprehension — which is sad, because the way it works is very interesting. It’s quite the rabbit hole, though, so let’s take our trusty spade and start digging. The very first thing we encounter is that Lean implicitly converts the ¬(a ↔ ¬a) into (a ↔ ¬a) → False. This is because Lean uses dependent type theory to represent logical statements and their proofs, so we need to discuss how these kinds of theories are used with formal logic.


Powered by WordPress