Abstract: In the talk with the same title I gave at the "Hommage à Grothendieck" meeting on February 19th and 20th, I wrote down two definitions of "pretopos", the original one given by Grothendieck and Verdier in SGA4 (1972), and the one given in M.M. & G.E. Reyes, "First order categorical logic" (1977). In the talk, I will present the proof, already given in "First order categorical logic", of the equivalence of the two definitions. Some further comments will be given on the relations of Grothendieck's sheaf-theoretic approach on the one hand, and the "direct quantificational" approach on the other hand, to first-order logic. The talk is purely expository: all results and proofs (sometimes in slightly different language) already appear in "First order categorical logic".