El cálculo circular es un cálculo de prueba que manipula construcciones de estilo gráfico denominadas circunstancias , a diferencia de los objetos tradicionales de estilo árbol, como fórmulas o secuencias . Las circunstancias vienen en una variedad de formas, pero todas comparten una característica principal, que las hace diferentes de los objetos más tradicionales de manipulación sintáctica. Esta característica es la capacidad de dar cuenta explícitamente de la posible compartición de subcomponentes entre diferentes componentes. Por ejemplo, es posible escribir una expresión donde dos subexpresiones F y E , aunque ninguna sea una subexpresión de la otra, aún tengan una ocurrencia común de una subexpresión G (a diferencia de tener dos ocurrencias diferentes de G , una en F y otra en E ).
El enfoque fue introducido por G. Japaridze [1] como una teoría de prueba alternativa capaz de "domesticar" varios fragmentos no triviales de su lógica de computabilidad , que de otro modo habían resistido todos los intentos de axiomatización dentro de los marcos tradicionales de teoría de prueba. [2] [3] El origen del término "circuente" es CIRcuit+seQUENT, ya que la forma más simple de los circuentes, si bien se asemejan a circuitos en lugar de fórmulas, pueden considerarse como colecciones de secuentes unilaterales (por ejemplo, secuentes de un nivel dado de un árbol de prueba de estilo Gentzen) donde algunos secuentes pueden tener elementos compartidos.
La versión básica del cálculo circular [1] fue acompañada de una " semántica abstracta de recursos " y de la afirmación de que esta última era una formalización adecuada de la filosofía de los recursos tradicionalmente asociada a la lógica lineal . Basándose en esa afirmación y en el hecho de que la semántica inducía una lógica propiamente más fuerte que la lógica lineal (afín), Japaridze argumentó que la lógica lineal era incompleta como lógica de recursos. Además, argumentó que no sólo el poder deductivo sino también el poder expresivo de la lógica lineal eran débiles, ya que ésta, a diferencia del cálculo circular, no lograba captar el fenómeno omnipresente de compartir recursos. [4]
La filosofía de recursos del cálculo circular considera los enfoques de la lógica lineal y la lógica clásica como dos extremos: el primero no permite compartir nada, mientras que en el segundo “se comparte todo lo que se puede compartir”. A diferencia del cálculo circular, ninguno de los dos enfoques permite casos mixtos en los que se comparten algunas subfórmulas idénticas y otras no.
Entre las aplicaciones posteriores del cálculo circunspecto se encuentra su uso para definir una semántica para una lógica puramente proposicionalmente favorable a la independencia . [5] La lógica correspondiente fue axiomatizada por W. Xu. [6]
Desde el punto de vista sintáctico, los cálculos circulares son sistemas de inferencia profunda con la característica única de compartir subfórmulas. Se ha demostrado que esta característica acelera ciertas demostraciones. Por ejemplo, se han construido demostraciones analíticas de tamaño polinomial para el principio de pigeonhole proposicional. [4] Solo se han encontrado demostraciones analíticas cuasipolinomiales para este principio en otros sistemas de inferencia profunda. [7] En sistemas de resolución o analíticos de estilo Gentzen, se sabe que el principio de pigeonhole solo tiene demostraciones de tamaño exponencial . [8]
Medios relacionados con el cálculo de Cirquent en Wikimedia Commons