In "The Lambda Calculus - Its Syntax and Semantics" by H.P. Barendregt (WorldCat) is this statement, the first sentence of chapter 2 after the introduction chapter, so in a way this sets the tone of the book and is useful to understand.
The principal object of study in the λ-calculus is the set of lambda terms modulo convertibility. (p. 22)
Then a few paragraphs later is found convertibility. (p. 23)
The basic equivalence relation of λ-terms is that of convertibility. This relation will be generated by axioms. In order to formulate these axioms, a substitution operator is needed. M[x := N] denotes that the result of substituting N for x in M. ...
Then for 2.1.4 Definition ...
Provability in λ of an equation is denoted by λ ⊢ M = N or often just by M = N. If λ ⊢ M = N, then M and N are called convertible.
What does "lambda terms modulo convertibility" mean?
Based on a comment for this question it seems a different synonym for modulo would clear things up.
In reading TAPL (Types and Programming Languages) by Benjamin C. Pierce (WorldCat) one can get an understanding of axiom with regards to λ-calculus so no need to explain that.
X modulo Y
informally meansX, ignoring Y
. $\endgroup$