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.


  • 6
    $\begingroup$ 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. $\endgroup$ Nov 1, 2016 at 6:01
  • $\begingroup$ @random-jack Good. I know where I was mistaken now. Thank you. $\endgroup$
    – gp120
    Nov 1, 2016 at 6:54
  • 1
    $\begingroup$ It might be interesting to note that this property, which is called the disjunction property, holds in many constructive logics. $\endgroup$ Nov 1, 2016 at 10:41
  • $\begingroup$ @RandomJack Also, for any formula 'f', which is not a contradiction, nor a tautology, $\not$$\vdash$f and $\not$$\vdash$$\lnot$f. $\endgroup$ Nov 1, 2016 at 17:01
  • $\begingroup$ 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. $\endgroup$
    – DanielV
    Nov 1, 2016 at 21:34


You must log in to answer this question.

Browse other questions tagged .