Exercise 1.7.10 from Enderton's A Mathematical Introduction To Logic Enderton writes in Section 1.7 that he is providing only an informal and intuitive definition of "effective procedure", and so I am questioning whether or not I have a decent understanding of what precisely he means in the following definition:

DEFINITION. A set $\Sigma$ of expressions is decidable iff there exists an effective procedure that, given an expression $\alpha$, will decide whether or not $\alpha \in \Sigma$.

To ensure I have a decent working understanding, I am looking at this (slightly paraphrased) exercise from section 1.7.


  
*Let $\Sigma$ be an effectively enumerable set of well-formed formulas.
  Assume that for each $\tau$, at least one of $\Sigma \vDash \tau$ or $\Sigma \vDash \neg \tau$.
  Show the set of tautological consequences of $\Sigma$ is decidable.
  

Here is my reasoning, and I'll say where I'm confused.
If for every wff $\tau$ we have exactly one of $\Sigma \vDash \tau$ or $\Sigma \vDash \neg \tau$, then the set of $\tau$ such that $\Sigma \nvDash \tau$ is the set of $\tau$ such that $\Sigma \vDash \neg \tau$. In this case both the set of $\tau$ such that $\Sigma \vDash \tau$ and its complement are effectively enumerable (Enderton's Theorem 17G). The set of $\tau$ such that $\Sigma \vDash \tau$ is then decidable by Kleene's Theorem (Enderton's Theorem 17F).
Suppose on the other hand that there is a wff $\tau$ we have both $\Sigma \vDash \tau$ and $\Sigma \vDash \neg \tau$. In this case $\Sigma$ is not satisfiable. Therefore $\Sigma \vDash \tau$ for every wff $\tau$. My "effective decision procedure" to decide whether or not a given formula $\tau$ is a consequence of $\Sigma$ is then simply to immediately return YES for every input.
My confusion: This seems... too easy. I am worried that I have somehow illegally used knowledge of $\Sigma$ to come up with these procedures in the two subcases, that somehow being able to determine which subcase we are in must be considered as part of the effective procedure. But I see looking at Enderton's definition of "decidable" that he is requiring only existence of a procedure, but maybe not necessarily the ability to actually conveniently find it on a case by case basis?
Any clarification would be appreciated... thank you.
 A: Your reasoning is completely correct -- that is exactly how it goes.
It is indeed the case that calling something "decidable" does not require knowing what the decision procedure is, only knowing that some decision procedure is out there somewhere.
This is the point of some classical "trick questions" that ask, for example, whether
$$ A = \{ n \mid \text{the decimal expansion of $\pi$ contains less than $n$ sevens} \} $$
is decidable.
We don't know whether $\pi$ contains infinitely many sevens or not (though it is strongly suspected that is does), but we do know that $A$ is decidable. Either it is empty (and $\varnothing$ is clearly decidable) or it contains all numbers larger than some constant, namely how many sevens there are in $\pi$. Every set of the latter form is also clearly decidable, so no matter which of these is the case, $A$ is decidable.
Or in other words, whether a set is decidable or not is a property only of the set itself, not a property of what you know about the set.

This is a typical example of a non-constructive existence proof. Such proofs are considered perfectly valid in ordinary mainstream mathematics.
Your intuition that this reasoning is "somehow illegal" is not crazy, though. Even though there are few people nowadays who hold that it should be actually illegal, interesting mathematics can still result from investigating what can be proved without resorting to such tricks. This leads to intuitionistic logic and more generally constructive mathematics, a quite respectable specialty subject.
