 Proofs and Theorems  The notions of proof and theoremhood are defined as usual; we define them generally as they will apply to each of the deductive systems discussed in this entry. Specifically, for any deductive system S, a proof in S is a finite sequence of formulas of the language \(\scrL\) of S—\(\scrL_\Box,\) in the case of SQML—such that each formula is either an axiom of S or follows from preceding formulas in the sequence by a rule of inference of S. A proof is a proof of the formula occurring last in the sequence. A formula \(\varphi\) of \(\scrL\) is a theorem of S—\(\vdash_{S} \varphi\)—if there is a proof of it in S. And if \(\Gamma\) is a set of formulas of \(\scrL,\) then \(\varphi\) is a theorem of \(\Gamma\) (in S)—\(\Gamma \vdash_{S} \varphi\)—if, for some finite subset \(\{\psi_1,\ldots,\psi_n\}\) of \(\Gamma,\) \(\psi_1 \to (\ldots \to (\psi_n \to \varphi)\ldots)\) is a theorem of S.