A Possible and Necessary Consistency Proof

After Gödel's incompleteness theorems and the collapse of Hilbert's programme Gerhard Gentzen continued the quest for consistency proofs of Peano arithmetic. He considered a finitistic or constructive proof still possible and necessary for the foundations of mathematics. For a proof to be meaningful, the principles relied on should be considered more reliable than the doubtful elements of the theory concerned. He worked out a total of four proofs between 1934 and 1939. This thesis examines the consistency proofs for arithmetic by Gentzen from different angles. The consistency of Heyting arithmetic is shown both in a sequent calculus notation and in natural deduction. The former proof includes a cut elimination theorem for the calculus and a syntactical study of the purely arithmetical part of the system. The latter consistency proof in standard natural deduction has been an open problem since the publication of Gentzen's proofs. The solution to this problem for an intuitionistic calculus is based on a normalization proof by Howard. The proof is performed in the manner of Gentzen, by giving a reduction procedure for derivations of falsity. In contrast to Gentzen's proof, the procedure contains a vector assignment. The reduction reduces the first component of the vector and this component can be interpreted as an ordinal less than epsilon_0, thus ordering the derivations by complexity and proving termination of the process.

Boxicity and maximum degree

A d-dimensional box is a Cartesian product of d closed intervals on the real line. The boxicity of a graph is the minimum dimension d such that it is representable as the intersection graph of d-dimensional boxes. We give a short constructive proof that every graph with maximum degree D has boxicity at most 2D2. We also conjecture that the best upper bound is linear in D.

Splittings of free groups, normal forms and partitions of ends

Splittings of a free group correspond to embedded spheres in the 3-manifold M = # (k) S (2) x S (1). These can be represented in a normal form due to Hatcher. In this paper, we determine the normal form in terms of crossings of partitions of ends corresponding to normal spheres, using a graph of trees representation for normal forms. In particular, we give a constructive proof of a criterion determining when a conjugacy class in pi (2)(M) can be represented by an embedded sphere.

A Flexible Class of Regenerating Codes for Distributed Storage

In the distributed storage setting introduced by Dimakis et al., B units of data are stored across n nodes in the network in such a way that the data can be recovered by connecting to any k nodes. Additionally one can repair a failed node by connecting to any d nodes while downloading at most beta units of data from each node. In this paper, we introduce a flexible framework in which the data can be recovered by connecting to any number of nodes as long as the total amount of data downloaded is at least B. Similarly, regeneration of a failed node is possible if the new node connects to the network using links whose individual capacity is bounded above by beta(max) and whose sum capacity equals or exceeds a predetermined parameter gamma. In this flexible setting, we obtain the cut-set lower bound on the repair bandwidth along with a constructive proof for the existence of codes meeting this bound for all values of the parameters. An explicit code construction is provided which is optimal in certain parameter regimes.

Topics in bifurcation theory

I. Existence and Structure of Bifurcation Branches

The problem of bifurcation is formulated as an operator equation in a Banach space, depending on relevant control parameters, say of the form G(u,λ) = 0. If dimN(G_u(u_O,λ_O)) = m the method of Lyapunov-Schmidt reduces the problem to the solution of m algebraic equations. The possible structure of these equations and the various types of solution behaviour are discussed. The equations are normally derived under the assumption that G^O_λεR(G^O_u). It is shown, however, that if G^O_λεR(G^O_u) then bifurcation still may occur and the local structure of such branches is determined. A new and compact proof of the existence of multiple bifurcation is derived. The linearized stability near simple bifurcation and "normal" limit points is then indicated.

II. Constructive Techniques for the Generation of Solution Branches

A method is described in which the dependence of the solution arc on a naturally occurring parameter is replaced by the dependence on a form of pseudo-arclength. This results in continuation procedures through regular and "normal" limit points. In the neighborhood of bifurcation points, however, the associated linear operator is nearly singular causing difficulty in the convergence of continuation methods. A study of the approach to singularity of this operator yields convergence proofs for an iterative method for determining the solution arc in the neighborhood of a simple bifurcation point. As a result of these considerations, a new constructive proof of bifurcation is determined.

Three essays on game theory and bargaining

A PhD Dissertation, presented as part of the requirements for the Degree of Doctor of Philosophy from the NOVA - School of Business and Economics

Fred: An approach to generating real, correct, reusable programs from proofs

