Judgements of Higher Levels and Standardized Rules for Logical Constants in Martin-Löf's Theory of Logic

DSpace Repository


URI: http://hdl.handle.net/10900/130950
Dokumentart: Aufsatz
Date: 1989
Source: Proceedings of the Workshop on Programming Logic, Båstad, Sweden, 21-26 May 1989. Ed. by Peter Dybjer, Lars Hallnäs, Bengt Nordström, Kent Petersson and Jan M. Smith. Programming Methodology Group, University of Göteborg and Chalmers University of Technology 1989, Report 54, pp. 494-517
Language: English
Faculty: 7 Mathematisch-Naturwissenschaftliche Fakultät
Department: Informatik
DDC Classifikation: 004 - Data processing and computer science
100 - Philosophy
Keywords: Logik , Beweistheorie , Logische Partikel , Per Martin-Löf [Person]
Other Keywords:
Proof Theory
Logical Constants
Per Martin-Löf
License: Publishing license including print on demand
Order a printed copy: Print-on-Demand
Show full item record


The aim of these notes is to carry over some of what I did in my thesis [see P. Schroeder-Heister, A Natural Extension of Natural Deduction, J. Symb. Log. 49 (1984), 1284-1300] to the framework of Martin-Löf's logical theory, in particular the idea of rules of higher levels (which in Martin-Löf's non-formalistic approach will become hypothetical judgements of higher levels) and the general schema for introduction and elimination rules for logical constants (which will have to be extended to a schema containing formation and detraction rules).

This item appears in the following Collection(s)