%0 Journal Article %T Free Magmas %A Marco Riccardi %J Formalized Mathematics %@ 1898-9934 %D 2010 %I %R 10.2478/v10037-010-0003-0 %X This article introduces the free magma M(X) constructed on a set X [6]. Then, we formalize some theorems about M(X): if f is a function from the set X to a magma N, the free magma M(X) has a unique extension of f to a morphism of M(X) into N and every magma is isomorphic to a magma generated by a set X under a set of relators on M(X). In doing it, the article defines the stable subset under the law of composition of a magma, the submagma, the equivalence relation compatible with the law of composition and the equivalence kernel of a function. We also introduce some schemes on the recursive function. %U http://versita.metapress.com/content/d0w1560800176886/?p=61b23553b62540b9a78312c2f3ea4bb9&pi=2