A problem of decidability (predicate metalogic)

Question

I have been stumped by the following and would greatly appreciate any hints or advice as to how to proceed:

For some first-order predicate logic system:

Let Γ be a decidable set of wffs such that for any closed wff σ, either Γ|= σ or Γ|= ¬σ (but not both). Prove that the set of all closed wffs deducible from Γ is decidable.

Here '|=' is taken to mean the consequent is deducible from the antecedent, and wff=well-formed formula.

Thanks to anyone who takes a stab - it is much appreciated!

Answer 1

We give a very informal argument. Let $\Delta$ be the set of all closed formulas deducible from $\Gamma$.

We can list all proofs from $\Gamma$ as a sequence $\pi_1,\pi_2,\pi_3,\dots$. (Proofs are certain sequences of sentences.) For each proof $\pi_i$, check whether $\alpha$ or $\lnot\alpha$ is the last sentence in $\pi_i$. Since one of $\alpha$ or $\lnot\alpha$ is provable from $\Gamma$, this process will terminate, and give us a (very inefficient) decision procedure for membership in $\Delta$.