Students learn the recursive grammar rules that determine if a string of symbols is a Well-Formed Formula. The session culminates in a translation challenge where students formalize a short argument from a peer's thesis draft.