Safety Signature for Geometric Constructions
Shahar Lev (TAU)
Abstract:
This is a part of an on-going project aiming at getting
a unified theory of constructions as they are used in
different branches of Mathematics. Taking a purely logical
view, such a unification has previously been achieved
of the notion of computability used in recursion theory
and the set-theoretical notion of constructibility.
This was done by using the notion of safety
signature - a generalization of the usual notion of a
first-order signature in which constructibility
and decidability issues are taken into account.
In this talk we use Tarski's formalization
of Euclidean Geometry in order to characterize
within a similar strictly syntactical framework the oldest
type of constructions studied in mathematics: Euclidean
ruler and compass constructions.
Joint work with Arnon Avron.