Proofs from a Geometric Perspective
Anjolina Grisi de Oliveira

Tese apresentada à Pós-Graduação do Centro de Informática da Universidade Federal de Pernambuco em Fevereiro de 2001 para Obtenção do Grau de Doutor em Ciência da Computação

Banca Examinadora: Kátia Silva Guimarães (CIn-UFPE), José Dias dos Santos (CIn-UFPE), Marcelo Finger (DCC/IME-USP), Luiz Carlos Pereira (Filosofia/PUC-Rio), Antônio Carlos da Rocha Costa (UCPel).

Orientador: Ruy J. G. B. de Queiroz

(Durante a elaboração deste trabalho, o autor recebeu apoio financeiro da CAPES)

(Para obter o arquivo postscript com o texto integral clique aqui)


We are here concerned with the study of proofs from a geometric perspective. By first recalling the pioneering work of Statman in proposing such kind of study in his doctoral thesis Structural Complexity of Proofs (1974), we review two recent research programmes which approach the study of structural properties of formal proofs from a geometric perspective: (i) the notion of proof-net, given by Girard in 1987 in the context of linear logic; and (ii) the notion of logical flow graph given by Buss in 1991 and used as a tool for studying the exponential blow up of proof sizes caused by the cut-elimination process, a very recent programme (1996-2000) proposed by Carbone in collaboration with Semmes. We consider these two works as our starting point in the investigation of proofs from a geometric perspective, and they shall guide the formulation of our present proposal.

Statman's geometric perspective does not seem to have developed much further than his doctoral thesis, but the fact is that it looks as if the main idea, i.e. extracting structural properties of proofs in natural deduction using appropriate geometric intuitions, offers itself as a very promising one. With this in mind, and having at our disposal some interesting and rather novel techniques developed for proof-nets and logical flow graphs, we have tried to focus our investigation on a research for an alternative proposal for looking at the geometry of natural deduction systems. The lack of symmetry in natural deduction systems is one of the aspects which represents a challenge for such a kind of study. Of course, one alternative to deal with the problem of lack of symmetry in ND systems is to look at multiple-conclusion calculi. We already have in the literature different approaches involving such calculi. For example, Kneale's (1958) tables of development (studied in depth by Shoesmith and Smiley (1978)) and Ungar's (1992) multiple-conclusion natural deduction. Our proposal is similar to both Kneale's and Ungar's in various aspects, mainly in the presentation of a multiple conclusion calculus inspired in natural deduction systems. However, we wish to bring our system, which we have named as n-graphs, into the current state-of-affairs by incorporating some of the techniques developed for proof-nets (e.g., splitting theorem, soundness criteria, sequentialization), and at the same time study its structural properties via a geometrical representation of of proofs. A future development should also include the study of the complexity of ND derivations in the lines of the work of Carbone for the sequent calculus.

Última atualização: 18 de Dezembro de 2001, 11:42:40 GMT-0200.