The theory of the untyped -calculus is the theory induced by a single axiom, which is known as :
The theory is then closed under the usual rules that make equality an equivalence relation (reflexivity, symmetry, transitivity) and a congruence (i.e. respecting every constructor - in this case just abstraction and application).
The theory is the main subject of study of Barendregt's seminal book [Barendregt 1984].
Barendregt, Henk. 1984. Lambda Calculus: Its Syntax and Semantics. Amsterdam: North-Holland. [link]
@book{barendregt_1984,
address = {Amsterdam},
title = {Lambda {Calculus}: {Its} {Syntax} and {Semantics}},
isbn = {978-0-444-87508-2},
publisher = {North-Holland},
author = {Barendregt, Henk},
year = {1984}
}