PROCEEDINGS OF THE SECOND WORKSHOP ON LOGICAL FRAMEWORKS

Edinburgh

May 1991

Eds G. Huet, G. Plotkin & C. Jones

Contents

Foreword . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 Workshop Programme . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 Abstracts of Demonstrations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 Abstracts of Talks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 List of Participants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 F. Barbanera, S. Berardi Witness Extraction in Classical Logic through Normalization 25 D. A. Basin, R. L. Constable Metalogical Frameworks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Y. Bertot A Canonical Calculus of Residuals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 T. Coquand A semantics of evidence for classical arithmetic . . . . . . . . . . . . . . . . . . . . . . . . . . . 87 R. Diaconescu, J. Goguen, P. Stefaneas Logical Support for Modularisation. . . . . . . . 101 G. Dowek A Complete Proof Synthesis Method for the Cube of Type Systems . . . . . . . . . 135 A. Felty A Logic Program for Transforming Sequent Proofs to Natural Deduction Proofs 165 G. Huet A case study in Axiomatisation and Proof Development in the Coq Proof Assis-

tant. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 185 C. Jones Completing the Rationals and Metric Spaces in LEGO . . . . . . . . . . . . . . . . . . . . . . . 209 Y. Lafont Negation versus Implication . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 223 S. Matthews, A. Smaill, D. Basin Experience with F S_{0} as a Framework Theory …. 231 T. F. Melham A Mechanized Theory of the π-calculus in HOL . . . . . . . . . . . . . . . . . . . . . . . . 253 D. Miller Unification of Simply Typed Lambda-Terms as Logic Programming . . . . . . . . . . 273 C. Murthy Finding the Answers in Classical Proofs: A Unifying Framework . . . . . . . . . . . 287 T. Nipkow Order-Sorted Polymorphism in Isabelle. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 307 C. Phillips Well-founded Induction and Program Synthesis Using Proof Plans . . . . . . . . . . 323 D. Pym Towards an Algebraic Framework for Defining Sequential Logics . . . . . . . . . . . . . . . 335 J. M. Smith An Interpretation of Kleene’s Slash in Type Theory . . . . . . . . . . . . . . . . . . . . . . 337 N. Szasz A Machine Checked Proof that Ackermann’s Function is not Primitive Recursive 343

⋆⋆ ⋆ ⋆ ⋆ ⋆ ⋆ ⋆⋆ ⋆ ⋆ ⋆ ⋆ ⋆ ⋆ ⋆^{Logical Frameworks}

Foreword

This document is the preliminary proceedings of the Second Annual Workshop on Logical Frameworks, funded by the Esprit Basic Research Action 3245 “Logical Frameworks: Design, Implementation and Experiment”.

This workshop was held at St Cecilia’s Hall in Edinburgh from the 19th to the 24th of May 1991; it was attended by 93 people. The programme was put together by Gerard Huet and Gordon Plotkin. Local arrangements were looked after by George Cleland, Monica Lekuse and Gordon Plotkin. Paul Anderson and George Cleland took care of computing provision.

These preliminary proceedings have been collected from LaTEX sources, using electronic mail and spliced together (thanks to all who read the guidelines). They comprise 19 of the 28 papers presented at the meeting.

This document may be obtained by anonymous ftp from Edinburgh University (compressed file export/bra/proc91.dvi.Z on “cumbrae”, internet address 129.215.160.150, login name “anonymous”).

2

Workshop Programme: Logical Frameworks, 1991

Sunday, May 19th

6.30–9.30pm  Reception
7.30–8.30pm  Concert

Strathclyde University Chamber Choir

Monday, May 20th

9.00–9.10am  Welcome to Workshop
9.10–10.00am David Basin and Robert Constable

Invited Talk: Meta-logical frameworks

10.00–10.30am Tobias Nipkow

Order-Sorted Polymorphism

10.30–11.00am Coffee Break
11.00–11.45am Christine Paulin-Mohring

Properties of Programs extracted from proofs in the Calculus of Inductive Definitions

11.45–12.30pm Yves Bertot

An Effective Calculus of Residuals

12.30–2.00pm Lunch
2.00–3.00pm  Presentation of Demonstrations

Goteborg Demo Thierry Coquand, Bengt Nordstrom, Lennart Augustsson: ALF Cambridge Demo Tom Melham: Theorem-proving tools in the HOL system. Edinburgh Demo Randy Pollack: LEGO INRIA Rocquencourt Demo Gerard Huet, Amy Felty, B. Werner, H. Herbelin, Gilles Dowek: Presenting the system Coq, version 5.6.

3.00–4.30pm  Demonstration sessions, (tea available)
4.30–5.00pm  Discussion of Demonstrations

Tuesday, May 21st

9.00–10.00am Tom Melham

Invited Talk: A Mechanized Theory of the pi-calculus in HOL

10.00–10.30am Claire Jones

Completing the Rationals and Metric Spaces in LEGO

10.30–11.00am Coffee Break
11.00–11.45am Nora Szasz

A Machine checked proof that Ackermann’s function is not primitive recursive

11.45–12.30pm Per Martin-Lof

Choice sequences in type theory

12.30–2.00pm Lunch
2.00–3.00pm  Presentation of Demonstrations

Cambridge Demo Larry Paulson, Toby Nipkow: Polymorphic Isabelle. Edinburgh Demo Alan Smaill, Colin Phillips: The CLAM proof planner. INRIA Sophia-Antipolis Demo Laurent Thery: Using Centaur as a front end for theorem provers Paris VII Demo M. Parigot, P. Manoury, M. Simonot, C. Raffalli: PROPRE: an experimental language for programming with proofs.

3.00–4.30pm  Demonstration sessions, (tea available)
4.30–5.00pm  Discussion of Demonstrations

Wednesday, May 22nd

9.00–10.00am N.G. de Bruijn

Invited Talk: Algorithmic correctness check for the delta-lambda calculus

10.00–10.30am Yves Lafont

Programming languages inspired by classical logic

10.30–11.00am Coffee Break
11.00–11.45am F Barbanera and Stefano Berardi

Program Extraction for Classical logic

11.45–12.30pm Michel Parigot

Free Deduction: an analysis of computations in classical logic

12.30–2.00pm Lunch
2.00–5.30pm  EC Review (details to be confirmed)

Thursday, May 23rd

9.00–10.00am Dale Miller

Invited Talk: Unification of Simply Typed Lambda-Terms as Logic Programming

10.00–10.30am David Pym

Towards an Algebraic Framework for Defining Sequential Logics

10.30–11.00am Coffee Break
11.00–11.45am Razvan Diaconescu and Joseph Goguen

Logical Support for Modularisation

11.45–12.30pm Thierry Coquand

A question about classical logic

12.30–2.00pm Lunch
2.00–2.45pm  Herman Geuvers

Iteration and Recursion on Inductive and Coinductive Types

2.45–3.30pm  Jan Smith

An interpretation of Kleene’s slash in type theory

3.30–4.00pm  Tea
4.00–4.45pm  Gilles Dowek

Proof synthesis in Barendregt’s cube

4.45–5.30pm  Gilles Amiot

Second order unification and some applications

6.30pm  Leave for Banquet at Dalhousie Castle Hotel

Friday, May 24th

9.00–10.00am Robert Harper

Invited Talk: A Calculus of Modules for LF and Elf

10.00–10.30am Amy Felty

A Logic Program for Transforming Sequent Proofs to Natural Deduction Proofs

10.30–11.00am Coffee Break
11.00–11.45am Philippa Gardner

ELF+: a type theory for representing logics

11.45–12.30pm Sean Matthews, David Basin and Alan Smaill

Experience with FS0 as a Framework Theory

12.30–2.00pm Lunch
2.00–2.45pm  Z Luo

Data Refinement in Type Theory

2.45–3.30pm  Chet Murthy

Extracting proofs from Classical Logic

3.30–4.00pm  Tea
4.00–4.45pm  Vincent Danos

New ways to look at lambda-calculus: pure nets and dynamic algebras

4.45–5.30pm  Stefano Berardi

Program extraction for Predicative Systems.

Abstracts of Demonstrations

Cambridge Demo

Tom Melham Theorem-proving tools in the HOL system

Abstract

The HOL system is an LCF-style proof assistant for reasoning in a version of higher order logic based on Church’s formulation of simple type theory. The LCF approach to theorem proving is fairly well known, so this demonstration of the HOL system will concentrate primarily on the theorem-proving tools that have been built on top of the system, rather than on the core system itself.

Cambridge Demo

Larry Paulson, Toby Nipkow Polymorphic Isabelle

Abstract

Isabelle has been extended with order-sorted polymorphism. The sort system for type variables allows object-logics to exploit the meta-level polymorphic type system in a controlled fashion. Many-sorted first-order logic is obtained by declaring polymorphic quantifiers, where the type variables may range over, say, the types of integers and lists (for suitable element types). Higher-order logic is obtained by allowing the type variables to range over function types and the type of truth values.

The demonstration will present the formalization of higher-order logic and demonstrate proofs involving a formalization of propositional logic within higher-order logic. This illustrates the use of Isabelle to reason inductively about the structure of proofs.

Edinburgh Demo

Randy Pollack LEGO

Abstract

Lego is a proof checker for several type theories related to the Calculus of Constructions, intended for research in machine-checked mathematics. Examples checked in Lego include SN of second-order lambda calculus (Berardi), Tarski’s fixpoint theorem, the binomial theorem for rings, some elementary topology and metric spaces, the deduction theorem for first order logic, derivation of sorting programs, and Coquand’s proof of Girard’s paradox. This work owes much to many people, most immediately Th. Coquand, R. Harper, G. Huet, and Z. Luo.

The demonstration will show the following features of Lego:

Type theories Lego supports the Edinburgh Logical Framework (LF), the Pure Calculus of Constructions, and Luo’s Extended Calculus of Constructions (ECC) with a predicative hierarchy of cumulative universes and Sigma Types.

Refinement and Direct Proof The principal means of constructing proofs is interactive proof refinement by resolution. There are also features supporting direct bottom-up proof, and mixing of refinement and direct proof.

Definitions Each of the type theories is extended with a notion of definition. These definitions serve both for notational extension and (using the propositions as types paradigm) for formalizing a context of proved theorems.

Inferred Polymorphic Instantiation All of the supported type theories have explicit polymorphism. Lego has an algorithm to infer some explicit polymorphic instantiation.

Typical Ambiguity Lego has an algorithm to infer universe numbers, thus providing typical ambiguity. Lego also implements the let polymorphism this typical ambiguity induces. To the user this system looks very like Type:Type, although the typechecker maintains universe stratification.

Among the aspects of mathematical reasoning we are not satisfied with in Lego are equality reasoning, lack of “inductive types”, and the notion of tactics. Currently we are experimenting with adding reductions to a context (as in ALF). For the future, I am working on a new implementation with a simpler and more uniform notion of refinement, and supporting Generalized Type Systems extended with Sigma Types and cumulativity.

Lego is available from LFCS, Computer Science Department, The King’s Buildings, University of Edinburgh EH9 3JZ, UK.

Edinburgh Demo

Alan Smaill, Colin Phillips The CLAM proof planner

Abstract

The CLAM system takes a meta-level description of a theorem-proving task, and a number of tactic specifications (known as methods), in order to return a combination of tactics that are likely to yield a proof of a given conjecture. We show the system in use in the domain of inductive proofs, interfaced to different implementations of type theory.

Goteborg Demo

Thierry Coquand, Bengt Nordstrom, Lennart Augustsson ALF

Abstract

ALF (Another Logical Framework) is an implementation of a logical framework. It runs under X-windows and uses windows extensively to make derivations easier.

INRIA Rocquencourt Demo

Gerard Huet, Amy Felty, B. Werner, H. Herbelin Gilles Dowek Presenting the system Coq, version 5.6.

Abstract

Coq is an implementation of the Calculus of Inductive Constructions, under development at INRIA Rocquencourt and ENS Lyon. We first show Gilbreath’s trick (G. Huet), which illustrates the methodology for proving inductive mathematical statements in a top-down fashion, using a basic set of 5 tactics. Next, we present our new user interface, using the CAML widgets of D. de Rauglaudre (A. Felty). We then present the extraction of running ML programs from inductive proofs (B. Werner). As an application, we demonstrate the behaviour of a program corresponding to an A-translation of a classical proof of Higman’s lemma (H. Herbelin). Finally, we present a prototype implementation of a new engine with existential variables for proof synthesis (G. Dowek).

INRIA Sophia-Antipolis Demo

Laurent Thery Using Centaur as a front end for theorem provers

Abstract The demonstration comprises two parts:

– first, we use Amy Felty’s theorem prover, build a proof in the Intuitionistic Sequent Calculus, and display it in different formats: Sequent proof, Natural Deduction Proof tree, and textual proof. The prover is written in lambda-Prolog, and we use the Z implementation of lambda-Prolog, which is 15 times faster than elp.

– second, we use HOL as a logical engine; the front end is more sophisticated due to the complexity of the HOL environment.

This is ongoing work of Laurent Théry for his Ph.D. thesis.

Paris VII Demo

M. Parigot, P. Manoury, M. Simonot, C. Raffalli PROPRE: an experimental language for programming with proofs

Abstract

PROPRE is an experimental programming language based on the paradigm “proofs as programs”. Programs are terms of λ-calculus extracted from proofs of termination of functions defined by sets of equations, using deterministic proof strategies. Each strategy is based on a particular form of induction. In this demo we will show examples of derivation of programs using these strategies. We will show what we are able to do and what we are not able to do, at the present time.

10

Abstracts of Talks

Gilles Amiot Second order unification and some applications

Abstract

Second order unification is an extension of standard unification (defined by Herbrand, Robinson). This extension is obtained by adding to the language second order variables. There are two possible extensions: the first is to add function variables, and the second is to add predicate variables. We present the results on the decision problem for both cases (the first was completely investigated by Goldfarb and Farmer, and the second by Amiot). Unification has numerous applications. In particular, it has applications in proof theory and proof search. In order to illustrate these applications, we show how decision problems in linear logic can be linked with unification. In particular we derive new undecidability results for linear logic from undecidability results for second order unification.

F Barbanera and Stefano Berardi Program Extraction for Classical logic

Abstract

Statman and Prawitz considered Intuitionistic Natural Deduction System for logic and arithmetic, with the non-logical part reduced to (maybe induction and) atomic rules of the form:

\frac{A_{1}, …, A_{n}}{A}

(with A_{1}, …, A_{n}, A atomic). Then they added, together with double negation rule, reductions to eliminate the use of double negation for maximum formulas (Statman), or for non-atomic formulas (Prawitz). For arithmetical systems the double negation rule for atomic formulas is constructively correct . A sample of Statman reductions is:

\frac{[¬A&B] ; ⋮ ; False}{\frac{A&B}{A}}

reduces to:

\frac{[¬A] \frac{[A&B]^{1}}{A}}{\frac{False}{\frac{[¬A&B] ; ⋮ ; False}{A} Double Neg.} 1}

One cannot define such reductions for ∨ and ∃; thus, one is forced to put:

A ∨ B = ¬(¬A&¬B)
∃xA = ¬(∀x¬A)

One obtains, that way, a Classical Natural Deduction System for Arithmetic. The main technical results for it are:

1. Strong Normalization and Church-Rosser;

2. A closed normal proof of False contains only closed atomic formulas, or negations of closed atomic formulas.

From 1 and 2 one may infer consistency, as did Prawitz. In our paper, we use it, instead, to extract the “witness” of an existential statement, in the following way:

If one has a closed classical proof of (∃x(f(x) = 0)), just add the atomic rule:

\frac{f(x) = 0}{False}

and get a closed proof of False (of course, the new rule is semantically incorrect!).

Points 1 and 2 hold in the extended system, because we only added an atomic rule. By 1, one obtains a closed normal proof of False ; by 2, such a proof contains only closed atomic formulas, or their negations. Thus, one proves False using only a finite number of times this new rule, say:

\frac{f(a_{1}) = 0, …, f(a_{n}) = 0}{False}

(a_{1}, …, a_{n} closed values of type Integer) and this forces f(a_{1}) = 0, or …, or f(a_{n}) = 0.

Of course, the problem is to pick up some a_{i} such that f(a_{i}) = 0; some non-deterministic choice must be allowed. Prawitz’s suggestion was to add the following new reduction: replace a proof of an atomic A with any proper subproof of the same A (if any!), proviso that the assumptions of the subproofs are included in the assumptions of the proof. With such a new reduction, we prove that we get rid of all applications of the new rule, but one at the end:

\frac{f(a_{i}) = 0}{False}

This forces f(a_{i}) = 0 to be true, as wished. We use a system exploiting ideas similar to Kripke forcing semantics to explain and obtain the technical results outlined above.

David Basin Robert Constable Meta-logical frameworks

Abstract

In computer science we speak of implementing a logic; this is done in a programming language, such as Lisp, called here the implementation language. We also reason about the logic, as in understanding how to search for proofs or in knowing it is consistent; in the terminology of mathematical logic, these arguments are conducted in the metalanguage of the object language being implemented. We also reason about the implementation itself, say to know it is correct. This is done in a programming logic. How do all these logics relate? This paper considers that question and more.

We show that by taking the view that the metalogic is primary, these other ones are related to it in standard ways. The metalogic must be suitably rich so that the object logic can be presented as an abstract data type, and it must be suitably computational (or constructive) so that an instance of the type is an implementation. The data type abstractly encodes all that is relevant for metareasoning, i.e. not only the term constructing functions but also the principles for reasoning about arbitrary terms and computing with them.

Our work can also be seen as an approach to the task of finding a generic way to present logics and their implementations, which is for example the goal of the Edinburgh Logical Frameworks (LF) effort. This approach extends well beyond proof-construction and includes computational metatheory as well.

Stefano Berardi Program extraction for Predicative Systems

Abstract

We consider two extensions of an algorithm, due to Takayama, which simplifies proofs of a specification to programs which satisfy the given specification. We also prove, using a naive settheoretical semantic, that the simplified algorithms have still the same input/output behaviour of the original ones, and thus that they satisfy the original specification.

Yves Bertot An Effective Calculus of Residuals

Abstract

Considering a natural semantics specification of lambda-calculus, we show that a formal manipulation of the inference rules permits to introduce effective residual computations. These computations have applications in all kinds of marked reduction systems used in proving theorems in the lambda calculus, e.g. the finite developments theorem etc.

Thierry Coquand A question about classical logic

Abstract

We present Gentzen’s first proof of consistency of arithmetic formulated in the framework of inductive definitions. This reformulation suggests naturally a semantics of evidence for classical arithmetic. While toying with an example of Gabriel Stolzenberg that involves a typically classical lemma (infinite box principle), it appeared that there is another way of doing the cutelimination than Gentzen’s method. We present this algorithm, its proof of partial correctness, and the conjecture of total correctness.

Vincent Danos New ways to look at lambda-calculus: pure nets and dynamic algebras

Abstract

Pure nets and dynamic algebra are two new models of computation directly issued from linear logic. The talk will give an elementary presentation of these models, state their basic computational properties and compare them to lambda-calculus.

N.G. de Bruijn Algorithmic correctness check for the delta-lambda calculus

Abstract

The delta lambda calculus is a lambda-typed lambda calculus with facilities for built-in definitions. A term in that calculus can efficiently represent a complete mathematical theory, with axioms, definitions, theorems and proofs. Correctness of a theory can therefore be interpreted as the correctness of a single lambda term. The talk will describe an algorithm that provides the essential kernel for a correctness checking program. Given a lambda term, that kernel produces, more or less in linear time, a list of subtasks. To every application occurring in the term there corresponds exactly one subtask. The subtasks are all of the following form: show that in the context C the type of A is definitionally equal to B.

Razvan Diaconescu and Joseph Goguen Logical Support for Modularisation

Abstract

Modularisation is important for managing the complex structures that can arise in large theorem proving problems, and in large software and/or hardware development projects. This paper studies some properties of logical systems that support the definition, combination, parameterisation and reuse of modules. These properties include: (1) the preservation of various kinds of conservative extension under pushouts; (2) distributive laws for information hiding over sums; and (3) (Craig style) interpolation properties. Our results illuminate some interesting differences between equational style logics and first order style logics, encouraging us to conclude that, on the whole, equational style logics are more suitable for modularisation than first order style logics. We represent logical systems as institutions, and modules as sets of sentences. An important technical foundation is a novel categorical axiomatisation of the notion of “inclusion”. We also show how to subsume the deduction-based approach of π-institutions under that of ordinary institutions, so that our results also apply to that setting.

Gilles Dowek Proof synthesis in Barendregt’s cube

Abstract

We sketch a few recent results in automated theorem proving in type systems of the Cube. We first present a complete proof synthesis method extending Huet’s resolution. Because type systems of the cube verify the proofs-as-objects paradigm, the proof synthesis method is a one level process that merges unification and resolution. We also study two variants of this method, the first is incomplete but much more efficient and the second is a pre-unification algorithm. Then we present an algorithm for second order matching in all the systems of the cube and sketch proofs of undecidability of higher order matching in seven of these systems.

Amy Felty A Logic Program for Transforming Sequent Proofs to Natural Deduction Proofs

Abstract

In this talk, we show that an intuitionistic logic with second-order function quantification, called hh^{2}, can serve as a meta-language to directly and naturally specify both sequent calculi and natural deduction inference systems for first-order logic. For the intuitionistic subset of first-order logic, we present a set of hh^{2} formulas which simultaneously specifies both kinds of inference systems and provides a direct and concise account of the correspondence between cut-free sequential proofs and normal natural deduction proofs.

The logic of hh^{2} can be implemented using such logic programming techniques as providing operational interpretations to the connectives and implementing unification on λ-terms. With respect to such an interpreter, our specification provides a description of how to convert a proof in one system to a proof in the other. The operation of converting a sequent proof to a natural deduction proof is functional in the sense that there is always one natural deduction proof corresponding to each sequent proof. Our specification, in fact, provides a direct implementation of the transformation in this direction.

Philippa Gardner ELF+: a type theory for representing logics

Abstract

Using the framework ELF, we cannot distinguish which part of the type theory corresponds to the encoded logic without appealing to the particular encoding under consideration. We define a new framework, ELF+, based on ELF. With ELF+, we can identify the substructures of the type theory that correspond to the encoded logics. This enables us to characterize the notion of adequacy for such encodings.

When we represent a logic in ELF+, we identify the variables of the logic with certain variables of the type theory. Therefore, substitution for the object logics must behave in a similar way to substitution for the type theory. This motivates the presentation of the logics and their corresponding ELF+ substructures as indexed categories, so that encodings become functors between indexed categories. Adequate representation is then determined by conditions on such functors. Herman Geuvers Iteration and Recursion on Inductive and Coinductive Types. Abstract In his thesis T. Hagino introduces a typed lambda calculus with categorical data types, which includes both inductive and coinductive types. The reduction rules in this calculus only represent the iteration scheme and not recursion (which has to be “coded”.) Coquand and Mohring encapsulate a notion of inductive type in a higher order type theory, which has real recursion and also captures the notion of inductive proof. In this talk we want to discuss the differences between iteration and recursion and extend a Coquand-Mohring-like higher order type system with coinductive types with a form of recursion.

Robert Harper A Calculus of Modules for LF and Elf

Abstract

The logical framework LF is a language for defining logical systems based on the judgementsas-types principle. Elf, an implementation of LF, provides an operational interpretation of LF types, so that LF signatures may be read as logic programs. As a result the LF lambda calculus is used both as a logic definition language and as a meta-programming language for manipulating object logics. In practice this methodology leads to relatively large signatures with a natural structure that cannot be adequately expressed in the basic LF lambda calculus. In particular, it would be desirable to support incremental construction of logic definitions and meta-programs (a form of “code inheritance”), parameterization and instantiation, and the interpretation of one system within another. In addition to the static structure of presentations, it is also important to provide mechanisms to initiate and control search. We present an initial design of a calculus of modules for LF and Elf, and illustrate its use with a number of examples.

[This talk represents joint work with Frank Pfenning.]

Claire Jones Completing the Rationals and Metric Spaces in LEGO

Abstract

This talk will describe the work carried out in implementing/proving some elementary theorems of analysis in the Extended Calculus of Constructions using the LEGO system. Two main areas have been considered, firstly the completion of a metric space (defining a constructions function of type Metric -> Metric) and secondly the construction of the reals from the rationals. Many interesting issues arise from this e.g. how best to represent sets, subsets and functions.

Yves Lafont Programming languages inspired by classical logic

Abstract I will discuss the relations between:

1. the proof theory of intuitionistic and classical logic

2. exceptions and the continuations in functional programming.

This is inspired by the recent constructive interpretation of classical logic by J.Y. Girard.

Z Luo Data Refinement in Type Theory

Abstract

We consider a type-theoretic approach to program specification and data refinement and show that a type theory with a strong logical power and good structural mechanisms provides a uniform and adequate formalism for modular development of programs and specifications.

Per Martin-Löf Choice sequences in type theory Sean Matthews, David Basin and Alan Smaill Experience with FS_{0} as a Framework Theory

Abstract

Feferman has proposed a logic, “FS_{0}”, as an alternative framework for encoding logics and also for reasoning about those encodings. We have implemented a version of this system and performed experiments that support this claim. Specifically, we describe a formalization of predicate calculus and the development of a derived rule that manipulates formulas with bound variables. This application will be of interest to researchers working with frameworks which internalize bound variables in the meta-logic. We suggest that formalizing and reasoning about bound variables is not as difficult as is often supposed, and leads to a more powerful theory about the encoded logic.

Tom Melham A Mechanized Theory of the pi-calculus in HOL

Abstract

The pi-calculus is a process algebra in the style of CCS, developed by Milner, Parrow and Walker for modelling concurrent systems in which the pattern of interconnection between processes can change over time. This talk will describe work in progress on a mechanized formal theory of the pi-calculus in higher order logic using the HOL theorem prover. The main aim of this work, which is being done jointly with Mike Gordon at the Computer Laboratory in Cambridge, is to provide a tool to support both reasoning about applications using the pi-calculus and metatheoretic reasoning about the calculus itself.

Dale Miller Unification of Simply Typed λ-Terms as Logic Programming

Abstract

The unification of simply typed λ-terms modulo the rules of βη-conversion is often called “higher-order” unification because of the possible presence of variables of functional type. This kind of unification is undecidable in general and if unifiers exist, most general unifiers may not exist. In this paper, we show that such unification problems can be coded as a query of the logic programming language L_{λ} in a natural and clear fashion. In a sense, the translation only involves explicitly axiomatizing in L_{λ} the notions of equality and substitution of the simply typed λ-calculus: the rest of the unification process can be viewed as simply an interpreter of L_{λ} searching for proofs using those axioms.

Chet Murthy Extracting Proofs from Classical Logic

Abstract

Recently there has been much interest in the problem of finding the computational content of classical reasoning. Work in this area has for the most part focused on re-interpreting various classical results. These different initial starting points result in (ostensibly) completely different notions of computation, spanning the range from concurrent, to sequential algorithms, and yielding semantics of valuations, finite domains, and coherence spaces. In this paper, we attempt to provide a unifying framework for viewing some of these diverse attempts, showing that work of Murthy, and Barbanera and Berardi can be smoothly integrated into the same framework, and seen as different facets of the same phenomenon. We make the first steps toward integrating Girard’s classical interpretation into this framework, in the process isolating a new classical reduction, computing under λ-abstraction, which must be added in order to represent his system. We argue that the computational content of a classical proof is most simply understood as a program in an almost-functional language (enriched with Felleisen’s “control” operator, C), and that this interpretation yields, under various restrictions, the different methods of extracting computations from classical proofs we examine.

Tobias Nipkow Order-Sorted Polymorphism

Abstract

ML-style polymorphism can be generalized from a single-sorted algebra of types to an ordersorted one by adding a partially ordered layer of “kinds”, “sorts”, or “classes” on top of the types. The resulting type system has been implemented in Isabelle to permit type variables in polymorphic constants to range over certain user-definable subsets of all types. It is shown how order-sorted polymorphism allows a simple specification of type restrictions in many logical systems. It can also be used to explain Standard ML’s equality types and Haskell’s type classes and provides a simple extension of the Hindley/Milner type inference algorithm based on ordersorted unification.

Christine Paulin-Mohring Properties of Programs extracted from proofs in the Calculus of Inductive Definitions

Abstract

The Calculus of Constructions extended with Inductive Definitions is a suitable framework for the development of certified programs as the computational meaning of constructive proofs. We previously defined for the pure Calculus of Constructions a notion of realizability which interprets a proposition as a set of programs typed in the non-dependent part of the Calculus. In this talk, we shall study the extension of such interpretation to the Inductive Definitions.

Michel Parigot Free Deduction: an analysis of computations in classical logic

Abstract

Free Deduction (FD) is a deduction system for classical logic designed to understand computations (i.e. cut-elimination) in classical logic - a task which is not achieved by sequent calculus. From a logical viewpoint FD behaves like sequent calculus. But from a computational point of view it allows both a local cut-elimination procedure (like sequent calculus) and a global one (like intuitionistic natural deduction). The main advantage provided by the global elimination procedure is the possibility to state and prove Church-Rosser and Strong Normalisation results for this calculus.

Colin Phillips Well-founded Induction and Program Synthesis Using Proof Plans

Abstract

The Mathematical Reasoning Group in the Department of Artificial Intelligence at Edinburgh University has developed an approach to the synthesis of programs using proof plans - high level descriptions of proofs which control the automatic search for a proof from which a program can be derived using the proofs as programs technique. The proofs in question employ various forms of induction and techniques have been developed for automating the search for a form of induction appropriate to a given proof.

In this paper I will discuss a modification of this approach which involves using transfinite induction and the automated search for the appropriate well-founded relation. This is being implemented in a version of Martin-Lof’s extended by Nordstrom’s Acc Type. I shall be comparing this approach with that previously employed in the Mathematical Reasoning Group.

David Pym Towards an Algebraic Framework for Defining Sequential Logics

Abstract Intuitionistic type-theoretic logical frameworks are inadequate in several respects:

- They are intuitionistic — weak logics are difficult;

- The notion of logic as proposition-object together with proof-object is present, but too restrictive and not analysed;

- There is no analysis of sequent calculus;

- There is no analysis of proof reduction;

- There is no clean, general access to a model theory;

- There is no analysis of the notion of a framework — characterization of encoding etc..

We propose a framework based on early ideas of Kelly, some recent developments of Hagino, and the hierarchical sensibilities of (Generalized) Type Systems. To this end we propose notions of algebra and dialgebra for indexed functors. Then fibred adjunctions permit the definition of generalizations of Hagino’s datatypes and (syntactic) specification language. Starting from an axiomatization of some primitive monoidal connectives, one can obtain, uniformly, Gentzen-type axiomatizations of all such inductively defined logics.

