Adjoint a premise in a intuitionistic natural deduction first order logic

Question

Let assume we have a proof for the sequent $P\vdash A$; how to derive a proof for the sequent $P,B\vdash A$?

I obtain a such proof with introduction and elimination rules for conjunctions. From $P\vdash A$ and $B\vdash B$ we get $P,B\vdash A\wedge B$ by introducing the conjunction, hence we derive $P,B\vdash A$ by eliminating the conjunction.

This is the correct way?

Answer 1

Different formalizations of natural deduction handle this in different ways. The two main options are:

1. Have explicit "structural" rules of inference such as the weakening rule $$ \frac{P, Q \vdash B}{P, A, Q \vdash B} $$

2. Embed the structural rules in the "assumption" axiom such that it reads $$ \frac{}{P, A, Q \vdash A} $$ which lets you carry through unused assumptions all the way to the leaves of the proof tree and ignore them there.

Your description "intuitionistic natural deduction first order logic" is not precise enough to tell which of the solutions have been chosen by the author of the formalization you're working with, but if your conjunction intruction rule is $$ \frac{P\vdash A \qquad Q\vdash B}{P,Q \vdash A\land B} \quad\text{rather than}\quad \frac{P\vdash A \qquad P\vdash B}{P \vdash A\land B} $$ then it seems likely that it would be using structural rules, so you should look for something like the above weakening rule in your source material.