The formal system can be taken to be any formulation of the standard propositional calculus. With soundness and completeness at hand, ⊢A∨B⇒⊨A∨B⇒[⊨A or ⊨B]⇒[⊢A or ⊢B]. I want to know how to prove this using only syntactical concepts and whether there is a general algorithm that converts a proof of ⊢A∨B into a proof of A or a proof of B. I guess there should be one, for if either A or B must be provable, then enumerate all proofs in an appropriate order until one is found.
Thanks.