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.
[PDM] Is it clear what style to use? ([TM] Natural deduction)
Discharged: See next comment.
[AT] This remark about the proof system really doesn't say anything. Overall, the proof system is quite a separate issue for the description of the language, and in fact has nothing to do with the description of the language. Maybe we should omit this entirely. Especially since we do not really know that much about this (yet, I hope).
Discharged: This document should only say that the issue of proof is covered elsewhere.
[TM] How is undefinedness taken into account? There are at least two ways: either following P. Burmeister, "Partial algebras -- survey of a unifying approach towards a two-valued model theory for partial algebras", Algebra Universalis 15, 306-358 (1982) or following D.S. Scott, "Identity and Existence in Intuitionistic Logic", Lecture Notes in Mathematics 753, 660-696 (1979). (Following Scott)
Discharged: See previous comment.
[TM] Does the proof system act on sentences of the institution, which can be faithfully represented in the language, or on axioms of the language, which seems to be difficult? (On sentences of the institution.)
Discharged: See previous comment.
[TM] The proof system should be sound, but this is easy to achieve: just allow no derivations. So shouldn't we try to achieve some form of completeness? (Yes. Suggestion: if we use higher-order logic as meta-theory for the semantics, we have the notion of completeness w.r.t. (possibly non-standard) generalized Henkin models. This suggestion is independent of the question of whether higher-order logic is actually used as meta-theory.)
Discharged: See previous comment.