﻿ MISANU
ὅδε οἶκος, ὦ ἑταῖρε, μνημεῖον ἐστιν ζῴων τῶν σοφῶν ἀνδρῶν, καὶ τῶν ἔργων αὐτῶν

Seminar for GENERAL PROOF THEORY

PROGRAM

Plan rada Seminara za opstu teoriju dokaza za april 2016.

Predavanje treba da se odrzi u sali 301f Matematickog instituta (Knez Mihailova 36, III sprat). Obratite, molim Vas, paznju na vreme odrzavanja predavanja. Na Seminaru za opstu teoriju dokaza predavanja nece biti svake nedelje, nego samo s vremena na vreme.

Ponedeljak, 25. april, u 18:00
Peter Schroeder-Heister, Eberhard Karls Universität Tübingen
BEYOND LOGIC: DEFINITIONAL REFLECTION AND NEGATION IN RULE-BASED REASONING

Abstract: In traditional (philosophical and mathematical) logic we find what I have called the dogma of the primacy of the categorical over the hypothetical. It means that categorical proof or truth comes first, and hypothetical proof or consequence is defined in terms of the categorical concept, for example as the ``transmission'' of truth or provability from the assumptions to the assertion. This has found its philosophical elaboration, for example, in the proof-theoretic semantics of Dummett and Prawitz, where assumptions are essentially place-holders for assertive proofs. Its technical counterpart is the Curry-Howard correspondence, according to which only variables can occur as terms in assumption position. A view which takes hypothetical judgements and therefore assumptions more seriously, could start from the model of Gentzen's sequent calculus, which for the first time in logic incorporated the idea that assumptions can be altered (rather than only ``discharged'') in the course of a derivation, by means of so-called ``left'' introduction rules.

In my talk I shall deal with a generalisation of this idea beyond logic towards the idea of general rules systems. The most advanced theory of such systems is found in the theory of inductive definitions as well as in logic programming. I will inparticular deal with the latter and expose some ideas concerning extensions of definitional reflection. Defitional reflection is an approach that uses the evaluation of definitional rules on the assumption side and leads to a powerful extension of definite Horn clause programming, in particular when we consider clauses with variables. The corresponding inversion principles for logical rules can be viewed as special cases of this more general approach. In a sense this calls into question the traditional Aristotelian view that logic is a universal inference machine into which content is ``plugged in'' by means of axioms or assumptions.

A further extension deals with the addition of refutation rules, i.e. introduction rules for assumptions, as part of the definitional database. This leads to a more sophisticated way of dealing with negation. Here the dogma mentioned above shows up as the dogma of the primacy of assertion over denial. I shall argue in favour of a system in which negation by failure can be present along with a more direct (``strong'') negation.

***********************************************************