Proof Theory of Analogical Reasoning and Juridical Logic

The logical background of juridical reasoning systems is determined by the
tension between

a. arguments should be demonstrably sound

b. decisions have to be achieved within limited time and space.

In this lecture we develop a proof theory of analogical reasoning starting
from the breathtaking summation of 1/n^2, an analogical conclusion which made
Euler famous.

We demonstrate, how minimalist legal systems (as English Common law)/
maximalist legal systems (as Austrian,German and in general Latin law)make
use of analogies to extend/restrict deductions in the sense of mathematical
logic. We reduce the well-known specific deduction rules in German law (e.g.
E CONTRARIO)to simple forms of analogical reasoning.

A Reconstruction of the 1910

It has always been conceded that the 1910 *Principia* does not deny the existence of classes, but claims only that the theory it advances can be developed so that the apparent commitment to classes is eliminable by the method of contextual analysis. I argue that the work has an illuminating reconstruction within a framework which *admits* the existence of classes. To preserve many of *Principia*'s most distinctive theses, it is sufficient to maintain that classes are dependent on or presuppose propositional functions in a way I explain. So reconstructed, the work contains a theory of our knowledge of classes whose elegance has not, to my mind, been adequately appreciated.

What can be done with formal mathematical texts?

In the past few decades, logicians, mathematicians, computer
scientists, and philosophers have spent much energy developing
libraries of formal mathematical texts: they have designed high-level
languages that capture various aspects of the mathematical vernacular
and implemented computer programs that process these libraries
efficiently. In this talk I discuss these libraries and discuss how
they are processed, especially with reference to how proof libraries
can help one to learn a body of mathematical knowledge. To illustrate
this kind of learning I focus on a particular aspect of the recent
proof of Gdel's completeness theorem carried out within the MIZAR
system by Patrick Braselmann and Peter Koepke; this example will
illustrate how a proof environment (in this case, the MizarMode
environment for the Emacs text editor) can be used to study a formal
exposition of a landmark theorem of mathematics. I close by warning
against certain tempting conclusions concerning these formal texts,
for example, the conclusion that because they have been checked by a
computer they are infallible, and that because they are completely
formal they provide a universal standard for settling mathematical and
philosophical debates.

References:

- Patrick Braselmann and Peter Koepke: "Goedel's completeness theorem" URL: http://megrez2.cs.shinshu-u.ac.jp/mmlquery/fillin.php?filledfilename=p hparticle.mqt&argument=article+goedelcp
- The MIZAR Project. URL: http://www.mizar.org
- Josef Urban: MizarMode: An integrated proof assistance tool for the MIZAR way of formalizing mathematics. Journal of Applied Logic (to appear).

Themes from Goedel: Foundational Aspects of Modern Set Theory

In this talk I will discuss a number of themes in contemporary set
theory that have their origin in the work of Kurt Goedel. Themes
will include: the distinction between intrinsic and extrinsic
justifications of new axioms; the program for large cardinal axioms;
the status of the continuum hypothesis; inner models for large
cardinals; and the question of whether there are set-theoretic
statements that are in some sense absolutely undecidable.

I will argue that a cluster of results show that there is a good deal
of structure and unity beyond ZFC and that there is a precise sense in
which every question of complexity strictly ``below'' that of the
Continuum Hypothesis is settled by large cardinal axioms. I will then
discuss the various ways in which something new emerges at the level
of the Continuum Hypothesis and examine various positions to the
effect that it does not admit of a solution. I will close by
examining recent results of Hugh Woodin and a scenario for axioms
extending ZFC that are as complete for the universe of sets as the
axioms of PA are for the natural numbers.