  The basic operation on justifications is application. The application operation takes justifications \(s\) and \(t\) and produces a justification \(s\cdot t\) such that if \(s :( F \rightarrow G)\) and \(t : F\), then [\(s\cdot t ]: G\). Symbolically,