Connecting The Informal and Formal Definitions of Decidable With Each Other

Question

From pg. 64 of Lambda Calculus and Combinators, the author formally and informally defines the notion of "decidability":

1 Formal Definition

Definition 5.4 A pair of sets $\mathcal{A}$, $\mathcal{B}$ of natural numbers is called recursively separable iff there is a recursive total function $\phi$ whose only output-values are $0$ and $1$, such that

$$ n \in \mathcal{A} \implies \phi(n) = 0, $$ $$ n \in \mathcal{B} \implies \phi(n) = 1 $$

A pair of sets of terms is called recursively separable iff the corresponding sets of Godel numbers are recursively separable. A set $\mathcal{A}$ (of numbers or terms) is called recursive or decidable iff $\mathcal{A}$ and its complement are recursively separable.

2 Informal Definition

Shortly thereafter, the author states

Informally speaking, a pair $\mathcal{A}$, $\mathcal{B}$ is recursively separable iff $\mathcal{A} \cap \mathcal{B}$ is empty and there is an algorithm which decides whether a number or term is in $\mathcal{A}$ or in $\mathcal{B}$.

3 How to Connect These Definitions

Why is the existence of a recursive total function $\phi$ satisfying the properties of (1) logically equivalent to the notion that "there is an algorithm which decides whether a number or term is in the disjoint $\mathcal{A}$ or $\mathcal{B}$"?

Answer 1

The author himself wrote informally speaking, the second is not a definition in the same sense of the first.

Intuitively, since a recursive function is defined by either $\mu$-recursion or composition of simpler functions, the existence of a total recursive function provides an effective method to compute the answer.

The informal part of the above reasoning is that we didn't really define what we mean by "effective method".

The usual formalization involves the definition of a computational model, which provides a rigorous framework for the notion of algorithm. Once you have done that, you can prove the equivalence in a mathematical sense.