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...
Modified Bottle Cap for Improving Children’s Arithmetic Ability
Modified Bottle Cap for Improving Children’s Arithmetic Ability
The preliminary study showed that the main problem, however, faced by kindergarten students are lack of mathematics skill, such arithmetic ability in kindergarten Galis. Therefore,...
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...
Predicate calculus
Predicate calculus
The predicate calculus is the dominant system of modern logic, having displaced the traditional Aristotelian syllogistic logic that had been the previous paradigm. Like Aristotle’s...
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...

