The notion of an Effective Procedure was introduced by Alonzo Church for the purpose of demonstrating the unsolvability of certain problems.
Useful books in this area are Marvin Minsky (lightweight, but very interesting) Boolos&Jeffrey (middle ground) or Hartley Rogers (a classic text for serious logicians).
Absolute unsolvability results are difficult to produce because the meaning of unsolvable remains unclear until the methods permitted in a solution are spelt out. (who knows what can be done with a bit of divine inspiration?) The result obtained by Church has nonetheless an absolute character, because the notion of effective procedure which he used in his unsolvability results was subsequently shown to be equivalent to a variety of quite different formulations.
Among the alternative formulations are:
All of these are essentially equivalent in power to what we may think of informally as a digital computer with unlimited memory (unlimited secondary memory will do). Each of the above systems can be thought of alternative ways of encoding algorithms, or alternative programming languages.
The general topic of computability, studied independently of how algorithms are represented, is known as recursion theory. Certain elementary terms from that theory are convenient for us in elementary logical treatises.
A set is effectively decidable if there exists an effective procedure which will determine whether any candidate is a member of that set.
Such an effective procedure will always terminate within a finite number of computation steps giving the determination of whether the candidate is or is not a member of the set.
A set is effectively semi-decidable if there is an effective procedure which, given a candidate member of the set, will terminate after a finite number of steps if that candidate is a member, confirming the membership.
If the candidate is not a member the procedure will either terminate without confirming membership, or else will never terminate.