Abstract: 

The completeness theorem guarantees that any consistent theory has a model, but it is not hard to show that a computable version of this statement does not hold: there is a computable, consistent theory with no computable model. For example, a slight modification of the proof of Tennenbaum's Theorem implies that the theory ZF has no computable model. Recently, however, Pakhomov discovered an interesting limitation of this example: there is a theory which is definitionally equivalent to ZF and has a computable model ("definitional equivalence" is a strong form of bi-interpretability). One can interpret this result as saying that if we just formulate ZF in a different (but equivalent) language, then it does have a computable model. In light of this, Pakhomov raised the question of whether every computable consistent theory is definitionally equivalent to a theory with a computable model. James Walsh and I have constructed a counterexample to Pakhomov's question---a computable, consistent theory for which no definitionally equivalent theory can have a computable model. The proof uses a mix of computability theory and tame model theory, in the guise of Laskowski's theory of mutual algebraicity. I will discuss the background of our result and some of the ingredients of the proof, focusing on the role played by model theory.

Zoom ID：717 463 6082