 Let \(TA\), \(VA\), and \(DA\) mean respectively that \(A\) is a first order translation of an informal argument that is intuitively valid “in virtue of form alone”, that \(A\) is valid according to the standard model theoretic definition of validity for first order logic, and that \(A\) is derivable in a first order formal system of deduction, \(D\), that is sound and complete in the usual sense. Then informally, we have that \(DA\) implies \(TA\). If an argument is formally derivable, we regard it as valid in virtue of its form alone. At least that is often taught to students. And also \(TA\) implies \(VA\)—something also taught to students. By completeness, \(VA\) implies \(DA\). And so it follows that \(TA\)—an informal notion—is equivalent to \(DA\), a formal notion, for the case of first order logic. (It might be assumed in addition that any intuitively valid argument is formalizable in a first order language, but Kreisel does not assume this.)