First order theory for a given sentential logic

Question

Is it possible to extract the axioms and inference rules of a sentential/zeroth-order logic into a first order theory? Does this kind of "hoisting" have a name?

I'm trying to figure out how to check whether a finitely-valued sentential logic is consistent with an arbitrary collection of axioms and inference rules. I'd like to, if possible, use the same machinery for checking both the axioms and the inference rules.

I think that's equivalent to asking if the finitely-valued semantics is complete. I'm not trying to tackle soundness with this construction.

Let bold ($\mathbf{I}$) Łukasiewicz-style operators represent logical connectives in the finitely-valued sentential logic under examination and $\land, \lor, \to$ represent connectives in classical logic. $\mathbf{I}$ is a logical symbol in the logic under examination, but a function symbol in the first-order theory.

Modus ponens in logic under examination:

$$ \frac{a \;\;\text{and}\;\; \mathbf{I} a b}{b} $$

Weakining (as a tautology)

$$ \frac{\cdot}{\mathbf{I}a\mathbf{I}ba} $$

Written as laws in a first order theory with $D$ being the domain of truth values in the logic under examination and $T$ being a predicate that identifies designated truth values in $D$ .

"Hoisting" of modus ponens. Because it's an inference rule, we consider the truth-ness of the premises and the conclusion independently.

$$ \forall ab \mathop{:} D \mathop{.} \; T(a) \land T(\mathbf{I}ab) \to T(b) $$

"Hoisting" of weakening. Because it's only intended to be a tautology, we check the truth-ness of the expression at the very end.

$$ \forall a b \mathop{:} D \mathop{.} \; T[\mathbf{I}a\mathbf{I}ba] $$

Answer 1

Yes, it is usually possible to model a propositional logic as a first-order theory whose domain of discourse represents the set of truth-values in the propositional logic and whose axioms represent the propositional axioms and inference rules. (I say "usually" because you could devise a bizarre propositional logic with side-conditions on the inference rules that would make them hard to model.)

I don't know of a name for this process in general, but for a large class of propositional logics, the first-order theory will be an equational theory of the sort studied in universal algebra, and the process amounts to giving an algebraic semantics for the logic. E.g., classical propositional logic corresponds to the theory of Boolean algebras and intuitionistic propositional logic corresponds to the theory of Heyting algebras.