Let's say I have a Hilbert style system, with a few axioms and rules of inference, and I want to find a proof for some formula $\varphi$, is it possible to create an algorithm that would find a proof for it with the given system (guaranteeing it'd be in finite time)?
I know a bit of programming, but I think answering this question goes beyond my abilities.
You can only find proofs for any given valid formula, if your calculus is complete. Under the precondition that your calculus is complete, it is possible to create an algorithm that will terminate for every valid formula. However, if your language is undecidable (e.g. first-order logic), you cannot find an algorithm that will terminate for every (valid and non-valid) formula.