Gottlob Frege's magnum opus, "The Basic Laws of Arithmetic" (Die Grundgesetze der Arithmetic in German) constitutes one of most impressive and meticulous attempts at developing a rigorous foundation for mathematics based on logic. Unfortunately, Bertrand Russell derived a contradiction from Basic Law V, one of the axioms of Frege's system, and so mathematicians had to search for new foundations, moving from Frege's naive set theory to the system of axiomatic set theory that we use today.
But I have a question of another one of Frege's Basic Laws. Now Frege originally worked in a strange diagrammatic language that very few people have ever taken the time to learn. But Richard Heck, in the introduction to his new book "Reading Frege's Grundgesetze", puts Frege's Basic Laws into modern logical symbolism, and he states Basic Law IIb as follows: $\forall F (M_x Fx) \rightarrow M_x Gx$. That seems like the universal instantation (AKA universal elimination) axiom of second-order logic, except for the part about the $M_x$. What does the $M_x$ mean?
Any help would be greatly appreciated.
Thank You in Advance.