How to avoid elimination of the initial fact when the modus ponens (or the cut rule) is used?

Question

I have FOL knowledge base that describes the actions of some agent:

is_goal(learning)
is_goal(learning)->is_goal(reading)

If both formulas are true then the final knowledge base (after applying the modus ponens or the cut rule) reads simply:

is_goal(reading)

It is true conclusion but I am uneasy about the fact that the initial fact (is_goal(learning)) and the used implication is eliminated from the KB and hence - I can not use them directly further. Well, in natural deduction they are not elimintated but in sequent calculus (where the entire KB consistes of the current set of sequences) such elimination certainly occurs.

How to handle such elimination issues while using FOL as the formalisms for knowledge base and Gentzen sequent calculus as the reasoninig/inference tools for this knowledge base?

Answer 1

The solution (in a theory that does that kind of elimination that you mention), is to use contraction first.

$$ \underline{\quad \quad \Gamma, A, B \vdash C \quad \quad} \\ \underline{\Gamma, A, A, A \to B \vdash C} \\ \Gamma, A, A \to B \vdash C $$

Reading from the bottom, if you want to prove $C$ from $A$ and $A \to B$, then, using contraction, it suffices to prove $C$ from $A$, $A$ and $A \to B$. Apply modus ponens (the left introduction rule for $\to$), and then we have to prove $C$ from $A$ and $B$. The proposition $A \to B$ could also be kept with another application of contraction.