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

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)