A. Avron: Transitive Closure and Inductive Reasoning

From: Helmut Veith (kgs-owner@dbai.tuwien.ac.at)
Date: Fri May 31 2002 - 20:18:39 MEST

  • Next message: ivc.zuef@univie.ac.at: "Activities of the Institut Wiener Kreis / Vienna Circle Institute"

    Collegium Logicum

    Lecture Announcement

    A. Avron, Tel Aviv University
    Thursday, June 6, 5 pm


    We argue that the concept of transitive closure is the key for
    understanding finitary inductive definitions and inductive reasoning.
    Hence the ability to define the transitive closure of any given relation
    and make appropriate inferences concerning it (including Gentzen-style
    formulations of induction principles) should be one of the most important
    features of every computerized system for doing Mathematics and every
    logical framework. We investigate languages with transitive closure
    operations and their expressive power. In particular, we show that with
    the simplest transitive closure operation one can define all recursive
    predicates and functions from 0, the successor function and addition, but
    addition is not definable from 0 and the successor function. We then show
    that in the presence of a pairing operation, the availability of the
    simplest transitive closure operation suffices for having all types of
    finitary inductive definitions (and corresponding inductive principles).
    Finally we show that in a language with a tansitive closure operation it
    is possible to give a new, concise presentation (and to our opinion, a new
    understanding) of the various comprehension axioms of ZF, which is based
    on purely syntactic considerations.

    Place: TU Vienna, Favoritenstrasse 9-11
    Institut f. Computersprachen, 3rd Floor
    Seminar room 185/2 (HA 03 08)

    This archive was generated by hypermail 2b30 : Fri May 31 2002 - 20:20:23 MEST