# Constructive Logic

## Goals of the course

This course is an introduction to constructive mathematics. We recall first
what is Hilbert's program, and the distinction between constructive and classical
reasoning. We explain how
to classify the complexity of mathematical notions and proofs in mathematics
using basic notions of logic. A typical example of reduction of logical complexity
can be seen in the use of point-free representation of topological spaces.
We illustrate this in two examples: a constructive development of Krull dimension,
with some algorithmtic applications, and a development of the notion of Prufer
domain, seen as a constructive approximation of the notion of Dedekind domain.

## Courses

**Course 1** Introduction to logic

**Course 2** Distributive lattices as topological spaces

**Course 1** Krull Dimension

**Course 1** Prufer Domain

## Exercises

Here are some exercises.

## Interesting links

The following paper provides a nice introduction
to constructive mathematics and to type theory

The home page of Henri Lombardi contains many
relevant papers. See also the book about finitely generated projective modules (in French)

The home page of Fred Richman contains also
relevant papers. In particular, see the paper on "Intuitionism as generalization".

A nice presentation of
Brouwer's influence on logic.