|
|
Centre for Logic, Epistemology and the History of Science (CLE) |
|
|
|
|
Rules and Instructions | Sites Pointing to CLE e-Prints |
|
ISSN 1519-9681 |
|
ISSN 1519-9614 |
|
|
||
| . | ||
|
Higher-Order Intuitionistic Logic |
||
|
||
.
|
|
Publication Information |
| The final version of
this paper is published as: Marcelo E. Coniglio; Cristina Sernadas, "A Hilbert-style axiomatization of higher-order intuitionistic logic". In H.A. Feitosa, F.T. Sautter (Eds.), "Lógica: teoria, aplicações e reflexões", pp. 25-58, Coleção CLE, Campinas, 2004. |
|
|
|
|
|
Two Hilbert calculi for higher-order
logic (or theory of types) are introduced. The first is defined in a language
that uses just exponential types of power type, and it is obtained by adapting
the sequent calculus for local set theory introduced by Bell in [3]. The
second one, originally introduced in [5], is defined in a language with arbitrary
functional types. Using usual topos semantics we show that both systems are
sound and complete.
|
|
|
|
|