My reading of Carnap's "The Elimination of Metaphysics Through Logical Analysis of Language" suggests to me that it is possible to form sentences in a language that are grammatically correct but logically meaningless. The consequence of this is that the statement, due to its logical incoherence, cannot be proven to be true or false. And likewise, if a statement cannot be proven, then it is meaningless. [...] So what's going on here? Am I missing the point of what Carnap is arguing entirely?
You have to be careful about what Carnap and other logical positivists are trying to do. They are not trying to prove a linguistic point about grammar and meaning. They are trying to prove an epistemological point about how language and meaning connect to the world, as expressed in their famous verification principle. The verification principle states that the only statements that are meaningful are those of logic and those that can be verified empirically. Let me illustrate:
Consider 3 statements:
- (a) The green frog caught the matrix because he was dialectic.
- (b) The man caught a disease because he was unlucky.
- (c) The man caught food poisoning because the shrimp he ate was bad.
That (a) is meaningless even though it is grammatically correct is uncontroversial, most people would consider (a) to be meaningless, while both (b) and (c) are meaningful sentences.
This is not what Carnap and the Positivists are saying, their claim is much stronger: They think that (b) is just as meaningless as (a), because the concept "unlucky" cannot be verified empirically. What does it mean for someone to be "unlucky"? Can you measure "unluckiness" or observe it with a microscope? Can you perform an experiment to prove that Sam is unlucky? No, and hence the term unlucky doesn't carry any meaning, and hence (b) is just as much gibberish as (a).
This is why they objected to Hegel, Heidegger, and other who used the same style. Statements about "Geist", "The Owl of Minerva", "Dasein", "Nothingness nothings", etc...fell in the same category as "unlucky" in that there was no way to verify them empirically, and so their philosophy was meaningless. Their goal wasn't the analysis of language for its own sake, but the elimination meaningless statements from philosophy, so that the only statements that remained were similar to those of the sciences - in the process they would get rid of metaphysics, which they thought a pejorative term.
So the real crux of my question is, how can Carnap (and other logical positivists) prove the axioms of their own theories/systems?
Well they couldn't, that's why Carnap and the Logical Positivists' program is considered to have failed (*). It is unique among philosophical school in that it declared dead by its own people after it faced several challenges including the one you allude to which is that the verification principle is itself a statement that cannot be verified empirically. See here and here for details, and this video of here's A.J. Ayer, leading British L.P, admitting it all turned out to be false - starting just before 34:00
And yet, I and many philosophers have read Heidegger and, while they may disagree on the interpretation of the work as a whole, they could probably agree to some extent on the meaning of some of the individual sentences. And further, one could still derive utility from this sentence even if it is not "true" in the logical sense. This argument could apply to many metaphorical statements too. Two people can still understand each other even if the statements are "meaningless" as defined by Carnap.
This is the same conclusion that Wittgenstein and others arrived at. Wittgenstein started out as holding views very similar to Carnap and the Logical Positivists: Logical statements and empirical statements are the only meaningful statements. But then he abandoned those views and in his later philosophy subscribed to the view that meaning is use: Statements derive their meaning not from the way correspond to empirical facts, but from the way we use them. The term "unlucky" is used in a certain way when we communicate and that is enough to give it meaning. See Ordinary Language Philosophy and Pragmatism.
(*) An additional note: That the logical positivist program is considered to have failed and was abandoned by the 1960s is the most common position, and is frequently mentioned in various introductory articles and courses. As I mentioned earlier, it was notable that several people who were themselves associated with the L.P movement had agreed that it failed, which is why most accept its failure as a fact.
Some philosophers, notably Michal Friedman, have argued that Logical Positivism shouldn't be dismissed, that it hasn't failed as completely as most sources claim, and that too many people dismiss it because it became fashionable to do so, without actually examining the ideas of LP. See Reconsidering Logical Positivism and this post.
Regardless of whether the L.P program failed completely or not, it's influence on philosophy in general and analytical philosophy in particular cannot be denied. One can argue that although the verification principle itself has challenges, the spirit of L.P with its emphasis on clarity and rigor has been passed on to subsequent schools of thought.