Banner Portal
The rules-as types interpretations of Schröder-Heister's extension of natural deduction


Dedução natural

Como Citar

HAEUSLER , E. H.; PEREIRA , L. C. P. D. . The rules-as types interpretations of Schröder-Heister’s extension of natural deduction. Manuscrito: Revista Internacional de Filosofia, Campinas, SP, v. 22, n. 2, p. 149–163, 1999. Disponível em: Acesso em: 22 mar. 2023.


From this theorem we can conclude that any Cartesian Closed Category with finite co-products is a model λR. The addition of types of arbitrary levels does not interfere with the basic semantical intuitions. The enlarged expressive power of λR relies, for exemple, on the possibility of considering certain assumption formation processes as the specification of programming modules (as in MODULA- II (Wirth (1985))): the modules hide their implementations, but specify the interface (types of the premises, of the discharged hypothesis ando f the conclusion) that they ought to have with the world.



Chi, W.H. (1991). Esquemas Abstratos para Dedução Natural Cálculo de Sequentes e λ-Calculus Tipado. Dissertação de Mestrado, Departamento de Informática, PUC-Rio.

Haeusler, E.H. & Pereira, L.C.P.D. (1992). A Denotational Semantics for Arbitrary Level Typed λ-Calculus, Monografias em Ciência da Computação (Departamento de Informática, PUC-RIO).

Poubel, H.W. & Pereira, L.C.P.D. (1993). A Categorical Approach to HIgher-Level Introduction and Elimination Rules, Reports in Mathematical Logic 27, pp. 3-19.

PRAWITZ, D. (1965). Natural Deduction. A Proof Theorical Study (Stockholm, Almqvist-Wiksell).

Schröder-Heister, P. (1984). A Natural Extension of Natural Deduction, Journal of Symbolic Logic, vol.49.

Wirth, N. (1985). Programming in Modula-2 (Berlin, Springer-Verlag).

Creative Commons License
Este trabalho está licenciado sob uma licença Creative Commons Attribution 4.0 International License.

Copyright (c) 1999


Não há dados estatísticos.