The usual axioms and inference rules of total many-sorted first-order logic have to be adjusted to take into account possible undefinedness of the values of terms, the definedness assertions and the two kinds of equations. Sort-generation constraints introduce extra inference rules, corresponding to (structural) induction principles, the consequences of which cannot be fully captured by first-order logic.