We define a signature as a triple $$\Sigma\ =\ (S,F,\mathrm{type})$$ where $S$ is a set of sorts, $F$ a set of $n$-ary function symbols $f$ of the type $\mathrm{type}(f)$ $=$ $(M_1,\dotsc,M_n\dashrightarrow M_{n+1})$, where $n\ge 0$ and all $M_i$ lie in $S$ ($1\le i\le n$).
A $\Sigma$-algebra for us is a pair $$A\ =\ (G,H)$$ where $G$ is a family of carrier sets for sorts in $S$, and $H$ is a family of (in general partial) functions of the correspoinding type, one function per symbol in $F$.
We consider an infinite set of fresh typed variables and define $\Sigma$-terms as usual: all nullary constants in $F$ are terms, all variables are terms, and if $t_1,\dotsc,t_n$ are terms of type $M_1,\dotsc,M_n$, and $\mathrm{type}(f)=(M_1,\dotsc,M_n\dashrightarrow M_{n+1})$, then $f(t_1,...,t_n)$ is a term of type $M_{n+1}$.
We define first-order formulas (over the equality and the $\mathrm{defined}$ predicate) as usual:
$t=t'$ is a formula where $t$ and $t'$ are terms,
$\mathrm{defined}(t)$ is a formula where $t$ is a term,
if $\varphi$ and $\varphi'$ are formulas, so are $\varphi\lor\varphi'$, $\neg\varphi$, $\forall x{\in}M\colon \varphi$, etc.
Given an assignment $\eta$ of the free variables of a formula $\varphi$, we define $A,\eta\models\varphi$ (the validity of $\varphi$ in an algebra $A$) inductively as usual. Special cases:
$A,\eta\models t=t'$ iff $t$, $t'$ are either both undefined or both defined with the same value under $\eta$.
$A,\eta\models\mathrm{defined}(t)$ iff $t$ (which contains partial function symbols in general) has a well-defined value in $A$.
So far, nothing really new has happened: yet another variation of a many-sorted first-order logics for partial algebras/structures has been described.
Question: which book or journal paper describes a classical, first-order proof system (providing a checkable and possibly useful relation $\vdash$ such that $A,\eta\vdash t$ implies $A,\eta\models t$) for
all partial algebras
all partial term-generated algebras (i.e., where each element of each carrier set is an interpretation of some ground term)?
Of course, you can use induction in the second case in addition.
Yes, I took a look into the To-Truth-Through-Proof book and into https://www.fecundity.com/codex/forallx.pdf, and they are somewhat far away. Are there books which are a better fit?
