Javascript must be enabled to continue!
PROVABILITY LOGIC IN THE GENTZEN FORMULATION OF ARITHMETIC
View through CrossRef
AbstractIn 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 PIPRA(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.
Title: PROVABILITY LOGIC IN THE GENTZEN FORMULATION OF ARITHMETIC
Description:
AbstractIn 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 PIPRA(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.
Related Results
Provability logic
Provability logic
Central to Gödel’s second incompleteness theorem is his discovery that, in a sense, a formal system can talk about itself. Provability logic is a branch of modal logic specifically...
ASP Formulation Development Journey, Optimisation and Validation for Mangala Field
ASP Formulation Development Journey, Optimisation and Validation for Mangala Field
Abstract
Mangala is a large low salinity, high quality fluvial oil field reservoir in India with STOIIP of over one billion barrels of waxy and moderately viscous cr...
Rationality and Logic
Rationality and Logic
An argument that logic is intrinsically psychological and human psychology is intrinsically logical, and that the connection between human rationality and logic is both constitutiv...
Greek and Roman Logic
Greek and Roman Logic
In ancient philosophy, there is no discipline called “logic” in the contemporary sense of “the study of formally valid arguments.” Rather, once a subfield of philosophy comes to be...
Arithmetical Vocabulary : A Factor In Verbal Problem Solving In Sixth Grade Arithmetic
Arithmetical Vocabulary : A Factor In Verbal Problem Solving In Sixth Grade Arithmetic
During the writer's experience of teaching in elementary and junior high schools in Kansas he had excellent opportunity through supervision and classroom teaching to note a more-th...
Arithmetic Word-Problem Solving as Cognitive Marker of Progression in Pre-Manifest and Manifest Huntington’s Disease
Arithmetic Word-Problem Solving as Cognitive Marker of Progression in Pre-Manifest and Manifest Huntington’s Disease
Background: Arithmetic word-problem solving depends on the interaction of several cognitive processes that may be affected early in the disease in gene-mutation carriers for Huntin...
The Julius Caesar Objection
The Julius Caesar Objection
Abstract
Recent research has revealed three important points about Frege’s philosophy of arithmetic. First, his attempt to derive axioms for arithmetic from principl...
A logic of defeasible argumentation: Constructing arguments in justification logic
A logic of defeasible argumentation: Constructing arguments in justification logic
In the 1980s, Pollock’s work on default reasons started the quest in the AI community for a formal system of defeasible argumentation. The main goal of this paper is to provide a l...