In this paper we describe our system for automatically extracting "correct" programs from proofs using a development of the Curry-Howard process. Although program extraction has been developed by many authors, our system has a number of novel features designed to make it very easy to use and as close as possible to ordinary mathematical terminology and practice. These features include 1. the use of Henkin's technique to reduce higher-order logic to many-sorted (first-order) logic; 2. the free use of new rules for induction subject to certain conditions; 3. the extensive use of previously programmed (total, recursive) functions; 4. the use of templates to make the reasoning much closer to normal mathematical proofs and 5. a conceptual distinction between the computational type theory (for representing programs)and the logical type theory (for reasoning about programs). As an example of our system we give a constructive proof of the well known theorem that every graph of even parity, which is non-trivial in the sense that it does not consist of isolated vertices, has a cycle. Given such a graph as input, the extracted program produces a cycle as promised.

Protocols between programs and proofs

In this paper we describe a new protocol that we call the Curry-Howard protocol between a theory and the programs extracted from it. This protocol leads to the expansion of the theory and the production of more powerful programs. The methodology we use for automatically extracting “correct” programs from proofs is a development of the well-known Curry-Howard process. Program extraction has been developed by many authors, but our presentation is ultimately aimed at a practical, usable system and has a number of novel features. These include 1. a very simple and natural mimicking of ordinary mathematical practice and likewise the use of established computer programs when we obtain programs from formal proofs, and 2. a conceptual distinction between programs on the one hand, and proofs of theorems that yield programs on the other. An implementation of our methodology is the Fred system. As an example of our protocol we describe a constructive proof of the well-known theorem that every graph of even parity can be decomposed into a list of disjoint cycles. Given such a graph as input, the extracted program produces a list of the (non-trivial) disjoint cycles as promised.

Interactive theorem provers: issues faced as a user and tackled as a developer

Interactive theorem provers (ITP for short) are tools whose final aim is to certify proofs written by human beings. To reach that objective they have to fill the gap between the high level language used by humans for communicating and reasoning about mathematics and the lower level language that a machine is able to “understand” and process. The user perceives this gap in terms of missing features or inefficiencies. The developer tries to accommodate the user requests without increasing the already high complexity of these applications. We believe that satisfactory solutions can only come from a strong synergy between users and developers. We devoted most part of our PHD designing and developing the Matita interactive theorem prover. The software was born in the computer science department of the University of Bologna as the result of composing together all the technologies developed by the HELM team (to which we belong) for the MoWGLI project. The MoWGLI project aimed at giving accessibility through the web to the libraries of formalised mathematics of various interactive theorem provers, taking Coq as the main test case. The motivations for giving life to a new ITP are: • study the architecture of these tools, with the aim of understanding the source of their complexity • exploit such a knowledge to experiment new solutions that, for backward compatibility reasons, would be hard (if not impossible) to test on a widely used system like Coq. Matita is based on the Curry-Howard isomorphism, adopting the Calculus of Inductive Constructions (CIC) as its logical foundation. Proof objects are thus, at some extent, compatible with the ones produced with the Coq ITP, that is itself able to import and process the ones generated using Matita. Although the systems have a lot in common, they share no code at all, and even most of the algorithmic solutions are different. The thesis is composed of two parts where we respectively describe our experience as a user and a developer of interactive provers. In particular, the first part is based on two different formalisation experiences: • our internship in the Mathematical Components team (INRIA), that is formalising the finite group theory required to attack the Feit Thompson Theorem. To tackle this result, giving an effective classification of finite groups of odd order, the team adopts the SSReflect Coq extension, developed by Georges Gonthier for the proof of the four colours theorem. • our collaboration at the D.A.M.A. Project, whose goal is the formalisation of abstract measure theory in Matita leading to a constructive proof of Lebesgue’s Dominated Convergence Theorem. The most notable issues we faced, analysed in this part of the thesis, are the following: the difficulties arising when using “black box” automation in large formalisations; the impossibility for a user (especially a newcomer) to master the context of a library of already formalised results; the uncomfortable big step execution of proof commands historically adopted in ITPs; the difficult encoding of mathematical structures with a notion of inheritance in a type theory without subtyping like CIC. In the second part of the manuscript many of these issues will be analysed with the looking glasses of an ITP developer, describing the solutions we adopted in the implementation of Matita to solve these problems: integrated searching facilities to assist the user in handling large libraries of formalised results; a small step execution semantic for proof commands; a flexible implementation of coercive subtyping allowing multiple inheritance with shared substructures; automatic tactics, integrated with the searching facilities, that generates proof commands (and not only proof objects, usually kept hidden to the user) one of which specifically designed to be user driven.

