Premium
PROVABILITY LOGIC IN THE GENTZEN FORMULATION OF ARITHMETIC
Author(s) -
Gentilini Paolo,
Gentilini P.
Publication year - 1992
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.19920380150
Subject(s) - mathematics , arithmetic function , completeness (order theory) , gödel's completeness theorem , discrete mathematics , calculus (dental) , mathematical proof , algebra over a field , arithmetic , pure mathematics , mathematical analysis , medicine , geometry , dentistry
In this paper are studied the properties of the proofs in PRA of provability logic sentences, i.e. of formulas which are Boolean combinations of formulas of the form P IPRA ( h ), where h is the Gödel‐number of a sentence in PRA. The main result is a Normal Form Theorem on the proof‐trees of provability logic sequents, which states that it is possible to split the proof into an arithmetical part, which contains only atomic formulas and has an essentially intuitionistic character, and into a logical part, which is merely instrumental. Moreover, the induction rules which occur in the arithmetical part are implicit. Some applications of the Normal Form Theorem are shown in order to obtain some syntactical results on the PRA ‐completeness of modal logic. In particular a completeness theorem for Boolean combinations of modalities is given.