Such a framework provides a quite general analysis of (dependent) type theories, including logically weak theories (cf. intuitionistic linear logic-as-linear dependent type theory, considered as sequent calculus together with a notion of proof-object, from the point of view of finitary algebraic presentation. These proposals provide an analysis of the notion of a framework and access to a general notion of Model Theory. One of our (long term) aims is to provide theorems such as: general conditions for the presence of cut-elimination (cf. early work of Kelly), natural deduction systems, connection (matrix) calculi, etc.. Related work: P. Schroeder–Heister; P. Aczel; E. Moggi; J. Power; C. Wells; E. Ritter; D. Rydeheard.

Jan Smith An interpretation of Kleene’s slash in type theory

Abstract

Kleene introduced the notion of slash to investigate the disjunction and existence properties under implication for intuitionistic arithmetic. In this talk an interpretation of Kleene’s slash to type theory is presented. Besides translations of Kleene’s results, the main application of the slash in type theory is that conditions are given for a typeable term, containing free variables, to have a normal form beginning with a constructor.

Nora Szasz A Machine checked proof that Ackermann’s function is not primitive recursive

Abstract

A completely machine checked proof of Ackermann’s result on the growth of primitive recursive functions is presented. The proof is written in an implementation of Martin-Löf’s set theory in ALF. The ALF system was used to carry out the editing and checking of the proof.

List of Participants

Gothenburg & Stockholm

Lennart Augustsson  augustss@cs.chalmers.se
Thierry Coquand  coquand@cs.chalmers.se
Veronica Gaspes  vero@cs.chalmers.se
Clas Lofwall  clas@sics.se
Lena Magnusson  lena@cs.chalmers.se

Per Martin-Löf

Bengt Nordstrom  bengt@cs.chalmers.se
Kent Petersson  kentp@cs.chalmers.se
Herbert Sander  herbert@cs.chalmers.se
Jan Smith  smith@cs.chalmers.se
Nora Szasz  nora@cs.chalmers.se
Alvaro Tasistro  tato@cs.chalmers.se
Karlis Tcherans  karlis@cs.chalmers.se

Paris 7

Gilles Amiot  amiot@frmap711.bitnet
Vincent Danos  danos@frmap711.bitnet
Jean-Louis Krivine  krivine@frmap711.bitnet

Thierry Lacoste

Pascale Manoury  eleph@frmap711.bitnet

Patrick Meche

Michel Parigot  pelz@lri.lri.fr
Christophe Raffalli  raffalli@frmap711.bitnet

Paul Roziere INRIA Roquencourt

Gilles Dowek  dowek@margaux.inria.fr
Hugo Herbelin  herbelin@margaux.inria.fr
Gerard Huet  huet@margaux.inria.fr
Yves Lafont  lafont@dmi.ens.fr
Christine Mohring  cpaulin@lip.ens-lyon.fr
Amy Felty  felty@margaux.inria.fr
Benjamin Werner  werner@margaux.inria.fr

INRIA Sophia-Antipolis

Yves Bertot  bertot@mirsa.inria.fr
Thierry Despeyroux  td@mirsa.inria.fr
Gilles Kahn  kahn@mirsa.inria.fr
Laurent Thery  thery@mirsa.inria.fr

Edinburgh

Thorsten Altenkirch  alti@dcs.ed.ac.uk

Paul Anderson  paul@dcs.ed.ac.uk
David Basin  basin@aipna.ed.ac.uk
Gianluigi Bellin  glb@dcs.ed.ac.uk
Alan Bundy  bundy@aipna.ed.ac.uk
Rod Burstall  rb@dcs.ed.ac.uk

Pietro Cenciarelli  pic@dcs.ed.ac.uk

George Cleland  glc@dcs.ed.ac.uk
Philippa Gardner  pag@dcs.ed.ac.uk
Hilf Goguen  hhg@dcs.ed.ac.uk
Claudio Hermida  ch@dcs.ed.ac.uk
Claire Jones  ccmj@dcs.ed.ac.uk

Edmund Kazmierczak eka@dcs.ed.ac.uk

Monika Lekuse  mkl@dcs.ed.ac.uk
Zhaohui Luo  zl@dcs.ed.ac.uk
James McKinna  jhm@dcs.ed.ac.uk
Savi Maharaj  svm@dcs.ed.ac.uk
Sean Matthews  sean@aipna.ed.ac.uk
Robin Milner  rm@dcs.ed.ac.uk
Eugenio Moggi  em@dcs.ed.ac.uk
Colin Phillips  colinp@aipna.ed.ac.uk
Gordon Plotkin  gdp@dcs.ed.ac.uk
Randy Pollack  rap@dcs.ed.ac.uk
John Power  ajp@dcs.ed.ac.uk
David Pym  dpym@dcs.ed.ac.uk
Don Sannella  dts@dcs.ed.ac.uk
Alex Simpson  als@dcs.ed.ac.uk
Alan Smaill  smaill@dcs.ed.ac.uk

Torino

Franco Barbanera  barba@di.unito.it
Stefano Berardi  stephano@di.unito.it
Mario Coppo  coppo@di.unito.it

Manchester

Peter Aczel  petera@cs.man.ac.uk

Gilles Barthe

Christian Jelstrup  jelstrup@cs.man.ac.uk
Nax Mendler  mendler@cs.man.ac.uk
David Rydeheard  david@cs.man.ac.uk
Harold Simmons  hsimmons@cs.man.ac.uk

Cambridge

Martin Coen  Martin.Coen@cl.cam.ac.uk
Tom Melham  Tom.Melham@cl.cam.ac.uk
Toby Nipkow  tnn@cl.cam.ac.uk
Larry Paulson  Larry.Paulson@cl.cam.ac.uk

Oxford

Razvan Diaconescu  Razvan.Diaconescu@prg.ox.ac.uk
Joseph Goguen  goguen@prg.ox.ac.uk
Lincoln Wallen  Lincoln.Wallen@prg.ox.ac.uk
David Wolfram  David.Wolfram@prg.ox.ac.uk

Cornell

Robert Constable  rc@gvax.cs.cornell.edu
Chet Murthy  murthy@cs.cornell.edu
Anil Nerode  nerode@msiadmin.cit.cornell.edu

Tel Aviv University

Arnon Avron  aa@math.tau.ac.il

Einhoven

De Bruijn  wsdwnb@win.tue.nl

St. Andrews

Roy Dyckhoff  rd@cs.st-and.ac.uk

CMU

Bob Harper  rwh@cs.cmu.edu

Philips

Leen Helmink  helmink@prl.philips.nl

Udine

Furio Honsell  HONSELL@uduniv.cineca.it

EC Hussla

Nijmegen

Hermann Geuvers  herman@cs.kun.nl

Eindhoven/Nijmegen Bentham Jutting

RHBNC/LFCS

Ursula Martin  uhm@cs.rhbnc.ac.uk

U. Penn/LFCS

Dale Miller  dale@linc.cis.upenn.edu

Harvard/INRIA

Gabriel Stolzenberg  gabe@zariski.harvard.edu

Liege University

Pierre Wolper  pw@montefiore.ulg.ac.be

24

Witness Extraction in Classical Logic through Normalization

Franco Barbanera Stefano Berardi^{∗} Dipartimento di Informatica Corso Svizzera, 185 10149 Torino (Italy)

June 1991

Abstract

We show how the strong normalization property for reductions on proofs in classical higher order systems can be used to extract witnesses from proofs of existentially quantified formulas.

1 Introduction

It is an old and well known result that the set of ∑_{1}^{0} sentences (and hence, by leaving a free variable, even the one of ∏_{2}^{0} sentences) provable in classical logic coincide with that of the sentences provable in intuitionistic logic. The proof of this fact was given by Kreisel in [6]. Later Friedman in [3] showed that Kreisel’s difficult proof, which involves functional interpretation, could be condensed down to a simple syntactic argument, his A- translation. By means of this translation one manage to obtain an intuitionistic proof of a ∑_{1}^{0} (and then even of a ∏_{2}^{0}) formula out of a classical proof of the same formula. It is then possible to extract constructive content from classical proofs (if the formulas proved are of the kind above specified) by using the usual extraction algorithms for intuitionistic logic after having performed Friedman’s translation.

Recently efforts have been made in order to develop methods to extract directly the constructive content from classical proofs. Murthy [7], by building on the work of Griffin [5] and Plotkin [8], has managed to give a consistent algorithmic interpretation to the rule of double negation, the classical axiom, in much the same manner as the other rules of logic are given algorithmic interpretations by constructive realizability. This algorithmic interpretation turns out to be Fellaisen’s non-local operator C [2], a relative of call/cc (call with current continuation) from Scheme [1]. Then by Murthy’s result one can employ classical logic as a formal system to deal with non-functional programs using C.

The present paper aims at being a contribution in the direction of developing methods to extract directly, without passing trough translations like Friedman’s one, the constructive content from classical proofs of ∑_{1}^{0} (and ∏_{2}^{0}) formulas. Our method build’s on results of Prawitz which we reformulate and slightly improve. In [9] Prawitz defined reduction rules for natural deduction systems of first order classical and intuitionistic logic and for such reductions gave normalization results. Similar reductions, together with a strong normalization result, were given by him in [10] even for second order classical and intuitionistic logic. He used the strong normalizazion result in order to infer consistency properties for various logics.

∗barba,stefano@di.unito.it

What we show in the present paper is that Prawitz reductions (and the strong normalization for them) can be used for an unespected purpose, i.e. to extract witnesses from classical proofs of existential formulas. The logical system we consider are stronger than the ones considered by Prawitz : we consider all the possible extensions of higher order classical logic by means of atomic rules, i.e. the extensions of higher order classical logic by means of Post Systems. A particular attention will be given to that particular extension corresponding to higher order Peano Arithmetic (P A^{ω}).

Our strong normalization result can be viewed as strengthening Prawitz’s one because one of the reduction rules we consider is more general that Prawitz’s corresponding one, and its application is not postponed until all the other rules are no more applicable as Prawitz did.

Our method of witness extraction works in the following way. If we have a system obtained by adding a Post system to higher order classical logic and in it have a proof of an existentially quantified atomic proposition (recall that for the case of P A^{ω} each (unary) predicate can be reduced to an atomic proposition of the form f(x) = 0), what we do is adding a new rule to the Post system corresponding to the negation of the existentially quantified atomic proposition. It is then possible to obtain a proof of ⊥ which we put in normal form using the strong normalization result. From a lemma we give about the shape of normal forms we get that the normal form of the so obtained proof of ⊥ has necessarily to be formed only by rules of the Post system, and then it is easily to get from it the term witnessing the existential formula.

It is worth to point out that this method of witness extraction would work even if we used as reduction rules the ones defined by Statman. Statman’s rules would improve the method of extraction from an efficiency point of view and then could be considered in case of an implementation of it.

It is worth to point out that the method of extracting a witness we choosed has a nice and simple interpretation in terms of Kripke semantics and partial valuations. This interpretation is the subject of a forthcoming paper.

Section 2 will consist in a presentation of Post Systems. In Section 3 it will be given a presentation of higher order classical logic extended with Post systems. We shall define, in Section 4, a set of reduction rules on proofs in such higher order systems, and present a strong normalization result, whose proof will be given in the appendix. Section 5 will be devoted to the use of the strong normalization result for extracting witnesses from proofs of existential formulas.

2 Post Systems

In this section we introduce a notion of formal system without logical symbols, but dealing only with atomic propositions and entailment relations among them. Such systems are known as Post Systems. A particular Post system will be the core of the complex systems for classical logic we shall introduce later.

Let us assume to have a countable set of term variables { x_{0}, x_{1}, x_{2}, … } and let F be a set of function symbols, each with its own arity n ≥ 0 . The set of terms over F is the free algebra built out of the term variables, using F as set of constructors. Then a term is either a variable or an expression of the form ft_{1} … t_{n} where f ∈ F , f has arity n and t_{1}, …, t_{n} are terms.

In the following terms will be denoted by t, u, v, …

Let now P be a set of predicate symbols, each with its own arity n ≥ 0. The Propositions in the language of F and P are expressions of the form p(t_{1} … t_{n}), with p ∈ P, p of arity n and t_{1}, …, t_{n} terms over F.

Given a set F of function symbols and a set P of predicate symbols, an Atomic Rule in the language of F and P is a pair

< x, A >

where A = A_{1}, …, A_{n+1} is a list of n + 1 propositions of F and P and x = x_{1}, …, x_{m} is the list of all the variables in A_{1}, …, A_{n}.

Definition 2.1 A Post System is a triple

< F, P, Σ >

where F is a set of function symbols, P is a set of predicate symbols and Σ is a set of atomic rules in the language of F and P.

In the following we shall denote a Post system < F, P, Σ > simply by Σ. Atomic rules will be denoted by r, s, … In literature atomic rules are sometimes referred to as Post Productions or Horn Clauses.

Let r =< x, A > with A = A_{1}[x], …, A_{n}[x], A_{n+1}[x] and x = x_{1}, …, x_{m}. The intuitive meaning of r is the following : for every list t = t_{1}, …, t_{m},

if A_{1}[t], …, A_{n}[t] then A_{n+1}[t]

We introduce now the notion of Atomic Proof. For each atomic proposition A we have a countable set of proof variables of type A : {x_{0}^{A}, x_{1}^{A}, x_{2}^{A}, …}.

Definition 2.2 Let Σ be a Post system. We say that π is an atomic proof for the atomic proposition A, denoted by π : A, if we can infer π : A using the following rules :

x^{A} : A \frac{π_{1} : A_{1}[t] … π_{n} : A_{n}[t]}{r(t, π_{1}, …, π_{n}) : A_{n+1}[t]}

where x^{A} is any proof variable of type A and r =< x, A >, with A = A_{1}, …, A_{n+1}, is any element of Σ.

We shall denote by

x_{1}^{A_{1}} : A_{1}, …, x_{n}^{A_{n}} : A_{n} ⊢_{Σ} π : A

the fact that π is a proof of A in Σ with free variables all in the set { x_{1}^{A_{1}}, …, x_{n}^{A_{n}}} .

We sometimes shall use the notation π^{A} instead of π : A. We shall write

A_{1}, …, A_{n} ⊢_{Σ} A

(to be read A_{1}, …, A_{n} entail A in Σ ) if there exists a π such that

x_{1}^{A_{1}} : A_{1}, …, x_{n}^{A_{n}} : A_{n} ⊢_{Σ} π : A

When n = 0 we shall also write

Σ ⊢ A

(to be read ”A is a theorem in Σ”).

2.1 An Example of Post System

We introduce now a particular Post system which will play a central role in the following.

Definition 2.3 We define the Post system < F_{0}, P_{0}, Σ_{0} > in the following way :

F_{0} = a set of function symbols, one for each primitive recursive function.
P_{0} = {⊥, =} with ⊥ of arity 0 and = of arity 2.
Σ_{0} = one rule for each equation defining a primitive recursive function together with

the following rules:

<< x >, < 0 = s(x), ⊥ >>

<< x, y >, < s(x) = s(y), x = y >>

<< x >, < x = x >>

<< x, x, y >, < x = y, A[x], A[y] >> for each proposition A of F_{0} and P_{0} .

Then the Post system < F_{0}, P_{0}, Σ_{0} > is a Post system concerning arithmetic of primitive recursive functions. The rules of Σ_{0} characterize the primitive recursive functions and state that 0 is not a successor and that the successor function is injective. The last two rules characterize the equality between integers.

3 A Notion of Higher Order Classical System

As already mentioned, we wish to deal with the problem of ”witness extraction” not only for higher order arithmetic, but for all the systems extending classical higher order logic with a set of rules which can be described by means of a Post system. Given a Post system Σ containing at least a 0-ary predicate ⊥(like Σ_{0} of the previous section) we extend it to an higher order classical system. Such system is no more than a particular way of presenting the system of higher order classical logic enriched with the rules represented in Σ . We represent proofs as λ-terms (thus in linear form) because in such a way they are easier to ”handle”.

Let then Σ be any Post system containing a 0-ary predicate symbol ⊥. We define in what follows a notion of Higher Order Classical System C _{Σ} which extends Σ.

The expressions of the system C_{Σ} are of four kinds: types, predicates, terms and proofs. In the system we have two constants : ι (the type of terms of Σ) and Prop (the type of propositions of C_{Σ}).

The types T of C_{Σ} and a subset of them : the types of predicates of C_{Σ} (T_{P}) are defined by the following productions:

T ::= ι|T_{P}
T_{P} ::= Prop|T → T_{P}

We shall use T,U,… to denote types. For each type T of C_{Σ} We assume to have an infinite number of variables x_{0}^{T} , x_{1}^{T} , … of type T for each type T of C_{Σ} .

The terms of C_{Σ} are the terms of Σ.

Let At be any proposition of Σ, t a term and T, U types.

The predicates P T of type T of C_{Σ} is inductively defined in the following way :

AtProp  x^{T}
(¬P Prop)Prop  (P Prop ∧ P Prop)Prop
(∀x^{T} .P Prop)Prop  (λx^{T} .P^{U})^{T →U}
(P^{T →U}P^{T})^{U}  (P^{ι→T} t)^{T}

The propositions of C_{Σ} are the predicates of type Prop.

From now on we shall consider only predicates that are in βη-normal form, i.e. predicates that contain no subterm of the shape (λx^{T} .P)E^{T} or λx^{T} .P x^{T} with x^{T} not free in P. Normal forms may be obtained through a normalization process, whose convergence to a unique normal form may be proved as in simply typed lambda-calculus. To restrict ourselves to normal predicates, if P is a predicate and E^{T} an expression (predicate or term) of type T, then P [x^{T} := E^{T}] will denote the normal form of the term obtained out of P by replacing x by E .

Let us define now the notion of proof of a proposition in C_{Σ} . As stated before, we shall consider only βη-normal propositions.

For each proposition A of C_{Σ} we have an infinite number of proof variables of type A. Let r =< x, A >∈ Σ and E^{T} be any expression of type T. We say that p is a proof for the proposition A, denoted by p : A, if we can infer p : A using the following rules :

\begin{matrix}x^{A} : A & \frac{p_{1} : A_{1}[t] … p_{n} : A_{n}[t]}{r(t, p_{1}, …, p_{n}) : A_{n+1}[t]} \\ [x^{A} : A] & [x^{¬A} : ¬A] \\ ⋮ & ⋮ \\ \frac{p : ⊥}{λx : A.p : ¬A} & \frac{p : ⊥}{N x : ¬A.p : A} \\ \frac{p_{1} : ¬A p_{2} : A}{(p_{1}p_{2}) : ⊥} & \frac{p : A_{1} ∧ A_{2}}{π_{i}(p) : A_{i}} \\ \frac{p : A}{λx : T.p : ∀x^{T} .A}(∗) & \frac{p : ∀x^{T} .A}{(pE^{T}) : A[x := E]} \end{matrix}

(*) x not free in B for any proof variable x^{B} free in p.

Let us informally summarize the main features of C_{Σ}. The types of C_{Σ} are built out of the constants ι and Prop using the arrow (→ ). We have forbidden, for sake of simplicity, types where ι occurs on the righthand side of →, like ι → ι, Prop → ι,. . .. Type of predicates are those of the form T_{1} → … → T_{n} →Prop, i.e. they are classes of predicates with arguments in T_{1} … T_{n}. The only other type is the type ι of terms of Σ.

The propositions of C_{Σ} are either atomic propositions of Σ, or negation or conjunction of propositions, or universal quantifications over objects, or expressions of the shape P (E_{1}, …, E_{n}) where P is a predicate. Predicates are either propositions or variables or λ-abstractions or applications. Predicates should be identified up to βη-conversion. We did it by considering only βη-normal predicates.

The rules of the system are the rules of Σ, introduction and elimination rules for ¬, ∧, ∀ and double negation.

We shall denote by

x_{1}^{A_{1}} : A_{1}, …, x_{n}^{A_{n}} : A_{n} ⊢_{C_{Σ}} p : A

the fact that p is a proof of A in C_{Σ} with free variables all in the list x_{1}^{A_{1}}, …, x_{n}^{A_{n}}.

We sometimes shall use the notation p^{A} instead of p : A. We shall write

A_{1}, …, A_{n} ⊢_{C_{Σ}} A

(to be read A_{1}, …, A_{n} entail A in C_{Σ}), if there exists a p for which

x_{1}^{A_{1}} : A_{1}, …, x_{n}^{A_{n}} : A_{n} ⊢_{C_{Σ}} p : A

When n = 0 we shall also write

C_{Σ} ⊢ A

(to be read A is a theorem in C_{Σ}).

3.1 An Example of Classical System : Higher Order Peano Arithmetic

In this subsection we show that Higher Order Peano Arithmetic (P A^{ω}) can be presented as a classical higher order system.

Let Σ_{0} be the Post system defined in the previous section. If we consider the classical system C_{Σ_{0}}, in it we have the language of arithmetic, atomic axioms expressing basic facts about integers and higher order classical logic. To show that C_{Σ_{0}} is exactly P A^{ω} it is enough to explain how to express the induction rule in the former.

Before doing it a few definitions are necessary, i.e. how to encode natural numbers and the logical connectives → and ∃.

A → B  =_{def} ¬(A ∧ ¬B)
N  =_{def} λn : ι.∀X : ι → Prop.X(0) → (∀x : ι.X(x) → X(s(x))) → X(n)
∀x ∈ N.A =_{def} ∀x : ι.N(x) → A
∃x ∈ N.A =_{def} ∃x : ι.N(x) ∧ A

Let P be a predicate of type ι →Prop in P A^{ω}. We can express the induction rule on P in the following way:

Ind[P] =_{def} ∀x ∈ N.P [0] → (∀y ∈ N.P [y] → P [s(0)]) → P [x]

Lemma 3.1 C_{Σ_{0}} ⊢ ∀X : ι → Prop.Ind[X].

Proof. Left to the reader. It is useful to check first that A, A → B ⊢_{C_{Σ_{0}}} B, C_{Σ_{0}} ⊢ N(0) and C_{Σ_{0}} ⊢ ∀x : ι.N(x) → N(s(x)).□

We have thus shown that C_{Σ_{0}} is indeed P A^{ω}.

4 Strong Normalization for Classical Proofs

In this section we introduce a set of reduction rules on proofs in classical systems. These rules are the usual Prawitz’s reduction rules for intuitionistic logic and four reduction rules dealing with double negation [9,10]. For these rules we shall give a result of strong normalization. In the next section we shall show that such a result, besides implying consistency result, provides also a mean to extract witnesses from existential proofs.

The reduction rules for intuitionistic logic transform a proof by eliminating consecutive applications of introduction and elimination rules for the same connective.

Definition 4.1 The reduction rules for intuitionistic logic are the following :

¬-int) (λx^{A}.p^{⊥})^{¬A}(q^{A})  →  p^{⊥}[x := q^{A}]
∧-int) π_{i} < p_{1}^{A_{1}}, p_{2}^{A_{2}} >  →  p_{i}^{A_{i}}
∀-int) (λx^{T} .p^{A})^{∀x^{T} .A}(E^{T})  →  p^{A}[x^{T} := E^{T}]

In order to define the reduction rules dealing with double negation, we have first to introduce standard proofs of

A ⊢_{C_{Σ}} ¬¬A  ¬A_{i} ⊢_{C_{Σ}} ¬(A_{1} ∧ A_{2})  ¬A[E] ⊢_{C_{Σ}} ¬∀x^{T} .A

Let p^{¬A}, p^{¬A_{i}}, p^{¬A[E]} be proofs, and x, y, z, c fresh variables.

σ[p^{A}] =_{def} (λy^{¬A}.(y^{¬A}p^{A})^{⊥})^{¬¬A}
σ_{i}[p^{¬A_{i}}] =_{def} (λz^{A_{1}∧A_{2}}.(p^{¬A_{i}}π_{i}(z)^{A_{i}})^{⊥})^{¬(A_{1}∧A_{2})}
σ_{E}[p^{¬A_{E}}] =_{def} (λc^{∀x.A}.(p^{¬A_{E}}c^{∀x.A}(E)^{A_{E}})^{⊥})^{¬∀x.A}

We may now define the reduction rules dealing with double negation. These rules transform a proof in order to have applications of the rule of double negation performed on simpler and simpler formulas. If a proof is normal with respect these reductions then double negation is applied only on atomic formulas.

Definition 4.2 The reduction rules for application of double reduction rules are the following:

¬-class (N x^{¬¬A}.p[x]^{⊥})^{¬A} → (λx^{A}.p[σ[x]]^{⊥})^{¬A}

∧-class (N x^{¬(A_{1}∧A_{2}}.p[x]^{⊥})^{A_{1}∧A2} → < q_{1}^{A_{1}}, q_{2}^{A_{2}} >^{A_{1}∧A_{2}} with q_{i}^{A_{i}} = (N x^{¬A_{i}}.p[σ_{i}[x]]^{⊥})^{A_{i}}

∀-class (N x^{¬∀y^{T} .A}.p[x]^{⊥})^{∀y^{T} .A} →  (λy^{T} .q^{A})^{∀y^{T} .A}  with q^{A} = (N x^{¬A}.p[σ_{y}[x]]^{⊥})^{A}

At-class p^{At}[q^{At}] → q^{At} where At is any atomic proposition of Σ and p^{At}[q^{At}] is a proof of At containing a proper subproof q of At such that FV(q) ⊆ FV(p).

In order to clarify the sort of transformation performed by the rules for double negation given above we give also their version in natural deduction.

[¬A]  [A]
\overline{⊥}
[¬¬A]  \overline{¬¬A}
⋮  ⋮
⊥  ⇝  ⊥
\overline{¬A}  \overline{¬A}

\underline{[A_{1} ∧ A_{2}]}  \underline{[A_{1} ∧ A_{2}]}
\underline{[¬A_{1}] A_{1}} \underline{[¬A_{2}] A_{2}}
⊥  ⊥
\overline{¬A_{1} ∧ A_{2}}  \overline{¬A_{1} ∧ A_{2}}
[ ¬A_{1} ∧ A_{2} ]  ·  ·
·  ·  ·
·  ⊥  ⊥
⊥  ⇝  \overline{A_{1}}  \overline{A_{2}}
\overline{A_{1} ∧ A_{2}}  \overline{A_{1} ∧ A_{2}}

\underline{[∀x.A[x]]}

[¬A[y]]  A[x]

(\overline{⊥}) / (\overline{¬∀x.A[x]})

[¬∀x.A[x]]  ⋮
⋮  ⊥
⊥ ⇝ \overline{A[y]}
\overline{∀x.A[x]}  \overline{∀y.A[y]}

The reduction (At-class) is more general of the similar one considered by Prawitz [10]. Given the reduction rules we can now define the reduction relations among proofs induced by them.

Definition 4.3 Given two proofs p and q we have that p ⟶ q if q is obtained by replacing one redex in p by its contractum. ⟶^{∗} is the reflexive and transitive closure of ⟶

The reduction relation ⟶^{∗} has several familiar properties. For instance :

Lemma 4.1 (i) If x : A ⊢ p : A and p ⟶^{∗} p′, then x : A ⊢ p′ : A (Subject Reduction property). (ii) If p[x] ⟶^{∗} q[x] and E is a list of expressions having the same types as x, then p[E] ⟶^{∗} q[E] .

Proof Left to the reader. Essentially the lemma holds because the classes of the propositions starting with ¬, ∧, ∀ and of the propositions of Σ are all closed by substitution. □

The reduction relation ⟶^{∗} defined above is clearly not confluent because of the presence of the rule At-class). Therefore a proof can have several different normal forms. What we shall prove however is that ⟶^{∗} is strongly normalizing.

Theorem 4.1 The reduction relation ⟶^{∗} is strongly normalizing, i.e. for any proof p there always exists a finite bound n to the length of any reduction path p ⟶^{∗} p_{1} ⟶^{∗} p_{2} ⟶^{∗} . . ..

The proof of this theorem will be given in the Appendix.

It is worth noting that this result of strong normalization is stronger than the one proved by Prawitz [9,10], since he considered only a particular case of our rule At-class) and since in [10] the reductions on atomic proofs can be performed only at the very end of the reduction path, when no other reduction is possible. Our strong normalization result then holds even when these restrictions are taken out.

5 Witness Extraction in Classical Logic

In this section we show that the strong normalization for the reductions on proofs has an unexpected use:

if P A^{ω} ⊢ p : ∃x ∈ N.P [x] and P is a decidable predicate, then it is possible to extract in an effective way from p an integer n such that P A^{ω} ⊢ P [n].

Indeed it is possible to have something stronger, i.e. if we have C_{Σ} ⊢ ∃x.At[x] (with At proposition of Σ) then it is possible to find in an effective way a term t such that C_{Σ} ⊢ At[t]. We shall consider for the witness extraction the case of P A^{ω} for its interest. The generalization for the case of any C_{Σ} is straightforward.

The restriction about P (i.e. P is a decidable predicate) given for the case P A^{ω} is useful because, if we consider predicates where the only predicate symbol is ”=” (which is decidable), we can always put them in the form f(x) = 0.

Let Σ be any Post system containing at least a 0-ary predicate symbol ⊥. We shall first prove a technical lemma about normal proofs in C_{Σ} and then we use it to derive Prawitz’s equiconsistency result for Σ and C_{Σ}. We then explain how such result can be used to extract a witness from a proof.

Lemma 5.1 Let p be a normal proof in C_{Σ} and At = At_{1}, …, At_{n} be any sequence of propositions of Σ (¬At denotes ¬At_{1}, …, ¬At_{n}). Then

(i) If A is not atomic and x : At ⊢_{C_{Σ}} p : A then p is x_{i}^{¬At_{i}} for some i or p ends with an introduction. (ii) If At is any proposition of Σ and x : At ⊢_{C_{Σ}} p : At then p contains only rules of Σ, double negations on propositions of Σ or expressions of the form x^{¬B}q^{B} with x free or bound and B atomic. (iii) If C_{Σ} ⊢ p : ⊥ then Σ ⊢ p : ⊥.

Proof. (i) By induction on the structure of p, distinguishing the various cases according to the outermost symbol of p (the last rule used to form p in Natural Deduction style).

• If p is a variable we have finished.

• p cannot be r(t, p_{1}, …, p_{n}) because A is not atomic.

• If p ends with an introduction we have finished.

• If p ends with an elimination then p is either (q_{1}^{¬A}q_{2}^{A})^{⊥} or (π_{i}q^{A_{1}∧A_{2}})^{A_{i}} or (q^{∀x.A}E)^{A[E]}. The first subcase leads to a contradiction, since A is not atomic and cannot be ⊥. In the remaining subcases we have to note that q^{A_{1}∧A_{2}} and q^{∀x.A} cannot be variables because in such a case they would be x^{¬At_{i}} for some i and A_{1} ∧ A_{2} and ∀x.A ≠ ¬At_{i}. Then we can apply the induction hypothesis on q^{A_{1}∧A_{2}} and q^{∀x.A} obtaining that q^{A_{1}∧A_{2}} ≡< q_{1}^{A_{1}}, q_{2}^{A_{2}} > and q^{∀x.A} ≡ λx.q_{1}^{A}. This forces p not to be normal, contradiction.

• If p is (N x^{¬A}.q^{⊥})^{A} then, since A is not atomic, p would not be normal.

(ii) By induction on the structure of p.

• p cannot be a variable because it is a proof of At and the variables are x_{1}^{¬A_{1}}, …, x_{n}^{¬A_{n}}.

• If p is r(t, p_{1}, …, p_{n}) we have finished by induction hypothesis on p_{1}, …, p_{n}.

• p cannot end with an introduction since otherwise At would be a composite formula.

• If p ends with an elimination then p is either (q_{1}^{¬A}q_{2}^{A})^{⊥} or (π_{i}q^{A_{1}∧A_{2}})^{A_{i}} or (q^{∀x.A}E)^{A[x:=E]}. By applying (i) to q_{1}^{¬A}, q^{A_{1}∧A_{2}} and q^{∀x.A} we have that such proofs are either x_{i}^{¬A_{i}} for some i or they end with an introduction. The first subcase can apply only to q_{1}^{¬A}. From q_{1}^{¬A} ≡ x_{i}^{¬At_{i}} we deduce that p ≡ (x_{i}^{¬At_{i}}q_{2}^{A})^{⊥} and then the thesis follows by the induction hypothesis on q_{2}^{A}. In the second subcase we would have q^{¬A} ≡ λx^{A}.q^{′⊥}, q^{A_{1}∧A_{2}} ≡< q_{1}^{A_{1}}, q_{2}^{A_{2}}. and q^{∀x.A} ≡ λx.q^{′A} and then p would not be normal, contradiction.

• If p is (N x^{¬At}.q^{⊥})^{At} we have that x : ¬At, x : ¬At ⊢_{C_{Σ}} q^{⊥} : ⊥ and then we have finished by the induction hypothesis on q^{⊥}.

(iii) Let us assume that C_{Σ} ⊢ p : ⊥. We want to prove Σ ⊢ p : ⊥, i.e. that p consists only of rules of Σ. By (ii) p consists only of rules of Σ, double negations on atomic propositions and of expressions of the form x^{¬B}q^{B}. Let us assume, by contradiction, that there is some subterm of p of the form (N x^{¬B}q^{⊥})^{B} or x^{¬B}q^{B} for some B of Σ. In the first case we distinguish two subcases:

1. for some N x.q in p we have x ∈ F V (q)

2. for all N x.q in p we have x ∉ F V (q).

In subcase 1, let (N x^{¬B}.q^{⊥})^{B} be a subproof of p minimal among the subproofs N x′.q′ such that x′ ∈ F V (q′). Thus for each N x′.q′ inside q we have x′ ∉ F V (q′). By (ii) each occurrence of x^{¬B} in q^{⊥} is in some expression of the form (x^{¬B}q^{′′B})^{⊥}. Let us choose now a minimal (x^{¬B}q^{′′B})^{⊥} in q^{⊥}. Then x^{¬B} ∉ F V (q^{′′B}). Hence F V (q^{′′B}) ⊆ F V (N x.q) ∪ { variables bound by some N in q }. Since for each N x′.q′ occurring in q we have x′ ∉ F V (q′), we deduce that F V (q^{′′B}) ⊆ F V (N x.q). This contradicts the fact that p is normal, because (N x.q)^{B} ⟶ q^{′′B}. In subcase 2, for all (N x^{¬B}.q^{⊥})^{B} occurring in p^{⊥} we have that x^{¬B} ∉ q^{⊥}. Thus no variable, free or bound , occurs in p. Therefore F V (q) = F V (p) = ∅ and then p^{⊥} ⟶ q^{⊥}, contradicting the fact that p is normal. There is still left to derive a contradiction in the second case, when some (x^{¬B}q^{B})^{⊥} occurs in p^{⊥}. Since F V (p^{⊥}) = ∅, x^{¬B} must be bound by some (N x^{¬B}.q^{⊥})^{B} in p. Thus we are in the first case and have finished. □

From point (iii) of the Lemma above and from the strong normalization Theorem it is easy to derive Prawitz’s equiconsistency result.

Theorem 5.1 (Prawitz) For any Post system containing ⊥ :

Σ ⊢ ⊥ ⇔ C_{Σ} ⊢ ⊥.

Proof. If Σ ⊢ p : ⊥ then C_{Σ} ⊢ p : ⊥ because Σ is a subsystem of C_{Σ}. If C_{Σ} ⊢ p : ⊥ then, by the strong normalization Theorem, there exists a normal form p′ of p. Hence C_{Σ} ⊢ p′ : ⊥ and then, by point (iii) of the previous lemma, Σ ⊢ p′ : ⊥.□

Prawitz used this result to infer the consistency of P A^{ω}(P A^{ω} ⊬ ⊥) from the consistency of Σ_{0}, which it is easy to prove. We show now how Prawitz’s result can have a computational use.

Let us assume to have

P A^{ω} ⊢ p : ∃x ∈ N.(f(x) = 0).

By ”expanding” the abbreviations used we have then

P A^{ω} ⊢ p : ¬∀x : ι.¬(N(x) ∧ (f(x) = 0))

Let now

r =<< x >, < (f(x) = 0), ⊥ >>

be a fresh atomic rule. In natural deduction style this rule would have the following shape :

r)\frac{f(x) = 0}{⊥}.

The central remark is now that P A^{ω} + r ⊢ ⊥. In fact, if we put

