Resumen de Una formalització de les construccions geomètriques
Geometric constructions have been studied by mathematicians from ancient Greece until now. Although most attention has been given by the ruler and compass, during the last decades interest in this subject has revived, and includes now other instruments such as origami. A global analysis of instruments and the main results about them has led us to introduce a formal language that allows a unified treatement of instruments and their constructions and related theorems. The main concepts of this language are axioms, tools and maps. Tools formalize geometric instruments. A tool has associated axioms, which are the basic processes that can be done with the instrument. We give a formal definition of a construction as a sequence of axioms, which includes all the information that is needed to describe the process that takes place. The language we introduce needs to be systematic, but also flexible and open, so that new instruments and constructions can be included.
Once concepts of a tool and a construction are defined, we establish a classification of tools following two different equivalence relations: geometric equivalence and virtual equivalence. These classifications allow the reformulation of not only known results, like Mohr-Masheroni theorem, but also a proof of new relations between tools.
A map is a geometric and arithmetic object which is a tool plus an initial set of points and curves. Maps have associated layers, where points and curves are created iteratively. Because of the complexity of maps and their layers, we can often say little about them. Their study is related to some problems in computational geometry. For some maps, we are able to study the asymptotic growth of the cardinality of the number of points and curves on each layer. We make a complete characterization of the map of the rusty compass, and give details of points and curves in each layer. We also introduce a classification of the maps, that relates those that have the same set of constructible points. The Poncelet-Steiner theorem can be explained in a very natural way using maps. The language of maps allows us to establish new relations between tools. The classification of maps gives an arithmetic classification of tools. We present new results of arithmetic equivalence, using algebraic concepts such as the degree of an axiom and the signature of a tool.
On the other hand, we study the structure of constructions, and associate them with two types of measures. As the first type of extrinsic measures, we define the level and the virtual level. Levels come from the use of the layers of maps associated with the constructions. Intrinsic measures of a construction are length, weight, order and rank. These measures allow us to give criteria of minimality and optimality of a construction. We calculate these measures for the basic arithmetic and algebraic constructions and deduce relations between different layers from the maps of the ruler and compass, origami and conics.
Throughout the thesis, we illustrate our formalization with several catalogs: a catalog of axioms, which contains the axioms of the most famous instruments, a catalog of tools, where we present the main tools known and the constructions one can do with them, and a catalog of maps, which compiles the results of constructibility, and incorporates some maps associated with new tools, and the corresponding set of constructible points. Finally, we present a catalog of constructions, consisting of around seventy constructions described by the new language that we have introduced, its measures and the proof of their correctness. The digital version of the thesis includes links to interactive animations that can reproduce the steps of the constructions.
