Нашли опечатку? Выделите ее мышкой и нажмите Ctrl+Enter
Название: Intuitionistic type theory
Автор: Per M.-L.
Аннотация:
Mathematical logic and the relation between logic and mathematics have been interpreted in at least three different ways:
(1) mathematical logic as symbolic logic, or logic using mathematical symbolism;
(2) mathematical logic as foundations {or philosophy) of mathematics ;
(3) mathematical logic as logic studied by mathematical methods, as a branch of mathematics.
We shall here mainly be interested in mathematical logic in the second sense. What we shall do is also mathematical logic in the first sense, but certainly not in the third.
The principal problem that remained after Principia Mathematica was completed was, according to its authors, that of justifying the axiom of reducibility (or, as we would now say, the impredicative comprehension axiom). The ramified theory of types was predicative, but it was not sufficient for deriving even elementary parts of analysis. So the axiom of reducibility was added on the pragmatic ground that it was needed, although no satisfactory justification (explanation) of it could be provided. The whole point of the ramification was then lost, so that it might just as well be abolished...