Whenever I get around to studying modern mathematical logic I have this feeling of awe, as if I managed to get a glimpse of the potential of the "true nature of the world".
Take the Löwenheim–Skolem theorem (mentioned in the post). It essentially tries to answer "what is the potential of illusion" within the first order logic, and shows that the potential is pretty damn big. You can be mind-blowingly confused about the "true nature of your reality". As you, a first-order logic creature, walk around, explore and interact with your space you can fool yourself into believing all kinds of marvellous things (for example that real numbers are "continuous", that they're inherently more complicated than naturals), you can even prove such things like our good friend Cantor did, never knowing that you were in fact always in a boring, aleph-zero universe. A universe built out of strings, or maybe natural numbers, nothing more than that. It's just that the daemon (engineer) ruling your world is incredibly clever and is adeptly laying out the bricks as you walk around, always putting them down just in time before you manage to turn your head around. And you'll never be able to catch that daemon and unravel the whole scheme.
I am looking forward to the next parts! I have also always wanted to understand forcing.
Second-order logic. (Not really to "replace", but to augment--to deal with those situations where first-order logic creates issues.) But I understand that not everyone would agree with that (apparently Scott Aaronson himself falls into this category, based on some of his comments in the comment section of the article).
Second-order logic is generally avoided in discussion of mathematical foundations because it is not very "foundational"; it is too vague or "mysterious" to serve as a comfortable foundation. Unlike FOL, it itself is incomplete.
In a formal set theory, like ZFC, we postulate the existence of the set of natural numbers. This is something most logicians are comfortable with as being "mathematically foundational" ("God made the natural numbers; all else is the work of man"). Then, to describe the set of sets of natural numbers we use the powerset axiom that defines what exactly we mean by "all sets of natural numbers." Then, Löwenheim–Skolem appears and says that there are models of this set theory where the number of sets that satisfy this definition is countable (not inside the logic, but looking from the outside), to which we say: well, so be it. The reason this happens is because there is a fundamental limitation to the power of describing things using finite strings of symbols. Second-order can just say, no, when I say "all subsets" I mean absolutely all. But can we precisely formalise, i.e. write down in symbols, what we mean by "all" using some basic, "simple" foundation? The answer is no. Second-order logic just vaguely gestures toward "all" and says, "by all we mean all". It circumvents the limitations of formalisation -- i.e. describing things in finite sentences -- by alluding to non-describable things.
Most logicians feel this isn't very foundational to rely on allusions to things that aren't themselves reducible to axioms in a basic foundation.
Even when higher-order logics are used in formal mathematics, like various set theories or Isabelle's HOL, they are (at best) picked to be as powerful as (multi-sorted) FOL rather than "actual" SOL.
> In a formal set theory, like ZFC, we postulate the existence of the set of natural numbers.
But if your theory is a first-order theory, you cannot pin down "the set of natural numbers" to the one you and everyone else is actually thinking of; no matter what set of axioms you use to define "the set of natural numbers" (the Peano axioms, etc.), there will be semantic models other than the set of natural numbers you are thinking of that satisfy those axioms. The only way to precisely pin down "the set of natural numbers" to one semantic model--the one you actually want--is to use second-order logic.
So it seems to me that there is a genuine tradeoff here. If you want enough expressive power to be able to precisely pin down what semantic model your theory is talking about, you need to accept that your theory will be making statements that are non-constructive--you can have an axiom that says every set has a power set, but you can't construct that power set in the general case. If you want your theory to be constructive, so that for every set that your theory says exists, you can see how to construct it explicitly, you need to accept that your theory will have multiple semantic models and only one of them is the one you want, and your theory can't pin it down for you.
It's not about being constructive. ZFC easily allows defining sets non-constructively. It's about accepting a theory whose meaning refers to objects that are not generally viewed as sufficiently basic. There seems to be a limitation on precisely describing uncountable infinities using finite strings of characters from a finite alphabet.
I agree that "constructive" was not a good term. This...
> It's about accepting a theory whose meaning refers to objects that are not generally viewed as sufficiently basic.
...is fine as a better phrasing for what I was thinking of. My point is that there is a tradeoff between the property "the theory is built entirely from objects that are sufficiently basic" and the ability to precisely pin down a single semantic model; having either one means giving up the other.
The usual objection, which I happen to agree with, is that this is a false tradeoff. The two are inextricably linked.
In the case of second-order logic, although it seems like we're getting a precise, single semantic model, in fact all we've done is push the ambiguity to the metatheory which we use to interpret the semantics of second-order logic.
For example, there's the infamous "CH statement" of second-order logic, which has a model if and only if the Continuum Hypothesis holds in the metatheory. I mean sure that's precision if you believe that the Continuum Hypothesis has an absolute truth value (that is you can confidently say "yes CH is true/false in reality") but that's really just the same thing to me at the end of the day as choosing a particular model for a first-order theory and saying "yes that model is the one true model" (which I don't really philosophically agree with in the first place since I'm usually not a strong Platonist).
Even the choice to use full semantics instead of Henkin semantics (an example of what is essentially multi-sorted FOL as @pron refers to) is an ambiguous choice one must make in deciding second-order semantics.
> In the case of second-order logic, although it seems like we're getting a precise, single semantic model, in fact all we've done is push the ambiguity to the metatheory which we use to interpret the semantics of second-order logic.
So how would this work in, say, the case of the natural numbers? What ambiguity gets pushed to the metatheory if I claim that the second order theory of the natural numbers pins down a single semantic model (the "standard" natural numbers and that's all)? If it matters, assume we are using full semantics, not Henkin semantics (see further comments on that below).
> Even the choice to use full semantics instead of Henkin semantics (an example of what is essentially multi-sorted FOL as @pron refers to) is an ambiguous choice one must make in deciding second-order semantics.
I'm not sure I would call this choice "ambiguous" since the difference between the two choices is perfectly clear, and only one of them (full semantics) preserves the key property of second order logic, of pinning down a single semantic model.
Caveat: All of this is essentially philosophy at this point and so there's no rigorous argument I can present that second-order logic is wrong. But I think you've asked reasonable questions so let's dive in.
So the CH statement (let's call it CH_2 where 2 is for second-order) I was referring to actually uses the empty vocabulary (i.e. only the usual symbols from second-order logic). In particular that means it also applies to second-order Peano Arithmetic.
So does your model of the natural numbers satisfy CH_2 or not (or put differently, is your proposed model of the natural numbers actually a model of the natural numbers)? Depends on your metatheory.
More problematically, what this demonstrates (because CH is independent of ZFC) is that second-order logic loses the absoluteness of semantic truth. That is the statement "M is a model of my theory T under a given interpretation I" can flip-flop between true and false and back again as you continue to expand your background model of your metatheory (think of e.g. Cohen forcing).
So while you may have specified exactly one model, it's getting pretty hard to see just exactly which one it is.
First-order logic does not have this phenomenon, which is why we can often get away with not going into too much detail about our metatheory in FOL (and why recursive metatheories built of FOL "all the way down" aren't too problematic). If M is a model of T under I then it will continue to be a model of T under expansion of my background model. So as long as I sketch out the basics of my metatheory (and by implication my background model), I know I'm good.
Philosophically this means that in the realm of SOL the only way you can be sure that you've really got "the" standard model and haven't mistakenly grabbed another one is if you can confidently state the truth value of every one of a never-ending stream of theorems which cannot be proved using your metatheory.
Indeed statements like "Theorem A is independent of theory T" are very murky and difficult to understand in a second-order setting. For example, CH_2 is definitely not provable using second-order PA, but does that mean we can accept systems with either CH_2 or Not(CH_2)? Well that seems to be false if we take "a single canonical model" at face value, which would imply that only one of the two can be "true," but then how do you decide whether to accept CH_2 or Not(CH_2)? No syntactic argument will suffice since we've lost completeness.
That's not to say I think that second-order logic has no value. I think second-order logic, interpreted using first-order semantics, is a valuable language. However, I agree very much with Vaananen's contention that in practice, SOL reduces to multi-sorted FOL.
> if second-order logic is used in formalizing or axiomatizing mathematics, the choice of semantics is irrelevant: it cannot meaningfully be asked whether one should use Henkin semantics or full semantics. This question arises only if we formalize second-order logic after we have formalized basic mathematical concepts needed for semantics. A choice between the Henkin second-order logic and the full second-order logic as a primary formalization of mathematics cannot be made; they both come out the same.
> in the realm of SOL the only way you can be sure that you've really got "the" standard model and haven't mistakenly grabbed another one is if you can confidently state the truth value of every one of a never-ending stream of theorems which cannot be proved using your metatheory
Let me try to restate this and see if it helps.
I say I've specified a second order formal theory that has the standard natural numbers as its unique semantic model. But "the standard natural numbers", from the standpoint of set theory, is a set, and I can apply set theory operations to it to obtain other sets. For example, I can apply the power set operation. Or I can apply the construction that is used to obtain omega-1 (the first uncountable ordinal). So it's not really true that my semantic model "only" includes the standard natural numbers. Unless I simply disallow any set theory operations altogether (which throws away most of the usefulness of the theory), I have to accept that my semantic model includes sets I might not have thought of when I set up my formal theory.
So, now that I have recognized that, for example, I can apply two different operations to my set N (the set of standard natural numbers), the power set operation P and the omega-1 construction O, I then have an obvious question: are P(N) and O(N) the same set, or different sets? And if CH is indeed logically independent of my formal theory, then the answer is that there are two semantic models of my formal theory, not one: one model in which P(N) and O(N) are the same set, and another model in which they aren't. So I haven't fully pinned down a unique semantic model after all.
Or, if CH is not independent of my formal theory, then I don't know what, exactly, my semantic model is--what sets are in it--until I figure out whether CH holds in my model or not, and that might take a while. And there are actually an infinite number of possible cases where this kind of issue might arise.
Is this a fair summary of the issue you have been trying to describe?
A late reply, but hopefully late is better than never.
Sort of. I think talking about it as if it's a phenomenon unique to sets (although indeed things are ultimately traceable back to the close relationship between second order logic and set theory) obfuscates things somewhat.
Let's take a step back. You give me a theory (second order Peano Arithmetic, let's call it PA2). Let's call the unique model (from the point of view of the metatheory) that satisfies PA2 N. Let's call our metatheory T and the implicit background model of T M.
We decide to test whether we both have the same N by asking whether N satisfies a sentence s in the language of PA2.
It turns out that whether N satisfies s depends on a theorem t that is independent of T. Do we agree on the same N? Perhaps we have different M that respectively do and don't satisfy t.
Okay that's fine, maybe our different M can be unified under a single M* that subsumes both to give us a definitive answer on N. Unfortunately it turns out that as we look at increasingly larger M* the answer of whether N satisfies s flips back and forth. There is no universal M* we can appeal to.
That's basically what's going on here when I say that all second-order logic has done is push ambiguity to the metatheory (and metamodel).
Now you can maybe argue that second-order logic is at least less ambiguous. After all the overall structure of N is assured right? We don't have non-standard natural numbers right? Well this is a bit tricky to say. Perhaps our metamodel M is actually ill-founded (which is possible from the perspective of a metametatheory even if it satisfies something like ZFC), causing N to have non-standard natural numbers as well. Now there is the possible objection that if you mess with the metamodel all bets are off. But the problem is that second-order logic with full semantics, because it lacks completeness, constantly relies instead on the metatheory and by extension metamodel to actually do proofs. That is you rarely have interesting, new proofs in second-order logic, but rather meta-proofs using the metatheory. So it is totally fair game to start examining the metamodel if everything you're doing is meta-proofs!
Moreover, from my perspective as someone who disagrees with strong, mono-universe Platonism (a term I made up that refers to people who believe that every axiom has an objective truth value and we cannot "choose" axioms in any real sense but rather are only on a journey to discover the "true" axioms of mathematics), giving up completeness is a really hard pill to swallow.
This makes it really hard to understand notions like "independence" and "consistency." If we lose completeness, consistency is no longer a sufficient criterion to admit a theory, which makes it hard to define something like independence. If we say both t and Not(t) are consistent with T, does that mean both t and Not(t) perfectly admissible axioms to add to T? The answer in the absence of completeness is no. We must investigate further. And in the case of categoricity such as with PA2, the answer is a definitive no. Only one can be admissible not both.
This can lead to really strong philosophical positions that I disagree with. For example, ZFC2 (second-order ZFC) is categorical. So either CH or Not(CH) is "true." But both are potentially consistent with ZFC2 (I'm handwaving this because second-order logic losing completeness makes even talking about consistency kind of weird unless you have completeness for your metatheory and metamodels).
But CH seems to me so clearly artificial. It's just a weird artifact of random cardinals we've made up. You're telling me that I'm either allowed to use it or not allowed to use it, but we don't know which? That seems way too strong to me.
This is especially problematic if we think back to M* where it's not clear at all when we should stop going up the hierarchy of M*s, since our answer keeps going back and forth.
That's why although I'm okay with second-order logic as a formal tool, I prefer to think in a metatheory that embraces completeness (you'll see I did that when I started talking about t being independent of T), which usually ends up being some version of FOL. Otherwise I think it's very difficult to work with mutually incompatible mathematical axiom sets for different problems since you're basically assuming completeness at a philosophical level when you do that.
At the end of the day, from my point of view, while models are important tools for examining mathematical theories as objects in their own right, the realm of formal mathematics is proofs. I hold the ability to completely formalize an argument in a computer, even if to actually do so would be extremely tedious and even impractical, as my standard for mathematical proof. A proof that is actually impossible to completely formalize constitutes "hand-waving" for me.
By that philosophical standard, we must have completeness because we are putting proofs first. This is what Vaananen means when he says that we realistically can't choose between full semantics and Henkin semantics if we wish to use second-order logic for mathematical foundations. If you want to preserve that sort of rigor, you really do need completeness and by extension you really need to default to Henkin semantics, which ends up just being multi-sorted FOL.
The traditional reason that logicians do not trust second-order logic is that usually attempts to try to formalize it start to lean back on first-order logic, e.g. by depending on a background theory of ZFC which is a first-order theory or via Henkin semantics which are also essentially first-order logic semantics and share all the same paradoxes of first-order logic.
Hence the solutions that second-order logic presents to the issues of first-order logic are really just smoke and mirrors that fall apart and turn into the same problems of first-order logic on closer inspection.
Thanks, I will read that more. I am still confused, maybe you can tell me: for 'normal math'(what is usually taught in a formal 3 year degree), is first order logic enough (for getting all the results). What I am trying is to see where this second order logic fits in to what I use already.
Simply put first order logic is enough to do almost all of mathematics and is certainly enough to cover all the results of an undergraduate degree.
More generally speaking the term "first order logic" is ambiguous by itself since we are not specifying our domain of discourse. For example, take the group axioms (e.g. there exists an identity element, every element has an inverse, etc.). In this context our domain of discourse is the elements of a single group. Hence while we can say things such as "there exists only one identity element," which is existential quantification over the elements of the group, we cannot say things such as "there exists a group with only one element" since that is quantification over groups themselves and disallowed by first order logic.
However, if we change our domain of discourse and instead e.g. use ZFC (a first order theory) as our starting point and simply augment ZFC with the language of group theory, then both statements are expressible, since both elements of a group and a group itself are sets in ZFC.
So insofar as something like ZFC is enough to do almost all of mathematics, first order logic is enough to do almost all of mathematics.
You can do a lot of math (almost all of it?) without ever touching logic. It's only important when you ask yourself things like "hmm, okay, the reals are closed under taking supremum of bounded sets, isn't that too much to ask for? how do I know reals are possible?". And of course the great logicians showed us that you can find "significant problems" already in natural numbers.
Thats not what i meant. I mean certainly you are using some logic for doing math, do you agree with this? And if you agree, is the logic we use 1st or 1st and 1nd order?
The overwhelming majority of math is done using informal logic, similar to using pseudocode to describe an algorithm. Almost no one proves mathematical theorems using formal logic, whether it's first order logic or otherwise.
Normal practice is not that formal (except for logicians ;), but would definitely be second order logic. It's common to quantify over "all functions such that..." or over set of sets for example. Second order logic is more expressive.
Thanks. I dont understand why for all elements of a set is first order and for all functions is second order - since functions (lets say R->R) are elements of the powerset of the cartesian product of RxR. So functions in math are usually part of first order logic, no?
As said by @dwohnitmok it depends on the domain you consider. If you have a proposition quantifying over objects and functions operating on said objects, it's second order. But if you have a proposition considering only said functions as objects, it is first order (with a different domain: not the base objects, but functions over those objects).
And again: you can ignore such subtleties for most of mathematics.
From outside this all looks like “Glasperlenspiel” to me. That “mathematical reasoning” assumes that there should a “logic” behind its “operations”, but why should that be so it’s never told, it’s just assumed.
Most modern mathematicians don't work with foundations but it was a hot topic at the beginning of the 20th century. Most mathematicians today wouldn't even be able to tell you when they are using the axiom of replacement, an important but technical piece of ZFC. Before the work on foundations mathematicians frequently relied on intuition to explain their ideas. The point of mathematical precision is to be able to transmit mathematical ideas with fidelity to other mathematicians; common intuitions are important for that even today.
However, it is frequently the case that mathematical intuition breaks down and paradoxical ideas need to be reckoned with. One historical example is Weierstrass's "monster": a function that is everywhere continuous but nowhere differentiable. The intuition at the time was that a continuous function could only fail to be smooth at a set of isolated points, a very tame set. It is no coincidence that he came up with this example in a period when his school was trying to recast calculus on more rigorous footing.
As for the motivation for founding mathematics on formal systems, it's because set theory is so useful for writing down mathematical ideas but naive set theory is plagued with contraditions, such Russel's paradox. Common language, too, is afflicted with contradictions such as Richard's paradox. The question was how to separate the wheat from the chaff so one does good mathematics and not nonsense. Influential mathematicians like Hilbert set out programs to establish set theory and arithmetic on a sound footing so that its use would not be held suspect. This required a more thorough mathematical development of logic as started by Boole, Frege, and others (my recollection of the precise history of these ideas is vague at this point).
So concurrently we saw the mathematization of logic, arithmetic, and language and the establishment of a reasonable set theory that did not give rise to antinomies. None of the answers were entirely satisfactory but they were good enough that common mathematical activity could continue without too much doubt. When there are questions of precision, one tries to fall back on the informal mathematical language of sets which is commonly presumed to be formalizable in systems such as ZFC.
A lot of development since then in formal mathematical systems has to do with the study of computation and the mechanization of mathematical reasoning.
But is this actually 'fooling yourself'. It looks more like an approximation. What is space happens to be discrete but the discrete points are very small compared to every day life? Then for most purposes approximating a space coordinate with real numbers is a pretty good approximation. Never mind that the possible state space of the universe could actually be smaller than such a single real number. The thing is, a human brain can presumably only grasp finitely many things but actually having to reason about finitely many things is difficult. Note that theorems about numbers are easier when they are about 'natural numbers' than about 'all numbers smaller than 2^32' because all theorems then will have preconditions that limit their size in order to exclude integer overflow and hence get somewhat hairy. So as a cognitive trick working with infinite sets works pretty well. However, complicated reasonings about the nature of these infinities turn into navel gazing pretty quickly. The thing to strive for, I think, is extending the finite and the discrete with the infinite and the continuous but but not having the illusion that we can actually say very much about the nature of the infinte.
In the context of the Löwenheim–Skolem theorem and "Skolem's Paradox", what does it mean for 'the domain of a model to be countable'?
My only guess is that the number of 'objects and/or relations' in the model forms a set of countable size.
Contrast this with the size of the objects in the model. e.g., if you have a set of countably infinite cardinality where the elements might be sets of uncountably infinite size.
In short: They both rely on a "background model" that you are implicitly working in. The "background model" and the model in discussion then disagree on which sets are countable.
That is e.g. you fix some model (perhaps a model that satisfies ZFC). Then you work within that model to create a submodel .You can then describe the submodel using properties of the outer model. In fact it turns out that you can have submodels of ZFC that are proper sets in the outer model, i.e. a single set can contain an entire subuniverse of sets that themselves satisfy the entirety of the ZFC axioms.
Using the outer model you can then talk about global properties of the submodel.
In the case of the Löwenheim–Skolem theorem it turns out that you can have a submodel satisfying the axioms of ZFC that can have arbitrary infinite cardinality in the outer model. In particular you can have a submodel of ZFC that has only a countably infinite number of sets as measured by the outer model. And in fact every element of that set can also be a set of countably infinite size according to the outer model.
According to the submodel there is no notion of the cardinality of itself, since ZFC does not have a set of all sets. Likewise the submodel "thinks" many sets within it are countably infinite. This is how the submodel is able to still satisfy ZFC.
However, the outer model disagrees with the submodel and instead thinks that the submodel is "impoverished." The submodel is missing the functions that it needs to "realize" that bijections exist between certain sets. These functions exist in the outer model.
I'm rusty with this stuff but I'm pretty sure your guess is correct, a countable model is one with countably many objects.
For other readers who might not be familiar, I'll mention that Skolem's paradox is about how there are countable models of set theory, and yet it is a theorem of set theory that uncountable sets exist, so these countable models must contain sets that are uncountable according to the model.
I think it seems less paradoxical if you think of it like this: in order for a set to be countable, there needs to exist an injection from that set to the natural numbers. So a countable model can have a set that internally looks uncountable: there is in fact an injection from that set to the natural numbers, it's just that the injection isn't included in the model.
Indeed, the statement is that for any list of axioms there exists a countable set of objects satisfying them.
For example, you could write down axioms for the real numbers by specifying that there should be relations called + and x with the standard properties such as commutativity, as well as an ordering relation < such that for all elements x and y there is an element z for which: x < z < y.
Clearly the real numbers are a model for these axioms. But as it turns out the countable set of rational numbers is a model as well.
> Clearly the real numbers are a model for these axioms. But as it turns out the countable set of rational numbers is a model as well.
You missed the crucial property that rules out the rationals (more precisely, the rationals with their standard ordering): one way of stating it is that every sequence that has an upper bound in the set, must have a least upper bound in the set. The rationals do not satisfy this property (for example, consider the sequence of successive decimal expansions, each one to one more decimal place, of sqrt(2)), but the reals do.
The challenge for me is to understand how there can still be countable sets that also satisfy that property of the reals. (Obviously any countable set can be put into one-to-one correspondence with the rationals, but for a countable set that satisfies the least upper bound property of the reals, such a correspondence with the rationals would put an ordering on the rationals that was not the standard one.)
In fact, he did not miss anything. Using the language he started with (variables range over 'numbers', and the relations are <, >, +, and *), the reals and the rationals indeed have the same properties (elementary theory as logicians would put it). The reason things like \sqrt2 present no problems is that it is simply impossible to define such 'sequences of numbers' in this theory (you are only allowed to 'refer' to numbers by your variables, not ordinary sets and the usual language for sets is missing).
If I remember right, the fact he was referring to was proved by Tarsky.
> he reason things like \sqrt2 present no problems is that it is simply impossible to define such 'sequences of numbers' in this theory (you are only allowed to 'refer' to numbers by your variables, not ordinary sets and the usual language for sets is missing).
Doesn't that mean that you can't even define the reals using the language he started with? If your language doesn't even let you express the difference between the reals and the rationals, it seems to me that the thing to do is to extend your language until it can.
> it seems to me that the thing to do is to extend your language until it can.
This depends on what you mean by define. If you mean a unique model than this is impossible. The reason is compactness theorem (every theory in which every finite set of formulas has a model has a model). The basic idea is to add constants and introduce axioms stating they are different. This will allow models of, say reals where there are plenty of reals that are not real reals (sorry for the pun, I could not resist). Nonstandard analysis takes it a bit further and makes it a bit more precise and useable.
If you mean you want to deal with (naively) definable reals only then intuitively there are only countably many of those that you can define (by formulas, etc) and you are missing a huge chunk of the real line again.
As I understand it, there is no compactness theorem in second-order logic, only in first-order logic. So your objection would not apply to extending one's language by using second-order logic.
True, the first order logic is unique in that it satisfies compactness and L-S. Extending the language to second order language (although this is not quite standard terminology) is a whole new ball of wax since the concept of a model changes as well. You can introduce a quantifier over 'unique' reals but this is a rather hollow extension since the nature of that quantifier remains just as vague. I also fail to see why the uniqueness of reals is so important. Using second order language you would have to forcefully /
'declare' every such object.
You're right that it is not possible to define the reals using the language he started with, but it's worse than that. It's also not possible to define the natural numbers using any first order theory. There is no way to extend a first order theory so that it defines the natural numbers and only the natural numbers and furthermore there is no way to define a first order theory that defines the reals and only the reals.
Having said that, you were originally right that no theory of the reals can be satisfied by the rationals, but that's for a fairly unrelated reason.
At a minimum any theory of real numbers will imply a theorem of the form "There exists an x such that x * x = 2". The set of rational numbers doesn't contain any such x and hence the rational numbers will not satisfy any theory of real numbers.
>Clearly the real numbers are a model for these axioms. But as it turns out the countable set of rational numbers is a model as well.
This wouldn't be correct, it's never the case that the set of rational numbers can satisfy a theory of real numbers, it's more subtle than that.
It's that for any theory of the real numbers, there exist subsets of the real numbers that are countable that satisfy that theory. For example the subset of all computable real numbers will satisfy any theory of real numbers despite it being countable. It's simply not possible to define a first order theory that describes the real numbers as a whole and only the real numbers as a whole.
However, there will never be any theory of real numbers that can be satisfied by the set of rational numbers. At a minimum any theory of real numbers would imply theorems that require the existence of a number that when squared was equal to 2. The rational numbers can not satisfy such a theorem.
It's great that Scott is having his stab at solving the exposition problem for the Continuum Hypothesis. I'm looking forward to the future parts of the series!
The Continuum Hypothesis is also very interesting because it is a poster child in a discussion between adherents of the "traditional dream solution" of the Continuum Hypothesis and the intriguing "multiverse philosophy of set theory". In short, the former is the attempt to devise new axioms which would settle the hypothesis. The latter is the position to embrace all possible mathematical universes.
It starts with background material in logic and set theory (fast-paced, but reasonably easy to follow and fairly complete in what it covers). Contents:
1. General background in logic
2. Zermelo-Fraenkel set theory
3. The consistency of the continuum hypothesis and the axiom of choice
4. The independence of the continuum hypothesis and the axiom of choice
I haven't gone through the whole thing, but what I've read is pretty clear. And the whole book is only 150 pages. This is not a textbook - no exercises.
(Disclaimer: I'm a mathematician, but not a logician or a set theorist.)
> Yes, there’s a “self-hating theory,” F+Not(Con(F)), which believes in its own inconsistency. And yes, by Gödel, this self-hating theory is consistent if F itself is—which means that it has a model (involving “nonstandard integers,” formal artifacts that effectively promise a proof of F’s inconsistency without ever actually delivering it). But this self-hating theory can’t be sound: I mean, just look at it! It’s either unsound because F is consistent, or else it’s unsound because F is inconsistent.
I’m not following. What does “unsound” mean here? How can a theory be consistent but unsound?
"Consistent" means that there is no proposition P such that both P and not-P have proofs within the theory. If F itself is consistent, then F+Not(Con(F)) will also be consistent, since Con(F) will have no proof in this theory. (Conversely, if F itself is inconsistent, then Con(F) will have a proof in this theory (since any proposition will have a proof in an inconsistent theory), so F+Not(Con(F)) will also be inconsistent.)
"Sound" means that there exists some semantic model of the theory that the theorems of the theory accurately describe. This cannot true of the theory F+Not(Con(F)), since there are only two possibilities:
(1) F itself is consistent--which means that, while F+Not(Con(F)) is also consistent, it can't be sound, because the theorem (by virtue of being an axiom) Not(Con(F)) cannot accurately describe any semantic model of the theory; or
(2) F itself is inconsistent--which means that the theory F+Not(Con(F)) has no possible semantic model at all (since F, a subset of the theory, cannot--no inconsistent theory can have any semantic model), and therefore cannot be sound (since to be sound a theory must have some semantic model).
1. is not true. There are semantic models of `F + Not(Con(F))` that accurately describe the theory. The difference is that these models contain nonstandard natural numbers (these nonstandard numbers become the Godel numberings of the proofs of `Not(Con(F))`) if `F` is "truly" consistent (according to the standard model of PA).
The fact that there must be semantic models of any consistent theory is a cornerstone of first-order logic and is e.g. not true of second-order logic. This follows from Godel's Completeness Theorem (not Incompleteness Theorems).
> There are semantic models of `F + Not(Con(F))` that accurately describe the theory.
That depends on what you allow to count as "accurately describing" the theory. See below.
> The difference is that these models contain nonstandard natural numbers (these nonstandard numbers become the Godel numberings of the proofs of `Not(Con(F))`) if `F` is "truly" consistent (according to the standard model of PA).
These "proofs" are only "proofs" if you accept "proofs" with an infinite number of steps. In the post I originally responded to in this subthread, there is a quote from the Aaronson article that describes it this way:
"it has a model (involving “nonstandard integers,” formal artifacts that effectively promise a proof of F’s inconsistency without ever actually delivering it)"
Aaronson doesn't accept these "proofs" as being valid, which is why he takes the position that F + Not(Con(F)) is unsound--or, to put it the way I was putting it, that Not(Con(F)) does not accurately describe the theory since F is consistent but Not(Con(F)) says it isn't. That is also the position I have been taking.
The position you are taking is that Not(Con(F)) does accurately describe the theory--and therefore that the theory F + Not(Con(F)) is in fact sound--because we can reinterpret the formula Not(Con(F)) to mean, not "there is some standard natural number that gives a proof that F is inconsistent", but "there is some non-standard natural number that gives a proof that F is inconsistent". Then, as noted, you would also have to reinterpret the notion of "proof" to allow "proofs" that contain an infinite number of steps and never actually end, since that is what a proof whose Godel number is a non-standard natural number would look like. And since such a proof never actually ends, it never actually delivers a formula that says "F is not consistent", so it never actually makes the formal system inconsistent.
In the end this is not really a dispute about the math--we agree on what the formal theory is, what its possible semantic models are, and what properties those models have--but on the use of words like "proof" and "accurately describe". So there isn't really a way to resolve such a dispute; we just have to be aware that there are two different viewpoints on how such ordinary language words can be used to describe the math.
> The fact that there must be semantic models of any consistent theory is a cornerstone of first-order logic and is e.g. not true of second-order logic. This follows from Godel's Completeness Theorem (not Incompleteness Theorems).
No. They are numbers that cannot be reached from zero by applying the successor operation. In other words, they are part of a separate infinite "chain" of numbers that "looks like" the integers (negative, zero, and positive), but is not the same as the chain of numbers that starts from zero and is the "standard" natural numbers. The first-order axioms of arithmetic cannot rule out the existence of such chains; those axioms imply that there is a chain that starts from zero (the "standard" natural numbers), but they cannot prove that it is the only chain that exists.
Yes, that's how I remember it being explained. But what sort of proof could correspond to a non-standard number? It seems like it would have to be rather strange, but if non-standard numbers aren't infinite, how can the proof be infinite?
> what sort of proof could correspond to a non-standard number? It seems like it would have to be rather strange
Yes.
> if non-standard numbers aren't infinite, how can the proof be infinite?
I am not an expert on this, but as I understand it, it has to do with how Godel numbering would have to work if non-standard numbers can be Godel numbers. Basically, only a standard natural number can be the Godel number of a finite proof; any proof that has a non-standard number as its Godel number must be infinite (i.e., it must have an infinite number of steps). But unfortunately I cannot explain why that is true. Maybe another poster here can, or can correct me if my understanding is wrong.
My usual interpretation of this is not that we have strange proofs, but rather to interpret this as a failure of Godel encodings to completely capture the notion of proof.
That is the statement Con(T) isn't really a statement about the consistency of T, but rather a statement that is "close enough" to suffice for many, but not all purposes.
Aaronson is using a slightly less common definition of soundness (arithmetical soundness) than the usual one you'll see. Usually we talk about the soundness of entire logical systems (e.g. the soundness of first-order logic) rather than particular theories within that system.
Here arithmetical soundness is tightly coupled to the idea of Godel encodings of theorems and proofs. That is a system like ZFC does not have a direct notion of theorems and proofs. Instead a statement such as `Con(ZFC)` is actually a statement about the (non-)existence of a certain natural number fulfilling certain conditions. More specifically `Con(F)` is usually a statement stating that the natural number corresponding to a Godel encoding of a proof of a clearly contradictory statement (e.g. `1 = 0`) does not exist, whereas `Not(Con(F))` is a statement that such a Godel encoding does exist (which usually makes `Not(Con(F))` the more fundamental statement of the two and `Con(F)` is really `Not(Incon(F))` but I digress).
Arithmetical soundness requires the notion of "standard natural numbers." In particular, as stated elsewhere in this thread, first-order Peano Arithmetic can be satisfied by many different models, only one of which we designate as our familiar "standard natural numbers."
Arithmetical soundness then is the property that natural numbers which satisfy the conditions of these statements encoded via Godel encodings are all standard natural numbers. So for example `Not(Con(F))` corresponds to a statement about the existence of a natural number. If `F` is "truly" consistent then `Not(Con(F))` can only be satisfied by a non-standard natural number. On the other hand if `F` is "truly" inconsistent then `Not(Con(F))` can be satisfied by a standard natural number.
You've noticed that I've put the word "truly" in quote marks. This is for two reasons:
1. The usual way to rigorously define "truly" is to appeal to some standard model. Hence the arrow of definition should be going the other way; the concept of a standard natural number that underlies arithmetical soundness is what lets talk about "true" consistency.
2. Whether it makes sense to talk about "the" standard model of a given theory or whether there are multiple possible standard models becomes a matter of philosophy. The former position corresponds to essentially a version of Platonism. The latter position is what is often known as the "multiverse" theory of mathematical logic. Through the philosophical viewpoint of the latter, we can never say absolutely whether a given theory is arithmetically unsound or not, only that it is arithmetically unsound relative to a given model of the natural numbers.
I am looking forward to the next part but he has already said something that will be a a problem later on: he said that according to L-S theorem there are countable sets that are models of set theory (ZFC to be precise). This is not really true since it contradicts Goedel's incompleteness theorem. What the method of forcing uses, however, is a pair of theorems by Mostowski: the reflection and the collapse theorem that let one find a model of any finite(ly axiomatizable) portion of ZFC. Finite axiomatizations of set theory (say, GB) have similar tricks. His intuition is right on though.
> he said that according to L-S theorem there are countable sets that are models of set theory (ZFC to be precise). This is not really true since it contradicts Goedel's incompleteness theorem
Could you clarify this a bit? I think Scott's very open to suggestions and corrections
I should have said that one cannot prove this in ZFC (of course there may be models of ZFC in which this is true) since that would meant one can prove Con ZFC in ZFC. Mostowski's theorems however are provable in ZFC and are enough for the arithmetic proofs that are produced by the method of forcing.
I have also found that students have a much easier time with forcing after learning about ultraproducts (and Los theorem) and boolean valued forcing (even though technically, the modern version using partially ordered sets of 'conditions' is much more convenient). Then you can think of forcing as a way of taking a 'model' where properties of elements are described by 'boolean valued' probabilities and collapsing it to a bona fide set theoretic universe.
The story told to me by my set theory teacher back in college was that a Paul Cohen was an Analyst who attended a symposium on Set Theory and said "hey, this is all the set theorist do? This is easy!". He then switched his field to Set Theory, developed forcing, and proved a bunch of important open questions in the field.
I don’t know if it’s true, but I’d like to believe.
He was drawn to logic by discussions with Feferman and worked unsuccessfully on other problems in logic before moving to independence questions in set theory.
I've heard a version of this too. With the additional details that after the result was announced, he struggled and took quite a bit of time to get it ready for publication.
Set theory was definitely my favorite course that I took in pure mathematics. It blew my mind how you can study “infinity” and find much structure; which I had previously thought was a fairly vague concept. It doesn’t seem surprising to me now, but definitely did then.
It might also have had something to do with the professor teaching the course, who was incredible.
So what I took away was that the Continuum hypothesis is boring. But this Löwenheim Skolem on the other hand, that sounds like some pretty crazy stuff.
Idiot’s tldr: There are problems that math, as we currently understand it, cannot solve.
“Even though Cantor proved that there are uncountably many real numbers, that only means there are uncountably many reals for us. We can’t rule out the possibly that God, looking down on our universe, would see countably many reals.”
An important second part of that quote is also that, from god's perspective, there would be impossible numbers that only a meta-god could access, and so on and so on.
And it's not so much that math as we currently understand it cannot solve some problems, but more along the lines that math has used math to prove that there are some problems that math cannot solve.
Take the Löwenheim–Skolem theorem (mentioned in the post). It essentially tries to answer "what is the potential of illusion" within the first order logic, and shows that the potential is pretty damn big. You can be mind-blowingly confused about the "true nature of your reality". As you, a first-order logic creature, walk around, explore and interact with your space you can fool yourself into believing all kinds of marvellous things (for example that real numbers are "continuous", that they're inherently more complicated than naturals), you can even prove such things like our good friend Cantor did, never knowing that you were in fact always in a boring, aleph-zero universe. A universe built out of strings, or maybe natural numbers, nothing more than that. It's just that the daemon (engineer) ruling your world is incredibly clever and is adeptly laying out the bricks as you walk around, always putting them down just in time before you manage to turn your head around. And you'll never be able to catch that daemon and unravel the whole scheme.
I am looking forward to the next parts! I have also always wanted to understand forcing.