Provability logic is a modal logic, in which the box (or "necessity") operator is interpreted as 'it is provable that'. The point is to capture the notion of a proof predicate of a reasonably rich formal theory, such as Peano arithmetic. There are a number of provability logics, some of which are covered in the literature mentioned in the References section. The basic system is generally referred to as GL or L or K4W.

PropertyValue
dbpprop:abstract
  • Provability logic is a modal logic, in which the box (or "necessity") operator is interpreted as 'it is provable that'. The point is to capture the notion of a proof predicate of a reasonably rich formal theory, such as Peano arithmetic. There are a number of provability logics, some of which are covered in the literature mentioned in the References section. The basic system is generally referred to as GL or L or K4W. It can be obtained by adding the modal version of Löb's theorem to the logic K (or K4). It was pioneered by Robert M. Solovay in 1976. Since then until his passing in 1996 the prime inspirer of the field was George Boolos. Significant contributions to the field have been made by Sergei Artemov, Lev Beklemishev, Giorgi Japaridze, Dick de Jongh, Franco Montagna, Vladimir Shavrukov, Albert Visser and others. Interpretability logics present natural extensions of provability logic.
  • La lógica demostrativa es una lógica modal, en la que el operador caja (o "necesidad") es interpretado significando 'debe ser demostrado que'. El aspecto que se desea capturar es la noción de un predicado de demostración de una teoría formal razonablemente rica, tal como la aritmética de Peano. Existen varias lógicas demostrativas, algunas de las cuales están tratadas en la literatura en la sección de referencias. El sistema básico es generalmente llamado GL o L o K4W. El mismo se puede obtener agregando la versión modal del teorema de Löb a la logica K (o K4). El tema fue desarrollado por Robert M. Solovay en 1976. Desde entonces el principal investigador del tema ha sido George Boolos. Los siguientes especialistas han realizado contribuciones significativas al tema: Sergei Artemov, Lev Beklemishev, Giorgi Japaridze, Dick de Jongh, Franco Montagna, Vladimir Shavrukov, Albert Visser entre otros. Las lógicas de interpretabilidad constituyen extensiones naturales de la lógica demostrativa.
dbpprop:hasPhotoCollection
dbpprop:reference
rdfs:comment
  • Provability logic is a modal logic, in which the box (or "necessity") operator is interpreted as 'it is provable that'. The point is to capture the notion of a proof predicate of a reasonably rich formal theory, such as Peano arithmetic. There are a number of provability logics, some of which are covered in the literature mentioned in the References section. The basic system is generally referred to as GL or L or K4W.
  • La lógica demostrativa es una lógica modal, en la que el operador caja (o "necesidad") es interpretado significando 'debe ser demostrado que'. El aspecto que se desea capturar es la noción de un predicado de demostración de una teoría formal razonablemente rica, tal como la aritmética de Peano. Existen varias lógicas demostrativas, algunas de las cuales están tratadas en la literatura en la sección de referencias. El sistema básico es generalmente llamado GL o L o K4W.
rdfs:label
  • Provability logic
  • Lógica demostrativa
owl:sameAs
skos:subject
foaf:page