# First order theory for a given sentential logic

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]$$

• As an aside to my answer below: what you call "implication introduction" is usually known as "weakening". "Implication introduction" is usually used as the name of an inference rule in natural deduction. Commented Dec 9, 2018 at 22:25