# [plt-scheme] Check for function equality?

On Thu, 2009-02-19 at 18:26 -0500, Marco Morazan wrote:
. . .
>* Others have suggested using theorem provers. This is also something
*>* that can lead you down an enlightening path. :-)
*
This brings up an interesting question. We know that there is no
decision procedure for First-Order Predicate with Equality, but
Herbrand's Theorem tells us there is a semi-decision procedure, that is,
there is a procedure that halts on any theorem saying "it's a theorem",
but some non-theorems cause it to spin. Is there anything analogous for
the Halting Problem or function equivalence, or are we in a situation
like Second-Order Predicate Calculus which has no semi-decision
procedure because any such could be used to build a decision procedure
for FOPC?
-- Bill Wood