Japaridze's polymodal logic (GLP) is a system of
provability logic 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.
Examples
...
with infinitely many provability
modalities. This system has played an important role
in some applications of provability algebras in
proof theory
Proof theory is a major branchAccording to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. Barwise (1978) consists of four corresponding part ...
, and has been extensively studied since the late 1980s. It is named after
Giorgi Japaridze Giorgi Japaridze (also spelled Giorgie Dzhaparidze) is a Georgian-American researcher in logic and theoretical computer science. He currently holds the title of Full Professor at the Computing Sciences Department of Villanova University. Japaridze i ...
.
Language and axiomatization
The language of GLP extends that of the language of classical
propositional logic
Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations b ...
by including the infinite series of necessity operators. Their dual possibility operators are defined by .
The axioms of GLP are all classical tautologies and all formulas of one of the following forms:
*
*
*
*
And the rules of inference are:
* From and conclude
* From conclude
Provability semantics
Consider a sufficiently strong
first-order theory
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quan ...
such as
Peano Arithmetic
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearl ...
.
Define the series of theories as follows:
* is
* is the extension of through the additional axioms for each formula such that proves all of the formulas
For each , let be a natural arithmetization of the predicate
is the
Gödel number of a sentence provable in .
A ''realization'' is a function that sends each nonlogical atom of
the language of GLP to a sentence of the language of . It extends to all formulas
of the language of GLP by stipulating that commutes with the Boolean connectives, and
that is , where
stands for (the numeral for) the Gödel number of .
An arithmetical completeness theorem
[G. Japaridze]
"The polymodal logic of provability"
''Intensional Logics and Logical Structure of Theories''. Metsniereba, Tbilisi, 1988, pp. 16–48 (Russian). for GLP states that a formula is provable in GLP if and only if, for every interpretation , the sentence is provable in .
The above understanding of the series of theories is not the only natural understanding yielding the soundness and completeness of GLP. For instance, each theory can be understood as augmented with all true sentences as additional axioms.
George Boolos
George Stephen Boolos (; 4 September 1940 – 27 May 1996) was an American philosopher and a mathematical logician who taught at the Massachusetts Institute of Technology.
Life
Boolos is of Greek- Jewish descent. He graduated with an A.B. ...
showed that GLP remains sound and complete with analysis (
second-order arithmetic
In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics.
A precur ...
) in the role of the base theory .
Other semantics
GLP has been shown
to be incomplete with respect to any class of
Kripke frames.
A natural topological semantics of GLP interprets modalities as derivative operators of a
polytopological space In general topology, a polytopological space consists of a set X together with a family \_ of topologies on X that is linearly ordered by the inclusion relation (I is an arbitrary index set). It is usually assumed that the topologies are in non-d ...
. Such spaces are called
GLP-spaces whenever they satisfy all the axioms of GLP. GLP is complete with respect to the class of all GLP-spaces.
[L. Beklemishev and D. Gabelaia]
"Topological completeness of provability logic GLP"
''Annals of Pure and Applied Logic'' 164 (2013), pp. 1201–1223.
Computational complexity
The problem of being a theorem of GLP is
PSPACE-complete In computational complexity theory, a decision problem is PSPACE-complete if it can be solved using an amount of memory that is polynomial in the input length (polynomial space) and if every other problem that can be solved in polynomial space can b ...
. So is the same problem restricted to only variable-free formulas of GLP.
[F. Pakhomov]
"On the complexity of the closed fragment of Japaridze's provability logic"
''Archive for Mathematical Logic'' 53 (2014), pp. 949–967.
History
GLP, under the name GP, was introduced by
Giorgi Japaridze Giorgi Japaridze (also spelled Giorgie Dzhaparidze) is a Georgian-American researcher in logic and theoretical computer science. He currently holds the title of Full Professor at the Computing Sciences Department of Villanova University. Japaridze i ...
in his PhD thesis "Modal Logical Means of Investigating Provability" (
Moscow State University
M. V. Lomonosov Moscow State University (MSU; russian: Московский государственный университет имени М. В. Ломоносова) is a public research university in Moscow, Russia and the most prestigious ...
, 1986) and published two years later
along with (a) the completeness theorem for GLP with respect to its provability interpretation (Beklemishev subsequently came up with a simpler proof of the same theorem) and (b) a proof that Kripke frames for GLP do not exist. Beklemishev also conducted a more extensive study of Kripke models for GLP.
Topological models for GLP were studied by Beklemishev, Bezhanishvili, Icard and Gabelaia.
The decidability of GLP in polynomial space was proven by I. Shapirovsky, and the PSPACE-hardness of its variable-free fragment was proven by F. Pakhomov.
Among the most notable applications of GLP has been its use in proof-theoretically analyzing
Peano arithmetic
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearl ...
, elaborating a canonical way for recovering
ordinal notation
In mathematical logic and set theory, an ordinal notation is a partial function mapping the set of all finite sequences of symbols, themselves members of a finite alphabet, to a countable set of ordinals. A Gödel numbering is a function mappin ...
up to from the corresponding algebra, and constructing simple combinatorial independent statements (Beklemishev ).
An extensive survey of GLP in the context of provability logics in general was given by
George Boolos
George Stephen Boolos (; 4 September 1940 – 27 May 1996) was an American philosopher and a mathematical logician who taught at the Massachusetts Institute of Technology.
Life
Boolos is of Greek- Jewish descent. He graduated with an A.B. ...
in his book ''The Logic of Provability''.
[G. Boolos, ]
The Logic of Provability
'. Cambridge University Press, 1993.
Literature
*L. Beklemishev
"Provability algebras and proof-theoretic ordinals, I" ''Annals of Pure and Applied Logic'' 128 (2004), pp. 103–123.
*L. Beklemishev, J. Joosten and M. Vervoort
"A finitary treatment of the closed fragment of Japaridze's provability logic" ''Journal of Logic and Computation'' 15 (2005), No 4, pp. 447–463.
*L. Beklemishev
"Kripke semantics for provability logic GLP" ''Annals of Pure and Applied Logic'' 161, 756–774 (2010).
*L. Beklemishev, G. Bezhanishvili and T. Icar, "On topological models of GLP". ''Ways of proof theory, Ontos Mathematical Logic'', 2, eds. R. Schindler, Ontos Verlag, Frankfurt, 2010, pp. 133–153.
*L. Beklemishev, "On the Craig interpolation and the fixed point properties of GLP". ''Proofs, Categories and Computations''. S. Feferman et al., eds., College Publications 2010. pp. 49–60.
*L. Beklemishev
"Ordinal completeness of bimodal provability logic GLB" ''Lecture Notes in Computer Science'' 6618 (2011), pp. 1–15.
*L. Beklemishev
"A simplified proof of arithmetical completeness theorem for provability logic GLP" ''Proceedings of the Steklov Institute of Mathematics'' 274 (2011), pp. 25–33.
*L. Beklemishev and D. Gabelaia
"Topological completeness of provability logic GLP" ''Annals of Pure and Applied Logic'' 164 (2013), pp. 1201–1223.
*G. Boolos
"The analytical completeness of Japaridze's polymodal logics" ''Annals of Pure and Applied Logic'' 61 (1993), pp. 95–111.
*G. Boolos,
The Logic of Provability' Cambridge University Press, 1993.
*E.V. Dashkov, "On the positive fragment of the polymodal provability logic GLP". ''Mathematical Notes'' 2012; 91:318–333.
*D. Fernandez-Duque and J.Joosten
"Well-orders in the transfinite Japaridze algebra" ''Logic Journal of the IGPL'' 22 (2014), pp. 933–963.
*G. Japaridze
"The polymodal logic of provability" ''Intensional Logics and Logical Structure of Theories''. Metsniereba, Tbilisi, 1988, pp. 16–48 (Russian).
*F. Pakhomov
"On the complexity of the closed fragment of Japaridze's provability logic" ''Archive for Mathematical Logic'' 53 (2014), pp. 949–967.
*D.S. Shamkanov
"Interpolation properties for provability logics GL and GLP" ''Proceedings of the Steklov Institute of Mathematics'' 274 (2011), pp. 303–316.
*I. Shapirovsky
"PSPACE-decidability of Japaridze's polymodal logic" ''Advances in Modal Logic'' 7 (2008), pp. 289–304.
References
{{reflist
Modal logic
Proof theory
Provability logic