| Autor(es) | David Nelson (1918–2003); A. A. Márkov (1903–1979); N. N. Vorobiov |
| Fecha / periodo | 1949–1984 · Siglo XX · Estados Unidos y URSS |
| Tipo | Formal |
| Deriva de | Lógica intuicionista |
| Derivan de ella | — |
| Tres leyes | Identidad: ✓ (\(A \to A\)) · No contradicción: matizado (\(\sim(A \land \sim A)\) no es teorema; N3 conserva la explosión, N4 no) · Tercio excluso: ✗ (\(A \lor \sim A\) no es teorema) |
En la lógica intuicionista, negar \(A\) es mostrar que \(A\) lleva a lo absurdo: \(\neg A\) equivale a \(A \to \bot\). La falsedad es derivada, parasitaria de la verdad. Nelson propone que la falsedad tenga una construcción propia. Refutar «todos los números tienen la propiedad \(P\)» debería consistir en exhibir un contraejemplo, no solo en mostrar que la suposición contraria es absurda. Para ello introduce una negación fuerte, \(\sim\), junto a la intuicionista, con condiciones de refutación directas para cada conectiva. El gesto distintivo es la simetría entre verificación y falsación: cada fórmula tiene condiciones de prueba y condiciones de refutación, ninguna reducible a la otra.
Sistema N3 (Nelson, «Constructible Falsity», 1949; formulación axiomática de Vorobiov, 1952). Axiomas:
Reglas: modus ponens y las reglas de cuantificadores intuicionistas.
La negación intuicionista es definible: \(\neg A := A \to \sim A\). Los axiomas de \(\sim\) son reglas de reducción: empujan la negación fuerte hasta los átomos. Por eso toda fórmula equivale a una en la que \(\sim\) solo afecta a átomos.
Sistema N4 (Almukdad y Nelson, «Constructible Falsity and Inexact Predicates», 1984). Es N3 sin el axioma \(\sim A \to (A \to B)\). Es paraconsistente: \(A, \sim A \not\vdash B\). Un átomo puede estar a la vez verificado y refutado sin que el sistema se trivialice. Nelson y Almukdad lo motivan con predicados inexactos, para los que las condiciones de aplicación y de no aplicación pueden solaparse.
Propiedades.
Semántica. Nelson la derivó de la realizabilidad de Kleene: define a la vez «\(e\) realiza \(A\)» y «\(e\) realiza la falsedad de \(A\)». En semántica de Kripke, sobre un orden parcial de estados de información se definen dos relaciones persistentes, verificación \(\models^+\) y refutación \(\models^-\). Para los átomos se asignan por separado. En N3 se exige que ningún estado verifique y refute el mismo átomo; en N4 no. Algebraicamente, Rasiowa estudió los N-reticulados (reticulados de Nelson), para N3.
Ejemplo. Sea \(A(x)\): «\(x\) es primo». La fórmula \(\sim\forall x A(x)\) se prueba exhibiendo \(4\) y una prueba de \(\sim A(4)\), es decir, una factorización. La intuicionista \(\neg\forall x A(x)\) solo exige deducir absurdo de «todos son primos».
N3 toma el cálculo intuicionista positivo tal cual y le añade una negación constructiva de la falsedad; la motivación y la semántica proceden de la realizabilidad de Kleene, de quien Nelson fue el primer doctorando. En la URSS, Márkov (1950) y Vorobiov (1952) la estudiaron dentro del constructivismo soviético; Vorobiov dio la axiomatización estándar. La noción de falsedad construible circuló así por dos escuelas constructivistas casi a la vez.
Sobre N4 se apoyan desarrollos muy posteriores, que el catálogo registra como afinidades y no como descendencia, porque llegan cuando la lógica conexiva y la programación lógica ya existían. Wansing construyó en 2005 su lógica conexiva C sobre N4, cambiando la cláusula de refutación del condicional por \(\sim(A \to B) \leftrightarrow (A \to \sim B)\). En programación lógica, Gelfond y Lifschitz (1991) introdujeron una negación «clásica» en los programas extendidos, y Pearce mostró que se analiza con la negación fuerte de Nelson en su lógica del equilibrio. La afinidad con la paraconsistencia es de resultado, no de origen: N4 es paraconsistente, pero procede de una tradición independiente de Jaśkowski y de da Costa.
La lógica de Nelson fue durante décadas un tema especializado de la escuela constructivista. Su interés creció con la paraconsistencia, con la teoría de la prueba bilateral, que trata la prueba y la refutación como nociones primitivas, y con las aplicaciones a la representación del conocimiento. Para la pregunta «¿una lógica o muchas?», muestra que incluso dentro de una misma familia, la constructiva, hay más de una negación legítima, y que una lógica puede tener dos negaciones a la vez con comportamientos distintos. Lo que llamamos «negación» no es un concepto único que la lógica deba capturar, sino varios.