| Autor(es) | Arthur N. Prior (1914–1969) |
| Fecha / periodo | 1955–1967 · Siglo XX · Nueva Zelanda y Reino Unido |
| Tipo | Formal |
| Deriva de | Lógica megárica y escuela dialéctica · Terminismo y teoría de la suposición (n.º 32) · Lógica modal · Lógicas polivalentes |
| Derivan de ella | Lógicas temporales computacionales |
| Tres leyes | Identidad: ✓ (clásica) · No contradicción: ✓ (clásica, y en cada instante) · Tercio excluso: ✓ en los sistemas bivalentes de Prior, pero en el tiempo ramificado «peirceano» falla \(FA \lor F\neg A\) |
La lógica temporal de Prior trata los tiempos verbales como operadores sobre proposiciones: «ha sido el caso que \(A\)», «será el caso que \(A\)». La lógica heredada de Frege y Russell trataba las proposiciones como intemporales, y el tiempo, si aparecía, como una variable más sobre instantes. Prior sostuvo que las proposiciones con tiempo verbal («está lloviendo») cambian de valor de verdad y que esa variación es lógicamente significativa. Su gesto distintivo es aplicar a los tiempos el aparato de la lógica modal: el pasado y el futuro son modalidades, y las propiedades del tiempo (lineal, ramificado, denso, sin fin) corresponden a axiomas.
Operadores.
Lógica temporal mínima \(K_t\) (Lemmon, en la línea de Prior):
Reglas: modus ponens, y de \(\vdash A\) inferir \(\vdash GA\) y \(\vdash HA\).
Semántica. Un marco es un conjunto de instantes \(T\) con una relación de precedencia \(<\). \(FA\) es verdadera en \(t\) si \(A\) es verdadera en algún \(t'\) con \(t < t'\); \(PA\), si lo es en algún \(t'\) con \(t' < t\). \(K_t\) es correcta y completa respecto de todos los marcos. Los dos últimos axiomas expresan que pasado y futuro usan la misma relación, en sentidos opuestos.
Correspondencias entre axiomas y propiedades del tiempo.
Modalidades diodoreas (Prior, «Diodoran Modalities», 1955). Diodoro definía lo posible como lo que es o será verdadero. Prior formaliza: \(\Diamond A := A \lor FA\) y \(\Box A := A \land GA\). Qué lógica modal resulta depende de la estructura del tiempo: Dummett y Lemmon (1959) mostraron que sobre el tiempo lineal da al menos S4.3, y Bull (1965) probó que la lógica del tiempo de los números reales es exactamente S4.3; sobre los enteros resulta una extensión más fuerte.
Argumento dominador. Según Epicteto (Disertaciones II 19), Diodoro sostenía que son incompatibles: (1) todo lo verdadero pasado es necesario; (2) de lo posible no se sigue lo imposible; (3) algo es posible que ni es ni será verdadero. Diodoro rechazaba (3). Prior reconstruyó el argumento con premisas temporales adicionales, mostrando qué supuestos implícitos hacían falta.
Tiempo ramificado (Past, Present and Future, 1967). El futuro se representa como un árbol de historias posibles que comparten el pasado. Prior distingue dos lecturas de \(F\):
La distinción la sugirió Kripke en una carta a Prior de 1958.
Futuros contingentes y trivalencia. Prior exploró también la solución trivalente de Łukasiewicz para los enunciados sobre el futuro, y la comparó con las opciones bivalentes.
Extensiones. Kamp (1968) introdujo los operadores binarios «desde» y «hasta», y probó que bastan para expresar todo lo expresable en primer orden sobre órdenes lineales completos. Pnueli (1977) aplicó la lógica temporal lineal a la verificación de programas.
Ejemplo. «Sócrates ha sido joven y será un anciano», dicho en el 430 a. C., se formaliza \(PA \land FB\). La misma oración, dicha en el 390 a. C., cambia de valor; la fórmula es la misma.
Prior partió de la lógica antigua y medieval. Su reconstrucción de las modalidades de Diodoro, en diálogo con el argumento dominador, fue el primer paso, y la reinterpretación de Ockham sobre los futuros contingentes le dio el sistema «ockhamista» del tiempo ramificado. Tomó de la lógica modal el aparato formal: los tiempos son operadores modales normales, y la semántica relacional, que Kripke le comunicó, los adaptó a instantes ordenados. Declaró su deuda con Łukasiewicz, cuya lógica trivalente nació del problema de los futuros contingentes. La sugerencia inicial de Findlay (1941), sobre un cálculo de tiempos verbales, le dio la idea del proyecto.
La descendencia principal es computacional. Pnueli adaptó un sistema de la tradición de Prior, a través del manual de Rescher y Urquhart (1971), y de ahí salieron LTL, CTL y la verificación de modelos. La afinidad con la lógica aviceniana es una lectura: Rescher (1967) estudió sus modalidades temporales, y Hodges y Johnston (2017) proponen un modelo que reduce sus modalidades aléticas a temporales.
Prior trabajó en Christchurch (Nueva Zelanda) y después en Manchester y Oxford, fuera de las corrientes dominantes de la filosofía del lenguaje. Su lógica fue a la vez un programa filosófico: defendía una metafísica del tiempo en la que el presente es privilegiado y el pasado y el futuro no existen del mismo modo. Para la pregunta «¿una lógica o muchas?», la lógica temporal muestra que la estructura del tiempo que se supone (lineal o ramificada, discreta o densa) produce lógicas distintas, y que la elección entre ellas depende de tesis metafísicas o de las necesidades de una aplicación. La propia disputa entre peirceanos y ockhamistas muestra que el tercio excluso sobre el futuro es una decisión filosófica, no un dato.