 Hintikka finds this type of allegation unfounded. First, \(\mathbf{IFL}\) shares many of the important metalogical results with \(\mathbf{FO}\) (cf. Subsect. 4.1). Second, just like \(\mathbf{IFL}\), also \(\mathbf{FO}\) can be translated into second-order logic. The only difference is that in the former case a larger variety of quantifier (in)dependencies must be encoded by Skolem functions than in the latter. Why would the former translation render \(\mathbf{IFL}\) a part of mathematics while the latter would allow \(\mathbf{FO}\) to remain a logic (Hintikka 1991: 26–27)? Third, one must make a distinction between what is needed to understand an \(\mathbf{IFL}\) sentence, and what is needed to mechanically deal with the validities (logical truths) of \(\mathbf{IFL}\). Due to its non-axiomatizability, there are no mechanical rules for generating the set of all validities of \(\mathbf{IFL}\). However, to understand a sentence is to know what things are like when it is true, not to know what things are like when it is logically true (Hintikka 1995: 13–14). Fourth, because of non-axiomatizability, the valid inference patterns in \(\mathbf{IFL}\) cannot be exhausted by any recursive enumeration. Insofar as important mathematical problems can be reduced to questions about the validity of \(\mathbf{IFL}\) formulas (Subsect. 5.3), progress in mathematics can be seen to consist (not of the discovery of stronger set-theoretical axioms but) of ever more powerful rules for establishing validity in \(\mathbf{IFL}\) (Hintikka 1996: 100; 2000: 135–136).