No it won't. You must first fix a specific theory to apply your solver to. It won't work for every arbitrary choice of theory even with recursively enumerable axioms.
No it won't. You must first fix a specific theory to apply your solver to. It won't work for every arbitrary choice of theory even with recursively enumerable axioms.
First of all, I should have written "recursively enumerable theory" or "theory with decidable axioms". But I think it's clear that I'm referring to things like ZFC, first-order PA or any other similar system.
With that out of the way, it's pretty easy to write a general theorem prover for such theories if you can solve the halting problem.
First define a TM G that takes as input 1. the description of another TM A that decides whether a particular sentence is an axiom of some theory T and 2. a sentence P. We enumerate all syntactically valid proofs with P as the conclusion and check whether all axioms are valid according to A and all inferences are sound. If we find a valid proof, we stop. (G can obviously be built.)
Then define H such that it takes the same inputs as G, and then (using the halting oracle) determines whether G would halt given A and P. If yes, return true, otherwise false.
Then H would be a decider for the language consisting of all pairs T |= P, where T is some recursively enumerable theory.
Yes it will? This works for any first-order theory with a recursive set of axioms. You are simply searching for proofs of implications from the axioms and using the halting oracle to tell if the search terminates or not. By the compactness theorem this is guaranteed to work.
Of course you have to input the axioms, how would a theorem prover work otherwise?
> By the compactness theorem this is guaranteed to work.
I think you mean completeness, but essentially yes.
In this case I meant compactness - if a statement follows from your (possibly infinite set of) axioms then it follows from a finite subset of them. But you can skin the cat in many ways, yeah (proof theory vs model theory way of looking at it I guess).