I met with a student recently who was a little confused by the relationship between first-order logic, ZFC, dependent types, Martin-Löf, and so on. Recalling S. Aaronson, I explained it by analogy to computers. Proof systems, like first-order logic1 [1 Here I'll be specifically refering to classical first-order logic with equality.] or dependent types, are like the operating system for your computer. By themselves, they do not do much; their main goal is to run particular programs. These pro...
