snnw·8년 전·discussGodel's theorem only applies to proof systems that can encode basic arithmetic, which most type systems cannot.