PhD Thesis

M. Ferrari. Strongly Constructive Formal Systems. PhD thesis, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, Italy, 1997.
Abstract
We propose a formalization of a notion of strongly constructived formal system, intuitively intended as a formal system characterized by a calculus with the following properties: any proof of a closed formula such as $A\vee B$ (of a closed formula such as $\exists xA(x)$) contains sufficient information to build up a proof of $A$ or a proof of $B$ (respectively, a proof of $A(t)$ for some closed term $t$). Our treatment far exceeds the class of intuitionistic systems and the class of system for which normalization or cut-elimination theorems can be stated. In the thesis we exhibith several superintuitionistic formal systems which turns out to be strongly constructive. Finally, we provide an example of a system which is not strongly constructive (more than this, not strongly semiconstructive), yet satisfying the disjunction property and the explicit definability property.
ps.gz

Contents

1 Introduction and preliminaries
  • Introduction
  • Preliminaries
  • Hilbert calculi
  • Natural Deduction

2 Fundamentals
  • Formal systems
  • Proofs and calculi
  • Generalized rules
  • Uniformity
  • Strongly constructive formal systems
  • Relations with program synthesis

3 Exhibiting strongly constructive logics
  • Generalities
  • Intuitionistic Logic
  • Kuroda Logic
  • Grzegorczyck Logic
  • Kreisel-Putnam Logic
  • Scott Logic
  • Harrop Theories

4 Exhibiting strongly constructive theories
  • Theories with closed evaluation
  • Intuitionistic arithmetic
  • Generalized induction
  • Descending chain principle
  • Markov principle

5 A constructive but not strongly constructive formal system
  • Basic recursion theory
  • Notions of representability
  • The formal system HA*