Name
Abstract | ||
|---|---|---|
In this note we show that Friedman's syntactic translation for intuitionistic logical systems can be carried over to Martin-Lat's type theory, inlcuding universes provided some restrictions are made. Using this translation we show that the theory is closed under a higher type version of Markov's rule. |
Year | DOI | Venue |
|---|---|---|
1995 | 10.1002/malq.19950410304 | MATHEMATICAL LOGIC QUARTERLY |
Keywords | Field | DocType |
FRIEDMAN-TRANSLATION, MARTIN-LOFS TYPE THEORY, PROOF THEORY, TYPE THEORY, INTUITIONISM, MARKOVS RULE | Discrete mathematics,Algebra,Pure mathematics,Type theory,Proof theory,Intuitionism,Syntax,Mathematics | Journal |
Volume | Issue | ISSN |
41 | 3 | 0942-5616 |
Citations | PageRank | References |
1 | 0.41 | 4 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Erik Palmgren | 1 | 233 | 43.17 |