I asked a similar question on cs.stackexchange, but I'd like to ask it a tad more specifically, and thought this would be a better place for it. I'm looking through a text on logic, and the problem is basically as follows:
Suppose we have an algorithm for deciding wether a sentence A implies a sentence B (A->B). Show that we can use this to determine if a given sentence A is satisfiable. I'm sort of lost on how to do this, and even a hint would be helpful.
Thanks
I don't know the setting, presumably there is some background theory $T$.
A sentence $\varphi$ is satisfiable if $\lnot\varphi$ is not a theorem. And $\lnot\varphi$ is not a theorem precisely if the implication $X\to \lnot\varphi$ fails to hold, where $X$ is your favourite always true sentence. If we have an algorithm for determining whether an implication holds, that algorithm is also an algorithm for determining whether an implication fails to hold.