Finite extension of decidable theory is decidable

177 Views Asked by At

Exactly what it says on the tin. I'm trying to prove that if T2 is a finite extension of decidable theory T1, then T2 is decidable.

1

There are 1 best solutions below

2
On

We may assume that $T_2$ is $T_1$ together with a single additional axiom $\alpha$. For any sentence $\varphi$, we have that $\varphi$ is a theorem of $T_2$ if and only if $\alpha\to\varphi$ is a theorem of $T_1$.

By assumption, there is an algorithm that will, on input $\psi$, decide whether or not $\psi$ is a theorem of $T_1$. To determine whether or not $\varphi$ is a theorem of $T_2$, apply that algorithm to $\alpha\to\varphi$.