I have recently been reading about first-order logic and set theory. I have seen standard set theory axioms (say ZFC) formally constructed in first-order logic, where first-order logic is used as an object language and English is used as a metalanguage.

I'd like to construct first-order logic and then construct an axiomatic set theory in that language. In constructing first-order logic using English, one usually includes a countably infinite number of variables. However, it seems to me that one needs a definition of countably infinite in order to define these variables. A countably infinite collection (we don't want to call it a set yet) is a collection which can be put into 1-1 correspondence with the collection of natural numbers. It seems problematic to me that one appears to be implicitly using a notion of natural numbers to define the thing which then defines natural numbers (e.g. via Von Neumann's construction). Is this a legitimate concern that I have or is there an alternate definition of "countably infinite collection" I should use? If not, could someone explain to me why not?

I think that one possible solution is to simply assume whatever set-theoretic axioms I wish using clear and precise English sentences, define the natural numbers from there, and then define first-order logic as a convenient shorthand for the clear and precise English I am using. It seems to me that first-order logic is nothing but shorthand for clear and precise English sentences anyway. What the exact ontological status of English is and whether or not we are justified in using it as above are unresolvable philosophical questions, which I am willing to acknowledge, and then ignore because they aren't really in the realm of math.

Does this seem like a viable solution and is my perception of first-order logic as shorthand for clear and precise English (or another natural language) correct?

Thank so much in advance for any help and insight!

  • $\begingroup$ I have thought about this as well, and as far as I can tell, yes. It seems to me that one just can't get around the natural numbers as the true meta-foundation of mathematics. Furthermore, the natural numbers are philosophically undefinable. One can define them inside set theory, but the language of set theory is defined by induction on the natural numbers. One can't get around it. But this is philosophy, and the above therefore just an opinion. $\endgroup$ – vhspdfg Dec 26 '15 at 22:30
  • $\begingroup$ What do you mean by philosophically undefinable? $\endgroup$ – JWP_HTX Dec 26 '15 at 22:41
  • $\begingroup$ If they are not taken as granted, what are the natural numbers? Some kind of set. But what is a set? That's even more nebulous than the question of what are the natural numbers. It seems the best we can do to define the concept of set without assuming it a priori is to define a set as an element of the definable imaginary substructure of the natural numbers given by applying Godel's completeness theorem to the axioms of set theory as encoded in the natural numbers. But this assumes the natural numbers as a priori! As Noah's answer said, we have to assume something to get off the ground. $\endgroup$ – vhspdfg Dec 26 '15 at 23:02
  • $\begingroup$ The metatheory certainly presupposes it, in most presentations. For example, the alphabet is usually said to include "infinitely many variables $v_0, \dotsc, v_n, \dotsc$". The metatheory also assumes definition and proof by well-founded induction on tormulas, which is essentially proof by ordinary induction on (some notion of) rank of a formula. $\endgroup$ – BrianO Dec 26 '15 at 23:53
  • $\begingroup$ See George Tourlakis, Lectures in Logic and Set Theory. Volume 1: Mathematical Logic (2003), page 8-on with a discussion on how to minimize the "numerical committment" in the syntax. $\endgroup$ – Mauro ALLEGRANZA Dec 27 '15 at 8:13

I think there are two (very interesting) questions here. Let me try to address them.

First, the title question: do we presuppose natural numbers in first-order logic?

I would say the answer is definitely yes. We have to assume something to get off the ground; on some level, I at least take the natural numbers as granted.

(Note that there's a lot of wiggle room in exactly what this means: I know people who genuinely find it inconceivable that PA could be inconsistent, and I know people who find it very plausible, if not likely, that PA is inconsistent - all very smart people. But I think we do have to presuppose $\mathbb{N}$ to at least the extent that, say, Presburger arithmetic https://en.wikipedia.org/wiki/Presburger_arithmetic is consistent.)

Note that this isn't circular, as long as we're honest about the fact that we really are taking some things for granted. This shouldn't be too weird - if you really take nothing for granted, you can't get very much done https://en.wikipedia.org/wiki/What_the_Tortoise_Said_to_Achilles. In terms of foundations, note that we will still find it valuable to define the natural numbers inside our foundations; but this will be an "internal" expression of something we take for granted "externally." So, for instance, at times we'll want to distinguish between "the natural numbers" (as defined in ZFC) and "the natural numbers" (that we assume at the outset we "have" in some way).

Second question: Is it okay to view first-order logic as a kind of "proxy" for clear, precise natural language?

My answer is a resounding: Sort of! :P

On the one hand, I'm inherently worried about natural language. I don't trust my own judgment about what is "clear" and "precise." For instance, is "This statement is false" clear and precise? What about the Continuum Hypothesis?

For me, one of the things first-order logic does is pin down a class of expressions which I'm guaranteed are clear and precise. Maybe there's more of them (although I would argue there aren't any, in a certain sense; see Lindstrom's Theorem https://en.wikipedia.org/wiki/Lindstr%C3%B6m%27s_theorem), but at the very least anything I can express in first-order logic is clear and precise. There are a number of properties FOL has which make me comfortable saying this; I can go into more detail if that would be helpful.

So for me, FOL really is a proxy for clear and precise mathematical thought. There's a huge caveat here, though, which is that context matters. Consider the statement "$G$ is torsion" (here $G$ is a group). In the language of set theory with a parameter for $G$, this is first-order; but in the language of groups, there is no first-order sentence $\varphi$ such that [$G\models\varphi$ iff $G$ is torsion] for all groups $G$! This is a consequence of the Compactness Theorem for FOL.

So you have to be careful when asserting that something is first-order, if you're working in a domain that's "too small" (in some sense, set theory is "large enough," and an individual group isn't). But so long as you are careful about whether what you are saying is really expressible in FOL, I think this is what everyone does to a certain degree, or in a certain way.

At least, it's what I do.

  • $\begingroup$ Great answer - thank you!! Let me see if I'm understanding you correctly - as far as the first question goes, are we assuming that a "natural numbers-like" collection exists outside of set theory, which we then use to construct FOL. In turn, we can construct the actual natural numbers within an axiomatic set theory? For instance, are we assuming something like PA get our external object? As far as the second question - I see your point, great answer :) $\endgroup$ – JWP_HTX Dec 26 '15 at 22:52
  • $\begingroup$ @Searching_for_a_foundation I would say yes to your question. In particular, the thing we build formally (say, in ZFC) which we call the "natural numbers" is supposed to match our informal intuitions about what $\mathbb{N}$ should be; and one criterion a "good" foundation of math should meet is that it be able to construct something which it proves is "like" the natural numbers. Now, depending who you talk do, you'll get different exact criteria here (or non at all :P) - should it satisfy PA? $I\Sigma_1$? Presburger arithmetic? - but yes, that is what I am saying. $\endgroup$ – Noah Schweber Dec 26 '15 at 22:56
  • 1
    $\begingroup$ @RobArthan I disagree - talking about "finite strings", an essential part of any syntax, presupposes a notion of "finiteness." There are various ways to grapple with this issue, but I think the most honest one is to just admit that we are starting out with a conception of something like $\mathbb{N}$. $\endgroup$ – Noah Schweber Dec 27 '15 at 23:42
  • 1
    $\begingroup$ @NoahSchweber: I don't disagree very strongly with you, but I do think that the concept of a sequence of signs is a more primitive one than the concept of a number. You can define a formal language without using concepts from arithmetic. $\endgroup$ – Rob Arthan Dec 28 '15 at 0:07
  • 1
    $\begingroup$ @RobArthan I don't understand how this can be so - if "sequence" makes sense, then "length of sequence" makes sense. Put another way, any reasonable theory of sequences of symbols naturally interprets at least the theory of $(\mathbb{N}; 0, S)$, and any such theory capable of talking about concatenation can interpret Presberger arithmetic. So I really don't see how sequences can be more primitive. But this is a philosophical point, of course. $\endgroup$ – Noah Schweber Dec 28 '15 at 0:09

There are three inter-related concepts:

  • The natural numbers
  • Finite strings of symbols
  • Formulas - particular strings of symbols used in formal logic.

If we understand any one of these three, we can use that to understand all three.

For example, if we know what strings of symbols are, we can model natural numbers using unary notation and any particular symbol serving as a counter.

Similarly, the method of proof by induction (used to prove universal statements about natural numbers) has a mirror image in the principle of structural induction (used to prove universal statements about finite strings of symbols, or about formulas).

Conversely, if we know what natural numbers are, we can model strings of symbols by coding them as natural numbers (e.g. with prime power coding).

This gives a very specific argument for the way in which formal logic presupposes a concept of natural numbers. Even if we try to treat formal logic entirely syntactically, as soon as we know how to handle finite strings of symbols, we will be able to reconstruct the natural numbers from them.

The underlying idea behind all three of the related concepts is a notion that, for lack of a better word, could be described as "discrete finiteness". It is not based on the notion of "set", though - if we understand what individual natural numbers are, this allows us to understand individual strings, and vice versa, even with no reference to set theory. But, if we do understand sets of natural numbers, then we also understand sets of strings, and vice versa.

If you read more classical treatments of formal logic, you will see that they did consider the issue of whether something like set theory would be needed to develop formal logic - it is not. These texts often proceed in a more "finitistic" way, using an inductive definition of formulas and a principle of structural induction that allows us to prove theorems about formulas without any reference to set theory. This method is still well known to contemporary mathematical logicians, but contemporary texts are often written in a way that obscures it. The set-theoretic approach is not the only approach, however.

  • $\begingroup$ By the way, one way to see the relationship is to look at nonstandard models of set theory. If we have nonstandard natural numbers in a model, then we also have nonstandard formulas, and vice-versa. The three concepts completely determine each other. $\endgroup$ – Carl Mummert Dec 29 '15 at 0:13
  • $\begingroup$ Examples of any books that consider logic without reference to set theory? $\endgroup$ – Fawzy Hegab Dec 29 '15 at 15:34
  • 1
    $\begingroup$ As I wrote in an answer somewhere else, it is very standard to look at finitistic metatheories, which don't even talk about infinite sets of natural numbers, much less general set theory. You would want to approach this via the literature on proof theory. In Model Theory, there is no reason to avoid set theory, and so they don't. In introductory texts, they typically just use the normal methods of mathematics, and they also have no reason to avoid set theory. But an enormous amount is known about what is needed in the metatheory, and set theory is far more than is generally required. $\endgroup$ – Carl Mummert Dec 29 '15 at 15:38
  • $\begingroup$ So, such stuff is in the releam of proof theory? $\endgroup$ – Fawzy Hegab Dec 29 '15 at 18:54
  • $\begingroup$ To some extent, yes. It is not the direct goal of "proof theory" as it is usually described. But the traditional area of "metamathematics" is closest to proof theory, out of the "big four" areas of mathematical logic today. $\endgroup$ – Carl Mummert Dec 29 '15 at 19:06

For the title question, I would say the answer is no (sort of). To define the language of first-order logic, you only need to talk about finite lists of signs drawn from a finite alphabet. For example, the alphabet might comprise the the 36 signs $a,b,c,\ldots,x, y, z,0,1, \ldots, 9$ together with a sign that I'll call a "space". You certainly don't need to define the notion "countably infinite" to ensure a countably infinite supply of variable symbols: you can just ensure that when you define how sequences of signs encode language constructs: e.g., by saying that a variable comprises a letter followed by a non-zero digit followed by a sequence of digits terminated by a space.

But having said that, to reason about syntax, you will need to reason by induction, and the dividing line between reasoning about sequences of signs and reasoning about natural numbers becomes a very fine one.

(See https://en.wikipedia.org/wiki/Formal_system#Logical_system for some more information on this kind of thing. For good reasons, logic texts often gloss over the details, as all that really matters is that formulas in the language can be represented as finitary objects.)

  • $\begingroup$ Thanks for your answer! I am wondering if you could clarify a few points for me - in particular, what is a sign? What do you mean by "wiring" the notion of countably infinite into a low-level definition of syntax. I am unfamiliar with these terms. $\endgroup$ – JWP_HTX Dec 27 '15 at 7:56
  • $\begingroup$ By "sign", I just mean some agreed way of representing elements of the alphabet. I have tried to clarify the answer. $\endgroup$ – Rob Arthan Dec 27 '15 at 15:53
  • $\begingroup$ Thanks for the clarifications - so to be clear, you are basically encoding the notion of countably infinite into the grammar of the language? $\endgroup$ – JWP_HTX Dec 27 '15 at 17:07
  • $\begingroup$ Yes, that's exactly right. $\endgroup$ – Rob Arthan Dec 27 '15 at 23:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.