I'm trying to structure a proof where there are several algebras instantiated over sets, where the properties that you get from the algebraic theories are important, but the properties of the sets themselves are also important.
This is why I want to ask whether extending a proof system with models of first order theories and first order theories is consistent.
Here is what I am saying:
Deductive rules include all of the deductive rules of system LK, as well as
from nothing infer $\vdash A$ where $A$ is an axiom of ZFC
Now, suppose you define first order formulas over a signature. Then for every such signature gives the set of formulas $\Phi$ with meta-variables $\phi \in \Phi$.
Then we unroll the satisfaction relation into the deduction rules as follows:
from $\vdash (\mathfrak{M}, \mathfrak{s}) \vDash \forall x, \phi$ infer $\vdash \forall y \in \mathfrak{M}, (\mathfrak{M}, \mathfrak{s}[x := y]) \vDash \phi$
and conversely, from $\vdash \forall y \in \mathfrak{M}, (\mathfrak{M}, \mathfrak{s}[x := y]) \vDash \phi$ infer $\vdash (\mathfrak{M}, \mathfrak{s}) \vDash \forall x, \phi$
Is this a standard way of "using multiple algebraic theories in a proof"? Would this cause the system to become inconsistent? Thanks.
Best Answer
Given that your proof system includes ZFC, the standard way to handle algebraic structure like this in a set-theoretic context is simply to interpret those concepts in set theory. In the language of set theory we can interpret the notions of signature, model, language, and it is simply a ZFC theorem that every model $\mathcal{M}$ in a given signature admits a satisfaction relation $\models$, as defined and proved by Tarski. And part of what that means is that $\mathcal{M}\models\forall x\,\phi$ if and only if for every $y$ in the domain of $\mathcal{M}$ we have $\mathcal{M}\models\phi[x:=y]$. That is, your biconditionals are just part of the Tarski recursion, defining what it means to have a satisfaction relation $\models$.
From this perspective, we don't need to add any new inference rules to the proof system—we are just proving things in ZFC.
However, a slightly revised and more formally correct perspective is that whenever we introduce defined terms to a theory, such as defining the concepts of ordinal, functions, sequences, models, signature, satisfaction $\models$ and so on in ZFC, then we have introduced a definitional expansion of the theory to include these defined terms. We can treat this formally by augmenting the formal system with the definitions of those defined terms. If one does this, then the right treatment of $\models$ would not be just what you wrote, but rather the full Tarski recursive definition of satisfaction.