 and modus ponens as the only inference rule: from \(\varphi\) and \(\varphi \to \psi\), infer \(\psi\). We write \(\Gamma \vdash_\mathrm{MTL} \varphi\) whenever there is a proof of \(\varphi\) from \(\Gamma\) in this system, i.e. there is a finite sequence of formulas which ends with \(\varphi\) and its members are instances of the axioms, elements of \(\Gamma\), or follow from previous ones by the inference rule (modus ponens). This Hilbert-style system is a strongly complete (finitary) axiomatization of the logic MTL, i.e. for each set of premises \(\Gamma\) we have: \(\Gamma \models_\mathrm{MTL} \varphi\) iff \(\Gamma \vdash_\mathrm{MTL} \varphi\). The validity problem of \(\mathrm{MTL}\) is known to be decidable, however its computational complexity has not yet been determined.