La informática y el cálculo de las raíces cuadradas

Question

Si uno se para verificar que

$$ \sqrt{2} < 3 $$

sería el subyacente formalización requieren de una lógica más expresivo de primer orden? O, FOL suficiente, dado que los números reales se pueden formalizar en la teoría de conjuntos?

Cómo acerca de la evaluación de los diferenciales, como

$$ \frac{d}{dy} (3x+2) $$

¿cómo expresivo que hace la lógica necesidad de ser?

Gracias

Answer 1

Comparando particular de números algebraicos (localizada lejos de sus Galois conjugados por las desigualdades, tales como el positivo de la raíz de $X^2=2$) se puede hacer en cualquier teoría que soporta cálculo aritmético. Por ejemplo, el primer orden de teoría de campos cerrados es decidable y que incluye decisiones acerca de las declaraciones de la forma $a > b$ la comparación de dos números algebraicos.

Modelo de la teoría de la diferencia (y la diferencia) de los campos y los anillos se lleva a cabo en una lógica de primer orden contexto similar a los campos. Teoremas se demuestran por segundo orden, métodos, pero el objeto de estudio es un primer orden de la teoría.