On intuitionistic branching tense logic with weak induction - Alonderis, Romas (Lietuvos matematikos rinkinys, 1998)
In the paper, the first-order branching tense logic calculus is given: LB J with the weak induction, that is to say with the axiom (A ∧ A O ☐ A) ⊃ ☐ A instead of the induction axiom (A ∧ ☐ (A ⊃ O A)) ⊃ ☐ A. The syntactical cut elimination theorem, Harrop’s theorem and the interpolation theorem is proved here with respect to the LB J calculus.