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

  1. all partial algebras

  2. 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?


Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.