Three dimensional Sklyanin algebras and Gröbner bases

We consider Sklyanin algebras $S$ with 3 generators, which are quadratic algebras over a field $\K$ with $3$ generators $x,y,z$ given by $3$ relations $pxy+qyx+rzz=0$, $pyz+qzy+rxx=0$ and $pzx+qxz+ryy=0$, where $p,q,r\in\K$. this class of algebras has enjoyed much attention. In particular, using tools from algebraic geometry, Feigin, Odesskii \cite{odf}, and Artin, Tate and Van Den Bergh, showed that if at least two of the parameters $p$, $q$ and $r$ are non-zero and at least two of three numbers $p^3$, $q^3$ and $r^3$ are distinct, then $S$ is Artin--Schelter regular. More specifically, $S$ is Koszul and has the same Hilbert series as the algebra of commutative polynomials in 3 indeterminates (PHS). It has became commonly accepted that it is impossible to achieve the same objective by purely algebraic and combinatorial means like the Groebner basis technique. The main purpose of this paper is to trace the combinatorial meaning of the properties of Sklyanin algebras, such as Koszulity, PBW, PHS, Calabi-Yau, and to give a new constructive proof of the above facts due to Artin, Tate and Van Den Bergh. Further, we study a wider class of Sklyanin algebras, namely
the situation when all parameters of relations could be different. We call them generalized Sklyanin algebras. We classify up to isomorphism all generalized Sklyanin algebras with the same Hilbert series as commutative polynomials on
3 variables. We show that generalized Sklyanin algebras in general position have a Golod–Shafarevich Hilbert series (with exception of the case of field with two elements).

Truth in complex adaptive systems models should be based on truth by constructive verification

It is argued that the truth status of emergent properties of complex adaptive systems models should be based on an epistemology of proof by constructive verification and therefore on the ontological axioms of a non-realist logical system such as constructivism or intuitionism. ‘Emergent’ properties of complex adaptive systems (CAS) models create particular epistemological and ontological challenges. These challenges bear directly on current debates in the philosophy of mathematics and in theoretical computer science. CAS research, with its emphasis on computer simulation, is heavily reliant on models which explore the entailments of Formal Axiomatic Systems (FAS). The incompleteness results of Gödel, the incomputability results of Turing, and the Algorithmic Information Theory results of Chaitin, undermine a realist (platonic) truth model of emergent properties. These same findings support the hegemony of epistemology over ontology and point to alternative truth models such as intuitionism, constructivism and quasi-empiricism.

Formative and summative assessment and the notion of constructive alignment

This paper discusses the different perceptions of first year accounting students about their tutorial activities and their engagements in assessment. As the literature suggests, unless participation in learning activities forms part of graded assessment, it is often difficult to engage students in these activities. Using an action research model, this paper reports the study of first year accounting students' responses to action-oriented learning tasks in tutorials. The paper focuses on the importance of aligning curriculum objectives, learning and teaching activities and assessment, i.e. the notion of constructive alignment. However, as the research findings indicate, without support at institutional level, applying constructive alignment to facilitate quality student learning outcomes is a difficult task. Thus, the impacts of policy constraints on curriculum issues are also discussed, focusing on the limitations faced by tutors and their lack of involvement in curriculum development.

Situated case-based reasoning as a constructive memory model for design reasoning

This paper describes an extended case-based reasoning model that addresses the notion of situatedness in designing through constructive memory. The model is illustrated through an application for predicting the corrosion rate for a specific material on a specific building.

Constructive development of the solutions of linear equations in introductory ordinary differential equations

The solution of linear ordinary differential equations (ODEs) is commonly taught in first year undergraduate mathematics classrooms, but the understanding of the concept of a solution is not always grasped by students until much later. Recognising what it is to be a solution of a linear ODE and how to postulate such solutions, without resorting to tables of solutions, is an important skill for students to carry with them to advanced studies in mathematics. In this study we describe a teaching and learning strategy that replaces the traditional algorithmic, transmission presentation style for solving ODEs with a constructive, discovery based approach where students employ their existing skills as a framework for constructing the solutions of first and second order linear ODEs. We elaborate on how the strategy was implemented and discuss the resulting impact on a first year undergraduate class. Finally we propose further improvements to the strategy as well as suggesting other topics which could be taught in a similar manner.