 There is some informal motivation for this scheme. In \({\textsf{LP}}\), because of the axiom scheme \(t{:}X{\rightarrow}X\), we have provability of \((t{:}X\land u{:}\lnot X){\rightarrow}\bot\) for any \(t\) and \(u\), and thus provability of \(\lnot t{:}X \lor\lnot u{:}\lnot X\). In any context one of the disjuncts must hold. The scheme above is equivalent to \(f(t,u){:}\lnot t{:}X \lor g(t,u){:}\lnot u{:}\lnot X\), which informally says that in any context we have means for computing a justification for the disjunct that holds. It is a strong assumption, but not implausible at least in some circumstances.