Logic

Open In Colab

Logic

This section is going to contain a proof of Church’s Theorem that satisfyability of first-order logic is undecidable. This will be a corollary of the undecidability of tiling. It also will be a place to connect to the Incompleteness Theorem (though this might deserve a section on its own) and to philosophical matters.