The historical origins of provability semantics are illustrated by so far unexplored manuscript passages of Gentzen and Gödel. Next the determination of elimination rules in natural deduction through a generalized inversion principle is treated, proposed earlier by the authors as a pedagogical device. The notion of validity in intuitionistic logic is related to the notion of formal provability through a direct translation. Finally, it is shown how the correspondence between rules and meaning can be used for setting up complete labelled sequent calculi, first for intuitionistic logic with the remarkable property of invertibility of all the logical rules, and then for modal and related logics.
Meaning in Use
Negri S.;
2015-01-01
Abstract
The historical origins of provability semantics are illustrated by so far unexplored manuscript passages of Gentzen and Gödel. Next the determination of elimination rules in natural deduction through a generalized inversion principle is treated, proposed earlier by the authors as a pedagogical device. The notion of validity in intuitionistic logic is related to the notion of formal provability through a direct translation. Finally, it is shown how the correspondence between rules and meaning can be used for setting up complete labelled sequent calculi, first for intuitionistic logic with the remarkable property of invertibility of all the logical rules, and then for modal and related logics.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
