I've been thinking recently about how logic interplays with independence results. I should preface this by saying I have essentially no background in logic or set theory, so apologies if these are not the right words to ask this question or if this question doesn't make sense.
Essentially, my current understanding is that if we take something like ZFC, that ultimately doesn't do much good without a some underlying structure such as the von Neumann universe to model it. How then does this model play with propositions that are independent of ZFC and in this model, why are we allowed to assume LEM. In my head, there are three possibilities. Either:
Within a model of ZFC (or any set of axioms) every proposition has some fixed truthiness. Thus, in $V$ for example, CH does have some fixed truth value, even if we don't know what it is. If this is the case, then that raises more questions. I think this implies that some things cannot be modeled by axioms. In particular, there is no axiomatic system whose models are themselves axioms. This is because then we would have a model which is literaly ZFC, not a model of ZFC, and within this model there are statements which do not have a fixed truthiness despite being in a model of some axiomatic system. What are the constraints then of what can and can't be modeled?
Within a model of ZFC (or any set of axioms) there are propositions which don't have some fixed truthiness. Then how can we assume LEM if we know there are propositions which are neither true, nor false. Moreover, can we inductively go up a chain of modeling until everything is true or false? If the answer is yes, is there a way to do that without resulting to some boring universe where simply every proposition is true (or something equally mundane?)
- Within a model of ZFC (or any set of axioms) the question of every proposition having some fixed truthiness itself does not have some fixed truthiness. But then, what is it independent of? What are the meta-axioms that govern models of axioms? Is there a hierarchy of meta-axioms that determine the truthiness of statements in these so-called "meta-axioms?" (I feel like this last one is especially speculative and I really don't know the right way to formalize what I'm thinking here)
Both of these posibilities are interesting, and I would really appreciate some insight into which is correct and what the implications of it are. Again, apologies if this is not the right way to ask this question, but hopefully the idea got accross. Thanks so much!
There are various points I'd like to address.
The Definition of a Model.
There seems to be confusion about what a "model" really is. Here is how I usually think of it: Everyone has some conception of mathematics proper—that is, principles that one accepts in the course of doing what they will call mathematics. The various philosophies of mathematics vary wildly in their first principles and how they are formulated—as the various philosophies have different ideas on what mathematics itself is. This is relatively important to the discussion, but I could not do it justice at the end of a paragraph, so I really suggest reading up on the literature and the mathematics surrounding this—such mathematics is called metamathematics, and it also differs considerably between the philosophies.
Regardless of how one starts, one may—if one is willing to do so, or perhaps one has to do so depending on one's philosophy—look at the notion of a "formal system". A formal system, loosely speaking, is made by an alphabet of symbols, string formation rules with that alphabet, rules for deriving different well formed strings from obtained well formed strings, and some well formed sentences taken as a starting point. The string formation and derivation rules are the syntax and logic, and the starting point sentences are the axioms of the formal system.
A formal system by itself is nothing more—it's a bunch of strings. Just by itself, it has varying importance to the different philosophies of mathematics. But what is important is how much these strings can match, that is model the behavior of what one already considers as mathematical objects. And this is what a model basically is: It is a one to one correspondence between the meaningless strings and an aggregate of mathematical objects and operations. With such a correspondence, one obtains a way to give meaning to the symbols; models of a formal system form the semantic part of the study of that formal system. This allows one to relate various mathematical objects in quite large scales, as there is no fixed meaning attributed to the symbols—it is like a tool for perfect mathematical analogy.
Truthiness of Propositions; and what LEM is.
Let us go back to the concrete example of ZFC. It is also just a bunch of strings constituting a formal system. Solely by itself, the symbols have no meaning. One has to bring the meaning in by mathematical interpretation of the symbols; and there may be various inherently distinct ways in which the system can be mathematically interpreted. Only within that context is one able to talk about the truthiness or falsity of statements in the system. Truth is borne by the interpretation—this is true even in natural language.
A good example is the continuum hypothesis: Kurt Gödel showed that there exists a mathematical interpretation, a model of ZFC such that the continuum hypothesis is true. Note that this already rules out a proof of the negation of the continuum hypothesis within ZFC; that is, a series of string derivations starting from the axioms and concluding in the string representing the negation of the continuum hypothesis. This is because Gödel's model is sound with the system, so all such derivations would yield an interpretation that concludes in a mathematical object falsifying the continuum hypothesis, whereas we observe from the interpretation that no such object can be found. On the other hand, Paul Cohen found a model of ZFC where the continuum hypothesis is false; by similar reasoning, this also excludes any proof of the continuum hypothesis itself. The grand conclusion is that we cannot find any derivation of strings, any proof in the formal system ZFC that results in the statement of any one of the continuum hypothesis and its negation; the issue is not decidable by ZFC's deductive power alone, and either statement can be soundly interpreted mathematically.
This seems to raise the following question: What about the law of the excluded middle? LEM exists in the logic of ZFC, so we can apply it to the continuum hypothesis to obtain the statement "Either the continuum hypothesis, or the negation of the continuum hypothesis". Isn't this outright contradictory to the results of Gödel and Cohen?
This is not a problem whatsoever. LEM, within ZFC, is a derivation rule; it is merely strings, and it has only to do with the syntax of ZFC. On the other hand, the results of Gödel and Cohen have to do with the semantics of ZFC. Even though we conventionally read the strings representing LEM in a semantic nature (that is, confusing a syntactic formulation of LEM with the semantic principle of bivalence that may be taken up in the process of modelling), this does not mean the combination of strings is inherently semantic and will apply to all interpretations. Such confusion merely arises from our tendency to interpret the symbols from the get go in an (in this case necessarily) incomplete manner—but the symbols only stay on the page.
I've glossed over a lot of specifics here. In particular, if one is not diligent, the possible philosophies and how they deal with the notion of formal systems can get really confusing; one really has to read through the literature, understand the mathematical results, and consider the correspondence between mathematicians to get a good idea of the discussion.
Some people consider LEM in a similar way to the continuum hypothesis or the axiom of choice (and I also share this opinion.); in fact, analyzed in this way, the axiom of choice and set comprehension imply LEM, syntactically. From the mainstream point of view, it is perhaps the simplest instance of a sentence that is independent from a (relatively) conventional theory: One may loosen the axioms/sentence formation of ZF so that LEM is not admitted—this system is called IZF. For IZF, one may find various models that falsify the sentence expressing LEM. This shows that IZF cannot prove LEM, in a similar way to Cohen's proof. But by mere inspection, one sees that the question of LEM's consistency in IZF is the question of ZF's consistency as a system, which is widely accepted. So if one sees ZF to be consistent, it is seen that LEM is independent from IZF. (This is why I believe I need to preface this by saying this is an example from the mainstream point of view.)
Loosely speaking, mathematics done without LEM is called constructive mathematics. There have been various formal systems not including LEM, like IZF, and their properties have been investigated both classically and constructively—that is, both with and without the aid of LEM itself. The issues concerning LEM are both mathematically and philosophically interesting; and many mathematicians, though making up a small minority in the very large community, work on these problems. The main point is that LEM is no different from the axiom of choice or the continuum hypothesis; LEM itself can become the independent statement of interest, and people can choose to accept or even reject it, as many accept or reject the axiom of choice or the continuum hypothesis.