# How to prove that ⊢A∨B implies ⊢A or ⊢B

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.

• In classical propositional logic we have $\vdash p \vee \neg p$, while $\not\vdash p$ and $\not\vdash\neg p$, where $p$ is a propositional variable. Nov 1, 2016 at 6:01
• @random-jack Good. I know where I was mistaken now. Thank you. Nov 1, 2016 at 6:54
• It might be interesting to note that this property, which is called the disjunction property, holds in many constructive logics. Nov 1, 2016 at 10:41
• @RandomJack Also, for any formula 'f', which is not a contradiction, nor a tautology, $\not$$\vdashf and \not$$\vdash$$\lnot$f. Nov 1, 2016 at 17:01
• In natural deduction, if you prove a statement of the form $A \lor B$, and if for every axiom of the form $x \lor y$ you knew which $x$ or $y$ was the constructable proposition, then you know which of $A \lor B$ is the constructable proposition. It can be established inductively, as none of the inferences lose that information. Nov 1, 2016 at 21:34