q =_{def} (λx^{N(x)∧(f(x)=0)}.r(π_{2}(x)^{(f(x)=0)})^{⊥}

then

P A^{ω} + r ⊢ λx.q : ∀x.¬(N(x) ∧ (f(x) = 0))

We can then obtain

P A^{ω} + r ⊢ p(λx.q) : ⊥.

Put in natural deduction style the proof p(λx.q) has the following shape:

\underline{[N(x) ∧ (f(x) = 0)]}

(\underline{f(x) = 0}) / ⊥

⋮  \overline{¬(N(x) ∧ (f(x) = 0))}
\underline{¬∀x.¬(N(x) ∧ (f(x) = 0))}  \underline{\overline{∀x.¬(N(x) ∧ (f(x) = 0))}}
\overline{⊥}

By the proof of Prawitz’s equiconsistency result, if p′ is any normal form of p(λx.q), we have that

Σ_{0} + r ⊢ p′ : ⊥.

No proper subterm of type ⊥ can occur in p′ because p′ is in normal form. On the other hand r may occur in p′ only in subproofs of the form r(t, q′) having type ⊥. Moreover r must occur in p′ since Σ_{0} ⊬ ⊥. Thus p′ itself is of the form r(t, q′) for some term t of Σ_{0} and r does not occur in q′. The subproof q′ must have the type (f(t)=0). Since r does not occur in q′ we have

Σ_{0} ⊢ q′ : (f(t) = 0)

Then it is easy to generate, by means of a normalization process, from a proof in higher order Peano arithmetic of ∃x ∈ N.f(x) = 0, a term t such that f(t) = 0.

It is worth noting that because of the presence of the rule (At-class) (and hence of the non-confluence of the reductions) it is possible to get different witnesses by following different reduction strategies. This is not possible in intuitionistic logic, where the witness that it is possible to ”extract” from a proof is unique.

6 Appendix : Strong Normalization for the Systems C_{Σ}

In this appendix we give the proof of the result claimed in section 4. i.e. that every proof p in a system C_{Σ} is strongly normalizing under the set of reduction rules defined.

Since the argument is quite complex, we shall split it in four subsections. In 6.1 we shall introduce, using Girard’s candidates [4], a Realization Semantic for the intuitionistic propositional part of C_{Σ} ; in 6.2 we shall extend such semantic to the classic propositional part of C_{Σ} ; this semantic will be further extended to the first and higher order part of C_{Σ} in 6.3. The strong normalization result will be proved in 6.4.

6.1 Realization Semantic for the Intuitionistic Propositional Fragment of C_{Σ}

In this subsection we introduce the notion of Girard’s candidate and prove that it can generate a Realization semantic for Σ, the connectives ¬, ∧ and the intuitionistic rules for them.

Let us firstly give two abbreviations to be used later. Let A be a proposition and p a proof in C_{Σ}.

n is a bound for p iff the reduction tree of p has a finite height ≤ n.

SN_{A} =_{def} {q|q is a proof of A for which there exists a bound }

We may now define Girard candidates.

Definition 6.1 Let A be a proposition and C a set of proofs. C is a Girard candidate for A if the following conditions are satisfied :

cand 1 C ⊆ SN_{A}

cand 2 If p ∈ C then for all proofs q,

(p ⟶ q) ⇒ q ∈ C

cand 3 If p ∈C, p does not start with an introduction symbol and for all proofs q of A we have that (p ⟶ q) ⇒ q ∈C, then p∈C.

If C is a candidate for A, then x^{A} ∈ C by (cand 3), just because x^{A} ⟶ q never holds. Let us introduce two more abbreviations.

GC =_{def} {C|C is a Girard candidate }

Let C be a candidate for A. Then

C^{∗} =_{def} A

C^{∗} is unique. If C is a candidate for A and B then by (cand 1) and (cand 3) we have that x^{A} ∈ C ⊆ SN_{B} and thus A = B.

We prove now that SN_{A} is a candidate, and that it is the only candidate for A if A is atomic.

Lemma 6.1 (i) SN_{A} ∈ GC. (ii) If C ∈ GC and C^{∗} = A with A atomic then C = SN_{A}.

Proof. (i) SN_{A} satisfies (cand 1) because SN_{A} ⊆ SN_{A}. It satisfies (cand 2) because if p ∈ SN_{A} and p ⟶ q then q ∈ SN_{A}. Suppose now that for all proofs q, p ⟶ q ⇒ q ∈ SN_{A}. There are only finitely many q’s such that p ⟶ q, say q_{1}, …, q_{m}. Let n_{i} be a bound for q_{i}, i = 1, …, m. Now max_{i}{n_{i} + 1} is a bound for p and hence p ∈ SN_{A}. Thus SN_{A} satisfies (cand 3). (ii) Let C ∈ GC and C^{∗} = A with A atomic. By (cand 1) we have only to prove that SN_{A} ⊆ C. Let then p ∈ SN_{A} and n be a bound for p. We prove p ∈ C by induction on n. Remark that p cannot begin with an introduction, otherwise A would be composite. Therefore, by (cond 3), it is enough to prove that for all proofs q, p ⟶ q ⇒ q ∈ C. If p ⟶ q then q has a bound n′ < n and , by the induction hypothesis on n′ we have that q ∈ C. □

Thus, if A is atomic, we may canonically interpret it by SN_{A}. We prove now that such ”interpretation” is sound with respect to the rules of Σ.

Lemma 6.2 Let r =< x, < A_{1}, …, A_{n+1} >>∈ Σ and C_{1}, …, C_{n+1} ∈ GC such that C_{i}^{∗} = A_{i}, i = 1, …, n + 1. Then

p_{1} ∈ C_{1}, …, p_{n} ∈ C_{n} ⇒ r(t, p_{1}, …, p_{n}) ∈ C_{n+1}

Proof. Let in this proof p be short for r(t, p_{1}, …, p_{n}) ∈ C_{n+1}. Since C_{i} ⊆ SN_{A_{i}}, p_{1}, …, p_{n} have bounds, say k_{1}, …, k_{n}. By induction on∑_{i=1}^{n} k_{i} we prove that p ∈ C_{n+1}. Since p begins with r, by (cand 3) it is enough to prove that p′ ∈ C for all p′ such that p ⟶ p′. A reduction on p can be performed either inside some p_{i} or can be (At-class), with p itself as redex. In the first case we deduce p′ ∈ C_{n+1} by induction on ∑_{i=1}^{n} k_{i} and the closure of C_{i} under ⟶. In the second case p′ is a subproof of some p_{j} and therefore p′ ∈ SN_{A_{n+1}}. By point (ii) of the previous lemma C_{n+1} = SN_{A_{n+1}}, thus p′ ∈ C_{n+1}.□

We interpret now the connectives ¬ and ∧ as operations on candidates. Let us give two more abbreviations.

C_{1}\underline{∧}C_{2} =_{def} \{p|p is a proof and π_{i}(p) ∈ C_{i}, i = 1, 2\}
\underline{¬}C =_{def} \{p|p is a proof and ∀a ∈ pa ∈ SN_{⊥}\}

By the consistency of the typing for π_{i}(p), pa, we deduce (C_{1}\underline{∧}C_{2})^{∗} ≡ C_{1}^{∗} ∧ C_{2}^{∗} and (\underline{¬}C)^{∗} ≡ ¬C^{∗}.

We check now that ∧ and ¬ indeed build new elements of GC.

Lemma 6.3 (i) \underline{∧} : GC → GC → GC (ii) \underline{¬} : GC → GC.

Proof. (i) Let C_{1}, C_{2} ∈ GC and C_{i}^{∗} = A_{i}, i = 1, 2. To prove (cand 1), if p ∈ C_{1}\underline{∧}C_{2} we have that π_{i}(p) ∈ C_{i} ⊆ SN_{A_{i}}. Thus p ∈ SN_{A_{1}∧A_{2}}. To prove (cand 2), let us suppose p ∈ C_{1}\underline{∧}C_{2} and p ⟶ q. Then π_{i}(p) ∈ C_{i} and π_{i}(p) ⟶ π_{i}(q). Thus π_{i}(q) ∈ C_{i} and therefore q ∈ C_{1}\underline{∧}C_{2}. To prove (cand 3), let us assume that p does not begin with an introduction and that for all proofs q, (p ⟶ q) ⇒ q ∈ C_{1}\underline{∧}C_{2}. First of all we remark that p ∈ SN_{A_{1}∧A_{2}}. This follows from (cand 3) for SN_{A_{1}∧A_{2}} and from the fact that for all proofs q, (p ⟶ q) ⇒ q ∈ C_{1}\underline{∧}C_{2} ⊆ SN_{A_{1}∧A_{2}}. Now we have to prove that π_{i}(p) ∈ C_{i}. Since π_{i}(p) begins with π_{i}, by (cand 3) it is enough to prove that, for all proofs q′, (π_{i}(p) ⟶ q′) ⇒ q′ ∈ C_{i}. Since p does not begins with a < −, − >, π_{i}(p) is not a π-redex. Thus q′ is either π_{i}(q) for some q such that p ⟶ q or it is a subproof of p and we applied a reduction (At-class) and A_{i} must be atomic. In the first case, since q ∈ C_{1}\underline{∧}C_{2} by hypothesis, we conclude that q′ ≡ π_{i}(q) ∈ C_{i}. In the second case q′ ∈ SN_{A_{i}} because p ∈ SN_{A_{1}∧A_{2}} and q′ is a subproof of p. Since A_{i} is atomic, by Lemma 6.1(ii) we have that C_{i} = SN_{A_{i}}. We then conclude q′ ∈ C_{i}. (ii) Let C ∈ GC and C^{∗} = A. To prove (cand 1) we remark that if p ∈ ¬C then, since x^{A} ∈ C, px^{A} ∈ SN_{⊥} and thus p ∈ SN_{⊥}. To prove (cand 2) we assume p ∈ ¬C and want to prove that, if p ⟶ p′, we have p′a ∈ SN_{⊥} for all a ∈ C. By definition of ¬C, pa ∈ SN_{⊥}. Since pa ⟶ p′a we conclude p′a ∈ SN_{⊥}. To prove (cand 3) we assume that p does not begin with an introduction and that, for all proofs p′, (p ⟶ p′) ⇒ p′ ∈ ¬C. Since a ∈ C ⊆ SN_{⊥}, we can proceed by induction on the bound n of a. We want to prove pa ∈ SN_{⊥} for all a ∈ C. First of all we remark that p ∈ SN_{¬A}. This follows by (cand 3) for SN_{¬A} and by the fact that, for all proofs q′, (p ⟶ p′ ⇒ p′ ∈ ¬C ⊆ SN_{¬A}. Since pa begins with an application, by (cand 3) for SN_{⊥} it is enough to prove that for all proofs b, (pa ⟶ b) ⇒ b ∈ SN_{⊥}. p does not begin with an abstraction, so pa is not a λ-redex. Thus the reduction can take place in p, a or can be (At-class). If p ⟶ p′, then by the induction hypothesis p′ ∈ ¬C and therefore p′a ∈ SN_{⊥}. If a ⟶ a′ then we have finished by the induction hypothesis and by the fact that a′ ∈ C (which follows by (cand 2). If we applied rule (At-class) then b is a subproof of either p or a. Since both p and a strongly normalize, then b ∈ SN_{⊥}. □

Thus candidates soundly interpret the formation of intuitionistic quantifier-free propositions. We prove now that they soundly interpret the intuitionistic rules for such propositions.

Lemma 6.4 Let C_{1}, C_{2}, C ∈ GC and C_{i}^{∗} = A_{i}, C^{∗} = A.

(i) p_{1} ∈ C_{1}, p_{2} ∈ C_{2} ⇒ < p_{1}, p_{2} >∈ C_{1} ∧ C_{2} (ii) p ∈ C_{1} ∧ C_{2} ⇒ π_{i}(p) ∈ C_{i}, i = 1, 2

(iii) ∀a ∈ C p[x := a]  ⇒  λx.p ∈ ¬C
(iv) p ∈ ¬C, a ∈ C  ⇒  pa ∈ SN_{⊥}

Proof. (i) We have to prove π_{i} < p_{1}, p_{2} >∈ C_{i}. Since C_{i} ⊆ SN_{A_{i}}, p_{1} and p_{2} have bounds, say n_{1} and n_{2}. Therefore we may proceed by induction on n_{1} + n_{2}. Since π_{i} < p_{1}, p_{2} > begins with π_{i}, by (cand 3) it is enough to prove that, for all proofs q, (π_{i} < p_{1}, p_{2} >⟶ q) ⇒ q ∈ C_{i}. If the reduction on π_{i} < p_{1}, p_{2} > takes place inside some p_{i}, then q ∈ C_{i} by the induction hypothesis and the closure of C_{i} under →. If π_{i} < p_{1}, p_{2} > itself is the redex being reduced, then either π_{i} < p_{1}, p_{2} >⟶ p_{i} or we apply a reduction (At-class) and A_{i} is a proposition of Σ and q is inside some p_{i}. In the first case p_{i} ∈ C_{i} by the hypothesis and then we have finished. In the second case q ∈ SN_{A_{i}} because p_{i} ∈ SN_{A_{i}}. By Lemma 6.1(ii), since A_{i} is atomic, we have C_{i} = SN_{A_{i}} and can conclude q ∈ C_{i}. (ii) If p ∈ C_{1}\underline{∧}C_{2} then π_{i}(p) ∈ C_{i} by definition of \underline{∧}. (iii) Let us assume that ∀a ∈ C p[x := a] ∈ SN_{⊥}. We want to prove ∀a ∈ C (λx.p)a ∈ SN_{⊥}. Since x^{A} ∈ C then p ≡ p[x := x^{A}] ∈ SN_{⊥}. Moreover, a ∈ C ⊆ SN_{A}. Thus p, a have bounds n, m. We prove (λx.p)a ∈ SN_{⊥} by induction on n + m. Since (λx.p)a ∈ SN_{⊥} begins with an elimi-nation of ¬, by (cand 3) it is enough to prove that for all proofs q, ((λx.p)a ⟶ q) ⇒ q ∈ SN_{⊥}. If the reduction takes place inside p or a we can deduce that q ∈ SN_{⊥} by the induction hypothesis, by the closure of C under → and by the compatibility of reductions with substitution (Lemma 4.1(ii)). If (λx.p)a itself is the redex being reduced, then either (λx.p)a ⟶ p[x := a] or we perform a reduction (At-class) and q is inside p or a. In the first case p[x := a] ∈ SN_{⊥} by the hypothesis and we have finished. In the second case, since p, a have a bound, q ∈ SN_{⊥} again. □

The interpretation we have outlined for the quantifier-free fragment of C_{Σ} is not necessarily sound with respect to the double negation rule.

In the next section we shall show that, by considering a suitable subset of Girard candidates, we can also interpret the rule of double negation.

6.2 Adding the Double Negation Rule

In this subsection we introduce a subset of Girard candidates (the Prawitz Candidates), which are exactly those which soundly interpret the double negation rule. Then we shall prove that Prawitz candidates are an interpretation of the quantifier-free fragment of C_{Σ}.

Definition 6.2 Let C ∈ GC.

(i) C is a Prawitz candidate if

(∀q = in¬C p[x := q] ∈ SN_{⊥}) ⇒ N x.p ∈ C

(ii) PC = {C ∈ GC|C is a Prawitz candidate }.

The Prawitz candidates soundly interpret the double negation rules by definition. Lemmas 6.1(ii),6.2,6.4 still hold for PC because PC ⊆ GC. Thus Prawitz candidates soundly interpret all propositional rules. In order to have an interpretation of the quantifier-free fragment of C_{Σ} we have only to check that SN_{A} ∈ PC for A atomic and that PC soundly interpret the connectives ¬ and ∧, i.e. that PC is closed under \underline{¬} and \underline{∧}.

Lemma 6.5 Let A be an atomic proposition. Then SN_{A} ∈ PC.

Proof. SN_{A} ∈ GC by Lemma 6.1(i)??. Thus we have only to check that SN_{A} is a Prawitz candidate, i.e. that

(∀q ∈ ¬SN_{A} p[x := q] ∈ SN_{⊥}) ⇒ N x.p ∈ SN_{A}.

Since x^{¬A} ∈ ¬SN_{A}, then p ≡ p[x : x^{¬A}] ∈ SN_{⊥}. Let n be a bound for p. We prove N x.p ∈ SN_{A} by induction on n. By (cand 3) for SN_{A}, it is enough to prove that for all proofs q, (N x.p ⟶ q) ⇒ q ∈ SN_{A}. If the reduction takes places in p, then q is N x.p′ for some p′ such that p ⟶ p′. In such a case, by the induction hypothesis and the fact that p[x := q] ⟶ p′[x := q], we conclude that q ≡ N x.p′ ∈ SN_{A}. If (N x.p)^{A} is the redex being reduced then, since A is atomic, we must have applied a reduction (At-class). Thus q is a subproof of p and, since p ∈ SN_{⊥}, q ∈ SN_{A}. □

We have now to prove that PC soundly interpret the formation of quantifier-free proposition, i.e. that PC is closed under \underline{¬} and \underline{∧}. To make such proof easier we first prove the following lemma.

Lemma 6.6 Let C_{1}, C_{2}, C ∈ GC and C_{i}^{i} = A_{i}, C^{∗} = A.

\begin{aligned}(i) p^{¬A_{i}} ∈ ¬C_{i} & ⇒ & σ_{i}[p] ∈ \underline{¬}(C_{1}\underline{∧}C_{2}) i=1,2 \\ (ii) p^{A} ∈ C & ⇒ & σ[p] ∈ \underline{¬}\underline{¬}C \end{aligned}

Proof. (i) Let p ∈ \underline{¬}C_{i}. By definition, σ_{i}[p] ≡ λx^{A_{1}∧A_{2}}.p^{A_{i}}(π_{i}(x)^{A_{i}})^{⊥}. By Lemma 6.4(iii), in order to have σ_{i}[p] ∈ ¬(C_{1}\underline{∧}C_{2}) it is enough to show that ∀q ∈ C_{1}\underline{∧}C_{2} p(π_{i}(q)) ∈ SN_{⊥}. This follows from Lemma 6.4(ii)(iv). □

Lemma 6.7 (i) \underline{∧} : PC → PC → PC (ii) \underline{∧} : PC → PC.

Proof. Let C_{1}, C_{2}, C ∈ PC.

(i) By Lemma 6.3(i) C_{1}\underline{∧}C_{2} ∈ GC. We have still to check that C_{1}\underline{∧}C_{2} is a Prawitz candidate, i.e. that (∀q ∈ ¬(C_{1}\underline{∧}C_{2}) p[x := q] ∈ SN_{⊥}) ⇒ N x.p ∈ C_{1}\underline{∧}C_{2}. As we did in the proof of Lemma 6.5, we first remark that p ∈ SN_{⊥}, and then we proceed by induction on the bound n of p. By (cand 3) we have to prove that for all proofs q, (N x.p ⟶ q) ⇒ q ∈ C_{1}\underline{∧}C_{2}. The only interesting case is when (N x.p)^{A_{1}∧A_{2}} is the redex being reduced. In such a case we must perform a reduction (∧-class), i.e.

N x.p ⟶ q ≡< N x_{1}.p[σ_{1}[x]], N x_{2}.p[σ_{2}[x]] >

and we have to prove that q ∈ C_{1}\underline{∧}C_{2}. By Lemma 6.4(i), it is enough to prove that N x_{i}.p[σ_{i}[x]] ∈ C_{i} for i = 1, 2. Since C_{i} ∈ PC, we have in fact to prove ∀q ∈ \underline{¬}C_{i} p[σ_{i}[q]] ∈ SN_{⊥}. By Lemma 6.6(i), σ_{i}[q] ∈ \underline{¬}(C_{1}\underline{∧}C_{2}). Thus, by hypothesis on p, p[σ_{i}[q]] ∈ SN_{⊥}. (ii) By Lemma 6.3(ii), \underline{¬}C ∈ GC. We have still to check that \underline{¬}C is a Prawitz candidate, i.e. that (∀q ∈ \underline{¬}\underline{¬}C p[x := q] ∈ SN_{⊥}) ⇒ N x.p ∈ \underline{¬}C. As we did in the proof of Lemma 6.5, we first remark that p ∈ SN_{⊥}, and then we proceed by induction on the bound n of p. By (cand 3) it is enough to prove that for all proofs q, (N x.p ⟶ q) ⇒ q ∈ \underline{¬}C. The only interesting case is when (N x.p)^{¬A} is the redex being reduced. In such a case we must perform a reduction (¬-class), i.e. N x.p[x] ⟶ q ≡ λx_{1}.p[σ[x_{1}]]. By Lemma 6.4(i), it is enough to prove that ∀a ∈ C p[σ[a]] ∈ SN_{⊥}. By Lemma 6.6(ii), σ[a] ∈ \underline{¬}\underline{¬}C. Thus, by hypothesis on p, p[σ[a]] ∈ SN_{⊥}. □

In the next section we shall extend the interpretation given here to the whole system C_{Σ}.

6.3 Predicative and Impredicative Quantification

In this subsection we interpret the types of C_{Σ} as particular sets, and quantification as an operation on such sets. Then we shall prove that such an interpretation is sound with respect to the formation of quantified propositions and with respect to the rules for such propositions.

For each type T of C_{Σ} we define a set [[T]] of higher order candidates, and a βη-normal index P : T for each F ∈ [[T]]. The definition is by simultaneous induction on T.

Definition 6.3 – [[P rop]] = PC

– [[ι]] = { the terms of C_{Σ}} If C ∈ PC the only index of C is C^{∗}. If t ∈ [[ι]] the only index of t is t itself.

– [[T → U]] = {F : [[T]] → [[U]]|F has some index }. where F : [[T]] → [[U]] has index P if ∀a ∈ [[T]](a has index E) ⇒ F (a) has index (the βη normal form of) P (E).

We define now some canonical elements in each [[T]].

Definition 6.4 (i) Let t be a term. Then SN_{t} =_{def} t ∈ [[ι]]. (ii) Let P be an atomic proposition. Then SN_{P} has been already defined at the beginning of 6.1 (iii) Let P be any atomic predicate of type T → U (i.e. an expression of the form X(E_{1}, …, E_{n})) and G ∈ [[T]] with index Q. Then we put

SN_{P} (G) =_{def} SN_{P (Q)} ∈ [[U]]

Lemma 6.8 Let T be a type and E : T.

(i) Each F ∈ [[T]] has a unique (βη-normal) index (ii) SN_{E} is a well defined element of [[T]] with index E.

Proof. By simultaneous induction on T. The cases T = P rop, ι are trivial or already proved. Let T = U → V. Suppose F ∈ [[T]] have indexes P_{1}, P_{2}. By induction hypothesis, if X is a variable and X : U then SN_{X} ∈ [[U]] and SN_{X} has index X. Thus F (SN_{X}) has indexes P_{1}(X) and P_{2}(X). By induction hypothesis on U, P_{1}(X) =_{β} P_{2}(X) and we deduce P_{1} =_{βη} P_{2} by η. Since P_{1}, P_{2} are βη-normal, P_{1} ≡ P_{2}. We want to prove now that SN_{E} is a well defined element of [[T]] with index E. We have only to check that, if G ∈ [[U]] has index Q, then SN_{E}(G)(≡ SN_{E(Q)}) is an uniquely determined element of [[U]] with index E(Q). By the induction hypothesis on U, the index of G is unique; thus SN_{E(Q)} is uniquely determined and , by the induction hypothesis on U, it is in [[U]]. □

If T is a type and F ∈ [[T]], we shall denote by F^{∗} (expression of type T) the only index of F. Remark that, by definition of [[T]], if T = U → V, we have that F (G)^{∗} =_{βη} F^{∗}(G^{∗}).

For each type T we define now a higher order candidate

\underline{∀} ∈ [[(T → P rop) → P rop]]

with index λP.∀X.P (X), to interpret quantification. We shall drop the subscript T when it is irrelevant.

Definition 6.5 Let F ∈ [[T → P rop]].

\underline{∀}_{T} (F) =_{def} \{p proof |∀G ∈ [[T]]p(G^{∗}) ∈ F (A)\}
By type consistency, each p ∈ \underline{∀}_{T} (F) has type ∀x^{T} .F^{∗}(x).

To prove that \underline{∀}_{T} ∈ [[(T → P rop) → P rop]] it is enough to check that \underline{∀}(P) ∈ [[P rop]]. We do it in two steps; first we check that \underline{∀}(F) ∈ GC, and then that \underline{∀}(F) ∈ PC.

Lemma 6.9 Let F ∈ [[T → P rop]]. Then \underline{∀}(F) ∈ GC.

Proof. We check (cand 1), (cand 2) and (cand 3). (cand 1) Let p ∈ \underline{∀}(F). If X is a variable and X : T then SN_{X} ∈ [[T]] and therefore p(X) ∈ F (SN_{X}) ⊆ SN_{F^{∗}(X)}. Thus p strongly normalizes. (cand 2) Let p ∈ \underline{∀}(F) and p ⟶ q. Then ∀G ∈ [[T]]p(G^{∗}) ∈ F (G) and p(G^{∗}) ⟶ q(G^{∗}) Thus ∀G ∈ [[T]]q(G^{∗}) ∈ F (G) and we conclude that q ∈ \underline{∀}(F). (cand 3) Suppose that for all proofs q, (p ⟶ q) ⇒ q ∈ \underline{∀}(F) and that p does not begin with an introduction. We want to prove \underline{∀} ∈ [[T]]p(G^{∗}) ∈ F (G). We first remark that, by (cand 3) for SN_{∀X.F^{∗}(X)}, since for all proofs q, (p ⟶ q) ⇒ q ∈ \underline{∀}(F) ⊆ SN_{∀X.F^{∗}(X)}, we can deduce p ∈ SN_{∀X.F^{∗}(X)}. By (cand 3) for F (G) it is enough to prove that for all proofs q′, (p(G^{∗}) ⟶ q′) ⇒ q′ ∈ F (G). Since p does not begin with a λ, the reduction on p(G^{∗}) either can take place in p or can be a reduction (At-class) with redex p(G^{∗} with F (G^{∗}) atomic. In the first case q′ is q(G^{∗}) for some q such that p ⟶ q and then we have q ∈ \underline{∀}(F) by hypothesis, and therefore q(G^{∗}) ∈ F (G). In the second case q′ is a subproof of p ∈ SN_{∀X.F^{∗}(X)} and therefore q′ ∈ SN_{F (a)^{∗}}. By Lemma 6.1(ii), since F (G)^{∗} is atomic, we have that F (a) = SN_{F (a)^{∗}} and we can conclude that q ∈ F (a). □

The lemma above then states that \underline{∀} soundly interpret the intuitionistic quantification. We prove now that the intuitionistic rules for quantification have a sound interpretation.

Lemma 6.10 Let T be a type and F ∈ [[T → P rop]].

(i) (∀a ∈ [[T]] p[x := G^{∗}] ∈ F (G)) ⇒ λx.p ∈ \underline{∀}(F) (ii) p ∈ \underline{∀}(F), G ∈ [[T]] ⇒ p(G^{∗}) ∈ F (G).

Proof. (i) We have to prove that ∀G ∈ [[T]] (λx.p)G^{∗} ∈ F (G). By (cand 3), since such proof begins with an application, it is enough to prove that for all proofs q, ((λx.p) ⟶ q) ⇒ q ∈ F (G). We first remark that if X is a variable and X : T then SN_{X} ∈ [[T]] and therefore p ≡ p[x := x] ∈ F (SN_{X}) ⊆ SN_{F^{∗}(X)}. Let n be a bound for p. We prove (λx.p)G^{∗} ∈ F (G) by induction on n. If q ≡ (λx.p′)G^{∗} with p ⟶ p′, then we still have p′[x := G^{∗}] ∈ F (G) by (cand 2) and p[x := G^{∗}] ⟶ p′[x := G^{∗}]. Thus, by the induction hypothesis we have q ≡ (λx.p)G^{∗} ∈ F (G). If (λx.p)G^{∗} is the redex being reduced, then either (λx.p)G^{∗} ⟶ p[x := G^{∗}] ≡ q or we perform a reduction (At-class), F (G)^{∗} is atomic and q is a subproof of p. In the first case, q ∈ F (G) by hypothesis on p. In the seco-nd case q ∈ SN_{F (G)^{∗}} because p strongly normalizes. Since F (a) is atomic, by Lemma 6.1(ii) F (G) = SN_{F (G)^{∗}} and we conclude that q ∈ F (G). □

We prove now that \underline{∀} soundly interpret also the classic quantification, i.e. that \underline{∀}(F) is also a Prawitz candidate. In order to make the proof easier, we first prove the following lemma.

Lemma 6.11 Let T be a type and F ∈ [[T → P rop]]. Then, for all G ∈ [[U]]

q ∈ \underline{¬}F (G) ⇒ σ_{G^{∗}}[q] ∈ \underline{¬}\underline{∀}(F).

Proof. We know that σ_{G^{∗}}[q] = λx.q(x(G^{∗})). By Lemma 6.4(iii) σ_{G^{∗}}[q] ∈ \underline{¬}\underline{∀}(F) if for all q′ ∈ \underline{∀}(F) we have that q(q′(G^{∗})) ∈ SN_{⊥}. This fact follows by definition of \underline{∀}(F) and \underline{¬}F (G). □

Lemma 6.12

\underline{∀}_{T} ∈ [[(T → P rop) → P rop]]

Proof. Let F ∈ [[T → P rop]]. We proved in Lemma 7.9 that \underline{∀}(F) ∈ GC. There is only left to prove

(∀q ∈ ¬\underline{∀}(F)p[x := q] ∈ SN_{⊥}) ⇒ N x.p ∈ \underline{∀}(F).

Let x : ¬∀z.F^{∗}(z). Then x ∈ \underline{¬}(F) and therefore p ≡ p[x := x] ∈ SN_{⊥}. Let n be a bound for p. We prove N x.p ∈ \underline{∀}(F) by induction on n. By (cand 3) for \underline{∀}(F) it is enough to prove that for all q′ (N x.p ⟶ q′) ⇒ q′ ∈ \underline{∀}(F). If q′ is N x.p with p ⟶ p′ then we still have ∀q ∈ \underline{¬}\underline{∀}(F) p′[x := q] ∈ SN_{⊥} because p[x := q] ⟶ p′[x := q] ∈ SN_{⊥}. Since p′ has a smaller bound than p, by the induction hypothesis we have q′ ≡ N x.p′ ∈ \underline{∀}(F). If N x.p is the redex being reduced, then we must apply a reduction (∀-class) and q′ is λz.N x_{1}p[σ_{z}[x_{1}]]. By Lemma 6.10(i), to prove q′ ∈ \underline{∀}(F) it is enough to prove ∀G ∈ [[T]] N x_{1}.p[σ_{G^{∗}}[x_{1}]] ∈ F (G). Since F (G) ∈ [[P rop]] ≡ PC, we are reduced to prove ∀q ∈ \underline{¬}F (G) p[σ_{G^{∗}}[q]] ∈ SN_{⊥}. By Lemma 6.11 q ∈ \underline{¬}F (G) ⇒ σ_{G^{∗}}[q] ∈ \underline{¬}\underline{∀}(F). Thus, by hypothesis on p, we conclude that p[σ_{G^{∗}} ∈ SN_{⊥}. □

In the next subsection we shall collect the work done up to now and shall define a formal Realization semantics for C_{Σ}. Strong normalization for proofs in C_{Σ} will follow as corollary.

6.4 A Realization Semantic for C_{Σ}

In this subsection we shall formally define a Realization Semantics for C_{Σ}, associating to each proposition A a ”natural” candidate C for A. Then we shall prove that such Realization Semantics is sound for C_{Σ}, i.e. that

x : A ⊢_{C_{Σ}}⇒ p ∈ C.

Since C ⊆ SN_{A}, it will follow that each proof p of C_{Σ} strongly normalizes.

We first interpret, inside the Realization Semantics, predicates and terms. In the previous subsections we have shown how to interpret each symbol inside a predicate but variables. An interpretation for variables is provided by the notion of predicate assignment.

Definition 6.6 A Predicate assignment ρ is a function with a finite set of variables {v_{1}, …, v_{2}} as domain, such that, for each v ∈ dom(ρ), each type T and each proposition A we have :

(i) v : T ⇒ ρ(v) ∈ [[T]] (ii) v : A ⇒ ρ(v) : A

Each variable v is interpreted, in a given assignment ρ, by ρ(v). ρ(v) is a higher order predicate if v is a predicate or term variable, and it is a proof if v is a proof variable. We can associate a substitution ρ^{∗} to ρ in the following way.

Definition 6.7 Let x be any variable, T a type and A a proposition.

(i) dom(ρ)^{∗} =_{def} dom(ρ)) (ii) x ∈ dom(ρ), x : T ⇒ ρ^{∗}(x) =_{def} ρ(x)^{∗} (iii) x ∈ dom(ρ), x : A ⇒ ρ^{∗}(x) =_{def} ρ(x)

From now on, if x ∉ dom(ρ), x : T, G ∈ [[T]], we shall denote by ρ_{x,G} the extension of ρ defined by

ρ_{x,G}(x) =_{def} G.

ρ_{x,G} is still a predicate assignment.

We are now ready to interpret any predicate of C_{Σ}.

Definition 6.8 Given a predicate assignment ρ, we extend it to a predicate P : T such that F V (P) ⊆ dom(ρ) by induction on P, as follows : ρ(At) = SN_{At} if At is a proposition of Σ ρ(A ∧ B) = ρ(A)\underline{∧}ρ(B) ρ(¬A) = \underline{¬}ρ(A) ρ(λx^{T} .P) defined by ρ(λx^{T} .P)(G) = ρ_{x,G}(P), ∀G ∈ [[T]] ρ(P Q) = ρ(P)ρ(Q) ρ(∀x.A) = \underline{∀}(ρ(λx.A))

Lemma 6.13 Let ρ, P, T be as above. Then ρ(P) is a well-defined element of [[T]] with index ρ(P)^{∗} = ρ^{∗}(P).

Proof. By induction on P, distinguishing the cases according to the outermost symbol of P.

• P = At. Then ρ(At) = SN_{At} ∈ [[P rop]] = PC by Lemma 6.5. Moreover SN_{At}^{∗} = At.

• P = A∧B. Then ρ(A∧B) = ρ(A)\underline{∧}ρ(B) ∈ [[P rop]] = PC by Lemma 6.7 and ρ(A), ρ(B) ∈ [[P rop]] = PC. Moreover ρ(A ∧ B)^{∗} = (ρ(A)\underline{∧}ρ(B))^{∗} = ρ(A)^{∗} ∧ ρ(B)^{∗} = (by the induction hypothesis) ρ^{∗}(A) ∧ ρ^{∗}(B) = ρ^{∗}(A ∧ B).

• P = ¬A. Then ρ(¬A) = \underline{¬}ρ(A) ∈ [[P rop]] = PC by Lemma 6.7. Moreover ρ(¬A)^{∗} = (\underline{¬}ρ(A))^{∗} = ¬ρ(A)^{∗} = (by the induction hypothesis) ¬ρ^{∗}(A) = ρ^{∗}(¬A).

• P = λx^{U}.Q^{V}. Then if G ∈ [[U]] then ρ(λx.Q)(G) = ρ_{x,G}(Q) ∈ [[U]] by the induction hypothesis on Q. Thus ρ(λx.Q) : [[U]] → [[V]]. Moreover ρ(λx.Q)(G)^{∗} = ρ_{x,G}(Q)^{∗} =(by the induction hypothesis) ρ_{x,G}^{∗}(Q) = (ρ^{∗}, x := G^{∗})(Q) = ρ^{∗}(Q)[x := G^{∗}] =_{β} (λx.ρ^{∗}(Q))(G^{∗}) = ρ^{∗}(λx.Q)(G^{∗}). Thus ρ(λx.Q) has index ρ^{∗}(λx.Q).

• P = Q^{U→V} R^{U}. Then ρ(QR) = ρ(Q)(ρ(R)) ∈ [[V]] because ρ(Q) ∈ [[U → V]] and ρ(R) ∈ [[u]]. Moreover ρ(QR)^{∗} = (ρ(Q)ρ(R))^{∗} = ρ(Q)^{∗}ρ(R)^{∗} = (by the induction hypothesis) ρ^{∗}(Q)ρ^{∗}(R) = ρ^{∗}(QR).

• P = ∀x^{T} .A. Then ρ(∀x^{T} .A) = \underline{∀}(ρ(λx^{T} .A)) ∈ [[P rop]] because \underline{∀} ∈ [[(T → P rop) → P rop]] by Lemma 6.12 and ρ(λx^{T} .A) ∈ [[T → P rop]]. Moreover ρ(∀x.A)^{∗} = ∀(ρ(λx.A))^{∗} = ∀x.ρ(λx.A)^{∗}(x) = (by the induction hypothesis) ∀x.ρ^{∗}(λx.A)(x) = ∀x.λx.ρ^{∗}(A)(x) = ∀x.ρ^{∗}(A) = ρ^{∗}(∀x.A).

□

In order to state a soundness theorem for the interpretation ρ(P) we have just outlined, we need one more definition.

Definition 6.9 An assignment ρ is a predicate assignment such that, for each variable x ∈ dom(ρ) and proposition A we have

x : A ⇒ ρ(x) ∈ ρ(A).

Theorem 6.1 (Soundness Theorem) Let ρ be an assignment and p be a proof such that F V (p) ⊆ dom(ρ). Then

p : A ⇒ ρ^{∗}(p) ∈ ρ(A).

Proof. By induction on p, distinguishing the cases according to the outermost symbol of p.

• p = x^{A}. By definition of assignment and ρ^{∗}(x) = ρ(x).

• p = r(t, p_{1}, …, p_{n}). By the induction hypothesis and lemma 6.2.

• p =< p_{1}, p_{2} >. By the induction hypothesis and Lemma 6.4(i).

• p = π_{i}(q). By the induction hypothesis and Lemma 6.4(ii).

• p = (λx^{B}.q^{⊥})^{¬B}. By the induction hypothesis and Lemma 6.4(iii).

• p = (p_{1}^{¬B}p_{2}^{B})^{⊥}. By the induction hypothesis and Lemma 6.4(iv).

• p = (λx^{T} .q^{A})^{∀x^{T} .A}. By the induction hypothesis and Lemma 6.10(i).

• p = (q^{∀x.A}(E))^{A[x:=E]}. By the induction hypothesis and Lemma 6.10(ii) we may deduce p ∈ ρ(λx.A)(ρ(E)) = ρ_{x,ρ(E)}(A). The thesis follows from the claim :

ρ_{x,ρ(E)}(A) = ρ(A[x := E]).

• p = (N x^{¬B}q^{⊥})^{B}. By the induction hypothesis and the definition of Prawitz candidate.

□

Corollary Each proof of C_{Σ} strongly normalizes. Proof. Let p : A, A : P rop and consider the assignment ρ defined by : if x : T, x ∈ F V (p) then ρ(x) =_{def} SN_{x} if x : B, x ∈ F V (p) then ρ(x) =_{def} x. Then ρ^{∗}(x) = x for each x ∈ F V (p) and ρ^{∗}(p) = p. By the previous theorem p = ρ^{∗}(p) ∈ ρ(A) ⊆ SN_{ρ^{∗}(A)} = SN_{A}. Thus, each proof p strongly normalizes. □

There is still left to prove the claim ρ_{x,ρ(E)}(A) = ρ(A[x := E]). Recall that A[x := E] denote the βη-normal form of A with E replaced for x. To consider the substitution alone we give the following definition.

Definition 6.10 sub(A, x, E) = the result of replacing each free occurrence of x by E in A.

With the definition above A[x := E] is the βη-normal form of sub(A, x, E). We can now split the proof of the claim in two parts : first we prove that ρ(sub(A, x, E)) = ρ_{x,ρ(E)} and second we can prove that A =_{βη} B ⇒ ρ(A) = ρ(B). In both cases we use the following property.

Lemma 6.14 Let P be a predicate ρ_{1}, ρ_{2} be an assignment and suppose that ρ_{1}(x) = ρ_{2}(x) for each x ∈ F V (p). Then ρ_{1}(p) = ρ_{2}(p).

Proof. By induction on p. We might also remark that we never use in the definition of p the values ρ_{1}(x), ρ_{2}(x) for x ∉ F V (p). □

We can now prove the following lemma.

Lemma 6.15 Let P be a predicate, E an expression, x a variable with the type of E , and ρ an assignment such that F V (P), F V (E) ⊆ dom(ρ). Then

ρ(sub(P, x, E)) = ρ_{x,ρ(E)}(P).

Proof. By induction on P. The only non-trivial case is when P = λy^{T} .Q. In such a case we may suppose that x ≠ y and have to prove ρ(sub(λy^{T} .Q, x, E)) = ρ(λy^{T} .sub(Q, x, E)). We have to check that, for every G ∈ [[T]]

ρ_{y,G}(sub(Q, x, E)) = (ρ_{x,ρ(E)})_{y,G}(Q).

By the induction hypothesis on Q we have that

ρ_{y,G}(sub(Q, x, E)) = (ρ_{y,G})_{x,ρ_{y,G}(E)}(Q).

By Lemma 6.14 ρ_{y,G}(E) = ρ(E), thus

(ρ_{y,G})_{x,ρ_{y,G}(E)}(Q) = (ρ_{y,G})_{x,ρ(E)}(Q) = (ρ_{x,ρ(E)})_{y,G}(Q).

□ We can now prove the claim by proving

ρ(sub(A, x, E)) = ρ(A[x := E]).

This follows from the following lemma.

Lemma 6.16 Let P, G be predicates, P =_{βη} G, ρ be an assignment and F V (P), F V (Q) ⊆ dom(ρ). Then

ρ(P) = ρ(Q).

Proof. It is enough to prove that, if P ⟶_{βη} P′, then ρ(P) = ρ(P′). this fact can be proved by induction on P. The only non-trivial case is when P itself is the redex being reduced, i.e. when P ≡ (λx.Q)R ⟶ sub(Q, x, R) or P ≡ λx.Q(x) ⟶ Q(with x ∉ F V (Q)). In the first case we apply Lemma 6.15, in the second one Lemma 6.14 and the fact that x ∉ F V (Q). □

References

1. Clinger W., Rees J. The revised^{3} report on the algorithmic language scheme. SIGPLAN Notices, 21(12):37-79, 1986.

2. Felleisen M., Friedman D., Kohlbecker E., Duba B. Reasoning with continuations. In Proceedings of the First Annual Symposium on Logic in Computer Science, 131-141, 1986.

3. Friedman H. Classically and intuitionistically provably recursive functions. In Scott D.S. and Muller G.H. editors, Higher Set Theory, vol.699 of Lecture Notes in Mathematics, 21-28. Springer Verlag, 1978.

4. Girard J.-Y. Une extension de l’interpretation de Godel a l’analyse, et son application a l’elimination des coupures dans l’analyse et la theorie des types. In Proceedings of the second Scandivian Logic Symposium, eds.J.E. Fenstad, Amsterdam, North-Holland, 63-92, 1971.

5. Griffin T.G. A formulae-as -types notion of control. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, 1990.

6. Kreisel G. Mathematical significance of consistency proofs. Journal of Symbolic Logic, 23:155-182, 1958.

7. Murthy C. Extracting constructive content from classical proofs. Ph.d. thesis, Department of Computer science, Cornell University, 1990.

8. Plotkin G. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 125-159, 1975.

9. Prawitz D. Natural deduction, a proof theoretical study. Stockolm, Almqvist and Winskell, 1965.

10. Prawitz D. Validity and normalizability of proofs in 1-st and 2-nd order classical and intuitionistic logic. In Atti del I Congresso Italiano di Logica, Napoli, Bibliopolis, 11-36, 1981.

Metalogical Frameworks

David A. Basin^{∗}  Robert L. Constable^{†}

July 1991

Abstract

In computer science we speak of implementing a logic; this is done in a programming language, such as Lisp, called here the implementation language. We also reason about the logic, as in understanding how to search for proofs or in knowing it is consistent; in the terminology of mathematical logic, these arguments are conducted in the metalanguage of the object language being implemented. We also reason about the implementation itself, say to know it is correct. This is done in a programming logic. How do all these logics relate? This paper considers that question and more.

We show that by taking the view that the metalogic is primary, these other parts are related in standard ways. The metalogic must be suitably rich so that the object logic can be presented as an abstract data type, and it must be suitably computational (or constructive) so that an instance of that type is an implementation. The data type abstractly encodes all that is relevant for metareasoning, i.e. not only the term constructing functions but also the principles for reasoning about arbitrary terms and computing with them.

Our work can also be seen as an approach to the task of finding a generic way to present logics and their implementations, which is for example the goal of the Edinburgh Logical Frameworks (ELF) effort. This approach extends well beyond proof-construction and includes computational metatheory as well.

1 Introduction

1.1 Role of Logical Frameworks and Formalized Metamathematics

At one time logic seemed to be a finished subject, and computers, like radio telescopes and linear accelerators, seemed to be the tools of big science. Now computers are ubiquitous and their software systems have brought logics to life. We see limitless expansion in both domains with computers destined to play a part in nearly every aspect of life and the logics of their systems needed to bring order and sense to this activity, as well as provide a basis for enabling the realization of ever bolder dreams. This is a new role for logic and with it come a host of new tasks and problems; this paper is about some of them, especially those that fall to computer scientists to address. Part of the job can be understood in terms of past accomplishments in computer science, and part belongs to a new subfield. Let us be more specific about this new role for logic and put these tasks in context, starting with the most familiar.

∗Department of Artificial Intelligence, University of Edinburgh, Scotland. Email: basin@aipna.ed.ac.uk. Partially supported by the North Atlantic Treaty Organization under a grant awarded in 1990.

†Department of Computer Science, Cornell University, Ithaca NY, USA. Email: rc@cs.cornell.edu. Partially supported by an SERC visiting fellowship and a Guggenheim fellowship.

LF in General Sense Formalized Metamathematics

• Wide variety of logics demands • Mechanized reasoning demands
general tools  general metareasoning facilities
(“Next 700 Theorem Provers”)  (“Metalogical Frameworks”)
• How to provide generic tools  • How to formalize metamathematics
for computer implementations  of logics
• define the logic  • represent the logic
– syntax, proof rules  – wffs, proofs, semantics
• automate theorem proving  • metatheory about proofs
– proof search  – derived rules

– decision procedures – normal form theorems

Figure 1: Congruence of Concerns

The first generation of software systems were brought under control with the development of automata theory, formal languages, and programming logics. Modern compilers are built with tools and techniques based on a deep understanding of parsing and compilation, and the methods of rigorous program development make it possible to achieve high levels of reliability for a range of specifiable programs.

Now the field seeks to do more, to extend the previous successes to a wider range of computing problems and to carry the techniques forward into more imaginative experimental systems which have formal logics as components. For instance there will be programming languages with type systems that are equivalent to logics, and the type checkers will be little theorem provers (maybe even big ones). There will be formal specification languages and program verifiers both based on a formal logic of some kind. There will be systems that support program synthesis and hardware synthesis. There will be data bases with rich query languages that are formal logics. There will be more experimental systems such as problem solving environments and programmer’s assistants. In all of these systems formal logic is playing its new role. Moreover, there will be many different logics and many different implementations of each. So as in the case of compiler construction, there will be an industry for building and modifying the implemented logics.

Thus far there are few tools designed specifically to support the activity of implementing logics. So systems are built from scratch using tools intended for other purposes. What is wanting is a framework for designing these logics and supplying the generic tools. One of the main goals of research in logical frameworks is to offer a setting to guide the building of these generic tools.

Another way to approach the topic of this paper is to consider the activity of generating formal mathematics, the project of Automath [8]. This has been taken up with considerable energy in computer science because it is seen as an integral part of some of the new kinds of systems mentioned above and because it is related to concerns of AI and because it is a generalization of programming, an activity central to computer science. For whatever reason (and there maybe other more subtle ones), this is now done by computer scientists. One of the subjects that is most promising to formalize is metamathematics, in part because the results of that work feed back directly to the task of generating formal theorems. In the context of formalizing metamathematics, we are confronted with many of the same questions facing the designer of a logical framework; some of these parallels are drawn in Figure 1. This paper considers why this is so. Moreover we claim that the vantage point of formalized metamathematics is a good way to look at the task of logical frameworks, and we advocate its primacy, hence the title of the paper.

Scientists actually doing formal mathematics have come to understand the importance of metareasoning from experience. They quickly saw that nearly all informal mathematics is a mixture of object theory and metatheory. The work of Howe [25], comes to our minds in this connection. Also the style of automating reasoning via tactics involves programming in a metalanguage, and if one applies the methodology of programming systems based on the proofsas-programs principle, such as Nuprl [12] and the Calculus of Constructions (CoC) [14], then many of these tactics should be extracted from metatheorems. A great deal of work has been done in this direction at Cornell, [27, 24, 2]. Also even if this principle is not underlying the programming style, it has been widely noticed that substantial economies in proof generation are possible if tactics are replaced by the metatheorems that they implement.

The key component, and least understood one, in an implemented logic is usually the inference engine, and our starting point is the observation that the experimental systems will need ways to quickly modify them, even the workhorse system will need ways to progressively enhance it. Our response to the situation is to conjecture that the problems of understanding, specifying and modifying the inference engine are best dealt with in the framework of a formalized metalogic, not in the setting of a hybrid system of languages nor in a framework that enables a generic definition of the syntax and proof structure of a logic. It will be important to reason about the object logic (the one being implemented) in a very expressive metalogic.

1.2 Conceptual Issues

Logicians have been concerned for years with treating their subject more abstractly and generally. The elementary formal systems of Smullyan were an attempt to characterize the deductive machinery of Principia Mathematica, and lately Feferman has proposed more usable formalisms [19, 18] such as F S_{0} for expressing proof theory. There are abstract semantic characterizations of logic [4, 5] and the theorem of Lindström in abstract model theory characterizing first-order logics. There are other efforts along these lines such as [1].

The work of logicians deals with many of the issues central to the problem of logical frameworks such as what is a logic, what are the different ways to present them and which are essentially the same, which are different. Their concern for the most general setting for major results such as Godel’s theorems, Löb’s theorem, Girard’s normalization methods, etc. is directly germane to the task of formalizing metamathematics. But some of the issues faced in defining a logical framework and formalizing mathematics on a machine are new. For example, how should bound variables be represented, as deBruijn indices or as special terms? How can a sequent based proof economize on storage? What is the best way to realize computational content? What is the essential difference between sequent style proofs and natural deduction style, and does it apply to all logics?

Inevitably discoveries about logical frameworks will contribute to a conceptual understanding of logic. From the vantage point of this paper we see that the efforts to formalize metamathematics will contribute as well. This might not be so obvious a priori.

1.3 Results

Beyond advocating the primacy of metalogic this paper contributes some specific technical results. We propose a particular way to specify logics, namely using types that one might call higher-order abstract data types or ADT’s for this paper. We show that an implementation of a logic can be seen then as an instance of the abstract data type. There are many interesting connections between these types and other approaches to data abstraction in type theory and programming languages.

We also look at constructive metatheory in action and illustrate by example why a framework for automating logic will want access to the results of formalized metamathematics. This practical need is remarkably congruent to the philosophical stance adopted by the first metamathematicians who used finitist or constructivist metatheories. This historical accident means that there is a deep literature of informal implicitly computational metatheory to draw on as well the explicitly computational results of modern computer scientists (unification, resolution, term rewriting, etc.) such as decision procedures, and moreover that formalizing these results makes them clearer and more general, thus fulfilling the promise of formalized mathematics. Indeed given the deep literature in proof theory, there is much to be done in this vein to bring it to life and make it available to applied logicians. But also new kinds of metamathematical result are needed in reasoning about implemented logics, and we mention some of them as well.

Finally we show that by taking a rich constructive metalogic as the basis for a logical framework, the context becomes simpler and the relationship between the concerns of logical frameworks and those of the formal metamathematics stand out.

Finally, rather than choosing a specific metalogic which is adequate (such as Nuprl or CoC), we talk about the requirements for such a theory.

2 Data Abstraction in Type Theory

In this section we provide a brief account of data abstraction within type theory. Our notion of data abstraction has similarities to two standard techniques used to define data within type theories; these are the techniques of defining data-types within minimal type theories such as CoC, and the definition of ADTs as Σ-types within predicative type theories.

Within minimal type theories, such as the Calculus of Constructions, standard data-types (e.g., pairing, lists, etc.) are encoded by inductive definitions. These data-types are specified by:

• naming a set (type) that members will inhabit;

• giving function constants (and their types) for constructing members of the set;

• providing rules for reasoning about type members and functions defined over them.

These declarations can be seen as capturing the rules for type formation, introduction, elimination, and computation. In theorem provers for CoC such as LEGO[9] these declarations are made within a context, and one reasons within the scope of these declarations. Theorems proved within contexts essentially have all of the context declarations (implicitly) quantified using Π-types.

When a type theory is enriched with Σ-types, a second approach is possible whereby the declarations of the ADT are packaged together with a (iterated) Σ-type; theorems are then proved within the context of these types. This has the conceptual advantage of unifying the LIST ˆ= A:T ype →

List:T ype # Nil:List # Cons : A × List → List # Lind: P:(List → T ype) → l:List → P (Nil)

→ ((h:A × t:List × P (t)) → P (Cons(h, t))) → P (l)

# P:(List → T ype) → l:List → g:P (Nil) → i:((h:A × t:List × P (t)) → P (Cons(h, t)))

Lind(P)(Nil)(g)(i) = g
∧ ∀h:A. ∀t:List. Lind(P)(Cons(h, t))(g)(i) = i(h, t, Lind(P)(t)(g)(i))

MSET ˆ= A:T ype → MSet:T ype # Empty:MSet # Add : A × MSet → MSet # ∀a, b:A. ∀s:MSet. Add(a, Add(b, s)) = Add(b, Add(a, s)) # Mind: P:(MSet → T ype) → l:MSet → P (Empty)

→ {i:((a:A × s:MSet × P (s)) → P (Add(a, s))) |
∀a, b:A. ∀s:MSet. ∀p:P (s). i(a, Add(b, s), i(b, s, p)) = i(b, Add(a, s), i(a, s, p))}
→ P (l)

# P:(MSet → T ype) → l:MSet → g:P (Empty)

→ i:{i:((a:A × s:MSet × P (s)) → P (Add(a, s))) |
∀a, b:A. ∀s:MSet. ∀p:P (s). i(a, Add(b, s), i(b, s, p)) = i(b, Add(a, s), i(a, s, p))}
Mind(P)(Empty)(g)(i) = g
∧ ∀a:A. ∀s:MSet. Mind(P)(Add(a, s))(g)(i) = i(a, s, Mind(P)(s)(g)(i))

Figure 2: List and Multi-set ADT

data-type definition into a single type and the practical advantage of allowing parameterization of one ADT by another. It can also be seen as a natural generalization of signatures in ML, Extended ML [40], and other languages implementing data-abstraction using dependent types. This is the approach we shall take. One complication is that such modularization requires predicative quantification and hence a type hierarchy. For simplicity, we shall use the first universe (which we call T ype) as the type of ADT parameters and set carriers.

Figure 2 contains two examples of ADTs: parameterized lists and finite multi-sets (sometimes called “bags”). Members of the LIST type are functions: when applied to a parameter type A, they return a tuple in which the first projection, the carrier of the ADT, is the type of lists over A whose members are built from the functions inhabiting the Nil and Cons projections. The multi-set ADT is similar except for the defined carrier equality and the elimination and computation rules which are modified to respect this equality (more will be said on this below). Some notation should be explained. First x: A#B denotes a Σ-type built from the types A and B. Free occurrences of x become bound in B. Sometimes, to emphasize its logical significance, we abbreviate this to ∃x: A. B, or conjunction (when x is not free in B) A ∧ B, or even pairing A × B. Similarly x: A → B represents the Π-type built from A and B and may be alternatively displayed as a ∀x : A. B or A ⇒ B. To axiomatize equalities we make use of the equality (or I-type) of Martin-Löf type theory; equality is a ternary type-constructor (t_{1} = t_{2} in T) that has a member precisely when t_{1} and t_{2} are equal members of T. In our presentations we shall omit the third argument (the type T) since it can generally be determined from the context. We also make use of the set type {x:A|B}; in this type x is bound in B and its members are a in A when B[a/x] is also inhabited. The proof rules for this type may be found in [12]. Finally, ˆ= is our notation for definitional equality.

The difference between these two ADTs is their specification of member equality. In an implementation of lists, members must be equal when they are built in identical ways from constructors. Indeed, when the induction combinator is known to be unique (which it is when the metalogic contains identity types), all implementing structures will be equivalent up to isomorphism. If we are working within a type theory such as Nuprl’s which has a type constructor list with term constructors nil and “.” (for cons) and an induction combinator list ind, then we can trivially build a member of the list ADT.

\begin{matrix}λA. ⟨A list, ⟨nil, ⟨λa. λt. (a.t), \\ ⟨λP. λl. λg. λi. list ind(l; g; h, l, v.i(h)(l)(v)), ⟨λP. λl. λg. λi. ⟨axiom, λa. λt. axiom⟩⟩⟩⟩⟩⟩ \end{matrix}

Other implementations are possible; for example, lists as iterated pairs, fringes of trees, and so forth. For multi-sets, any implementation of the MSET ADT must equate not only those members built in the same way, but also those sets which only differ in the order in which their members were added. Specifying carrier types for ADTs that have axiomatized equalities requires a quotient type constructor such as the one provided by Nuprl, or extensions to the underlying type theory in the spirit of those suggested by Backhouse [3]. For example, using the quotient type we can implement multi-sets as lists where the quotienting equality is equivalence under permutation.

One complication of packaging ADT declarations as Σ-types is that we must be able to open them and access the components of their members. To this end, projection functions must be created and named, but these may be automatically generated in a straightforward way. In subsequent sections we shall always assume that these projection functions have been defined and are named, when possible, by the binding variable associated with that component of the Σtype. For example, let L be member of LIST, then for T a type, L(T) is a tuple with List(L(T)) naming the first projection, Nil(L(T)) naming the second, and so forth. To simplify presentation in the remainder of the paper we will often make radical abbreviations in presenting projections from ADTs, and terms built from the constructor functions. For example, when types like L and T can be determined from context we will write terms like List(L(T)) and Nil(L(T)) more simply as List and Nil. Moreover we will use standard abbreviations in terms built from these constructors; for example we might abbreviate Cons(L(T))(t_{1}, Cons(L(T))(t_{2}, Nil(L(T)))) as Cons(t_{1}, Cons(t_{2}, Nil)), or even [t_{1}, t_{2}].

The most significant distinction between our ADTs and traditional ADTs is that we axiomatize induction (elimination) rules and computation rules. The addition of these rules is not difficult within either impredicative or predicative type theories and may be automatically generated from the constructor declarations. In [37], Paulin-Mohring details how induction and computation principles can be automatically generated from declarations of constructor functions and their types and arities within the Calculus of Constructions; The INRIA implementation of CoC contains such a facility. In [3], Backhouse gives a similar account for predicative type theories (e.g., Martin-Löf’s) and he also explains how these rules can incorporate quotiented equality relations like the kind needed for multi-sets. For brevity of presentation, we will not explicitly give the induction and computation rules associated with defined ADTs.

But these should be understood as being part of all ADTs defined.

As an example, within the context of the list ADT we may define the functions “head” and “tails” as follows.

hd(l) ˆ= Lind(λx. List)(l)(Nil)(λ⟨h, v, t⟩. h)
tl(l) ˆ= Lind(λx. List)(l)(Nil)(λ⟨h, v, t⟩. t)

From these definitions, using the Lind induction principle it is straightforward to prove theorems such as

⊢ ∀A:T ype. ∀L:LIST. ∀l:List. l ≠ Nil ⇒ Cons(hd(l), tl(l)) = l.

There are a couple subtleties that arise in the definition and application of functions over the ADT carriers. The first concerns the use of equality axioms in ADTs like the multi-set. Any defined functions must respect this equality and, as a result, many functions over lists, such as head and tails, have no analog for multi-sets since they do not respect the multi-set equality. This is sensible; since multi-sets are unordered, they have no “first” and “rest”. Functions respecting this equality can still be defined. For example, we can define multi-set membership provided we are careful (e.g., through the use of the set type constructor) that the definition does not provide a way of computing the “position” of the element in the multi-set. In future sections, we shall make use of defined functions on both lists and multi-sets such as member deletion (which we denote by “−”) and membership (“∈”). We shall also denote the empty list (multi-set) by “{}” and cons (add) by “+”.

Another subtlety concerns equality reasoning. Note that the computation rules allow us to reason about the the conversion behavior of defined functions; we may compute with them, but only in an indirect sense. That is, the computation axioms do not augment the framework logic with reduction rules that can directly be computed with (in the sense of, say, the direct computation rules of Nuprl). Instead, one computes by using equality reasoning to establish that a defined function is equal to some normal form, e.g. hd([1, 2, 3]) = 1. This kind of computation via rewriting can be automated and made fairly efficient. In [25], Howe gives an example of how this kind of equality simplification can be automated by rewrite tactics similar to Paulson’s conversions [38] and moreover how this can be accomplished (using derived inference rules) without direct construction of the corresponding equality proof. It would be interesting to study an alternative approach to computational equality in which direct computation rules are expressed in the ADT, perhaps in a type theory that contains a primitive for Howe’s lazy congruence relation [26].

3 Specifying Provers With Abstract Types

Textbook presentations of logics typically begin with an account of logical syntax, i.e., the presentation of syntactic entities such as terms, formulas, and proofs. Typical is the text of Gallier [20], which presents the formulas of the propositional calculus as those in the inductive closure of a collection of propositional functions. As this is a freely generated set, he observes that we can define functions on formula by recursion and prove properties of formula by induction. Van Dalen’s presentation [42] is similar, although he doesn’t explicitly refer to the propositional connectives as functions.

What these and most other presentations have in common is that they define logical syntax as sets built from functions having certain properties. Equally significant, they leave implementation details unspecified. It should not matter whether formulas are represented by ASCII

\begin{aligned}& Axiom \\ Γ, A ⊢ A \end{aligned}  \begin{aligned}& F alseE \\ Γ, f ⊢ G \end{aligned}

Γ ⊢ A Γ ⊢ B ; AndI ; Γ ⊢ A ∧ B  Γ, A, B ⊢ G ; AndE ; Γ, A ∧ B ⊢ G

Γ ⊢ A ; OrIL ; Γ ⊢ A ∨ B  Γ ⊢ B ; OrIR ; Γ ⊢ A ∨ B  Γ, A ⊢ G Γ, B ⊢ G ; OrE ; Γ, A ∨ B ⊢ G

Γ, A ⊢ B ; ImpI ; Γ ⊢ A ⇒ B  Γ, A ⇒ B ⊢ A Γ, B ⊢ G ; ImpE ; Γ, A ⇒ B ⊢ G

Figure 3: LJ Inference Rules

strings or trees built from cons cells; all that matters is their extensional properties. This kind of abstraction and desire for representation independence between the specification of a logic and its implementation suggests that they stand in the same relation as that between an abstract data-type or signature (in the parlance of ML modules [35]) and its implementing structure. Note, in particular, that the induction and recursion requirements are perfectly captured by our induction and computation rules.

In this section we illustrate this approach to specification by formalizing a theorem prover for a simple logic: a sequent calculus presentation of an intuitionistic propositional calculus. This system, LJ, is taken directly from Dyckhoff [16] and is due to Gentzen [21]. Figure 3 contains a bottom-up presentation of the rules of this logic. We have chosen LJ for two reasons. First, as it is simple it admits an exceptionally clean exposition. So the reader won’t feel cheated, in Appendix A we indicate how the term and proof types can be generalized in a straightforward way to the more complex predicate calculus. But we have a second reason, and that is a simple variant of this logic has certain useful structural properties that we will use to illustrate metatheoretic extensibility via proof-transformations in Section 5.

3.1 Well Formed Formula

Well formed formula (Wffs) of LJ are those terms freely generated from a collection of variables and propositional constructors. We shall assume that the set of propositional constructors is fixed in advance, although this restriction is not strictly necessary. The Wff and proof datatypes could be parameterized over sets of Wff and proof constructors and this can lead to a kind of theory-polymorphic metatheory. We do not explore this possibility though.

To specify variables, we will take as given in the framework logic a type Atom which is a collection of names that may be associated with variables.^{1} The decision not to represent variables using variables in the framework logic is deliberate and will be discussed in detail in Section 6 where we compare this to the alternative, which is used in frameworks like ELF. The

1This may be a base type of strings in the framework logic (e.g., the type of strings Atom in Nuprl’s type theory), or alternatively defined as a type of elements whose equality relation is decidable. We take such an approach to defining function and predicate names in the appendix.

WFF ˆ=

Wff:T ype # V ar:Atom → Wff # F alse:Wff # And : Wff × Wff → Wff # Or : Wff × Wff → Wff # Imp : Wff × Wff → Wff

Figure 4: Propositional Formula ADT

formalization of this as an ADT is given in Figure 4. Recall that this ADT, like all our ADTs, also comes equipped with the appropriate induction and computation principles.

3.2 LJ Inference Rules and Proofs

We have considerable flexibility in how we present proofs as an ADT. In this section we present a simple proof type for LJ and indicate alternatives that differ in their assumptions about the structure of proofs. Alternatives formalizations are significant as different types capture different models (implementations) of theorem proving and support different kinds of metatheoretic reasoning.

We begin with a simple encoding that captures a minimal amount of proof structure; essentially, the relationship between sequents that comprise proofs. It will have some similarities to ELF-style encodings since both explain the meaning of logical constants in the encoded logic through the declarations of constants in the framework logic. However unlike ELF encodings, where each proposition p has its own type of its proof-objects, Tr(p), we define a single type of proofs which we can equip with induction and computation principles.

To represent sequent calculus inference rules we must first define a data-type of sequents. In the system we formalize, a sequent is a pair where first component represents hypotheses and the second the conclusion. Furthermore, hypotheses are unordered and duplication is allowed; this eliminates the need for structural rules. Hence we model hypotheses using multi-sets of Wffs. The second component is simply a Wff.

SEQUENT ˆ= W:WFF → M:MSET → Sequent:T ype # MkSeq:MSet(M(Wff(W))) × Wff(W) → Sequent

Note that due to parameterization, any implementation of sequents depends on how both the Wff and multi-set ADT parameters are instantiated, and of course, the function inhabiting the sequent signature. Also note that by analysis of the component ADTs we may determine what principles may be employed to reason about and compute with sequents. For example, we may split sequents into their components, perform Wff induction on the conclusion, perform multiset induction on the hypothesis set, and so forth. For s a member of the carrier of this type, we will denote its first and second projections by Hyps(s) and Concl(s) respectively.

The LJ proof rules (Figure 3) specify a relationship between tuples of sequents (the premises of the rule) and a sequent (the conclusion). Proof rules have limited applicability and we express constraints and side conditions using dependent Π-types and set-types in the framework logic. The use of set types here is not strictly necessary (one could achieve similar specifications

LJ PROOF ˆ= W :WFF → M:MSET → S:SEQUENT →

LJ:T ype # Seq : LJ → Sequent # Axiom : s_{1} :{s:Sequent|Concl(s) ∈ Hyps(s)} → {p:LJ|Seq(p) = s} # F alseE : s_{1} :{s:Sequent|F alse ∈ Hyps(s)} → {p:LJ|Seq(p) = s} # AndI : p_{1} :LJ

→ p_{2} :{p:LJ|Hyps(Seq(p)) = Hyps(Seq(p_{1}))} → {p:LJ|Hyps(Seq(p)) = Hyps(Seq(p_{1})) ∧ Concl(Seq(p)) = And(Concl(Seq(p_{1})), Concl(Seq(p_{2})))}

# AndE : w_{1} :Wff → w_{2} :Wff → p_{1} :{p:LJ|w_{1} ∈ Hyps(Seq(p)) ∧ w_{2} ∈ Hyps(Seq(p))} → {p:LJ|Hyps(Seq(p)) = Hyps(Seq(p_{1})) + And(w_{1}, w_{2}) − w_{1} − w_{2} ∧ Concl(Seq(p)) = Concl(Seq(p_{1}))}

# OrIL : w_{1} :Wff → p_{1} :LJ → {p:LJ|Hyps(Seq(p)) = Hyps(Seq(p_{1})) ∧ Concl(Seq(p)) = OR(Concl(Seq(p_{1})), w)}

# OrR : w_{1} :Wff → p_{1} :LJ {p:LJ|Hyps(Seq(p)) = Hyps(Seq(p_{1})) ∧ Concl(Seq(p)) = OR(w_{1}, Concl(Seq(p_{1})))}

# OrE : w_{1} :Wff → w_{2} :Wff → p_{1} :{p:LJ|w_{1} ∈ Hyps(Seq(p))} → p_{2} :{p:LJ|w_{2} ∈ Hyps(Seq(p))

∧ Hyps(Seq(p)) − w_{1} = Hyps(Seq(p_{2})) − w_{2} ∧ Concl(Seq(p)) = Concl(Seq(p_{2}))}

→ {p:LJ|Hyps(Seq(p)) = Hyps(Seq(p_{1})) − w_{2} + Or(w_{1}, w_{2}) ∧ Concl(Seq(p)) = Concl(Seq(p_{1}))} # ImpI : w_{1} :Wff

→ p_{1} :{p:LJ|w_{1} ∈ Hyps(Seq(p))} → {p:LJ|Hyps(Seq(p)) = Hyps(Seq(p_{1})) − w_{1} ∧ Concl(Seq(p)) = Imp(w_{1}, Concl(Seq(p_{1})))}

# ImpE : w_{1} :Wff → w_{2} :Wff → p_{1} :{p:LJ|Imp(w_{1}, w_{2}) ∈ Hyps(Seq(p)) ∧ w_{1} = Concl(Seq(p))} → p_{2} :{p:LJ|Hyps(Seq(p_{1})) − Imp(w_{1}, w_{2}) + w_{2} = Hyps(Seq(p))} → {p:LJ|Hyps(Seq(p)) = Hyps(Seq(p_{1}))) ∧ Concl(Seq(p)) = Concl(Seq(p_{2}))}

Figure 5: LJ ADT

using additional axioms to capture these constraints) however they do provide an economy of expression as well as a way of tagging computationally uninteresting parts of the specification. For example, if LJ is the type of proofs, and for p in LJ, Seq(p) represents the sequent proved, then we can formalize AndI in the following way.

AndI : p_{1} :LJ → p_{2} :{p:LJ|Hyps(Seq(p)) = Hyps(Seq(p_{1}))}

→ {p:LJ|Hyps(Seq(p)) = Hyps(Seq(p_{1}))

∧ Concl(seq(p)) = And(Concl(Seq(p_{1})), Concl(Seq(p_{2})))}

This rule takes two members of the proof-type, p_{1} and p_{2} where the sequent proved in p_{2} has the same hypotheses as the sequent proved in p_{1}, and returns a member of the proof-type with the same hypotheses as p_{1} and a conclusion that is the conjunction of the conclusions of p_{1} and p_{2}. Other rules are presented in Figure 3.2.

Within the context of this proof type we may formulate the type of provable Wffs as follows.

Thm(w) ˆ= {p:LJ|Seq(p) = MkSeq(Nil, w)}

Similar in spirit to the ELF, the inhabitants of the carrier LJ encode proofs. For example, if A is the propositional variable V ar(W)(“A”), and similarly for B, then

ImpI(A, ImpI(B, axiom(MkSeq([A, B], A)))

is a member of Thm(Imp(A, ImpI(B, A))).

The LJ proof type specifies a bottom-up style of proof-construction where one works backwards from theorems (under assumptions) to theorems (eventually without assumptions). Of course no orientation is specified by the informal presentation of these proof-rules in Figure 3, and we have the freedom to formalize alternative proof presentations of these rules. Different proof types will capture different models of theorem proving and different metatheories.

To illustrate, let us briefly sketch an alternative formulation, an ADT for a (slightly novel) kind of top-down proofs. The carrier of the ADT will have as members proofs constructed by refinement of goals. Refinement proceeds by the user naming a goal and applying a proof rule; the result is 0 or more subgoals. Goals will not be organized as a tree or stack, but rather as an unordered set (so identical unproven subgoals will be collapsed). Each goal in the set will be a marked sequent, which is a sequent paired with a status indicator of whether it has been refined (Ref ) or is still unrefined (UnRef ). A proof begins with an injection of a Wff into the proof type (with a function we call Goal) and ends when all sequents have been refined. Figure 3.2 contains a partial definition of this proof type. Here MarkedSequents is the carrier of an ADT representing a set of sequents with status. This type has a constructor Mark that given a member of the Sequent type (built with MkSeq) and a status indicator returns a marked sequent. The marked sequent ADT also has defined operators for member addition and deletion. The function IsConjunct is defined by recursion on Wffs and is true when its argument is a conjunction. Similarly LeftConjunct and RightConjunct return the left and right conjuncts of a Wff that represents a conjunction.

Unlike the LJ ADT not all elements of this proof type represent theorems. The theorem type for this ADT could simply be formalized as

Thm(w) ˆ= {p:T op|∀m:MarkedSequents. m ∈ SubGoals(p) ⇒ Refined(m)}

where the proposition Refined(m) is true when the sequent m is marked as refined.

Formalizing different models of theorem proving is interesting in its own right; it can bring into focus how the logic will be used in theorem proving. Assumptions can be made explicit such as whether proofs are constructed top-down, bottom-up, or in no particular order, whether they are constructed sequentially or in parallel, whether proof are represented by trees, DAGS, stacks, and so forth. Metatheoretically, as we alter the proof type, we change what concepts we can express and what properties of encoded proofs we can prove in our framework logic. For example, within the context of the top-down proof type we can reason about incomplete proofs and routines (e.g., tactics) that extend and possibly complete these proofs. This is not possible with our LJ proof type. Our belief is that, in the broad sense of the word, the “metatheory” of a logic can go far beyond simply a theory of derivable rules and the more of a logic that we formalize the better we can reason about it.

4 Derived Rules

In the previous section we demonstrated that given our encoding of proof terms we can formulate a type of theorems in a straightforward way. All members of the LJ proof type are theorems, and members of TOP are theorems when all sequents are marked as refined. In both cases,

Top:T ype

# SubGoals : Top → MarkedSequents

# Goal : w:Wff

→ {p:Top|SubGoals(p) = {} + Mark(MkSeq(Nil, w), UnRef)} # Axiom : s_{1} :{s:Sequent|Concl(s) ∈ Hyps(s)}

→ p_{1} :{p:Top|Mark(s, UnRef) ∈ SubGoals(p)}

→ {p:Top|Subgoals(p) = Subgoals(p_{1}) − Mark(s, UnRef) + Mark(s, Ref)} # F alseE : s_{1} :{s:Sequent|F alse ∈ Hyps(s)}

→ p_{1} :{p:Top|Mark(s, UnRef) ∈ SubGoals(p)}

→ {p:Top|Subgoals(p) = Subgoals(p_{1}) − Mark(s, UnRef) + Mark(s, Ref)} # AndI : s_{1} :{s:Sequent|IsConjunct(Concl(s))}

→ p_{1} :{p:Top|Mark(s, UnRef) ∈ SubGoals(p)}

→ {p:Top|Subgoals(p) = Subgoals(p_{1}) − Mark(s, UnRef) + Mark(s, Ref) +Mark(MkSeq(Hyps(S), LeftConjunct(Concl(s_{1}))), UnRef) +Mark(MkSeq(Hyps(S), RightConjunct(Concl(s_{1})), UnRef)))}

# AndE : w_{1} :Wff

→ w_{2} :Wff

→ s_{1} :{s:Sequent|And(w_{1})(w_{2}) ∈ Hyps(s)} → p_{1} :{p:T op|Mark(s, UnRef) ∈ SubGoals(p)} → {p:Top|Subgoals(p) = Subgoals(p_{1}) − Mark(s, UnRef) + Mark(s, Ref)

+ Mark(MkSeq(Hyps(S) − And(w_{1}, w_{2}) + w_{1} + w_{2}, Concl(s_{1})), UnRef)}

...Other Proof Rules Similar

Figure 6: Top Down “Unstructured” LJ ADT

we can construct proofs for the encoded logic by demonstrating that these theorem types are inhabited in the framework logic. This is similar to the conventional uses of type theory as a logical framework. In this section we shall indicate how representing logics with ADTs provides a basis for metatheoretic reasoning that extends beyond simply capturing provability.

The most common method of augmenting an implementation of a logic with metatheoretic capabilities is to extend it with a metalanguage for writing tactics, which are programs that construct and manipulate proofs. Many theorem proving systems, for example LCF, HOL, and Nuprl, take this approach. Each is equipped with a programming language (in all three cases ML), and an interface between this language and the proof engine. This interface typically consists of types for object-logic syntax (e.g., terms, sequents, proofs) and functions that manipulate and construct members of these types. This approach to metareasoning can be directly used within our framework when the implementation of the framework logic supports a metalanguage. This capability is not unique to our approach and is shared by other approaches to logical encoding.

But there is an alternative that appears to be possible when two conditions are met. Specifically,

1. the framework logic is a programming logic, and

2. logics have been encoded in a way that renders it possible to reason about the encodings and define functions over them.

When the first condition is satisfied, which it is when the framework logic is a constructive type theory, then the logic itself is expressive enough to serve as both its own metalanguage and metalogic. When the second condition is also satisfied, which it is when induction and computation axioms are provided for the encoded data-types, we can use this metalogic to reason about the logical encodings and functions defined over these encodings. Functions may be defined explicitly (using the appropriate axiomatized recursion combinators), or alternatively built implicitly by constructive inductive proofs (e.g., the proofs-as-programs paradigm). These functions can implement general kinds of derived inference rules including term normalizers, decision procedures, and the like.

The approach to constructive metatheory we are proposing is very similar in spirit to the kind of metatheory developed in [24, 13] in which term rewriters, matchers, and normalizers, were implemented and formally reasoned about within the Nuprl type theory. The primary difference is that in the Cornell work, the metatheory was about a specific encoding of terms (e.g., Nuprl terms in [24]) and to be used in Nuprl theorem proving a connection had to be made between the encoded terms and Nuprl’s terms. Under our approach, data-types such as terms and proofs are specified within the context and metatheorems are never used at the “object level” (e.g., we never work with implementations of the encoded logic) so there are no difficulties involving reflection or moving between syntactic entities and their encodings. Derived rules are simply theorems about properties of the relevant proof types and functions defined over these types and are used to construct and manipulate members of these types within the framework logic. (More will be said on these points in Section 6.)

In this section we provide a simple example: a derived inference rule about the provability of a subclass of propositional Wffs. We take this example directly from Weyhrauch [43] where he states:

If you have a propositional Wff whose only sentential connective is the equivalence sign, then the Wff is a theorem if each sentential symbol occurs an even number of times.

Weyhrauch stated his theorem for a logic in which the Wff type includes the “iff” connective (which we denote by the prefix binary relation Iff ) and the proof system is classical. We can easily extend our Wff type (with this connective) and LJ proof type (with the rule of excluded middle) to encode this desired logic. Let C denote the context containing declarations of these types as well as definitions of the supporting ADTs. Furthermore, let parity be a function of type Wff → {0..1} that returns 1 exactly when its argument is built only from the Iff connective and variables, and furthermore, each variable occurs exactly an even number of times. This can be defined using the Wff recursion combinator in a straightforward way.

Now, within this context, we may formalize Weyhrauch’s theorem as

C ⊢ ∀w:Wff. parity(w) = 1 ⇒ T hm(w).

Let us sketch a constructive proof of this by induction on the complexity of the expression w. Given a Wff w such that parity(w) = 1, then w is a term built from Iff that must contain at least two occurrences of the same variable. Call this variable a; there are two cases. The first is w = Iff (a, a), but then we are done as C ⊢ T hm(Iff (a, a)) is provable. In the second case, w must contain more than one Iff connective. Then, because Iff is associative and commutative, we can rearrange and reassociate the variables in w to “shuffle” together two occurrences of a. More formally, there must be Wff w′ such that parity(w′) and

C ⊢ T hm(Iff (Iff (a, a), w′) ⇔ T hm(w).

Furthermore, we can “cancel” the Iff (a, a), that is

C ⊢ T hm(w′) ⇔ T hm(Iff (Iff (a, a), w′)).

Since parity(w′) = 1 and w′ is simpler (e.g., fewer variables) than w, we have Thm(w′) by the induction hypothesis. Hence, we can conclude Thm(w).

The above proof sketch should be formalizable within our framework logic in a straightforward way. Formalizing the theorem statement requires that we can define the parity function by recursion over the structure of Wffs. This is not difficult and can for example be implemented by a function which makes several passes over its Wff argument: first to check the connective structure and second to gather up the variables at the leaves to verify that each occurs an even number of times. Formalizing the proof requires reasoning about Wffs (and the parity) function) using the Wff induction principle. In particular, we must be able to derive alternative induction schemas such as induction over well-founded measures on Wffs. In the above proof, this measure would be the number of variables in the formula. Complete induction over this well-order (although not all well-orders) is interderivable with our axiomatized structural induction principle for Wffs.

A proof of the parity theorem will (within a constructive framework logic) construct a function that itself constructs proofs. Specifically, let par be a function inhabiting the type of the parity theorem and let w be a member of Wff such that parity(w) = 1. The existence of par formally asserts that w is provable and we may use this assertion in other proofs. Moreover, should we actually require the proof of w, we may generate it by evaluating par.

5 Proof Theory

The implementation of the object theory lets one investigate whether a specific proposition is provable. The metatheory lets us investigate whether there is a general method of settling the provability of a class of propositions, and whether there is even a good method for doing this.

For the IPC, Intuitionistic Propositional Calculus, there are well-known algorithms to decide provability. The first is due to Gentzen, based on his Hauptsatz, but it is not a good method. Basically he suggests searching the space of all possible proofs up to a certain depth. We can consider this space to be an infinite tree whose nodes are sets of sequents and whose edges are labeled by the rule name used to replace a sequent, call it the goal, by a finite number of subgoal sequents. We are thinking then of generating proofs top-down, and it is natural to use a top-down proof type. This tree of all possible proofs will contain any proof that exists, and if we knew that any proof must occur within a certain depth, then we could just search to that depth, which is a finite process. But indeed we do know from the Hauptsatz that we only need to search to a finite depth. Namely we know that if there is a proof, then there is one which uses only subformulas of the goal. Moreover, if in the search for a proof in the tree we encounter a node whose set of sequents appears earlier on the same path, then we can terminate the search along that path. Since only subformulas can appear in the sequents, there are only finitely many different nodes that can occur in this tree, so along any path, either we find a proof or repeat a node thus ending the search. Moreover we can precompute the depth at which this repetition must occur, so the argument is constructive.

For the classical propositional calculus, PC, there is a much simpler proof search strategy. First every rule can be seen to decompose a goal sequent into simpler sequents in that the formulas occurring in the subgoal sequents are all of smaller complexity than those in the goal. So the termination argument can be given in terms of a multiset ordering on the sets of sequents occurring at the nodes in the tree of all possible proofs. In addition, there is a fixed order for applying the rules which is guaranteed to work if any order does, so we need search only one path

Γ, C ⇒ (D ⇒ B) ⊢ G ; ImpE_{1} ; Γ, (C ∧ D) ⇒ B ⊢ G  Γ, C ⇒ B, D ⇒ B ⊢ G ; ImpE_{2} ; Γ, (C ∨ D) ⇒ B ⊢ G

Γ, D ⇒ B ⊢ C ⇒ D Γ, B ⊢ G ; ImpE_{3} ; Γ, (C ⇒ D) ⇒ B ⊢ G  Γ ⊢ G ; ImpE_{4} ; Γ, F alse ⇒ B ⊢ G

Γ, B, A ⊢ G

ImpE_{5} (for A atomic)

Γ, A ⇒ B, A ⊢ G

Figure 7: LJT Rules Replacing ImpE

in this tree. With these observations one is led to the tableau search procedure for example.

It is natural to ask whether there is a similar proof search procedure for the IPC. The complication is that Gentzen’s original system, LJ, uses the implication elimination rule

{H, A ⇒ B ⊢ A H, B ⊢ G \atop H, A ⇒ B ⊢ G}

and the subgoal sequent H, A ⇒ B ⊢ A might in fact be more complex than the goal sequent if A is more complex than G. So one cannot use a multiset ordering. Various methods have been discovered to circumvent this difficulty. One can compute the number of times the formula A ⇒ B needs to be used for example. Roy Dyckhoff has discovered a method [16], and in his paper he surveys other ones and recommends the source [15]. His idea is to replace the implication elimination rule with the five others given in Figure 7; he calls the resulting in the system he calls LJT In LJT all rules generate simpler subgoal sequents so that termination of the proof search can be guaranteed via the multiset ordering. He proves:

A formula of IPC is provable in LJ iff it is provable in LJT.

Here is a metamathematical result which is very useful. It is the basis for a good decision procedure for the IPC. Indeed Dyckhoff has implemented such an algorithm for the system MacLogic (see [17]). Suppose then that in an implemented object logic based on LJ one is looking for a decision procedure for IPC formulas. If we restrict ourselves to derived rules based on LJ, we will not find Dyckhoff’s method. But if we can prove metatheorems like his in the metalogic, then we can use them. So for instance, from a constructive proof of his theorem, we can build a decision procedure which takes a formula G, applies Dyckhoff’s procedure to find an LJT proof or report that there is no proof. If there is no LJT proof, then we know there is no LJ proof either, so we report failure. If there is an LJT proof, then by the constructive nature of the proof of the metatheorem, we can transform it to an LJ proof as required.

Indeed Dyckhoff’s result can be proved constructively. We outline such a proof below and suggest in a bit more detail how a formalization of it in type theory is used. First define the depth of a formula as follows:

depth(A) = depth(F alse) = 1 for A atomic,
depth(A ∨ B) = depth(A ⇒ B) = depth(A) + depth(B) + 1,

depth(A ∧ B) = depth(A) + depth(B) + 2.

This introduces an ordering on formulas. We extend it to an ordering on multisets of formulas in the natural way, namely B_{1} ≪ B_{2} iff B_{1} is obtained from B_{2} by replacing formulas in B_{2} by a finite set of those of smaller depth.

We prove two separate theorems:

Theorem 1 If a formula G of IPC is provable in LJ, then it is provable in LJT.

Theorem 2 If a formula G of IPC is provable in LJT, then it is provable in LJ.

We only need Theorem 2 to be proved constructively, but in fact constructive proofs of each theorem are just as clear and compact as classical proofs and provide more information, so we prove them this way. For Theorem 1 we follow Dyckhoff and prove a lemma about how to postpone uses of implication elimination. First a definition.

Definition 1 Call a proof awkward iff the final step is an elimination on A ⇒ B where A is atomic and does not occur as an hypothesis (i.e. on the left side of the sequent).

Lemma 1 If Δ ⊢ G is provable in LJ, then it has a nonawkward proof.

Proof: Let P be a proof of Δ ⊢ G, proceed by induction on the structure of P, i.e., by the induction rule provided by the proof data type. If it is not awkward we are done, so suppose it is, and the last step is

{Γ, A ⇒ B ⊢ A Γ, B ⊢ G \atop Γ, A ⇒ B ⊢ G}

where A is atomic and does not occur in Γ. Let P_{A} be the subproof of A from Γ and A ⇒ B. This must end with an elimination step since A is atomic and does not occur in Γ. We consider all (four) ways that this can happen, which are: False-elim, ∧-elim, ∨-elim and ⇒-elim. In each case we show how to build a nonawkward proof.

1. If the rule is False-elim, then F alse occurs in Γ. So we can use False-elim to prove Δ ⊢ G in the first place. Call this proof P′, it is not awkward.

2. If the rule is ∧-elim, say on C ∧ D, then the proof looks like

{{Σ, C, D, A ⇒ B ⊢ A \atop Σ, C ∧ D, A ⇒ B ⊢ A} Σ, C ∧ D, B ⊢ G \atop Σ, C ∧ D, A ⇒ B ⊢ G.}

Change this to the nonawkward proof P′

Σ, C, D, A ⇒ B ⊢ A Σ, C, D, B ⊢ G ; {Σ, C, D, A ⇒ B ⊢ G \atop Σ, C ∧ D, A ⇒ B ⊢ G.}

We know that there is a proof of Σ, C, D, B ⊢ G because we can cut in the formula C ∧ D and use the given proof of Σ, C ∧ D, B ⊢ G known by our assumption on the shape of P. Then we obtain the proof P′ we need by cut elimination on this subproof.

3. If the rule is ∨-elim, say on C ∨ D, then the proof looks like

{{Σ, C, A ⇒ B ⊢ A Σ, D, A ⇒ B ⊢ A \atop Σ, C ∨ D, A ⇒ B ⊢ A} Σ, C ∨ D, D ⊢ G \atop Σ, C ∨ D, A ⇒ B ⊢ G}

This can be converted to

\begin{matrix}{Σ, C, A ⇒ B ⊢ A Σ, C, B ⊢ G \atop Σ, C, A ⇒ B ⊢ G} & {Σ, D, A ⇒ B ⊢ A Σ, D, B ⊢ G \atop Σ, D, A ⇒ B ⊢ G} \\ Σ, C ∨ D, A ⇒ B ⊢ G \end{matrix}

The sequent

Σ, C, B ⊢ G

can be proved by just cutting in C ∨ D which requires proofs of Σ, C, B, C ∨ D ⊢ G and Σ, C, B ⊢ C ∨ D. The first one can be proved by weakening to remove the hypothesis C and then using the proof of Σ, D, B ⊢ G. Call this proof P̂. A similar modification is used to produce say P̄ which proves Σ, D, B ⊢ G.

4. If the rule is ⇒-elimination, say on C ⇒ D, then the proof looks like

\begin{matrix}\begin{matrix}{P_{A} \atop Σ, D, A ⇒ B ⊢ A} & {P_{C} \atop Σ, C ⇒ D, A ⇒ B ⊢ C} \\ Σ, C ⇒ D, A ⇒ B ⊢ A \end{matrix} & {P_{B} \atop Σ, C ⇒ D, B ⊢ G} \\ Σ, C ⇒ D, A ⇒ B ⊢ G \end{matrix}

Since we have already transformed the subproof of Γ, A ⇒ B ⊢ A to be nonawkward, we know that in the proof of Σ, C ⇒ D, A ⇒ B ⊢ A, C is either nonatomic or occurs in Σ. We now convert the given proof P so that the last step is by elimination on C ⇒ D. This step is not awkward. This produces the left subgoal of showing Σ, C ⇒ D, A ⇒ B ⊢ A and the right subgoal of showing Σ, D, A ⇒ B ⊢ G. The left subgoal can be proved from one of the subproofs of P and the right one is proved by elimination on A ⇒ B. One of the subgoals here is proved using a subproof of P and the other one, Σ, D, B ⊢ G is proved by cutting in C ⇒ D and applying cut elimination to the resulting proof. □

Now Theorem 1 is proved by induction on the multi-set ordering using the lemma, and Theorem 2 is proved by induction on the proof structure using cut followed by cut elimination. The straight forward proofs here are constructive.

Let LJT P roof(G) denote those LJT proofs of G, likewise for LJP roof(G). Then Dyckhoff’s decision procedure can be derived from a proof of the following theorem. First let S be a list of IPC formulas, say H_{1},...,H_{n}, G. We regard it as a sequent with goal G and the other formulas as hypotheses and write LJT P roof(S) for the set of its LJT proofs.

Theorem 3 Given any set {S_{1}, …, S_{n}} where S_{i} is a sequent over IPC formulas, we know for each S_{i} that ∃p : LJT P roof(S_{i}) ∨ ¬∃p : LJT P roof(S_{i}).

Corollary 1 For all formulas G of IPC either there is an LJT proof of it or not.

The corollary is proved by taking {G} as the set of formulas in the theorem. The theorem is proved by the multi-set induction defined above. For each S_{i} we consider all possible rules r that can be applied, noting that each one decomposes S_{i} into {U_{1}, …, U_{k}} for which the induction hypothesis holds. If the U_{j} are all provable for some rule r, then S_{i} is. If not, then there is no rule for proving S_{i}, so there is no proof of it.

The constructive proof of Theorem 3 and its corollary provides a function from formulas into a disjoint union. If the result is in the left disjunct, then we can pull out a proof of the formula; if it is in the right disjunct, then we know there is no proof (and if we wanted to we could pull out the evidence for this conclusion). So Theorem 3 gives a decision procedure for provability and a proof generating procedure for true formuals. The constructive proofs of Theorem 2 and Theorem 1 provides functions J : LJT P roofs ⇒ LJP roofs and T : LJP roofs ⇒ LJT P roofs. With these we can prove another corollary.

Corollary 2 For all formulas G of IPC either there is an LJ proof of it or not.

6 Comparison To Other Work

We conclude with a brief comparison to closely related work. First, we compare our framework logic with other frameworks, both in terms of the logic itself and how we encode logics within it. After, we discuss how our approach relates to other research in metatheory.

6.1 Framework Logics and Logical Encodings

Framework logics such as the ELF and Isabelle were designed with concerns different from metatheoretic reasoning and they are too weak to support it. Furthermore, as their concerns are different, logics are encoded within these frameworks in a way that does not support metatheoretic analysis. Let’s address these points individually.

The logical basis of the framework we propose is a constructive type theory and in this respect it is most similar to the LF logic of the ELF system. However, LF was designed to be as weak as possible (e.g., one cannot abstract over members of T ype) to make faithfulness and adequacy proofs easier. But this minimality only supports a very weak kind of metatheory, e.g., one can demonstrate that specific formulas have proofs. Both Taylor and Pollack, who have proved theorems about LF encodings (as reported in [41]), have had to formalize their proofs within the stronger Calculus of Constructions. Other framework logics, such as Isabelle and λ-Prolog, are based on higher-order intuitionistic logic and lack the propositions-as-types correspondence. Hence, demonstrations of provability do not construct proofs, and any kind of metatheoretic reasoning within the framework (none has been tried to our knowledge) would not construct functions over proofs. Furthermore, these logics do not provide a unified view of the relationship between the specification of a logic and its implementation.

Equally significant as differences in logics are differences in the way that they are used. Within the frameworks mentioned above one seeks to encode logics in a manner that internalizes parts of the structure of terms and proofs within the framework logic. By this we mean that syntactic notions and operations are subsumed by operations implemented in the framework logic. The alternative to this identification is to externalize these entities and operations by explicitly encoding syntax and functions over syntax.

The standard example of internalization is representing variable binding by λ-abstraction in the framework logic so that substitution can be implemented by β-reduction; supporting this internalization is one of principles behind the design of these framework logics. It is true that this has the advantage of liberating the logic encoder from concerns about substitution, bound variable renaming, and the like. But from a metalogical perspective, this choice seems inappropriate since it obscures the separation between the encoded logic and the framework logic; the terms in the framework logic which represent the terms and proofs of the encoded logic combine both meta and object level syntax. One can no longer view a logic’s presentation as a specification of an implementation. More importantly, the logic’s presentation cannot easily be the subject of metatheoretic analysis because analyzing variables and operations on them requires reasoning about the framework logic itself. It is no coincidence that most experiments in metatheoretic reasoning have picked algebraic problems (e.g., Taylor’s associative term-equality example [41]) that do not require such analysis.

Internalization manifests itself in other ways as well. Consider for example, the difference between how we formulate inference rules in the LJ proof type (Section 3.2), and how these rules would be formulated in the ELF-style. In ELF, AndI would be formulated natural deduction style along the lines of

AndI : ∀A, B:Wff. Tr(A) → Tr(B) → Tr(And(A, B)).

This rule is simpler than ours, but that is because it effectively internalizes much of the structure of proofs; rather than formalizing and reasoning about an explicit representation of proofs, which requires explicitly formalizing sequents (in the case of the sequent calculus) or assumption dependencies and discharging (in the case of natural deduction) and the like, these concepts are instead captured by the meaning of implication in the framework logic. Again there are tradeoffs. This style of natural deduction presentation has advantages in that it allows rapid specification and prototyping of theorem provers. But again, it is unsuitable for our needs. First, it is not always possible to find an ELF-style encoding, especially for more exotic consequence relations. It should, we suspect, be straightforward to directly describe the inference rules and proofs of a very wide range of logics using ADTs. Second, unlike our rules, ELF-style proof-rules cannot be seen as specifying an implementation of the logic, except in an indirect way via an interpreter for proof construction in the framework logic. Finally, there is a significant difference in our approaches when it comes to metareasoning. Since we specify a single inductively constructed proof type (as opposed to a family of proof types parameterized by Wffs), we can equip it with induction and computation rules which are necessary for most nontrivial kinds of metatheory.

With respect to encoding style, the use of the framework logic F S_{0} (as proposed by Feferman in [18] and carried out by Matthews [31]) is closest to our approach. F S_{0} is a theory of functions and classes of expressions embedded in second-order predicate calculus. The basic data-type is the S-expression and through this one defines by inductive definition the classes of formulas and proofs for desired logics. As with our approach, functions may be defined by primitive recursion (on S-expressions) and reasoned about by induction. F S_{0} appears to be designed as a minimal logic for allowing such reasoning (it is a conservative extension of primitive recursive arithmetic). By necessity, one cannot mix the syntax of the encoded logic and the framework logic; all notions of syntax must be explicitly encoded using S-expressions. In practice, this does not appear to cause significant problems. In [32] an example is provided about how one can formalize and reason about bound variables in F S_{0} in the context of a prenex normal form theorem for predicate calculus. The conclusion there, which we find comforting, is that this kind of formalization and reasoning is not as hard as is commonly assumed. It is worth noting that the F S_{0} account could be given directly in type theories such as Nuprl using inductive types to define terms and formulas.

6.2 Categorical Logics

Category theory like type theory is a unifying general language. Computer scientists have also found it a suitable context for investigating the basic questions being addressed here, such as what is a logic, what is an implementation, and so forth [23, 33, 28]. Moreover category theory has been the language of choice for some of the pioneering work on how to combine and relate large structures such as theories [10, 11]. It is also the standard setting in which to frame the algebraic approach to data types [7].

Our use of ADT’s to define logics shows a clear and simple connection to the study of algebraic data types in a general setting. The closest related work in categorical logic is Burstall and Goguen’s abstract account of model theory as institutions [23] and Meseguer’s abstract account of proof calculi and general logics [33]. Our approach has concentrated on proof theory, but the generality of type theory suggests ways of expressing many of the concepts from institutions. In relation to the categorical account of proofs, we can say that our approach is more concrete, for example our notion of an LJ proof is far more specific than Meseguer’s notion of an effective proof subcalculus. We have not tried to say what a proof calculus would be in general.

We are not aware of work in categorical logic which is directed at generalizing or supporting metamathematics. But the formulation of logic in categorical terms may help us see how to generalize our account of metamathematics.

6.3 Metatheory

Cornell work Our approach to formalized metareasoning bears closest resemblance to the research program on constructive metatheory carried out at Cornell. In [13], Constable and Howe demonstrate how one can synthesize tactics, decision procedures, and the like, through theorem proving in the Nuprl system. In [24], Howe describes a substantial implementation of this kind of approach in which theorems were proved about representations of Nuprl terms (e.g., that one could rewrite and normalize such terms). Moreover, Howe’s development included a means of associating representations of Nuprl terms, with Nuprl terms themselves, so his verified tactics and procedures could be applied to construct Nuprl proofs.

Another line of research was that of Constable and Knoblock [27] in which they formalized the structure of Nuprl proofs within an extension of Nuprl, called Nuprl^{1} which contained data types for Nuprl terms and proofs. So again one could prove theorems about proofs and construct tactics by theorem proving. They, in fact, defined a hierarchy of metalogics, Nuprl^{i} each one the object logic of the one above it. Recent work [2] has refined this technique, providing a single proof type (as opposed to a hierarchy of proof types) within Nuprl that refers to itself and can be formally reasoned about within the Nuprl system.

The kind of metatheory that we propose in this paper is similar in spirit to the previous Cornell research, but differs in several significant respects. First, the Cornell work has been concerned with encoding the terms and proofs of a specific logic (e.g., Nuprl) with specific types, and developing metatheory over these types. Here we are suggesting that this approach generalizes and can be used for a wide variety of logics. Moreover, we propose that this can be done in an abstract way (using ADTs) that does not commit the logic encoder to choose a specific representation in the framework logic. Of course, the downside of this abstraction is that we cannot directly compute over our representations of terms and proofs as can be done with the more direct Nuprl encodings.

A second important difference is that the Cornell work has been concerned with using such encodings by means of some kind of reflective mechanism. That is, to use the results of their metatheory, a connection must be made between representations of Nuprl terms and proofs (and statements proved about them) and actual Nuprl syntax. Here we suggest that all theorem proving can be done at one level: the metalevel. Although our encodings can be seen as specifying an implementation of that logic, no implementation ever need be constructed; instead all reasoning (about provability, derived rules, etc.) can take place within the framework logic. Hence, reflection is not central to our work since there is only one theory, the framework theory.

It is of course possible to propose that the framework logic be reflective (indeed if one were using Nuprl it would be). The advantages of using reflection in any practical formalization is one of the themes of the Cornell work, but we are not considering these practical concerns here. Moreover, it is interesting to consider an ADT account of object theories which are reflexive. We have not carried this out, but it is a line of inquiry which is in the spirit of this paper. The significant point is that one might be able to reduce the amount of detail needed in any reflexive axiomatization by separating the specification from its many possible implementations.

FOL approach A quite different approach to metatheory has been undertaken in the FOL system [43] and its ancestors. FOL is a first-order logic that supports multiple logical theories. In particular, one such theory may be a metatheory about first-order logic in which theorems may be proven about representations of first-order formula. One moves between these theories using a reflection principle. In the original FOL system, metalevel axioms were simply asserted; however the system has been redesigned (and renamed as GETFOL) in a way that these can be generated in a sound manner from an analysis of the implementation [22, 6]. Whereas for us, the metatheoretic encoding is primary, the GETFOL approach suggests that, at least in some instances, one can take a complementary view and generate a metatheory from an implementation coded in a certain way. The GETFOL work is ongoing, however, and it remains to be seen how general the GETFOL methodology is.

A Appendix: Predicate Calculus

In this appendix we give a brief account of how terms, formulas, and proof rules that involve side conditions on variables may be formalized within the ADT setting. The account we give here is fairly standard and closely follows [20, 42].

We begin by defining the terms of the predicate calculus which are built from variables and function applications. Function names are specified by an ADT FNAME that has an associated arity function and a decision procedure for equality of names. 0-ary functions are constants.

F NAME ˆ=
F name : T ype
# Arity : F name → Nat
# ∀x, y:F name. x = y ∨ x ≠ y

Note that we don’t insist that members of F name are enumerable. This could be added if required in the metatheory. The ADT of terms may now be given.

T ERM ˆ= fn:F NAME →
T erm : T ype
# V ar : Atom → T erm
# F unc : f:F name(fn) × NT uple(Arity(f), T erm) → T erm

NT uple(n, T) is the type of n-tuples with members from the type T.

To define Predicate Calculus Wffs we need an ADT of predicate names, PNAME, which is defined similarly to FNAME. Wffs are parameterized by predicate names and the T erm type.

W F F ˆ= f:F NAME → pn:P NAME → t:T ERM →

Wff : T ype # AWff : p:P name(pn) × NT uple(Arity(p), T erm(t)) → Wff # IMP : Wff × Wff → Wff # ALL : Atom × Wff → Wff ...other connectives defined similarly

To define proof rules for terms of the predicate calculus we must formalize the concept of free variables, eigenvariables, and substitution. All of these may easily be defined by recursion on Term and Wff using the induction principles these ADTs are equipped with. We use considerable syntactic sugar in the definitions that follow.

Let SET (Atom) be the ADT of sets parameterized by the type of variables Atom with carrier Set. Define F V_{T} on terms as follows.

\begin{aligned}F V_{T} (x) & = & \{x\} \\ F V_{T} (f(t_{1}, ...t_{n})) & = & F V_{T} (t_{1}) ∪ ... ∪ F V_{T} (t_{n}) \end{aligned}

where the arity of f is n. Similarly define F V on Wffs by the following equations.

\begin{aligned}F V (p(t_{1}, ..., t_{n})) & = & F V_{T} (t_{1}) ∪ ... ∪ F V_{T} (t_{n}) \\ F V (p_{1} → p_{2})) & = & F V (p_{1}) ∪ F V (p_{2}) \\ F V (∀a. p_{1}) & = & F V (p_{1}) − \{a\} \end{aligned}

Substitution must be defined both on formulas on terms. On terms, we define a substitution function which we shall display as t_{1}[t_{2}/x]_{T}.

y[t/x]_{T}  = if y = x then t else y
f(t_{1}, ..., t_{n})[t/x]_{T} = f(t_{1}[t/x]_{T} , ..., t_{n}[t/x]_{T})

Substitution on formulas will be displayed as f[t/x] and is as follows.

P (t_{1}, ..., t_{n})[t/x] = P (t_{1}[t/x]_{T} , ..., t_{n}[t/x]_{T})
(p_{1} → p_{2})[t/x] = p_{1}[t/x] → p_{2}[t/x]
(∀y.B)[t/x]  = if x = y then ∀y.B else ∀y.(B[t/x])

We say that a term t is free for a variable x in a Wff p when when t can be substituted for occurrences of x in a capture avoiding way. We define the propositional function F reeF or as follows.

F reeF or(t, x, p(t_{1}, ..., t_{n})) = T RUE (For T RUE an non-empty type)
F reeF or(t, x, p_{1} → p_{2})  = F reeF or(t, x, p_{1}) ∧ F reeF or(t, x, p_{2})
F reeF or(t, x, ∀y.p)  = x = y ∨ x ≠ y ∧ ¬(y ∈ F V (t)) ∧ F reeF or(t, x, p)

In addition, to formalize proof rules we will need to know when a variable can be serve as an eigenvariable; that is, when it does not occur free among the hypotheses Γ = [h_{1}, ..., h_{n}] of a sequent.

EigenV ar(Γ, x) = ¬y ∈ (F V (h_{1}) ∪ ... ∪ F V (h_{n})).

We conclude by indicating how a proof-type may be formalized for intuitionistic predicate calculus. This can easily be accomplished by slight modification to the type LJ PROOF given in Figure 3.2. Specifically, parameterize this type over the newly defined Wff type instead of the type of propositional Wffs. The rules of propositional calculus hold in predicate calculus so they carry over directly. We must add rules for quantifier introduction and elimination such as the following.

Γ ⊢ P ; AllI ; Γ ⊢ ∀x.P  Γ, P [t/x] ⊢ G ; AllE ; Γ, ∀x.P ⊢ G

Both rules have side-conditions. In the first, we insist that EigenV ar(Γ, x) holds. In the second, we must have that F reeF or(t, x, P) holds. Adding these rules is straightforward. We extend our proof type with the following two conjuncts.

# AllI : x:Atom
→ p_{1} :{p:LJ|EigenV ar(Hyps(Seq(p)), x)}

→ {p:LJ|Hyps(Seq(p)) = Hyps(Seq(p_{1})) ∧ Concl(Seq(p)) = All(x, Concl(Seq(p_{1})))}

# AllE : w_{1} :Wff
→ w_{2} :{w:Wff|IsAll(w) ∧ F reeF or(w_{1}, AllV ar(w), (AllBody(w))}
→ p_{1} :{p:LJ|AllBody(w_{2}[w_{1}/AllV ar(w_{2})]) ∈ Hyps(p_{1})}
→ {p:LJ|Hyps(Seq(p)) = Hyps(Seq(p_{1}) − AllBody(w_{2}[w_{1}/AllV ar(w_{2})]) + w_{2}
∧ Concl(Seq(p)) = Concl(Seq(p_{1}))}

Here, the auxiliary function IsAll is true when its argument is a universally quantified Wff. AllV ar and AllBody decompose ∀x.P into the binding variable x and the body P.

Note that there are alternative ways to formalize these rules. In particular ∀-introduction is often formulated to allow the user to choose the name of the eigenvariable. Another option is that in ∀-elimination, rather than restricting w_{2} to instances where F reeF or is true, one may appropriately rename bound variables so that the substitution is made in a capture avoiding way.

Acknowledgements

We gratefully acknowledge discussions with Nax Mendler, Alan Smaill, and Sean Matthews. Frank Pfenning provided helpful comments on a draft of this paper.

References

[1] Peter Aczel. Term Declaration Logic and Generalized Composita Proceedings of the Symposium on Logic in Computer Science. IEEE, Washington, DC, 1991.

[2] Stuart F. Allen, Robert L. Constable, Douglas J. Howe, and William E. Aitken. The semantics of reflect proof. In Symposium on Logic in Computer Science, Computer Society Press of the IEEE, 1990.

[3] Roland Backhouse, Paul Chisholm, Grant Malcolm, and Erik Saaman. Do-it-yourself type theory. Formal Aspects of Computing, 1(1):19–84, 1989.

[4] Jon Barwise. Axioms for abstract model theory. Ann. Math. Logic, 7:221-265, 1974.

[5] Jon Barwise and Solomon Feferman (editors). Model-Theoretic Logics. Springer-Verlag, NY, 1985.

[6] David Basin, Fausto Giunchiglia, and Paolo Traverso. Automating meta-theory creation and system extension. In AI*IA-91 (Italian Association for Artificial Intelligence, Palermo, Italy, 1991. To Appear.

[7] Jan Bergstra and John Tucker. Characterization of computable data types by means of a finite equational specification method. In Automata, Languages and Programming. Lecture Notes in Computer Science, vol 81, Springer-Verlag, NY, 1980, 76-90.

[8] N.G. de Bruijn. A survey of the project Automath. In To H.B. Curry: Essays in combinatory logic, lambda calculus and formalism. Academic Press, Reading, 1980,579-606.

[9] Rod Burstall. Computer Assisted Proof for Mathematics: an Introduction Using the LEGO Proof System. Technical Report ECS-LFCS-91-132, University of Edinburgh, 1991.

[10] Rod M. Burstall and Joseph A. Goguen. Putting theories together to make specifications. In 5th IJCAI, pages 1045 – 1058, Boston, Mass, 1977.

[11] Rod M. Burstall and Joseph A. Goguen. The semantics of clear, a specification language. In Advanced Course on Abstract Software Specification, LNCS 86, 1980.

[12] Robert L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986.

[13] Robert L. Constable and Douglas J. Howe. Implementing metamathematics as an approach to automatic theorem proving. In A source book of formal approaches to A.I., North Holland, 1990.

[14] Thierry Coquand and Gérard Huet. The Calculus of Constructions. Information and Computation, 95–120, 1988.

[15] Albert G. Dragalin. Mathematical Intuitionism – introduction to proof theory Translations of mathematical monographs vol. 67. American Mathematical Society, Providence, RI, 1988.

[16] Roy Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. Unpublished Manuscript (submitted to JSL).

[17] Roy Dyckhoff, Neil Leslie, and Stephen Read. MALT st andrews (maclogic – a proof assistant for first-order logic. Computerised Logic Teaching Bulletin, 2(1):51–60, 1989.

[18] Solomon Feferman. Finitary inductively presented logics. In Logic Colloquim ’88, North-Holland, 1988.

[19] Solomon Feferman. Inductively presented systems and the formalization of metamathematics. In D. van Dalen et al, editor, Logic Colloquium ’80, pages 95–128, North-Holland, Amsterdam, 1980.

[20] Jean H. Gallier. Logic for Computer Science. Harper & Row, 1986.

[21] Gerhard Gentzen. The Collected Papers of Gerhard Gentzen. North-Holland, Amsterdam, 1969.

[22] Fausto Giunchiglia and Paolo Traverso. Reflective reasoning with and between a declarative metatheory and the implementation code. In IJCAI ’91, 1991.

[23] Joseph Goguen and Rod Burstall. Institutions: Abstract Model Theory for Computer Science. Technical Report CSLI-85-30 Center for the Study of Language and Information, Stanford University, Palo Alto, CA, 1985.

[24] Douglas J. Howe. Automating Reasoning in an Implementation of Constructive Type Theory. PhD thesis, Cornell University, 1988.

[25] Douglas J. Howe. Computational metatheory in Nuprl. In 9th International Conference On Automated Deduction, pages 238–257, Argonne, Illinois, 1988.

[26] Douglas J. Howe. Equality in lazy lambda calculi In Proc. of the Fourth Annual Symp. on Logic in Computer Science, IEEE.,1990.

[27] Todd B. Knoblock and Robert L. Constable. Formalized metareasoning in type theory. In Proc. of the First Annual Symp. on Logic in Computer Science, IEEE., 1986.

[28] Joachim Lambek and Philip J. Scott. Introduction to Higher Order Categorical Logic. Cambridge University Press, Cambridge, 1986.

[29] F. William Lawvere. Adjointness in foundations. Dialectica, 23:281-296, 1969.

[30] David B. MacQueen. Using dependent types to express modular structure. In Thirteenth Annual ACM Symposium on Principles of Programming Languages, ACM, SIGACT, SIG-PLAN, 1986.

[31] Sean Matthews. Meta-Level and Reflexive Extension in Mechanical Theorem Proving. PhD thesis, University of Edinburgh, DAI, 1991. Expected.

[32] Sean Matthews, David Basin, and Alan Smaill. Experience with F S_{0} as a Framework Theory. Technical Report, University of Edinburgh, DAI, 1991. In preparation.

[33] Jose Meseguer. General Logics. In H.D. Ebbinghaus et al.(editors), Proceedings of Logic Colloquium 87. North-Holland, 1989.

[34] John C. Mitchell. Representation independence and data abstraction. In Thirteenth Annual ACM Symposium on Principles of Programming Languages, ACM, SIGACT, SIGPLAN, 1986.

[35] John C. Mitchell and Robert Harper. The essence of ML. In Fifteenth ACM Symposium on Principles of Programming Languages, 1988.

[36] John C. Mitchell and Gordon Plotkin. Abstract types have existential type. In Twelfth Annual ACM Symposium on Principles of Programming Languages, ACM, SIGACT, SIG-PLAN, 1985.

[37] Christine Paulin-Mohring. Inductive definitions in the calculus of constructions. In The Calculus of Constructions, Documentation and users’s guide, Project Formel, 1989.

[38] Lawrence C. Paulson. A higher-order implementation of rewriting. Science of Computer Programming, 3:119–149, 1983.

[39] Don Sannella and Andrzej Tarlecki. Specifications in an arbitrary institution. Information and Computation, 76:165-210,1988.

[40] Don Sannella and Andrzej Tarlecki. Toward formal development of ML programs: foundations and methodology. Technical Report 71, Laboratory for Foundations of Computer Science, 1989.

[41] Paul Taylor. Using Constructions as a MetaLanguage. Technical Report ECS-LFCS-88-70, University of Edinburgh, 1988.

[42] D. van Dalen. Logic and Structure. Springer-Verlag, 1980.

[43] Richard W. Weyhrauch. Prolegomena to a theory of formal reasoning. Artificial Intelligence, 13:133–170, 1980.

A Canonical Calculus of Residuals

Yves Bertot ^{†} INRIA Sophia Antipolis 06561 Valbonne Cedex France

July 1991

1 Introduction.

This work studies the notions of descendance and residuals. These notions are interesting for proof development systems in two respects. First, they are an important tool in the study of reduction systems, especially for comparing evaluation strategies and studying optimal evaluation [1, 5, 8, 12, 13]. As such, they have a natural place in any toolbox for reasoning about and proving properties of programming languages. Second, proof development systems often use rewriting themselves, and residuals can be used efficiently in the “debugging” of tactics, since tactics are very analogous to programs and residuals have already been shown to be useful in debugging programs, mostly in parallel programming languages, that are also based on rewriting [3].

Most presentations use a simple labeling of terms to describe descendance and residuals. For any reduction system, one simply produces a labeled version of the system, together with a procedure to transform a derivation on labeled terms in a derivation on unlabeled terms (called erasure) and a procedure to transform a derivation on unlabeled terms in a derivation on labeled terms, given a labeling of the initial term (called lifting). Intuitively, a node or a position in the resulting term descends from a node or a position in the initial term through a unlabeled derivation D if they share the same label in any labeled reduction obtained by lifting D, if the nodes of the initial terms are all labeled with distinct labels.

The use of labels to describe this notion of descendance is rather contrived. First of all, the labels have no importance as such, only an infinite set of distinct labels is required. Second, lifting an unlabeled derivation to a labeled one is a sequential process. One has to start with a labeled term, compute the labels for the term obtained after the first reduction, and continue recursively with the rest of the derivation. This does not take advantage of the inherent transitivity of the descendance relation: if D and D′ are two derivations such that the final term of D is the initial term of D′, if position A descends from position B through derivation D′ and position B descends from position C through derivation D then obviously A descends from C through the derivation that performs D then D′. The derivations D and D′ need not be elementary.

We rely on the property of descendance that any position in the final term of a derivation always descends from at most one position in the initial term. We prefer to consider the

†bertot@sophia.inria.fr

[figure: f; h; c; a; b]

Figure 8: Graphical representation of the tree f(h(a, b), c)

converse of the descendance relation, which is a function and which we call an origin function. In what follows, we present a data structure for representing origin functions that is concise and well adapted to these reduction systems, together with an interpretation method based on a canonical rewriting system. We give the definition and the main properties of origin functions for reduction systems such as the λ-calculus and term rewriting systems. We show that these origin functions, together with the language we use to represent them, are a suitable alternative to labeling for implementing the notion of descendance.

2 Mathematical Preliminaries.

2.1 Occurrences.

We denote N the set of natural numbers and N_{+} the set N − {0}. A graded alphabet is a set Σ given with a function α : Σ → N, called arity function. The set T (Σ) of Σ-terms is the least set verifying the following conditions:

1. For every operator g ∈ Σ such that α(g) = 0, one has g ∈ T (Σ),

2. For every operator f ∈ Σ such that α(g) = n > 0 and every n-tuple (t_{1}, …, t_{n}), one has f(t_{1}, …, t_{n}) ∈ T (Σ).

The operator f is called the head operator of the term f(t_{1}, …, t_{n}). In the following Σ-terms are regularly called terms, when the alphabet is obvious from the context.

Finite trees are a suitable graphical representation for terms, as shown in Figure 1. This representation also hints that an alternative presentation of terms is possible, defining first the drawing with all the lines (the tree domain) and then labelling the nodes with operators. This kind of presentation is given in [7, 9].

For any number i ∈ N_{+}, we denote s_{i} the function that maps any term f(t_{1}, …, t_{n}) such that n ≥ i to its i^{th} child, t_{i}, and is undefined for any term f(t_{1}, …, t_{n}) such that n < i. We denote O the set that contains the functions obtained by composing the function s_{i} and the identity of T (Σ), id. We claim that the elements of O represent correctly occurrences, as they are presented in [7, 9]. The usual presentation is to consider occurrences as strings of natural numbers. Our argument is that the functions s_{i} represent the elementary strings of one integer and that composing functions represents concatenating strings. We simply denote u(M) the subterm at occurrence u instead of denoting M/u. For this reason, we call occurrences the elements of O. We denote ∘ the composition operator, with the semantics that v ∘ u(M) = v(u(M)). For any two occurrences u and v, we note u ≤ v if there exists an occurrence w such that v = w ∘ u, and we say that u is a prefix of v (because u is applied first).

A tree domain, D, is a subset of O that verifies the following properties:

1. For any two occurrence u and v such that u ≤ v, if one has v ∈ D then one has u ∈ D,

2. For any two indices i and j such that i ≤ j and for any occurrence u, if one has s_{j} ∘ u ∈ D then one has s_{i} ∘ u ∈ D.

In the following we consider only finite tree domains and simply call them tree domains. For any term M, we denote D(M) the set of occurrences that are valid on this term, this set is a tree domain, which we call the domain of M.

2.2 Reduction Systems.

In the following we consider a reduction system represented by the binary relation →, and we write M → N to express that the term M reduces to N. However, this notation is not always sufficient since it does not give enough information on the manipulations that permit to go from M to N. For example, consider a term rewriting system that contains the following rule:

r :  I(x) → x

The reduction I(I(a)) → I(a) is a licit reduction for this system. But there are two ways to go from M to N: the first is to consider that I(x) matches I(I(a)), thus performing the rewriting at the top of the term; the other is to consider that I(x) matches I(a), thus performing the reduction on the first subterm of I(I(a)). The two reductions are usually considered to be different (and they are for the notion of descendance), and we need extra information to decide which reduction is actually performed. We thus write I(I(a)) →^{(id,r)} I(a) to denote the first reduction, expressing that a rewriting is performed applying rule r at the occurrence id on the initial term. The extra information we add on the arrow need not always be the couple of an occurrence and a rule. In the λβ-calculus, we only need an occurrence, since we know that the rule is always the β-rule.

Computations in a reduction system are represented by the reflexive transitive closure of the reduction relation, noted → →, and the elements of this relation are called derivations. Here again, we may need extra information to specify exactly a derivation, and we write M → →^{S} N, where S is a list whose elements specify exactly all the elementary reductions that compose this derivation. For tree rewriting systems, S is a list of couples (occurrence, rule).

Since derivations are elements of a transitive closure, they can be concatenated. If D = M → →^{S} N and D′ = N → →^{S′} P are two valid derivations in a reduction system, then M → →^{S;S′} P, there exists a derivation that goes from M to P by first performing the steps specified by S, then the steps specified by S′, which we denote D; D′. For any reduction system S, we denote Deriv(S) the set of all valid derivations in this system.

2.3 Origin Functions.

The intuition in a reduction M → N is that some parts of the result N descend from parts of M and some parts of N may have been created during the reduction. Origin functions are introduced to describe this notion of descendance.

For any reduction system S, an origin mapping Ω : Deriv(S) → (O → O) is a function verifying the following constraints:

1. If D = M →^{S} N is a derivation in Deriv(S) and f = Ω(D), then one has dom(f) ∈ D(N) and codom(f) ∈ D(M). This constraint is not very important, but it states that the function f expresses the origins of the nodes in N and that these origins are all in M.

2. If D and D′ are derivations in Deriv(S) such that D; D′ is well defined, then one has Ω(D; D′) = Ω(D) ∘ Ω(D′). This constraint expresses the intuition that the node at occurrence u descends from the node at occurrence w through the derivation D; D′ as soon as the node at occurrence u descends from the node at occurrence v by the derivation D′ and the node at v descends from the node at w by D.

The images of derivations by Ω are called origin functions.

3 Representing Origin Functions.

3.1 Origins for Projections.

Occurrences act on terms like projections and they may receive origin functions. When we write N = u(M), we may express that N is obtained by taking the subterm at occurrence u of M. Let f be the origin function associated to this manipulation. This origin function is very regular. The node at occurrence v in N descends from the node at occurrence v in u(M), that is, the node at occurrence v ∘ u in M. If f is the origin function associated to this reduction, we have f(v) = v ∘ u for any occurrence v ∈ D(N).

We introduce a mapping μ : O → (O → O) that summarize this phenomenon. The mapping μ is defined by the following property:

∀u, v ∈ O μ(u) = f ↔ f(v) = v ∘ u

The mapping μ is a morphism from O to (O → O). Actually, μ(id) is the identity of (O → O). The two spaces have a composition operator, ∘. With respect to these operators we have the following property:

∀u, v, w ∈ O μ(u) ∘ μ(v)(w) = μ(u)(μ(v)(w)) = w ∘ v ∘ u = μ(v ∘ u)(w)

Thus, we have μ(u) ∘ μ(v) = μ(v ∘ u), μ is contravariant. Last, μ is injective, since we have μ(u)(id) = u.

Notice that for any occurrence u, the function μ(u) is defined for every occurrence in O, instead of being defined only on a finite domain as are normal origin functions. When we state that the origin function f of a tree manipulation is equal to μ(u) (f = μ(u)), we actually express f has the same value as μ(u) for every occurrence where it is defined. We shall see later that the possibility to abstract the domain definition this way is actually very useful in an implementation of origin functions.

3.2 General Case.

All tree manipulations are not as regular as projections, and we want to describe origin functions of arbitrary complexity. However, we can take advantage of the regularity given by the fact that terms are recursively definable.

[figure: @; a; b; c([…], ); c([], ); c([], ); s_{2} ∘ s_{1}; s_{2} ∘ s_{2} ∘ s_{1}; s_{2}]

Figure 9: Graphical representation of origin functions.

When specifying the value of a term M, one only needs to provide an operator f and a tuple of terms (t_{1}, …, t_{n}) and say that M = f(t_{1}, …, t_{n}). The terms t_{1} to t_{n} may in turn be defined by the same operation, recursively, until one reaches leaves. When providing origins for the nodes in M, one only needs to provide an origin for the head node (at occurrence id) and use origin functions for the subterms t_{1} to t_{n}. These origin functions may in turn be defined by the same operation, recursively.

Denoting [f_{1}, …, f_{n}] a tuple of functions and (O → O)^{∗} the set of tuples of functions over occurrences, we introduce the mapping c : ((O → O)^{∗} × O) → (O → O) that maps a tuple of functions over occurrences and an occurrence to a function over occurrences defined by the following property:

1. For any tuple [f_{1}, …, f_{n}] ∈ (O → O)^{∗} and any occurrence u, c([f_{1}, …, f_{n}], u)(id) = u.

2. For any tuple [f_{1}, …, f_{n}] ∈ (O → O)^{∗}, any occurrences u and v, and any index i ≤ n, one has c([f_{1}, …, f_{n}], u)(v∘s_{i}) = f_{i}(v). This mimics the property that v∘s_{i}(f(M_{1}, …, M_{n})) = v(M_{i}).

3. For any tuple [f_{1}, …, f_{n}] ∈ (O → O)^{∗}, any occurrences u and v, and any index i > n, one has c([f_{1}, …, f_{n}], u)(v ∘ s_{i}) is undefined.

Example. Let us consider the following reduction, taken from the λ-calculus (we use a term representation instead of the usual concrete syntax for λ-terms, to emphasize the tree structure).

@(λ(x, @(x, b)), a) → @(a, b)

The origin function for this reduction, f, is defined by the following equations: f(id) = s_{2} ∘ s_{1} f(s_{1}) = s_{2} f(s_{2}) = s_{2} ∘ s_{2} ∘ s_{1} The function f can also be represented by the following notation:

f = c([c([], s_{2}), c([], s_{2} ∘ s_{2} ∘ s_{1})], s_{2} ∘ s_{1})

This representation permits to represent extensively an origin function on a domain, without having to write the elements of the domain. We actually construct a tree isomorphic to the term whose origins are described, labeling each node with the origin for the corresponding occurrence, as is shown in figure 2. Since it is an extensive representation of the origin function, the notation using function c is powerful enough to represent any origin function.

The composition of two functions described using function c is also representable using this function. Actually, one only needs that the function on the right-hand side of the composition operator be represented using c. One obtains the following equality:

f ∘ c([f_{1}, …, f_{n}], u) = c([f ∘ f_{1}, …, f ∘ f_{n}], f(u))  (1)

This equality is a direct consequence of the definition of c, but it can be explained intuitively. Let us consider the final term of a manipulation is P = op(t_{1}, …, t_{n}), that each of the terms t_{i} is obtained from a term N by a manipulation whose origin function is f_{i}, that the origin of the head node in N is u, and that N is obtained from the initial term M by a manipulation whose origin function is f. Then each of the terms t_{i} is obtained from M by a manipulation whose origin function is f ∘ f_{i} and the origin of the head node of P in M is given by the origin of the node of N at occurrence u, f(u).

The composition of a function represented using c and of a function represented using μ is also easy to describe, this time when the representation using c is on the left-hand side. Actually we have to use the fact that μ is composed of elementary occurrences s_{i}. One obtains the following equality:

c([f_{1}, …, f_{n}], u) ∘ μ(v ∘ s_{i}) = f_{i} ∘ μ(v)  (2)

Here again, this equality can be described intuitively. If P is obtained from N by taking the subterm at occurrence v ∘ s_{i}, if N = op(t_{1}, …, t_{n}), and if the j^{th} child of N is obtained from the initial term M by a manipulation whose origin function is f_{j}, then P is obtained by taking the subterm at occurrence v in the term t_{i}, whose origins are described by the function f_{i}.

4 Representing Origins with Trees.

4.1 A Formal Language of Origins.

We introduce the language Orig containing the two sorts F and T based on the following abstract syntax, where the index i ranges over N_{+}:

F = s_{i} | id | F ∘ F | c(T , F) | nil
T = [F∗]

We call Occ the subset of Orig that contains the trees constructed only with the operators s_{i}, id, and ∘. The operator nil is provided to represent undefined values.

Examples of trees in Orig are s_{1} ∘ s_{2} ∘ id, s_{1} ∘ nil, and c([s_{1} ∘ s_{2}, nil], c([], id)).

The trees of Occ can be used to represent occurrences, using the interpretation function ⟨⟨.⟩⟩ : Occ → O defined by the following properties:

1. ⟨⟨id⟩⟩ = id,

2. ∀i ∈ N_{+} ⟨⟨s_{i}⟩⟩ = s_{i},

3. ⟨⟨u ∘ v⟩⟩ = ⟨⟨u⟩⟩ ∘ ⟨⟨v⟩⟩.

The trees of Orig can be used to represent functions over occurrences, using the interpretation function [[.]] : Orig → (O → O) defined by the following properties:

1. [[nil]] = nil, where nil is the function that is undefined on any occurrence of O.

2. [[id]] = 1_{O},

3. [[s_{i}]] = μ(s_{i}),

4. [[t_{1} ∘ t_{2}]] = [[t_{2}]] ∘ [[t_{1}]],

5. [[c([t_{1}, …, t_{n}], t)]] = c([[[t_{1}]], …, [[t_{n}]]], [[t]](id)). Note that this function is undefined on id when t = nil.

Note that these trees differ from the notations we have used so far for origin functions in two respects. First, the composition operator takes its children in the reverse order, when compared to the composition of the functions the children represent. This happens because this composition operator is used in Orig to represent two kinds of compositions: the composition of occurrences and the composition of functions over occurrences. However, the two operations are related by the morphism μ, which is contravariant. This property must necessarily appear in one of the interpretations. The reader can check that this permits to have the following property:

∀t ∈ Occ [[t]] = μ(⟨⟨t⟩⟩)  (3)

Second, a tree with the head operator c accepts a tree of the same sort for second child, whereas the mathematical function c we use to describe origin function takes an occurrence as second argument, not an origin function. Here again, this property appears in the interpretation function, that forgets everything about the given origin function, except for the value in id. However, this property gives us the following equation:

∀t ∈ Occ [[c([t_{1}, …, t_{n}], t)]] = c([[[t_{1}]], …, [[t_{n}]]], ⟨⟨t⟩⟩)  (4)

4.2 Simplification and Computation.

To compute the value of the origin function [[t]] where t is a tree of Orig on an occurrence represented by a term u of Occ, we want an algorithm that takes u and t and returns a tree v ∈ Occ such that [[t]](⟨⟨u⟩⟩) = ⟨⟨v⟩⟩. The procedure we propose is based on the following remarks.

a. In the following cases the value [[t]] is easy to compute:

1. t ∈ Occ ⇒ [[t]](id) = ⟨⟨t⟩⟩ (equation 3),

2. t = c(M, t′) ∧ t′ ∈ Occ ⇒ [[t]] = ⟨⟨t′⟩⟩ (equation 4),

3. t = nil ⇒ [[t]] is undefined.

4. t = c(M, t) ∧ t′ = nil ⇒ [[t]] is undefined.

b. If one has u ∈ Occ and t ∈ Orig, then the value [[t]](⟨⟨u⟩⟩) is equal to [[t′]](id) where t′ = u ∘ t (this is because [[u ∘ t]](id) = [[t]] ∘ [[u]](id) and [[u]](id) = u).

Following these remarks, we provide a canonical rewriting system for which the normal form of any term in Orig matches one of the cases of remark a and such that the origin function represented by a term is preserved in any derivation. The procedure is then as follows, to compute [[t]](⟨⟨u⟩⟩) when t ∈ Orig and u ∈ Occ:

1. normalize the term u ∘ t in a term t′.

2. If the head operator of t′ is c then the second child of t′ is a term t′′ such that [[t]](⟨⟨u⟩⟩) = ⟨⟨t′′⟩⟩, else [[t]](⟨⟨u⟩⟩) = ⟨⟨t′⟩⟩.

The rewriting system ρ that we propose is composed of the following rules:

\begin{matrix}ρ_{1} : & (t ∘ t′) ∘ t′′ → & t ∘ (t′ ∘ t′′) \\ ρ_{2} : & s_{i} ∘ c([t_{1}, …, t_{i}, …, t_{n}], t) → & t_{i} \\ ρ_{3} : & c(T_{1}, c(T_{2}, t)) → & c(T_{1}, t) \\ ρ_{4} : & c([t_{1}, …, t_{n}], t) ∘ t′ → & c([t_{1} ∘ t′, …, t_{n} ∘ t′], t ∘ t′) \\ ρ_{5} : & id ∘ t → & t \\ ρ_{6} : & nil ∘ t → & nil \\ ρ_{7} : & t ∘ nil → & nil \\ ρ_{8} : & c([nil, …, nil], nil) → & nil \end{matrix}

Actually, rules ρ_{2} and ρ_{4} are rule schemas, corresponding to every possible combination of i and the length of the tuple between the square brackets […].

The fact that the represented function is preserved in every reduction must be proved for every reduction. For rule ρ_{1}, it comes directly from the associativity of composition, for rule ρ_{2} it commes from equation (2), for rule ρ_{3} it comes directly from point 5 of the definition of [[…]], for rule ρ_{4} it comes from equation (1), for rule ρ_{5} it comes directly from the fact that id represents the identity of O, for rules ρ_{6} and ρ_{7} it comes from the definition of composition, and for rule it comes from the definition of c.

That ρ is terminating is proved by a simple ordering on terms using weight P : Orig → N defined as follows:

– P (id) = 2,

– P (s_{i}) = 2,

– P (t_{1} ∘ t_{2}) = P (t_{1})^{2}P (t_{2}),

– P (c([t_{1}, …, t_{n}], t) = ( ∑_{1≤i≤n} P (t_{i})) + P (t).

– P (nil) = 2.

For any reduction t → t′ using this rewriting system, one has P (t′) < P (t).

All the critical pairs in this rewriting system are confluent. This can be verified automatically using the algorithm of completion of Knuth-Bendix [11]. These properties are enough to prove that this rewriting system is confluent. To complete our study of ρ, we simply need the following property. Property: For any term t normal for ρ, one has:

– t = t_{1} ∘ t_{2} ⇒ t ∈ Occ,

– t = c(M, t′) ⇒ t′ ∈ Occ ∨ t′ = nil.

Proof. First remark that any subterm of a normal term is also normal. We can then prove these properties by induction. If t = t_{1} ∘ t_{2}, then the head operator of t_{1} and t_{2} cannot be [ ] because of the syntax and it cannot be c or nil because t would not be normal. Then it is necessarily ∘, id, or s_{i}. If the term t_{i} has a head operator ∘ then the induction hypothesis yields t_{i} ∈ Occ, otherwise t_{i} is trivially in Occ.

Now, if t is normal and t = c(M, t′) then the head operator of t′ cannot be [ ] because of the syntax and it cannot be c because t would not be normal for ρ. Then we can apply the same reasoning for t′ as above and obtain t′ ∈ Occ or t′ = nil.

5 Applications.

5.1 Linear Term Rewriting Systems.

Term rewriting systems are usually described by rules of the form α → β where α and β contain variables. The meaning attached to these rules is that any instance of α can be replaced by the corresponding instance of β. To express that a rewriting can be performed in any context, one simply adds a rule of the form:

\frac{t_{i} → t′_{i}}{f(t_{1}, …, t_{i}, …, t_{n}) → f(t_{1}, …, t′_{i}, …, t_{n})}

for any operator f in the language and any rank i. Conditional rewriting systems can be obtained by removing some of these rules as in [14], or by adding a predicate P that limits the applicability of the rule, yielding a rule of the form:

\frac{t_{i} → t′_{i} P (f(t_{1}, …, t_{n}))}{f(t_{1}, …, t_{i}, …, t_{n}) → f(t_{1}, …, t′_{i}, …, t_{n})}

As shown by the Centaur experiment [4, 10], these rules can be directly transformed into executable code that allows the computation of derivations. An application of our work is to enhance this code, so that we compute the origin function of a derivation while computing this derivation.

We simply manipulate the rules that describe reductions, replacing uses of the formula t → t′ (which means t reduces to t′) by uses of the formula t → t′, w (which means t reduces to t′ with the origin function w), where the extra parameter w is written in the language Orig.

For conditional rules of the form above, the manipulation is systematic, yielding new rules of the following form:

\frac{t_{i} → t′_{i}, w P (f(t_{1}, …, t_{n}))}{f(t_{1}, …, t_{i}, …, t_{n}) → f(t_{1}, …, t′_{i}, …, t_{n}), c([s_{1}, …, w ∘ s_{i}, … s_{n}], id)}

The term added in the conclusion, c([s_{1}, …, w ∘ s_{i}, … s_{n}], id) is rather intuitive: the parts s_{1}, …, s_{j} (j ≠ i), …, s_{n} express that the children that are not affected by the reduction simply come from the corresponding children of the initial term. The part w ∘ s_{i} expresses that t′_{i} is obtained from t_{i} by a reduction whose origin function is w and t_{i} is obtained from the initial term by taking the i^{th} subterm. The part id indicates that the head node of the resulting term comes from the head node of the initial term.

Note that the use of the function μ in the interpretation [[.]] of trees of Orig enables us to express that the origins for the subterm t_{j} are simply given by the data structure s_{j}. Without μ and the possibility it gives to use occurrences as functions over occurrences, it would be impossible to abstract over the variables t_{j} and we would be obliged to provide a distinct term constructed using c([…], .) for every possible instance of t′. In this sense, our data structure is particularly adapted to structural semantics.

For the axiomatic rules of the form α → β, we can also have a systematic treatment, if we restrict our manipulation to linear rewriting systems. Such systems verify the constraint that all the variables in β appear in α and that the variables appearing in α appear only once. For these rules the descendance relation is simple to express: any node that appears under a variable of β in the resulting term descends from the node that appears at the same place relative to the same variable of α in the initial term. This definition is not ambiguous because we are working with linear rewriting systems. This manipulation yields rules like the following one:

double(x) → sum(x, x), c([s_{1}, s_{1}], nil)

The term added to the reduction, c([s_{1}, s_{1}], nil) is simple to understand: both children of the resulting term descend from the only child of the initial term. The head node of the resulting term is created by the reduction, its origin is undefined and represented by nil.

5.2 The λ-calculus.

The λ-calculus is also described using conditional rules, but some of these rules are not based on rewrite formulas. The kernel of the λ-calculus is the β-rule:

β  (λx.M)N → M[x\N]

The notation M[x\N] represents the term M where every free instance of the variable x is replaced by N. This operation must also contain some renaming of the bound variables in M, so as not to catch free variables in N. This operation can be described by the following rules:

subst x[x\T] = T
diff  y[x\T] = y  (y ≠ x)

app  \frac{M[x\T] = M′  N[x\T] = N′}{MN[x\T] = M′N′}

lambda \frac{M[y\z] = M′  M′[x\T] = M′′}{λy.M[x\T] = λz.M′′}  (z new)

To add computations over origin functions to these rules, we have to consider the whole notation M[x\N] to be a term, since the resulting term comes sometimes from N (rule subst) and sometimes from M (rule diff). In that case however, the β rule must be written as follows:

β  \frac{M[x\N] = M′}{(λx.M)N → M′}

Also, the rule subst does not look like a linear rule, since x appears twice in the initial term. It happens to be harmless, since this variable does not appear at all in the resulting term.

The language Orig is still adapted to represent origins in the substitution operation. The manipulation yields the following rules:

subst x[x\T] = T, s_{3}
diff  y[x\T] = y, s_{1}  (y ≠ x)

app  \frac{M[x\T] = M′, w_{1}  N[x\T] = N′, w_{2}}{MN[x\T] = M′N′,}
c([w_{1} ∘ c([s_{1} ∘ s_{1}, s_{2}, s_{3}], id), w_{2} ∘ c([s_{2} ∘ s_{1}, s_{2}, s_{3}], id)], s_{1})

lambda \frac{M[y\z] = M′  M′[x\T] = M′′, w}{λy.M[x\T] = λz.M′′, c([s_{1} ∘ s_{1}, w ∘ c([s_{2} ∘ s_{1}, s_{2}, s_{3}], id)], s_{1})}  (z new)

Note how the rule app has been manipulated. The function w_{1} is composed to a term that describes how M[x\T] descends from MN[x\T]. The same kind of manipulation appears in the rule lambda. Note that in this rule the first premise, which only computes a variable renaming, is not used in the origin computation.

This manipulation of the rules for substitution goes along with a manipulation of the rule β that yields the following rule:

\frac{M[x\N] = M′, w}{(λx.M)N → M′, w ∘ c([s_{2} ∘ s_{1}, s_{1} ∘ s_{1}, s_{2}], nil)}

All these rule manipulations can actually be automatized, as is shown in [2].

5.3 Coming Back to Labeling.

Labeling a term M with letters from an alphabet A corresponds to providing a function L : D(M) → A that maps any occurrence to the label carried by the corresponding node.

As we did for origin functions, we can define a function c_{A} : (O → A)∗ → (O → A) that permits to deduce the labeling of a term from the labelings of its subterms. If t_{1}, …, t_{n} are terms labeled using the labeling function L_{1}, …, L_{n}, if f is an operator and a is a label, then the term f^{a}(M_{1}, …, M_{n}) is actually labeled using the function L = c([L_{1}, …, L_{n}], a) such that L(id) = a and L(v ∘ s_{i}) = L_{i}(v). In this respect, the origin functions simply correspond to labeling function where we have simply taken the set of occurrence O as labeling alphabet.

To compute the labeling L′ of a term M′ resulting from a derivation starting from a term M labeled with a labeling function L, we can simply use the origin function of this derivation f. We simply have to write L′ = L ∘ f. A representation of L′ can easily be constructed if we use A and the function c_{A} to define a language analogous to Orig.

6 Conclusion.

In this paper, we have presented a new paradigm for the study of descendance and labelings in reduction systems such as term rewriting systems and the λ-calculus. We have shown that this paradigm is especially suited for implementing this notion and we have described a datastructure and a method to compute using this data structure.

This method of computation consists of a canonical term rewriting system. The fact that we use a canonical term rewriting system has the main advantage that we do not have to specify the evaluation strategy. This permits to parallelize any computation on these data structures. If we consider a derivation D = D_{1}; ⋯; D_{n}, we can compute in parallel and independently the origin functions of the sub-derivations D_{i} and then compose these origin functions to obtain an origin function for the complete derivation. This is a big advantage over usual labelings, where it is arduous to compose labelings and the lifting of a derivation to a labeled one has to be done sequentially.

The methods used in this paper permit to describe the simple labelings that are related to descendance. However, more elaborate labelings have also been developed to study other aspects of reductions [6, 12, 14]. Those labelings do not use a simple alphabet, but rather algebras based on an alphabet. It is interesting to see how the operators of our language Orig and the operators of these algebras interact, in order to provide an implementation of these elaborated labelings.

References

[1] H. P. Barendregt, The Lambda Calculus, Its Syntax and Semantics North-Holland, 1984.

[2] Y. Bertot, Une automatisation du Calculs des Résidus en Sémantique Naturelle, Ph.D Thesis, University of Nice, France, 1991.

[3] Y. Bertot, “Occurrences in Debugger Specifications”, Proceedings of ACM SIGPLAN’91 Conference on Programming Language Design and Implementation, Toronto, Ontario, Canada, 1991.

[4] P. Borras et al., “Centaur: the System”, Proceedings of the Third Symposium on Software Development Environments, ACM SIGSOFT’88, Boston, Massachusetts, 1988.

[5] H. B. Curry, R. Feys, Combinatory Logic, Vol. I, North-Holland, 1958.

[6] J. Field, “On Lazyness and Optimality in Lambda Interpreters: Tools for Specification and Analysis”, Proceedings of the 17th ACM Symposium on Principles of Programming Languages, San Francisco, California, 1990.

[7] J. H. Gallier, Logic For Computer Science, Harper & Row, 1986.

[8] G. Huet, J.-J. Lévy, “Call by Need Computations in Non-Ambiguous Linear Term Rewriting Systems”, IRIA Laboria Report 359, 1979.

[9] G. Huet, “Deduction and Computation”, Fundamentals in Artificial Intelligence, W. Bibel, Ph. Jorrand (editors), Springer Verlag LNCS 232, 1986.

[10] G. Kahn, “Natural Semantics”, Programming of Future Generation Computers, K. Fuchi, M. Nivat (editors), North-Holland, 1988 (also appears as INRIA Report no. 601).

[11] D. Knuth, P. Bendix, “Simple Word Problems in Universal Algebras”, Computational Problems in Abstract Algebra, J. Leech (editor), Pergamon, 1970.

[12] J.-J. Lévy, Réductions Correctes et Optimales dans le Lambda Calcul, Thèse de Doctorat d’état, University of Paris VII, France, 1978.

[13] J.-J. Lévy, “Optimal Reductions in the Lambda-Calculus”, to H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J. P. Seldin, J. R. Hindley (editors), Academic Press, 1980.

[14] L. Maranget, “Optimal Derivations in Weak Lambda-Calculi and in Orthogonal Term Rewriting Systems”, Proceedings of the Eighteenth ACM Symposium on Principles of Programming Languages, Orlando, Florida, 1991, pp. 255–269.

86

A semantics of evidence for classical arithmetic

Thierry Coquand^{∗} Chalmers University

Preliminary version, June 1991

Introduction

This short note presents Gentzen’s first proof of consistency of arithmetic, that was actually never published by Gentzen himself, but instead appeared first in a paper of Bernays [1] (but see also [3]). As emphasized by Bernays, this argument is easier to follow than the first published proof. It can be read directly as a game-theoretic analysis of the notion of classical truth: a formula is classically true iff there is a winning strategy for a game defined by this formula. This provides a semantics of evidence for classical first-order arithmetic (the term “semantics of evidence” seems due to B. Constable, see [2]). Furthermore, Gentzen’s proof leads directly to the result that an existential statement provable in classical arithmetic is provable intuitionistically.

More importantly, when expressed game-theoretically, the dynamic aspect of cut-elimination becomes clearer. We believe indeed that the main object of study here is the analysis of the possible sequence of moves in the strategies corresponding to classical proofs.

Such an analysis suggests strongly that it should be possible to find a cut-elimination proof of a different nature than Gentzen’s which reflects and is inspired by this dynamic aspect. We try to motivate this point by presenting such a proof for cuts of a low level of logical complexity, and by a conjecture expressing the termination of an internal communication, result that would refine Gentzen’s cut-elimination.

We discuss next a concrete example, due to Gabriel Stolzenberg, which suggests that it can be computationally inefficient to break a multiple cut in its component. In the simplest possible case that departs from usual cut-elimination, we sketch a way to do this “multiple cut-elimination.” Here also, it is directly checked that this “protocol for multiple cuts” works for cuts of low logical complexity.

At the end of the paper we present an inductive formulation of ω-logic, very close to Tait’s formulation [9], which is readily seen to provide a computational content of classical arithmetical truth.

The contributions of this (preliminary) paper are:

• an “historical” contribution: we think it will be fair to attribute the result that an existential statement proved in Peano arithmetic has an intuitionistic proof at least partially to Gentzen, since this is a direct corollary of his first proof of normalisation ^{1}, • a formulation of a conjecture that refines Gentzen’s cut-elimination, with a proof in a

∗coquand@margaux.inria.fr

1we conjecture that it is because Gentzen’s interpretation of a proof was in general a non deterministic algorithm that his first proof was for a while forgotten

restricted case (that hopefully will be completed for the less preliminary version of this paper),

• the analysis of a concrete example where it is clear that the “multiple-conclusion” logic we manipulate cannot be simulated in a functional way, and so, the discovery of features of multiple-conclusion logic that are typical of parallel algorithms. We sketch then how to extend this to a truly parallel cut-elimination for classical arithmetic.

I would like to thank Gabriel Stolzenberg, Lars Hallnäs, Jan Smith, Peter Dybjer, Hugo Herbelin and Chet Murthy for enjoyable discussions on this topic. Karlis Cerans provided crucial critics.

1 A semantics of evidence

We start with a fixed language for arithmetic that contains (computable) functions like addition, multiplication and (decidable) basic relations, like equality, ≤, … We suppose that whenever an atomic relation R is in this language we have another one R^{∗} which represents its complement, in such a way that (R^{∗})^{∗} is R.

The formulae are built inductively form atomic formulae by conjunction &, disjunction ∨, universal and existential quantification. The negation φ^{∗} is defined inductively from φ as usual.

To simplify things, we will suppose that all formulae are prenex formulae in which universal and existential quantifications alternate, that is of the form ∀x∃y∀z …, in which case we say that the formula is universal, or of the form ∃x∀y∃z …, in which case we say that the formula is existential. All quantifier free formulae are decidable.

1.1 The intuitionistic case

We recall first what is a possible game-theoretic semantics of evidence for intuitionistic logic, as presented for instance in A. Ranta’s thesis [8]. We consider the following game between Nature and Myself, which consists in making moves, that are existential or universal instantiations, in a given formula φ, which is called the configuration of the game. Myself is trying to establish the truth of formula φ, and Nature tries to produce a counter-example. If the formula is atomic, then it is decidable: if it is false, Nature wins, otherwise, Myself wins. If the formula is of the form ∃n A[n], Myself should produce an integer n_{0} and the game goes on with A[n_{0}]. If the formula is of the form ∀n A[n], Nature produces an integer n_{0} and the game goes on with the formula A[n_{0}].

For this game, a formula A can be defined to be intuitionistically true iff there is a winning strategy for Myself.

1.2 Extension to “multigames”

We can complicate this by allowing the configuration of the game to be a finite multiset of formulae. We write + the addition on multisets. The game stops when at least one formula is atomic and true, in which case Myself wins. In the other cases, Myself should make an instantiation whenever all formulae are existential, and Nature should make a move whenever at least one formula is universal, by instantiating the universal formulae. If all formulae are atomic and false, then Nature wins.

In this version, there is a winning strategy for Myself for the configuration of “excluded middle” A + A^{∗}, for any formula A : Myself simply waits for Nature to move, and mimics her move in the dual formula.

For this notion of game however, it is not the case that there is a winning strategy for ∃n∀m [A[n] ∨ A^{∗}[m]] even in the case where A is decidable. Indeed, suppose that Myself has such a winning strategy. Myself has to give a value n_{0} for n, because the formula is existential. We know that if A[n_{0}] does not hold, then we have ∀m A^{∗}[m]. Otherwise, Nature can win by playing m_{0} such that A[m_{0}] holds. By checking whether A[n_{0}] holds or not, we would thus extract a decision algorithm for ∃n A[n] ∨ ∀m A^{∗}[m].

Notice however that, as pointed out already, there is a winning strategy for the “equivalent” multiset formula ∃n A[n] + ∀m A^{∗}[m] : Myself waits for an instantiation m = m_{0} from Nature, and if A^{∗}[m_{0}] does not hold, win by playing n = m_{0} (if A^{∗}[m_{0}] holds, then Myself wins already after Nature’s move).

1.3 Games with “backtracking”

For getting a notion of game such that (intuitionistic) winning strategy contains classical provability, we allow backtracking for moves of Myself. This means that Myself can choose to complicate a configuration M + ∃n A[n] where all the formulae are existential by both instantiating the formula ∃n A[n] and keeping it, which produces the configuration M +∃n A[n]+A[n_{0}] where n_{0} is the integer chosen by Myself. The moves of Nature are the same as before.

For this notion of game, there is a winning strategy for Myself for the configuration φ iff φ is classically true.

Instead of showing formally this equivalence, we will limit ourselves to show that if there is a winning strategy for the configuration M + A + A, then there is a winning strategy for the configuration M +A, and if there is a winning strategy for the configuration M +A and a winning strategy for the configuration N + A^{∗}, then there is a winning strategy for the configuration M + N.

This is enough to show that the notion of truth defined by the existence of a winning strategy has good properties. For instance, if we have a winning strategy for N + A[0] and, for all n, a winning strategy for M + A[n]^{∗} + A[n + 1], then we deduce from these two closure properties that there is a winning strategy for all n for M + N + A[n].

The first claim is seen by simulating directly the moves of a strategy for M + A + A by moves for the configuration M + A.

The second claim is more difficult, and we will present it as the proof of termination of some internal communications between two players following winning strategies.

1.4 Two examples

There is now for instance a winning strategy for ∃n∀m [A[n] ∨ A^{∗}[m]]. Myself chooses any instantiation for n, for instance n = 0, and keeps the formula, waiting for a m = m_{0} given by Nature. If A^{∗}[m_{0}], then Myself wins, and if A[m_{0}] then Myself chooses n = m_{0} for its next move.

Another example, which shows that we cannot bound a priori the number of backtracking in Myself’s guess, is the following strategy for the statement

∃n∀m [f(n) ≤ f(m)],

seeing f as an oracle. Myself starts by guessing any value for n, for instance n = 0, and allows himself to backtrack. Nature plays then m = u_{1}. If f(0) ≤ f(u_{1}), Myself wins. If f(u_{1}) < f(0), Myself backtracks and plays n = u_{1}, and allows himself to backtrack. Nature plays then m = u_{2}. If f(u_{1}) ≤ f(u_{2}), Myself wins. Otherwise, Myself backtracks and plays n = u_{2}, and allows himself to backtrack, and so on.

This will stop eventually, because < is well-founded, but it is not possible to bound a priori (without knowing anything about f) the number of times that Myself will have to backtrack.

This explanation of classical truth appears in Gentzen, see [3, 1]. Note that Bernays, in [1], presents this proof using choice sequences, for representing the sequence of moves of Nature. We can use inductive definitions instead to represent the notion of choice sequence, as done for instance in [6].

1.5 The case of existence statement

Let us look at the special case of a winning strategy for a configuration ∃n A[n], where A[n] is a (decidable) atomic formula. We see the decision procedure for A[n] as an oracle. To have a winning strategy in this case means that Myself will do a finite number of wrong guesses for n, until he eventually finds a n_{0} such that A[n_{0}]. We can actually suppose that Myself always is doing some “auto-censure” by himself, so that he checks internally whether or not his guess is correct for an existential formula ∃n A[n], where A is atomic. With this assumption, a winning strategy for an existence statement is exactly a witness.

We thus get that the result “if an existence statement is provable in classical first-order arithmetic, then it is provable intuitionistically” follows from the identification of classical truth with the existence of a winning strategy.

1.6 Simple backtracking

In all the examples we have presented so far, the backtracking that Myself uses is of a particular nature. Myself never changes his mind about a value he has considered as wrong (we will precise this notion later). We call this behaviour of Myself simple backtracking.

This notion of simple backtracking is interesting because it does involve backtracking, but it is however a simple enough behaviour so that we can give a complete analysis of what is happening in the case where all players follow simple backtracking. In particular, we will be able to analyse later the case of multi-cuts for simple backtracking, that involves already real parallelism.

In order to analyse a little more this notion of simple backtracking, we introduce the following notations. In the history of configurations of a game which has M + A as an initial configuration, where A is existential, we follow the moves in A by writing A_{1}, A_{2}, … the instantiations of A (due to Myself), and then A_{11}, A_{21}, … the respective instantiations of these instantiations (due to Nature), and so on. If a formula B is of the form A_{n_{1}...n_{p}}, or A_{n_{1}...n_{p}}^{∗}, we say that n_{1} … n_{p} is the index of the formula B, and we write n_{1} … n_{p} = ind(B). We say that a sequence n_{1} … n_{p} is a direct extension of a sequence m_{1} … m_{q} iff p = q + 1, and n_{i} = n_{i} for i < p.

To say that the backtracking is simple for the formula A is to say that once we have observed the sequence of moves

A, A + A_{1}, A + A_{11}, A + A_{11} + A_{2}, …, A + … + A_{n_{1}...n_{p}}, …

with p even, then the next move of Myself will be A + … + A_{m_{1}...m_{q}}, where m_{1} … m_{q} is strictly bigger than n_{1} … n_{p} for the alphabetical ordering on sequence of integers.

This is the case if the formula A is of the form ∃x∀y B[x, y], where B is atomic, simply because in this case, Myself cannot play A_{111}. Simple backtracking holds thus when we consider formulae of low logical complexity.

If Myself follows a strategy that uses only simple backtracking for an existential formula A, then we can represent Myself’s moves in A (for a given game against nature) as a sequence of the form

A, A_{1}, A_{11}, A_{111}, A_{1111}, A_{112}, A_{1121}, A_{113}, …

Such a sequence can be read as follows (if the sequence of quantifiers of A is ∃x∀y∃z∀t …): Myself makes a first guess x = x_{1} about the value of x. Nature then answers y = y_{11}. Myself persists in his choice by guessing z = z_{111}, this choice being refuted by Nature, who plays t = t_{1111}. At this point, Myself changes his mind about the choice of z (he considers that Nature has really refutated it and does not persist in his choice, leaving the last refutation of Nature t_{1111} without answers). He tries then z = z_{112}. This is refuted by Nature who plays t = t_{1121}.

One can well imagine a strategy where Myself changes his mind also about the fact that he was wrong. This is a more subtle kind of behaviour.

The analogy with learning theory, that Myself makes successive guesses according to the moves of Nature, seems clear here and should be precised. We will limit ourselves here to point out this analogy.

It would be nice if we can insure that for all classically true multiset M, it is possible to find a winning strategy using only simple backtracking. Though we don’t have any concrete counter-example, we suspect that this is not the case, since we don’t see how to get a strategy for the configuration M + A from a strategy for the configuration M + A + A if we impose strategies to use only simple backtracking. Any strategy for M + A + A can be simulated by a strategy for M + A. Even if for both A, a strategy for M + A + A uses only simple backtracking, this may not be the case for the simulated strategy for M + A.

Here is an example of a sequence of move that uses more than simple backtracking:

A, A + A_{1}, A + A_{11}, A + A_{11} + A_{2},
A + A_{11} + A_{21}, A + A_{11} + A_{21} + A_{111},
A + A_{11} + A_{21} + A_{1111}, A + A_{11} + A_{21} + A_{1111} + A_{211}, …

The intuition is that Myself, when he plays A_{111}, changes his mind about his first backtracking, and does not answer to the refutation A_{21} of his last play. But when Nature refutes this last play A_{111} by playing A_{1111}, Myself changes his mind again and comes back to the choice of his second instantiation of A. Myself tries by playing A_{211} to refute the previous refutation of Nature A_{21} he had left without answers.

2 A dynamic view of cut-elimination

Let us imagine that we are playing against Nature for a given configuration. We can see a strategy for this configuration as a player we have at our disposition. Each time Nature plays, we transmit her move to this player. When all formulae are existential, we wait to see what is the move of this player on this configuration. We follow the strategy by copying his move.

With this picture in mind, we can conceive that it takes more or less time for the player to answer our question. We can consider a strategy to be total if we are sure that, eventually, after a finite amount of time, the player will answer. It is then natural to consider also partial strategies, that are like players who stay mute, thinking for a too long time about their next move.

Given two strategies for M + A and N + A^{∗}, we show how to build a “partial” strategy for M + N. The situation is exactly the same as in concurrency theory where partial processes appear when we use internal communication: a deadlock due to “infinite internal chatter” can happen when we combine these two strategies. But, and this is what the cut-elimination result expresses, if both strategies are winning strategies, then we do get a total strategy which is a winning strategy.

It seems possible to give a definition of this compound strategy by following Gentzen’s argument. This corresponds to a direct study of the following property of a multiset of formulae M “there exists a winning strategy for M”. One gives a direct inductive definition of this property, and one shows that if both M + A and N + A^{∗} have this property, then so does M + N. The argument is a double induction, first on the complexity of the cut-formula, and then on the proof that the strategies are winning. Such a proof is presented in the last section. If we follow this approach however, it is not so clear what is the “structure” of the algorithm we get.

It seems much more interesting to see if a direct termination argument can be given, based on an analysis of what are the possible interactions between two players I and II.

2.1 Definition of the compound strategy

Here is an informal description of how this compound strategy is built. We assume that Myself has at his disposition two coplayers I and II. The player I represents a strategy for the game of configuration M + A and the player II a strategy for the game of configuration N + A^{∗}. Myself follows then the following protocol for the game against Nature of configuration M + N.

As long as one formula in M or N is universal, Myself waits for an instantiation coming from Nature. It transmits then this instantiation to the player I or II that is concerned with it.

After a finite number of such moves, both M and N have only existential formulae, so that Nature is waiting for an existential instantiation by Myself. Myself noticed that at least A or A^{∗} is existential. Let us say that A is existential. In this case, Myself asks to the player I what is his move. Myself knows that I will answer, because all the formulae in the configuration of the player I are existential. There are two cases:

• I instantiates a formula in M, then Myself does the same move and the game goes on,

• I instantiates the formula A. This is the difficult case.

In the second difficult case, Myself has not yet available any play against Nature. Indeed, Nature does not “see” the formula A and so, cannot transmit I’s move as in the first case.

There is a simple subcase however for which it is clear what Myself should do: if the player I instantiates the formula A without keeping it. In this case, the formula A becomes A_{1}, and Myself transmits this move to the player II. The configuration of I is then M + A_{1}, and the configuration of II is N + A_{1}^{∗}. The situation is the same as before, except that Myself is now waiting for II’s move. This “ping-pong” kind of play between I and II (via Myself) goes on for a finite amount of time, because the formula A is finite.

If during this internal communication, the formula A (resp. A^{∗}) becomes true, then the dual formula becomes false, and the game goes on with only the player II (resp. I), since this player follows then a winning strategy for N (resp. M), the other player becoming inactive. If both players follow a winning strategy, it is then clear that Myself follows a winning strategy by copying one of these two players.

The only remaining subcase is when Myself gets to a position where, let say, I has a move in A, but this move is such that I keeps the formula A (allowing backtracking). In such a case, it is not so clear what Myself can do. Here is a possibility, that we shall analyse (and which corresponds to Gentzen’s solution).

Myself transmits the move to the player II, the formula A^{∗} becoming A_{1}^{∗}, but also Myself keeps a copy of the player II in its initial configuration. The motivation is that Myself does not know whether or not the choice of the player I is definitive, and so, it makes sure that he can continue in case of a change of mind of the player I.

Once this is done, the configuration is almost like the previous subcase, except that Myself allows I to backtrack in his choice.

How is the game going on?? Myself asks to the latest copy of the player II, who plays now with a configuration N + A_{1}^{∗}, what is his move. If this move is in N, it is transmitted to Nature. If this move is in A_{1}^{∗}, Myself proceeds as before, i.e.:

• if this move is without backtracking (II is sure of his guess), then the configuration of II becomes N + A_{11}^{∗}, and Myself transmits this move to the player I, whose configuration becomes M + A + A_{11},

• if this move is with possible backtracking, then Myself does as before. The configuration of II becomes N + A_{1}^{∗} + A_{11}^{∗}, and Myself transmits this move to the player I, whose configuration becomes M + A + A_{11}, but Myself also keeps a copy of the player I in his configuration M + A + A_{1}, in case of a possible backtracking of II, and so on.

This finishes the description of the cut-elimination process.

2.2 Analysis of the problem of termination

The partial correctness of the compound strategy described in the previous subsection is clear. That is, if the players I and II follow a winning strategy for their respective configuration, it is clear that, if a game between Nature and Myself terminates, then Myself wins. However, it is not clear that the internal moves between the two players I and II terminate. In this subsection, we want to analyse the nature of the problem of termination.

First, it is not restrictive to assume that both players I and II, when they make a move in A, are doing an instantiation with possible backtracking. Second, we can suppose that there is no moves by I in M and no moves by II in N, so that we can restrict our attention to the moves in the formula A only. That is, we suppose that we have a (partial) strategy for A and a (partial) strategy for A^{∗}, and we analyse what happens if we let the strategy for A play against the strategy for A^{∗}. We can then analyse the possible “interaction paths”: we are sure that we will observe the moves

A + A_{1}, A_{1}^{∗} + A_{11}^{∗},

and for the next move, there is a choice: A + A_{11} can become A + A_{11} + A_{111} or A + A_{11} + A_{2}, and so on.

What we have to show is that if these moves come from winning strategies, then this interaction path is finite.

The problem appears then to be the following. We know that a winning strategy (for the player I) will win against any player that does not backtrack (and hence, in any such game, the player I will backtrack only a finite number of time). We want to generalise this to a play against a winning strategy (of II), which may backtrack. It is possible to show that if the strategy for II bacKtracks only a finite number of time, then the game will stop (because we have then a finitely branching tree, which has finite branches). The problem is that, a priori, the only way to be sure that this will happen is to show that I will backtrack a finite number of time. So there is a circularity here.

We can however formulate this problem as a pure problem of termination. The interaction can be represented as a sequence of formulae

B_{0} = A^{∗}, B_{1} = A + A_{1}, B_{2} = A_{1}^{∗} + A_{11}^{∗}, B_{3} = A + A_{11} + A_{2}, …

such that each B_{k} is a sum of formulae C_{1} + … + C_{n} where

1. all C_{i} are existential for i < n, and C_{n} is universal, we call C_{n} the end formula of B_{k}, and we write h(B_{k}) = C_{n}, t(B_{k}) = C_{1} + … + C_{n−1},

2. there is exactly one i < n such that ind(C_{n}) is a direct extension of ind(C_{i}). Furthermore, ind(C_{n}) is the least direct extension of σ for the lexicographical ordering that does not occur already in B_{0}, … B_{k}; we say then that i is answered in B_{k},

3. for each i < k, the dual C_{i}^{∗} appears as the end formula of exactly one B_{j}, for one j < k,

4. if i is answered in B_{k}, then t(B_{k+1}) = t(B_{i}) + h(B_{k}).

The formulae B_{0}, …, B_{k} corresponds to the copies of the players I and II. We call such a sequence B_{0}, …, B_{k} an interaction sequence.

The refinement of Gentzen’s cut-elimination is that such an interaction sequence is finite, if the players follow a winning strategy. Gentzen’s argument (see the last section) provides only the existence of a winning strategy, without describing it. It does seem possible however to use a similar argument to show that the interaction sequence is finite, as will be shown in the next version of this paper.

2.3 Total correctness in some restricted cases

A termination argument is readily given if A is of low logical complexity, for instance of the form ∃x B[x], or ∃x∀y B[x, y]. This becomes more complicated in the case ∃x∀y∃z B[x, y, z], and we leave to the reader an analysis of all possible behaviours of cut-elimination in this case.

We conjecture the termination of the algorithm in the general case. We will prove here only the case of simple backtracking.

With this added assumption, we use that A is finite, of depth n, and we remark that the number of formulae extension of A_{n_{1}...n_{p}} occurring in the interaction sequence is finite, by induction on n − p.

2.4 No-counter example interpretation

Another method (maybe inspired by Gentzen’s proof) of giving a computational meaning of arithmetical truth is the no-counter example interpretation due to Kreisel. This is described for instance in the introduction of [6]. One can see the present “interaction approach” as an attempt towards the analysis of a computation at higher-type, in the spirit of Kleene 78 [5].

3 Towards a “symmetric” cut-elimination

We will analyse now a “multiple cut”. We will limit ourselves to the case of a cut of the following form: we suppose to have a strategy for the games of configurations M + A, N + A^{∗} + B^{∗} and L + B, and we try to build from these strategies a strategy for the game of configuration M + N + L.

It appears that there is only one choice if A or B is universal. If both A and B are existential however, there are several choices. The main point of this paper is to show that the usual two choices: first eliminate the cut between M + A and N + A^{∗} + B^{∗}, then between M + N + B^{∗} and L + B, or the opposite solution, first eliminate the cut between L + B and N + A^{∗} + B^{∗}, then between L + N + A^{∗} and M + A, not only lead to distinct results in general, but also are not natural w.r.t. the present game-theoretical analysis of cut-elimination.

3.1 A concrete example

This phenomena is particularly clear for the following concrete example, which is due to Gabriel Stolzenberg. It involves a typically classical lemma: the “infinite box principle”.

The example is the following. We suppose given as an “oracle” a stream of 0 and 1. Classically, there are infinitely many 0, or infinitely many 1. The question is about a possible computational meaning of this assertion.

Let us represent the stream of 0 and 1 by a parameter f which is a unary function symbol. We represent a computational meaning of the infinite box principle as a winning strategy for the game of configuration

∀x_{0}∃y_{0} [x_{0} ≤ y_{0} & f(y_{0}) = 0] + ∀x_{1}∃y_{1} [x_{1} ≤ y_{1} & f(y_{1}) = 1],

that we will write A(0) + A(1). Here is such a winning strategy: Myself waits for two instantiations x_{0} = u_{0} and x_{1} = u_{1} from Nature. When Myself gets these values, he computes the value of u =max(u_{0}, u_{1}) and asks to the oracle the value of f(u). If f(u) = 0 Myself wins by playing y_{0} = u and if f(u) = 1, Myself wins by playing y_{1} = u.

This interpretation seems very natural.

The question now is to see how to use this “computational” interpretation to do some effective computation. Let us analyse a trivial use of this lemma: from the infinite box principle, we deduce that there are at least two 0s or at least two 1s. Indeed, if there are infinitely many 0, there are two 0s (by picking the first two 0s), and similarly in the other case.

We have so a winning strategy for the configuration

∃a_{0}∃b_{0} [a_{0} < b_{0} & f(a_{0}) = f(b_{0}) = 0] + ∃x_{0}∀y_{0} [y_{0} < x_{0} ∨ f(y_{0}) = 1],

i.e. if there are infinitely many 0s, then there are two 0s. We will write M(0) + A(0)^{∗} this configuration. and a winning strategy for the configuration

∃a_{1}∃b_{1} [a_{1} < b_{1} & f(a_{1}) = f(b_{1}) = 1] + ∃x_{1}∀y_{1} [y_{1} < x_{1} ∨ f(y_{1}) = 0].

i.e. if there are infinitely many 1s, then there are two 1s. We will write M(1) + A(1)^{∗} this configuration.

Let us precise this winning strategy for the configuration M(0) + A(0)^{∗}. Myself starts by instantiating x_{0} = 0, keeping the formula A(0)^{∗}. Nature answers then by giving y_{0} = u. If we have u < 0 ∨ f(u) = 1, then Myself wins. If we have f(u) = 0, then Myself backtracks in his choice of x_{0}, and choses now x_{0} = u + 1. Nature answers by giving y_{0} = v. If we have v < u + 1 ∨ f(v) = 1, then Myself wins. If we have u + 1 ≤ v and f(v) = 0, then Myself wins by playing a_{0} = u and b_{0} = v.

We have now three winning strategies for the respective configurations M(0)+A(0), A(0)^{∗}+ A(1)^{∗} and A(1) + M(1), and we want a winning strategy for the configuration M(0) + M(1). Notice indeed that such a winning strategy will provide us with two 0s or two 1s.

One way to solve this problem is to “put parenthesis”. We analyse this way first.

3.2 “Usual” cut-elimination is not symmetric

It consists in reducing the problem of multiple cuts to the problem of simple cut. Symbolically, we want to do

CUT(M(0) + A(0), A(0)^{∗} + A(1)^{∗}, A(1) + M(1))

and we do this by doing either

(∗)  CUT(CUT(M(0) + A(0), A(0)^{∗} + A(1)^{∗}), A(1) + M(1))

or by doing

(∗∗)  CUT(M(0) + A(0), CUT(A(0)^{∗} + A(1)^{∗}, A(1) + M(1))),

using the algorithm described above.

We will not do it explicitly here, leaving this as an exercise for the reader. The important points are that

• we do not get the same algorithm doing (*) and doing (**),

• both algorithms (*) and (**) are not symmetric w.r.t. 0/1, that is, they do not provide the same answer if we interchange 0 and 1 in the values of the oracle f.

3.3 A symmetric cut-elimination

It is remarkable that, on this simple example, a way of doing cut-elimination suggested by “common sense”, which is neither (*) nor (**), furnishes an algorithm that is symmetric w.r.t. 0/1.

More generally, in the case of a cut between A, A^{∗}+B^{∗} and B where A and B are existential, there seems to be a canonical way of doing the cut-elimination in the case of simple backtracking. This way differs from the one where we put parenthesis in general.

We will analyse this on one possible interaction sequence (which corresponds to one possible interaction sequence for the example described above).

Since A and B are existential, the corresponding strategies guess first values for them, with possible backtracking: A_{1} and B_{1}. Then, Myself asks what is the move for A_{1}^{∗} + B_{1}^{∗}. Let say it is A_{11}^{∗}. In this case, we consider that the choice A_{1} has been refuted, and Myself transmits this refutation to the corresponding player. This player can either persist in his choice playing A_{111}, or changes his mind, playing A_{2}. In this last choice, since only simple backtracking is allowed, Myself can naturally consider that the choice A_{1} has been definitively refuted and will never come back to this choice again. So, Myself asks what is the move for A_{2}^{∗} + B_{1}^{∗}. If the answer is B_{11}, and the move for B_{1} + B_{11} is B_{2}, it is natural that Myself asks what is the move for A_{2}^{∗} + B_{2}^{∗}, and so on.

But this is not what will happen if Myself tries to evaluate

CUT(CUT(A, A^{∗} + B^{∗}), B).

For this “protocol”, Myself asks instead what is the move for A_{1}^{∗} + B_{2}^{∗}, forgetting completely what happened about A.

One can generally expect inefficiency (at least in the case of simple backtracking) if Myself follows the protocol

CUT(CUT(A, A^{∗} + B^{∗}), B).

In this case indeed, whenever the player associated with the formula B tries a new instantiation B_{i} for B, Myself comes back to the first instantiation for A, and asks what is the move for A_{1}^{∗} + B_{i}^{∗}.

Symmetrically, if Myself follow the protocol

CUT(A, CUT(A^{∗} + B^{∗}, B)).

In this case, whenever the player associated with the formula A tries a new instantiation A_{i} for A, Myself comes back to the first instantiation for B, and asks what is the move for A_{i}^{∗} + B_{1}^{∗}.

The symmetric protocol, which seems natural, is instead that Myself asks systematically the move for A_{i}^{∗} + B_{j}^{∗} where A_{i} (resp. B_{j}) is the last instantiation of A (resp. B) that has been played. Furthermore, if Myself follows this protocol, then a given game can be analysed as two sequences of interaction for A and B that are interleaved, hence a direct termination argument.

Notice that this is a new “ternary” way of doing cut-elimination, which is not reducible to a combination of two “binary” cuts.

In the case where A or B is universal, then the “ternary” cut-elimination is equivalent to a combination of “two” cuts (except of doing less copies.) This is what happened, in a iterated way, with the cut-elimination procedure presented above compared to Gentzen’s cut-elimination.

This analysis can be extended to the case of a “multi-cut” A, A^{∗} + B^{∗}, B, with A, B of arbitrary complexity, but the players follow a strategy of simple backtracking.

4 An inductive presentation of ω-logic

For sake of comparison, we reformulate usual definitions of ω-logic in the framework of generalised inductive definitions.

We define inductively when a multiset M of formulae is (classically) true. There are the following clauses:

• if M contains a true atomic formulae, then M is true,

• if there exists n_{0} such that M + A[n_{0}] is true, then M + ∃n A[n] is true,

• if there exists n_{0} such that M + ∃n A[n] + A[n_{0}] is true, then M + ∃n A[n] is true,

• if M + A + B is true, then M + A ∨ B is true,

• if M + A and M + B are true, then M + A & B is true,

• if M + A[n_{0}] is true for all integers n_{0}, then M + ∀n A[n] is true.

Only the last clause is not finitary.

If we forget the point that in the game-theoretic presentation we consider only prenex formulae, the main difference is that in the game-theoretic presentation, we have to use the last rule whenever one formula is universal in the multiset of sequents. It follows that if there is a winning strategy for a configuration M, then M is true with the present definition.

Lemma 1 The following properties hold

• if A is a false atomic formula, and M + A is true, then M is true,

• if M + A ∨ B is true, then M + A + B is true,

• if M + A & B is true, then M + A and M + B are true,

• if M + ∀n A[n] is true, then M + A[n_{0}] is true for all integer n_{0}.

Proof: All these properties are of the form: if M is true, then M′ is true, and they are proved directly by induction on the proof that M is true.

Lemma 2 If M + A + A is true, then so is M + A.

Proof: By double induction: first on the formula A, and then by induction on the proof that M + A is true, using the previous lemma 1.

Proposition 1 If M + A and N + A^{∗} are true, then so is M + N.

Proof: By double induction, first on the formula A, and then by induction on the proofs that M + A and N + A^{∗} are true. Let us look at one case: A is ∃n B[n] and M + A is true because M + B[n_{0}] + A is true. Then, by lemma 1, we know that N + B[n_{0}]^{∗} is true. By induction hypothesis, by a cut between N + A^{∗} and M + B[n_{0}] + A, we get that N + M + B[n_{0}] is true. By induction hypothesis, since B[n_{0}] is less complex than A, we get that N + N + M is true. By lemma 2, N + M is true.

Conclusion

We have presented a conjecture of termination of an internal communication, that would refine Gentzen’s cut-elimination. This conjecture is valid in the case of cuts of low logical complexity, and in a restricted case of “simple backtracking.” The same idea in the case of multiple cuts leads to a protocol of cut-elimination distinct in general from the one where we decompose the multiple cut in binary cuts.

One important point to precise is the connection between the symmetric protocol we presented and the fact, noticed by Hugo Herbelin, that there does exist a Gentzen like cutelimination procedure that lead to a symmetric answer. It is not clear at all yet what is the game-theoretical meaning of this procedure.

References

[1] Bernays P. (1968) “On the original Gentzen consistency proof for number theory.” In Intuitionism and Proof Theory, Kino, Myhill, Vesley eds.

[2] Constable, R. “The semantics of evidence.” Technical Report TR 85-684, Cornell University, Department of Computer Science, Ithaca, New York, May 1985.

[3] Gentzen G. (1969) “Collected Works.” North-Holland, Szabo ed.

[4] Isles, D. “A Finite Analog to the Lowenheim-Skolem Theorem.” Draft, 1990.

[5] Kleene, S.C. (1978) “Recursive Functionals and Quantifiers of Finite Types Revisited II.” in The Kleene Symposium, North-Holland, J. Barwise, H.J. Keisler and K. Kunen eds.

[6] Martin-Löf P. (1968) “Notes on Constructive Mathematics.” Almqvist & Wiksell ed.

[7] Martin-Löf P. “Hauptsatz for the Intuitionistic Theory of Iterated Inductive Definitions.” in Proceedings of the Second Scandinavian Logic Symposium, North-Holland, J.E. Fenstad ed.

[8] Ranta A., Ph. D. Thesis (1990), Stockholm.

[9] Tait W.W. (1968) “Normal Derivability in Classical Logic.” Springer Lecture Notes in Mathematics 72, J. Barwise ed.

100

Logical Support for Modularisation^{†}

Răzvan Diaconescu  Joseph Goguen^{‡}

Petros Stefaneas Programming Research Group, Oxford University

July 1991

Abstract: Modularisation is important for managing the complex structures that can arise in large theorem proving problems, and in large software and/or hardware development projects. This paper studies some properties of logical systems that support the definition, combination, parameterisation and reuse of modules. These properties include: (1) the preservation of various kinds of conservative extension under pushouts; (2) distributive laws for information hiding over sums; and

(3) (Craig style) interpolation properties. Our results illuminate some interesting differences between equational style logics and first order style logics, encouraging us to conclude that, on the whole, equational style logics are more suitable for modularisation than first order style logics. We represent logical systems as institutions, and modules as sets of sentences. An important technical foundation is a novel categorical axiomatisation of the notion of “inclusion”. We also show how to subsume the deduction-based approach of π-institutions under that of ordinary institutions, so that our results also apply to that setting.

1 Introduction

Modules are an important feature of many modern programming and specification languages, assisting with the development of large and complex systems. Modularisation for theorem proving has been studied less, and in fact most results have appeared in the context of formal software engineering, particularly specification languages. This paper studies some properties of logical systems that are important as support for modularisation, where modules are represented as sets of sentences in a logical system, and logical systems are represented as institutions. This notion of module is directly applicable to theorem proving, software specification languages, hardware description languages, and logic-based programming languages; with some extra effort, it can even be applied to imperative programming languages. See [12] for some general discussion and examples.

We show that while a number of properties hold for any institution that satisfies certain modest conditions, some other properties are more delicate, and only hold for institutions that are close to equational logic. Moreover, certain properties depend crucially on how they are formulated; for example, forms of Craig interpolation that are equivalent for first order logic are not at all equivalent for many other important institutions. There are also some desirable properties that are rarely satisfied in practice, such as a strong form of distribution for information hiding over sum.

†The research reported in this paper has been supported in part by grants from the Science and Engineering Research Council and the Fujitsu Corporation.

‡Also, SRI International, Menlo Park CA 94025.

We have been particularly interested in the comparison between equational logic and classical first order logic. It has been argued that certain properties of equational logic render it unsuitable for use in specification. However, results and arguments in this paper suggest that these reasons are not really valid, and in fact, that equational logic may be superior in certain respects.

A categorical axiomatisation of the notion of inclusion permits us to give simple definitions for operations on modules in the general setting of institutions. Also, we show how producing a suitable model theory “out of thin air” for logical systems based on deduction (as formalised by π-institutions) allows them to be seen as ordinary institutions, so that our results about institutions also apply to logical systems that are based on deduction rather than on satisfaction.

1.1 Some Motivation

Experience shows that it can be very difficult to develop and maintain the logical structures that occur in large proofs and in large software and/or hardware development projects. One systematic approach to these difficulties is to modularise systems into relatively small, “mind sized” pieces that can be developed and maintained separately, and can then be interconnected to form the whole [11]. For many applications, it is sufficient to consider a module to be a set of sentences. This is the case in theorem proving, software and/or hardware specification, and in logic-based programming languages such as pure Lisp, pure Prolog, and OBJ. There are a number of important operations and relations on such modules. Two basic operations are sum and renaming. The first simply combines the resources available from two or more modules, while the second changes the names of some internal features. Laws concerning such operations could be used, for example, to prove the correctness of an efficient implementation of module interconnection for a programming language. A third operation which makes this challenging is information hiding, whereby some internal features of a module are made inaccessible outside the module. One would like to know that everything true of the visible part of some combination of modules can be proved from what is known about the visible parts of the component modules. Unfortunately, this often fails for real systems, as well as for theories over most institutions.

A particularly important relation between theories is that of conservative extension, which says that any model of the subtheory can be expanded to a model of the supertheory. This property can be important for the reuse of modules. Properties of extensions also arise in connection with parameterised (i.e., generic) modules.

A promising approach to system development (whether proofs, programs, or chips) is to start from some specification modules, and a description of the system as an interconnection of these modules. This permits the design, and the verification of certain properties, such as security, to be carried out at a more abstract level than that of code. It should thus improve reliability, and with suitable mechanical support, might also improve the efficiency of the programming process. In addition, it promotes software reuse, because some modules may be taken either directly from a library, or may be modifications of library modules. To support the construction of such a software development environment, it would be helpful to know what laws are satisfied by the basic operations on modules.

Institutions allow us to discuss the crucial relationship between theories and models, without a commitment to either side at the expense of the other. This is important, because there is a tension between these two aspects of logic, particularly for applications to Computing Science, because on the one hand, we are primarily interested in certain models, such as specific VLSI chips, or specific programs running on specific machines, but on the other hand, these may be very large, complex objects, of which only certain specific properties are of particular interest. To check such properties, we manipulate syntactic representations of the models and their properties. However, the criteria of correctness for these manipulations must refer back to the models.

It follows from this discussion that we should define a module to be a syntactic entity, such as a set of sentences, and that we should carefully distinguish such entities from their denotations, which will be sets of modules. It also follows that we should define notions like “conservative extension” of theories semantically, and then seek syntactic criteria for checking such relationships. Thus, we do not agree with the approach of Maibaum, Sadler, Turski and others [28, 46], who do not deal with models at all, but only with sentences and deduction. In our view, such an approach cannot adequately formalise the actual situation in (say) software engineering, which involves models of concrete objects, as well as their descriptions. This is particularly illustrated by the inability of the purely syntactic notion of conservative extension to capture the underlying semantic property. On the other hand, we also disagree with the approach of Sannella, Tarlecki and others [39, 40, 41] who define modules to be classes of modules, because such a definition does not capture the fact that real modules are bits of text, rather than (say) sets of running chips. This is because designers and verifiers necessarily deal with descriptions, rather than with the models themselves.

Under this view, operations on modules should be operations on sets of sentences. However, it is highly desirable that such operations should be meaningful as operations on the corresponding denotations, as opposed to merely being arbitary textual “edit” operations. Once again, semantics provides a “reality check” for syntax.

It is necessary to use machinery as abstract as categories and institutions for the comparative study of modules over various logical systems. For example, an assertion of the form “the Craig Interpolation Property and the Export Distributive Law are equivalent” is not meaningful in the context of a single logical system; it needs to be quantified over logical systems. Perhaps an analogy will help to clarify this point. Suppose that we are interested in studying properties of groups; two such properties might be “commutativity” and “finiteness.” Then asserting that “commutativity and finiteness are equivalent” for some group where both properties happen to hold (such as _{2}) is valid, but not very meaningful: such an assertion should be universally quantified over groups (and then it is false).

1.2 Some History

The earliest work on software modularisation with which we are familiar is due to Parnas [34, 35, 33]. Modules differ from more traditional program structuring mechanisms such as subroutines, procedures and blocks, in that they may include a number of procedure and data definitions, may be parameterised, may import other modules, and may hide certain elements. Such modules can be separately compiled, and they support software reuse because they can also be separately specified and verified. A major motivation for modules in this sense is to facilitate the modification of software, by localizing the representation of data and the operations that depend upon it; this is called information hiding. This notion of module is essentially syntactic; it has to do with the texts that describe software systems. Thus, a semantic notion of module, such as that advocated by Sannella and Tarlecki [39, 40, 41], would fail to capture this basic aspect of modules.

The earliest work that we know on modules in specification is due to Burstall and Goguen, in connection with their specification language Clear [4, 5]. This approach has semantics based on the theory of institutions, and has been applied to various logic-based programming languages, particularly OBJ [8, 23] (which is based on order sorted equational logic), Eqlog [20] (which combines functional and logic programming), foops [21] (which combines functional and object oriented programming), and fooplog [21] (which combines all three paradigms). In [11], this approach is extended to module systems for imperative programming languages.

The earliest work we know that gives a calculus of modules is due to Goguen and Burstall [14]. Building on previous work on Clear, they studied laws that relate horizontal structuring relationships, and vertical implementing (also called “refinement”) relationships, concluding that the axioms of a 2-category should be satisfied. Clear introduced the ideas that a specification module is a theory, and that such modules are put together using colimits; these ideas have their origin in some earlier work on General Systems Theory [10, 17]. Clear provided operations for summing, renaming, extending, hiding, importing and (in the case of generics) applying modules. A number of general laws which apply in particular to module operations can be found in [10], and a number of others arise during the proofs in [5].

The so-called module algebra developed in the pioneering paper of Bergstra, Heering and Klint [2] represents another ambitious attempt to capture the horizontal structure of modules, by examining the equations that hold among certain basic operations upon modules, including sum and information hiding. These equations, together with constructors for signatures and sentences, form a many sorted equational presentation, about which some interesting results can be proved, including a normal form theorem. Unfortunately, this work has first order logic built into its choice of the constructors for signatures and sentences.

By contrast, the present paper starts with an arbitary logical system, and explores what properties it must have to support a practical calculus of modules. Every reasonable institution supports modules and certain simple operations on modules; we may then ask, what properties do these operations have? Note that this exploration should include properties that are not expressible as equational laws, such as the preservation of conservative extensions by pushouts.

Although [2] does not build on a general notion of logical system, it does abstract some interesting general principles from the special case of first order logic. In particular, we will see that the equivalence of Craig Interpolation with a distributive law for information hiding asserted in [2] is actually valid at the level of institutions, under certain conditions (namely, compactness and closure under implication and false); moreover, we can use essentially the same proof that they gave. Indeed, their paper was a major inspiration for the present paper, and in our opinion, opened a fascinating realm of new questions in the theory of institutions.

The original semantics of Clear [5] represented sums of theories by colimits, but failed to capture the use of subsignatures and subtheories that is natural in examples like equational logic and first order logic. The present paper shows how to capture such inclusions through a general axiomatisation of the notion of inclusion, such that sums are given by at least upper bounds of inclusions. A more concrete approach to inclusions is given by Sannella and Tarlecki in [39]. The desirability of using inclusions for theories first appeared in the thesis of Sannella [38], which gave a set theoretic semantics for Clear in the case of many sorted equational logic.

Another choice is whether to use theories, which are sets of sentences closed under entailment, or to use presentations, which are not necessarily so closed. Although the first choice represents the ideal, only finite sets can be actually implemented. However, designers and verifiers may need to know about consequences of a specification that do not happen to be in its original presentation, but instead appear in its theory. Therefore, a general approach should consider modules to be theories rather than presentations; then the problem for a practical implementation is how to manipulate finite sets of sentences in a way that respects the behaviours of their (generally infinite) corresponding closed theories, and of course, their models.

Much interesting work using institutions has been done by Tarlecki [42, 44, 45, 43] and by Sannella and Tarlecki [39, 40, 41]. See also [9] for some recent work on the semantics of module composition over institutions.

1.3 Summary

This paper includes the following:

1. a novel categorical characterisation of the notion of “inclusion,” which is used to explicate the notion of “theory extension”;

2. a lifting of exactness from the signatures of an institution to its theories;

3. an embedding of the category of π-institutions into the category of ordinary institutions;

4. a general discussion of Craig interpolation for institutions with inclusions;

5. a discussion of the intuitive significance of different distributive laws for information hiding over the sum of modules;

6. a proof that Craig interpolation is equivalent to a certain distributive law, for reasonable compact institutions with implication and false;

7. a discussion of the relationship between the syntactic and semantic formulations of conservative extension;

8. a proof that the middle distributive law holds for conservative extensions in reasonable semiexact institutions;

9. a proof that a pushout of a conservative (or persistent) extension is again conservative (or persistent) in a reasonable semiexact institution; and

10. a proof that the pushouts of two extensions conservative for initiality are again conservative for initiality in a reasonable semiexact institution.

1.4 Prerequisites

This paper assumes familiarity with basic category theory, including categories, functors, limits, colimits, and adjoints. The necessary material may be found in [27], [26], or in a more gentle style, [24]. By way of notation, we use “;” for composition, we let 1_{A} denote the identity morphism at an object A, and we let | | denote the class of objects of a category .

We have found that certain readers may have doubts about set-theoretic foundations when category theory is used. In fact, this paper stays well away from anything that is genuinely problematical, and nearly any foundation that has been proposed for category theory will do, including the “hierarchy of universes” discussed e.g., by Mac Lane [27], Section I.6.

1.5 Acknowledgements

We wish to thank Drs. José Fiadeiro, Piet Rodenburg, and especially Andrzej Tarlecki, for their very useful comments on drafts of this paper. We also thank Prof. Rod Burstall for his important role in creating the theory of institutions. In addition, we thank Drs. José Meseguer, Donald Sannella, Andrzej Tarlecki, José Fiadeiro, Piet Rodenburg, and Jan Heering, as well as Profs. Thomas Maibaum, Jan Bergstra and Paul Klint for their inspiring papers, without which the present paper would not have been written.

2 Basic Concepts

This section presents some concepts that are needed for the rest of the paper. The first subsection discusses factorisations and inclusions, while the second summarises some aspects of institutions, particularly how they interact with inclusion systems. The third subsection discusses exactness, and the fourth π-institutions.

2.1 Factorisations and Inclusions

We first present the standard notion of a factorisation system (as in [26]), and then use it in building a novel axiomatisation for the notion of “inclusion” that is used in our work on modules.

Definition 1 An image factorisation system for a category consists of a class M of monics and a class E of epics in such that

(1) both E and M are closed under composition,

(2) all isomorphisms are in both M and E, and

(3) every morphism f in can be factored as e; m with e ∈ E and m ∈ M “uniquely up to isomorphism” in the sense that if e′; m′ is another factorisation of f with e′ ∈ E and m′ ∈ M, then there is a unique isomorphism from the centre object C of e; m (i.e., the target of e and the source of m) to the centre object C′ of e′; m′ such that the diagram below commutes:

[figure: C; C′; A; B; e′; m′; e; m]

□

Our definition of inclusion system will use the following, which comes from [1]:

Definition 2 Let M be a class of arrows in a category . Then is M-inductive iff whenever all the injections of a co-cone over some diagram in lie in M, then there is a colimit of this diagram such that the universal arrow from the colimit to the co-cone also lies in M. □

Now the main concept of this subsection:

Definition 3 An inclusion system for a category consists of a class of monics and a class E of epics in such that:

(1) both E and are subcategories of such that |E| = | | = | |;

(2) all isomorphisms in are identities, and all isomorphisms in are in E;

(3) every morphism f in can be factored uniquely as e; i with e ∈ E and i ∈ ;

(4) is a partial order (i.e., for any objects A, B, there is at most one morphism A → B in and if there is also a morphism B → A in , then A = B);

(5) has finite least upper bounds (i.e., finite coproducts in ), denoted +; and

(6) is -inductive.

We will call the morphisms in inclusions, and use the notation A ↪ B. Also, we let ∅ denote the bottom element of (i.e., the empty least upper bound, which is also the initial object in ). Given i: A ↪ B and f : B → C, we let f _{A} denote the composition i; f, and call it the restriction of f to A. We will also say that a category with an inclusion system is inclusive. □

Most of the categories used in specification and programming have obvious and natural inclusion systems, including the following:

Example 4 The category Set of sets with the inclusions and E the surjections is an inclusion system. □

Example 5 Recall (e.g., from [22]) that a many sorted signature Σ consists of a set S of sorts and an S^{∗} × S-indexed family of sets Σ_{w,s} whose elements are the operation symbols of arity (i.e., input sorts) w ∈ S^{∗}, and value (i.e., output) s ∈ S. Also, a morphism (S, Σ) → (S′, Σ′) of many sorted signatures consists of a function f : S → S′ and a S^{∗} × S-indexed family of functions g_{w,s}: Σ_{w,s} → Σ′_{f(w),f(s)}. Then we get an inclusion system in a natural way by defining by (S, Σ) ↪ (S′, Σ′) iff S ↪ S′ and Σ_{w,s} ↪ Σ′_{w,s} for each w ∈ S^{∗} and s ∈ S, and defining E to be the (component-wise) surjective signature morphisms. □

Example 6 Similarly, the usual category of (unsorted) first order signatures has an obvious inclusion system. Recall that a first order signature is a pair (Σ, Π), where both Σ are Π are ωindexed families of sets, with Σ_{n} the operation symbols of arity n and Π_{n} the predicate symbols of arity n, for n ∈ ω. Also, a morphism (Σ, Π) → (Σ′, Π′) is a pair (f, g) of ω-indexed functions, where f_{n}: Σ_{n} → Σ′_{n} translates operation symbols, and g_{n}: Π_{n} → Π′_{n} translates predicate symbols. Then we get an inclusion system by defining by (Σ, Π) ↪ (Σ′, Π′) iff Σ_{n} ↪ Σ′_{n} and Π_{n} ↪ Π′_{n} for each n ∈ ω, and defining E to be the (component-wise) surjective signature morphisms. □

The inclusion systems axiom are sufficient to ensure that many familiar properties of inclusions hold in general, including the following:

Fact 7 is -right cancellable, in the sense that if f; g ∈ and g ∈ , then f ∈ .

Proof: Factor f as e; i with e ∈ E and i ∈ . Then e; i; g is a factorisation of f; g, with i; g ∈ because both i and g are inclusions. But f; g also factors trivially as 1; (f; g), and so (3) of Definition 3 gives e = 1 and f = i. Therefore, f ∈ . □

Fact 8 If is a category with an inclusion system ( , E), then its category of inclusions has all finite colimits. If has an initial object ∅, then ∅ is also initial in ; hence, has at most one initial object.

Proof: trivially has coequalisers because it is a partial order, and it has finite coproducts by (5) of Definition 3. □

Next, we discuss how the greatest lower and least upper bounds of objects in relate to constructions in ; these arguments have a set-theoretic flavour.

Proposition 9 Let be a category with an inclusion system ( , E) and with pullbacks. Let A ↪ B and A′ ↪ B be inclusions in . Then there is a unique pullback in of these inclusions such that the arrows of the pullback cone are also inclusions.

Proof: Let (P → A, P → A′) be a pullback in of the inclusions of A and A′ into B. Now factor the pullback arrows as P → A = e; C ↪ A and P → A′ = e′; C′ ↪ A′ where e, e′ ∈ E. Because of the uniqueness of the factorisation of P → B, it follows that C = C′ and e = e′. It now follows that (C ↪ A, C ↪ A′) is also a pullback cone, and the uniqueness of C follows from Fact 7. □

Definition 10 Let be a category with an inclusion system ( , E) and with pullbacks. Let A and B be objects of . Then the sum of A and B, denoted A + B, is the coproduct of A and B in , and the intersection of A and B, denoted A ∩ B, is the (unique) inclusion pullback in of the inclusions (A ↪ A + B, B ↪ A + B) given by Proposition 9. □

Proposition 11 Let be a category with an inclusion system ( , E) and with pullbacks. Then for any objects A, B ∈ | | we have:

1. the sum A + B is the least upper bound of A and B in ;

2. the intersection A ∩ B is the greatest lower bound of A and B in ;

3. sum and intersection are unique;

4. A ∩ B is included in A and B, and all three of these objects are included in A + B;

5. the intersection is the pullback in of the sum; and

6. if has pushouts, then the sum is the pushout in of the intersection.

Proof: The first two assertions follow directly from (4) of Definition 3. Then the sum A + B is unique by its definition as the least upper bound in of A and B, and the intersection is unique because it is the greatest lower bound in .

The maps A ∩ B ↪ A and A ∩ B ↪ B are inclusions by Propositions 9, and thus A ∩ B ↪ A + B is a composite of inclusions.

That the intersection is the pullback in of the sum follows from the definition of intersections and the previous proposition.

Now let Q be a pushout of the intersection. Let u: Q → A + B be the unique arrow such that (A → Q); u = (A ↪ A + B) and (B → Q); u = (B ↪ A + B). Because is -inductive, we can choose Q such that Q → A + B is also an inclusion. It then follows that both A → Q and B → Q are inclusions by right cancellability. Because A + B is the least upper bound of A and B, and because A, B ⊆ Q ⊆ A + B, we conclude that Q = A + B. □

Definition 12 An inclusion system for a category C is distributive iff the following two laws hold for all objects A, B, C in C:

1. A + (B ∩ C) = (A ∩ B) + (A ∩ C).

2. A ∩ (B + C) = (A + B) ∩ (A + C).

□

We can get a non-distributive inclusion system from any non-distributive lattice L, by letting C be L regarded as the partial order category with an arrow A → B iff A ≤ B in L.

Definition 13 Let and ′ be categories with inclusion systems ( , E) and ( ′, E′), respectively. Then an inclusion system morphism is a functor F : → ′ such that F : → ′, and F _{E} : E → E′, and ∩ and + are preserved. □

Fact 14 If F is a morphism of inclusion systems, then F (c) = F (i); F (e) is the ( ′, E′)-factorisa-tion of F (c) in ′ if i; e is the ( , E)-factorisation of c in . □

The following expresses a basic relationship between pushouts and inclusions that is mainly used in Section 5:

Definition 15 Let be an inclusive category. Then pushouts preserve inclusions in iff whenever a pair of arrows (A ↪ A′, A → B) has a pushout, then they have a pushout of the form (B ↪ B′, A′ → B′). □

2.2 Institutions

In a series of papers beginning in 1979, Burstall and Goguen have developed institutions as a formalisation of the intuitive notion of a logical system; the most recent and complete exposition is [16]. This approach gives axioms for the satisfaction relation ⊧_{Σ} that take account of the fact that one may wish to translate sentences and/or models from one signature to another. A special case of this translation may be familiar from first order model theory: let Σ ↪ Σ′ be an inclusion of first order signatures, and let M be a Σ′-model; then we can form M _{Σ}, the reduct of M to Σ. Similarly, if e is a Σ-sentence, then we can always view it as a Σ′-sentence (but there is no standard notation for this). The key axiom, called the Satisfaction Condition, says that truth is invariant under change of notation. This paper uses the precision of this formalisation of logical systems to discuss properties of modules over logical systems in a general way.

Definition 16 An institution consists of

1. a category Sign, whose objects are called signatures,

2. a functor Sen: Sign → Set, giving for each signature a set whose elements are called sentences over that signature,

3. a functor Mod: Sign → Cat^{op} giving for each signature Σ a category whose objects are called Σ-models, and whose arrows are called Σ-(model) morphisms, and

4. a relation ⊧_{Σ} ⊆ |Mod(Σ)| × Sen(Σ) for each Σ ∈ |Sign|, called Σ-satisfaction, such that for each morphism φ: Σ → Σ′ in Sign, the Satisfaction Condition

M′ ⊧_{Σ′} Sen(φ)(e) iff Mod(φ)(M′) ⊧_{Σ} e

holds for each M′ ∈ |Mod(Σ′)| and e ∈ Sen(Σ).

An institution is compact iff whenever E ⊧ e then there is a finite subset E′ ⊆ E such that E′ ⊧ e.

We may write φ(e) or even φe for Sen(φ)(e), and M′ _{φ} or possibly φ(M′), for Mod(φ)(M′); also we may drop the signature subscripts on the satisfaction relation when it is not confusing. If M is a Σ-model and E is a set of Σ-sentences, then we let M ⊧_{Σ} E mean that M ⊧_{Σ} e for each e ∈ E. Also, if E is a set of Σ-sentences and e is a single Σ-sentence, then we let E ⊧_{Σ} e mean that for each Σ-model M, if M ⊧_{Σ} E then M ⊧_{Σ} e. Finally, we let φ(E) = {φ(e) | e ∈ E}. □

Definition 17 An institution with an inclusion system ( ,E) on its category of signatures respects that inclusion system iff the functor Sen: Sign → Set is an inclusion system morphism, where Set has the inclusion system described in Example 4; for short, let us say that such an institution is inclusive. Given i: Σ ↪ Σ′ and a Σ′-model M, we may write i(M) as M _{i} or M _{Σ} and call it the reduct of M to Σ.

An inclusive institution is distributive iff the inclusion system on its signatures is distributive. □

Example 18 The many sorted algebraic institution is inclusive and distributive with the inclusion system of Example 5 on its signatures. □

Example 19 The unsorted first order institution is inclusive and distributive with the inclusion system of Example 6 on its signatures. □

Any non-distributive inclusion system can be turned into a trivial non-distributive inclusive institution, with the inclusion system as its category of signatures, and with no models and no sentences. However, all of the usual logical systems are distributive inclusive institutions, including first-order logic and equational logic.

Definition 20 A presentation is a pair (Σ, E) where Σ is a signature and E is a set of Σsentences. A presentation (Σ, E) is a theory iff E is closed under semantic entailment, in the sense that if E ⊧_{Σ} e then e ∈ E. We let E^{•} denote the closure of a set E of sentences^{1}.

If T = (Σ, E) is a theory, then its denotation, which we might write [[T]], is the full subcategory of Mod(Σ) with objects M such that M ⊧_{Σ} E.

If (Σ, E) and (Σ′, E′) are presentations, then a presentation morphism (Σ, E) → (Σ′, E′) is a signature morphism φ: Σ → Σ′ such that e ∈ E implies φ(e) ∈ E^{′•}. Let P res(I) denote the category of presentations over an institution I, and let T h(I) denote its subcategory of theories over I.

A presentation morphism φ: (Σ, E) → (Σ′, E′) over an inclusive institution is an inclusion iff φ is an inclusion; note that in this case, E ⊆ E′. We may also call such morphisms extensions. □

The following basic result is proved in [16], and the one below it has a similar flavour:

1It is easy to see that each presentation is contained in a least closed set of sentences.

Theorem 21 If the category of signatures of an institution I has [finite] colimits, then so does its category T h(I) of theories. □

Proposition 22 If I is an institution with a factorisation system ( , E) on its signatures, then ( _{T h}, E_{T h}) = ({Φ ∈ T h | Φ ∈ }, {Φ : (Σ, E) → (Σ′, E′) ∈ T h | Φ ∈ E and (Φ(E))^{•} = E′}) is a factorisation system on its theories. If I respects an inclusion system ( , E) on its signatures, and if its category of signatures has finite colimits, then ( _{T h}, E_{T h}) is an inclusion system for T h(I).

Proof: Given a theory morphism Φ : (Σ, E) → (Σ′, E′), let Φ = e; m be its factorisation in Sign, with centre object Σ′′. Let E′′ be the closure of e(E). Then e: (Σ, E) → (Σ′′, E′′) and m: (Σ′′, E′′) → (Σ′, E′) are theory morphisms, and so e; m is a factorisation of Φ in T h. It is easy to check that this forms a factorisation system.

If I respects the inclusion system ( , E), then (2), (3) and (4) of Definition 3 hold trivially, and _{T h} has finite coproducts by an argument similar to that given for Theorem 21 in [16]. The same approach works for condition (6). □

Fact 23 Under the hypothesis of the Proposition 22, the forgetful functor T h(I) → Sign is an inclusion system morphism. Moreover, it is limit and colimit preserving. □

The assumptions encapsulated in the following play a basic role in this paper:

Definition 24 An institution is reasonable iff it is inclusive and its signature category has finite colimits and finite limits. □

All of the institutions that are widely used in Computing Science are reasonable, including classical first order logic and equational logic, in both sorted and unsorted variants.

Corollary 25 If (Σ, E) and (Σ′, E′) are theories over a reasonable institution, then

1. (Σ, E) + (Σ′, E′) = (Σ + Σ′, (E ∪ E′)^{•});

2. (Σ, E) ∩ (Σ′, E′) = (Σ ∩ Σ′, Sen(Σ) ∩ Sen(Σ′) ∩ E ∩ E′).

Proof: The first equation follows from the proof of Theorem 21, and the same technique works for intersection, except that we do not need to take the closure because the intersection of the (Σ ∩ Σ′)-theories Sen(Σ) ∩ E′ and Sen(Σ′) ∩ E is already a (Σ ∩ Σ′)-theory. □

Following [16], we now present institution morphisms, which are useful for comparing and for transferring results among different logical systems.

Definition 26 Let I and I′ be institutions. Then an institution morphism Φ : I → I′ consists of

1. a functor Φ : Sign → Sign′,

2. a natural transformation α: Φ; Sen′ ⇒ Sen, and

3. a natural transformation β: Mod ⇒ Φ^{op}; Mod′

such that the following Satisfaction Condition holds

M ⊧_{Σ} α_{Σ}(e′) iff β_{Σ}(M) ⊧′_{Φ(Σ)} e′

for any Σ-model M from I and any Φ(Σ)-sentence e′ from I′. Institutions with institution morphisms form a category, which we denote INS. □

2.3 Exactness

An important model theoretic property of many logical systems is that finite colimits are preserved by the model functor. Thus, if we combine some theories T_{i} in a diagram T : I → T h(I) having colimit (i.e., result of combination) C, then the denotations of the T_{i} and C behave in the way one would hope: Mod(C) is the limit of the diagram Mod^{op}; T : I → Cat. In particular (and assuming that the categories of Σ-models are concrete), our intuition would lead us to hope that a model of T_{1} ⨁ T_{2} (the co-product) would consist of a pair of models, one of T_{1} and the other of T_{2}; i.e., we intuitively expect Mod(T_{1} ⨁ T_{2}) to be Mod(T_{1}) × Mod(T_{2}). The situation is similar for a pushout of theory morphisms T_{0} → T_{1} and T_{0} → T_{1}, which for simplicity we assume are theory inclusions, so that T_{0} is shared between T_{1} and T_{2}: we expect that a model of T_{1} ⨁_{T_{0}} T_{2} (the pushout) can be constructed from a pair of models, one of T_{1} and the other of T_{2}, by identifying their reducts to T_{0}; that is, we expect Mod(T_{1} ⨁_{T_{0}} T_{2}) to be the pullback of Mod(T_{1}) → Mod(T_{0}) and Mod(T_{2}) → Mod(T_{0}). This property, which we call exactness, seems to have first arisen in [41], and is also used in the pioneering work of Tarlecki [44] on abstract algebraic institutions, and of Meseguer [31] on categorical logics^{2}.

Definition 27 An institution is exact iff the model functor Mod: Sign → Cat^{op} preserves finite colimits, and is semiexact iff Mod preserves pushouts. □

Although many sorted logics tend to be exact, their unsorted variants tend to be semiexact. In particular, the model functor does not preserve coproducts for either unsorted first order logic or unsorted equational logic. This is undesirable from the point of view of modularisation, and is related to the well known fact that the sum of terminating term rewriting systems need not be terminating. A general conclusion is that unsorted logics are unnatural for many a