¿Se puede crear un programa de computadora que determine la validez de un argumento racional de acuerdo con la lógica?

Esto no es estrictamente una respuesta computacional, pero creo que es bastante relevante. El ensayo de 1951 de John Rawls, Esquema de un procedimiento de decisión para la ética [1], se acerca a cómo se podría hacer un programa informático de este tipo. Básicamente, el ensayo habla de cómo puede haber jueces de dilemas morales completamente racionales e imparciales. Está escrito de una manera muy matemática, explicando paso a paso lo que debería ser el caso para mantener que un juez racional tome decisiones objetivas cuando se trata de asuntos éticos.

[1] Página sobre Utexas

Seguro. Es lo que hago para vivir, aunque no soy el primero.

La parte lógica es esencialmente un problema resuelto. La idea de la programación lógica se remonta a computadoras anteriores, y los sistemas de programación lógica son casi tan antiguos como las computadoras. Si puede escribir su argumento en una lógica formal, la computadora puede justificar (o rechazar) la prueba.

No necesariamente puede hacerlo rápidamente: el espacio completo de la lógica de primer orden es una categoría difícil de resolver. En realidad, hay muchos tipos diferentes de lógica, algunos de los cuales son más manejables desde el punto de vista informático, e incluso pueden acercarse a lo que tenía en mente.

La parte “en tu cabeza” es el verdadero problema. La programación lógica es la basura clásica de entrada / salida de basura: si sus suposiciones son incorrectas, sus conclusiones serán incorrectas. La lógica en sí es una pequeña cosa, algo que puedo enseñar de pie sobre un pie. Sin embargo, el mundo es vasto, y su representación de él determina las conclusiones a las que llega.

En realidad, incluso la lógica en sí misma es engañosa: la palabra “no” significa cosas diferentes en contextos diferentes, y ser preciso sobre lo que quiere decir con “no” en cualquier caso es más difícil de lo que parece. Pero ese es un problema de lenguaje, no un problema de lógica o computadora. Usted es quien realmente no sabe a qué se refiere cuando formula el problema. La computadora le dirá lo que significa, lógicamente, pero si la lógica llega a conclusiones absurdas, entonces es culpa de las entradas, no del proceso.

Por lo tanto, tratar de extraer un argumento lógico de un texto escrito es difícil; De hecho, es imposible. La computadora puede adivinar lo que quisiste decir, aunque no particularmente bien. Es mucho más consciente de las ambigüedades que tú.

Creo que Joshua Engel ya ha proporcionado una respuesta muy sólida aquí, pero solo pensé en proporcionar una respuesta sucinta propia, que tiene una perspectiva ligeramente diferente.

Lo que está describiendo casi exactamente es un verificador de pruebas (también llamado verificador de pruebas automatizado ), que es un programa que toma un sistema formal y puede enumerar recursivamente teoremas en el lenguaje del sistema, o de hecho determinar si un teorema dado (y en consecuencia, una línea de razonamiento) es un miembro del lenguaje. Un sistema formal es esencialmente un conjunto de axiomas y un conjunto de reglas gramaticales (inferencia), que determinan declaraciones válidas en el lenguaje o “fórmulas bien formadas”. Ver http://en.wikipedia.org/wiki/Pro … para una breve introducción al tema.

Le ruego que lea sobre verificadores de pruebas automatizados y la teoría de fondo de la lógica matemática (formal), si así lo desea. Con el advenimiento de la informática moderna, los asistentes de prueba automatizados (hay varios decentes de código abierto en estos días que escucho), este campo se ha extendido en su utilidad de una disciplina esotérica de lógicos y matemáticos puros a una utilidad para matemáticos en otros áreas, y de hecho ciencias de la computación teóricas. En particular, el famoso teorema de los cuatro colores en la teoría de grafos se resolvió solo relativamente recientemente con la ayuda de un comprobador de pruebas automatizado ( Coq si la memoria sirve).

Nota al margen incidental: la lógica formal es un campo bastante bien definido en matemáticas, aunque es un área de investigación candente y lo ha sido desde principios del siglo XX (el trabajo de Hilbert, Godel, Russell e incluso Turing es crucial). Todavía hay muchas preguntas matemáticas y filosóficas sin respuesta en el campo.