La aritmética de Presberger se utiliza en la práctica para la verificación de software, por ejemplo, para demostrar que un fragmento de programa está libre de desbordamientos de subíndices de matrices. Básicamente, el programa tiene expresiones como a[3*i+k] y se quiere demostrar que el subíndice nunca es mayor que el tamaño de la matriz. Si tienes algo como a[m*n+k] la multiplicación de dos variables m y n sólo puede expresarse en aritmética Peano, lo cual es indecidible, pero a menudo es posible escribir programas sin tales multiplicaciones de variables en subíndices. (La multiplicación por constantes puede expresarse mediante sumas repetidas, por supuesto). El artículo de Wikipedia sobre aritmética de Presburger tiene algo de información al respecto.
Además, los compiladores de lenguajes de programación sofisticados se basan en la decidibilidad de teorías aún más débiles para manejar la inferencia de tipos y la igualdad de tipos. Lo mismo ocurre con la comprobación de modelos en el diseño de hardware, etc. Estas cosas son cada vez más importantes en el mundo real, y no muchos programadores e ingenieros saben mucho sobre ellas. Creo que es un buen momento para ser un lógico, incluso si no puedes conseguir un trabajo en el mundo académico.