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.
***********************************************************
Adresa elektronske poste Seminara: teorija.dokaza@gmail.com
***********************************************************