<!DOCTYPE html>
<html>
<head>
    <title>Set Theory and Analysis</title>
</head>
<body>
    <p>
        Tuesday, 31 March 2026 - 10:00 to 11:30  <br />
        Place: IM, konírna
    </p>
    <p>
        Speaker: Ansten Mørch Klev, Institute of Philosophy of the Czech Academy of Sciences<br />
        Title: Inductively defined domains
    </p>
    <p class="ql-ed">
        Abstract <br />
        <p>An intuitive description of the cumulative hierarchy might run as follows: whenever you have certain sets, ā, you may form the set of them, {ā}. Such a description of how the elements of a domain D are built up from below is called a fundamental inductive definition, and the domain D is called inductively defined. The given description of the cumulative hierarchy is, however, not a rigorous definition, since we have not made precise what it means to "have certain sets, ā". I will present Per Martin-Löf's constructive type theory as a theory of inductively defined domains. The cumulative hierarchy will be seen to be only one of infinitely many examples. Based on Martin-Löf's semantical explanations of his type theory, I will also try to explain how an element of an inductively defined domain may be regarded as a well-founded, in general infinite, labelled tree.</p>
    </p>
    <p>
         For more information see the seminar web page at <br />
         https://www.math.cas.cz/index.php/events/seminar/6
    </p>
    <p>
        Set Theory and Analysis mailing list <br />
        settfa@math.cas.cz <br />
        https://list.math.cas.cz/listinfo/settfa@math.cas.cz
    </p>
</body>
</html>