Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: mathematics

Topic: the empty set is a subset of other sets

David Egolf (Apr 01 2023 at 03:05):

In another thread, John Baez gave this proof:
John Baez said:

$X \subseteq Y$ is true if and only if $x \in X$ implies $x \in Y$. Suppose $X = \emptyset$. Then $x \in X$ is always false. A false statement implies anything, so in this case $x \in X$ implies $x \in Y$ for any set $Y$. Thus $\emptyset \subseteq Y$ for any set $Y$.

I was hoping to try and understand it a little better in this thread...hopefully learning a little bit about logic in the process.

It starts off by saying "$X \subseteq Y$ is true". I recently learned about the concept of a "proposition", which to my understanding is roughly something we can try to prove, or can assign a truth value to. Since we are assigning a truth value, maybe we have a proposition here: $X \subseteq Y$ ?
Except, it seems like this is impossible to prove (or disprove) as we have not specified what $X$ and $Y$ are yet (besides being sets). So perhaps $X \subseteq Y$ is not a proposition?

Instead, is $X \subseteq Y$ implicitly a "propositional function"? By propositional function, I believe is meant a function that maps elements of a set to propositions (is this related to something called a "predicate"?). In this case, I would worry about what the domain of this function is, as the collection of all (pairs of) sets is not a set, as far as I understand it.

Anyways, any clarification so far would be much appreciated!

Jacob Zelko (Apr 01 2023 at 04:18):

Hey David, something that might help with clarifying this is that we are setting up to prove the statement $X \subseteq Y$ only in the case of $X = \emptyset$. That's the rules of the game we are playing right now with proving the statement $X \subseteq Y$ -- we are not proving the general form of $X \subseteq Y$ but rather only $\emptyset \subseteq Y$. In that way, we avoid Russell's paradox which is what I think you may have been alluding to.

David Egolf (Apr 01 2023 at 04:27):

Jacob Zelko said:

Hey David, something that might help with clarifying this is that we are setting up to prove the statement $X \subseteq Y$ only in the case of $X = \emptyset$. That's the rules of the game we are playing right now with proving the statement $X \subseteq Y$ -- we are not proving the general form of $X \subseteq Y$ but rather only $\emptyset \subseteq Y$. In that way, we avoid Russell's paradox which is what I think you may have been alluding to.

I was wanting to work up to considering this statement: $X \subseteq Y$ is true if and only if $x \in X$ implies $x \in Y$. I believe this statement is true for any sets $X$ and $Y$.

I guess I get a little confused by talking about how $X \subseteq Y$ is true for some choices of $X$ and $Y$ and not for others, and was trying to think how that might be formalized. I was wondering if one could consider a function that takes in choices for $X$ and $Y$ and then tells us if $X \subseteq Y$ is true... but I'm not sure if the domain of this function makes sense!

David Egolf (Apr 01 2023 at 04:33):

I suppose I'm trying to understand truth tables a little better. Googling "truth table implication" gives us images like this:
implication truth table

This looks to me like $P$ and $Q$ might sometimes be true and sometimes be false, corresponding to different rows of the table here... and I'm wondering if that means that $P$ and $Q$ are both functions that spit out truth values. (e.g. "$x$ has four legs" is true at $x$="a tiger" and is false at $x$="an ostrich").

Or maybe I'm just overcomplicating things here and this truth table is only meant to be applied to statements having a fixed truth value? If so, I'm curious how to talk about implication in the context of statements about variables, which can have a varying truth value depending on the value of the variable.

David Egolf (Apr 01 2023 at 04:36):

I hope that at least partially clarifies the nature of my confusion!

Jean-Baptiste Vienney (Apr 01 2023 at 04:53):

David Egolf said:

this truth table is only meant to be applied to statements having a fixed truth value?

Yes, that's the goal of this table.

Jean-Baptiste Vienney (Apr 01 2023 at 04:57):

David Egolf said:

If so, I'm curious how to talk about implication in the context of statements about variables, which can have a varying truth value depending on the value of the variable.

If $A$ and $B$ are statements about variables $x,y,z...$ which can be either true or false then you can say that $A \vdash B$, in English "A logically entails B" if for every truth values of $x,y,z...$ we find that $A \Rightarrow B$ has the truth value $T$ using this table.

Jean-Baptiste Vienney (Apr 01 2023 at 04:59):

$A \vdash B$ thus means "each time A is true, then B is true".

Jean-Baptiste Vienney (Apr 01 2023 at 05:02):

When we say that $A$ implies $B$ in mathematics, it is almost always in the sense $A \vdash B$. But mathematicians often write $A \Rightarrow B$ to signify this because we don't want to go into formal logic and it's customary to do this.

Reid Barton (Apr 01 2023 at 05:10):

$X \subseteq Y$ is a proposition provided that $X$ and $Y$ are sets. The context should make it clear what $X$ and $Y$ refer to. Maybe they are variables, maybe they are sets with some fixed definitions. Or maybe they are sets defined in terms of some other variables.

From context, "$X \subseteq Y$ is true if and only if $x \in X$ implies $x \in Y$" really means "For all sets $X$ and $Y$, ..." so here $X$ and $Y$ are variables.

Reid Barton (Apr 01 2023 at 05:12):

If you like, and aren't deterred by size issues, you can introduce "the function that sends two sets $X$, $Y$ to the proposition $X \subseteq Y$". But I think it's more confusing than helpful to try to understand $X \subseteq Y$ itself as this function.

John Baez (Apr 01 2023 at 05:23):

@David Egolf - since mathematical logic of a traditional sort was my first love, I usually tend to think of my proofs as things that could be formalized in first-order logic, also known as predicate logic. This is a widely used framework for making math rigorous. It was developed by people like Boole and Peirce and Frege and Peano and Russell and Whitehead and Hilbert and Bernays and Goedel.

A lot of people here are experts in more modern approaches, but first-order logic is definitely worth knowing, because from 1920 to 2000, and probably even today, most logicians will instantly resort to it if you ask questions like "what sort of thing is "$X \subseteq Y$"?" It's a noble tradition and an excellent background for newer things like category theory and type theory and homotopy type theory. These newer things often rebel against classical first-order logic in various ways, but I think it's hard to understand these newer things without understanding what they're rebelling against!

John Baez (Apr 01 2023 at 05:28):

If you read the linked article on first-order logic you'll learn about technical terms like 'variables', 'functions', 'terms', 'predicates', 'formulas', and so on.

John Baez (Apr 01 2023 at 05:29):

In this setup, X and Y are variables, $\subseteq$ is a binary predicate, and $X \subseteq Y$ is a formula with 2 free variables, $X$ and $Y$.

John Baez (Apr 01 2023 at 05:30):

Something like "$X \subseteq Y$ if and only if $x \in X$ implies $x \in Y$" is a more complicated formula, and it's an informal way of saying

$X \subseteq Y \iff \forall x (x \in X \implies x \in Y)$

John Baez (Apr 01 2023 at 05:32):

This is again a formula with 2 free variables, $X$ and $Y$. But I was implicitly claiming it's true for all $X$ and $Y$, i.e.

$\forall X \forall Y (X \subseteq Y \iff \forall x (x \in X \implies x \in Y) )$

John Baez (Apr 01 2023 at 05:32):

This is a formula with no free variables, also known as a "sentence".

John Baez (Apr 01 2023 at 05:34):

This sentence could be an axiom of set theory in some version of set theory phrased in first-order logic. In any event, few people doing set theory in first-order logic would be upset by you asserting this sentence.

John Baez (Apr 01 2023 at 05:37):

You could look up the ZFC axioms in a book on mathematical to see some widely used axioms for set theory, but most (classical) mathematicians just have a sense for what kinds of sentences you can assert about $\subseteq$ and $\in$ as part of a proof, without anyone objecting. Many of them would call this formula

$X \subseteq Y \iff \forall x (x \in X \implies x \in Y)$

the "definition" of $\subseteq$.

Todd Trimble (Apr 01 2023 at 11:28):

I'll poke my nose in for just a bit. John just said that the last formula he wrote down can be regarded as the definition of the subset relation. One important thing to realize about definitions is that they are always declaration of "if and only if" type. For example, if a set $X$ is empty, then by definition [of empty set], $X$ has no elements. And conversely, if a set $X$ has no elements, then by definition $X$ is empty.

Todd Trimble (Apr 01 2023 at 11:29):

This can be a very convenient thing to remember when first learning how to construct proofs. In mathematics, we refer to and refer back to definitions all the time, even when we don't explicitly say so. Students who are just learning the art of constructing proofs should get into the habit of, early and often, mentioning when a definition is being invoked ("This means, by definition of blank, that..."), to make clear to themselves the overwhelmingly important role they play in mathematics and mathematical proof.

Todd Trimble (Apr 01 2023 at 11:29):

The formal content of mathematics pretty much boils down to definitions, axioms, statements of propositions (I'm including theorems, lemmas, corollaries, etc.), and proofs of propositions.

Todd Trimble (Apr 01 2023 at 11:29):

Another word that's come up here is "variable". Deploying variables is another thing that students need to learn to do, but it's usually something that's not taught too well. Roughly speaking, you could think of a variable as an "indefinite pronoun". Good practice is, whenever you introduce a variable $x$ in the course of a proof, say what type of thing $x$ refers to. Is $x$ supposed to be a real number, or an integer, or a subset of some other set, or what? All mathematics takes place within contexts, and declaring which context an introduced variable belongs to greatly aids clarity. (Mathematicians don't follow this practice as much as they should!)

Todd Trimble (Apr 01 2023 at 11:29):

Variables are also intimately tied with logical quantification, which has to do with correct handling of the phrases "for all" and "there exists". After you learn the bedrock of how propositional logic works, which governs the use of words "and", "or", "not", "implies" -- something that is typically taught by referring to truth tables, and something most students experience as relatively easy -- the next step is seeing how all this interacts with logical quantifiers. This takes a little more time for students than the propositional calculus.

Todd Trimble (Apr 01 2023 at 11:30):

An instructive exercise to cut your teeth on is to go through, in fine-grained detail, something like this. "Let $A, B, C$ be subsets of a domain $D$. Prove that $A \cap (B \cup C) = (A \cap B) \cup (A \cap C)$." Everything I've mentioned above comes into play: the definition of equality of sets, which is defined in terms of subset inclusion. This in turn involves universal quantification, which in turn involves introducing a variable and knowing how to deal with it correctly. Also, the definitions of union and intersection of sets, and the way in which the proof systematically reduces the proposition down to an analogous "distributive law" in propositional logic.

Todd Trimble (Apr 01 2023 at 11:30):

Since you may be learning all this stuff on your own, you'll need to get hold of a textbook. The late great Gian-Carlo Rota once upheld the Schaum's Outline Series of mathematical texts. These have hundreds and hundreds of worked problems and they will get you into a subject fast. And they are cheap; look for used copies online. The only way to learn how to do proofs is to do a ton of them, but at least by the looks of it, there are a lot of people here willing to help.

David Egolf (Apr 01 2023 at 14:27):

Jean-Baptiste Vienney said:

If $A$ and $B$ are statements about variables $x,y,z...$ which can be either true or false then you can say that $A \vdash B$, in English "A logically entails B" if for every truth values of $x,y,z...$ we find that $A \Rightarrow B$ has the truth value $T$ using this table.

This is helpful! I've seen that $\vdash$ symbol before, but I've never been clear on exactly what it means.
If we write the truth value of $A$ for a specific value of $x,y,z...$ as $A(x,y,z,...)$ and similarly for $B$, then if I understand you correctly, I think we have $(A \vdash B) \iff (A(x,y,z,...) \implies B(x,y,z,...) \textrm{ for all } x,y,z...)$.
This reminds me a little how we can define addition of functions point by point: $(f+g)(x) = f(x)+g(x)$. Although this seems a bit different, as $f+g$ still takes on a variety of values, while $A \vdash B$ I think has a fixed value of either true or false once we pick $A$ and $B$.

David Egolf (Apr 01 2023 at 14:32):

John Baez said:

If you read the linked article on first-order logic you'll learn about technical terms like 'variables', 'functions', 'terms', 'predicates', 'formulas', and so on.

Thanks for linking that article. I'll take a look and hopefully it will help make this all a bit clearer.

David Egolf (Apr 01 2023 at 14:36):

Todd Trimble said:

Since you may be learning all this stuff on your own, you'll need to get hold of a textbook. The late great Gian-Carlo Rota once upheld the Schaum's Outline Series of mathematical texts. These have hundreds and hundreds of worked problems and they will get you into a subject fast. And they are cheap; look for used copies online. The only way to learn how to do proofs is to do a ton of them, but at least by the looks of it, there are a lot of people here willing to help.

Thanks for mentioning the possible exercise on subsets (I may give it a spin in a bit!). And thanks for mentioning that series of texts! Solutions are incredibly helpful for self studying, so it is exciting to learn that there is a whole series of books that provide many worked problems! I'm amazed I didn't know about this series before.

I do find wikipedia articles like the one mentioned above to be helpful references, but usually after I've mostly learned a topic from elsewhere. So this is very helpful!

David Egolf (Apr 01 2023 at 15:05):

John Baez said:

In this setup, X and Y are variables, $\subseteq$ is a binary predicate, and $X \subseteq Y$ is a formula with 2 free variables, $X$ and $Y$.

Figuring out what a "predicate" is seems like a place to start. The wikipedia article says "A predicate takes an entity or entities in the domain of discourse and evaluates to true or false." However, further on, it says that "If P is an n-ary predicate symbol and $t_1, ..., t_n$ are terms then $P(t_1,...,t_n)$ is a formula." So, maybe predicates actually generate "formulas", not truth values. I'm unsure, though, if the term "predicate symbol" refers to predicates or to something different - like a variable $P$ that stands for an arbitrary unspecified predicate.

David Egolf (Apr 01 2023 at 15:14):

Looking at the book "Categorical Logic and Type Theory" by Jacobs, the author defines a category to organize predicates on a set. The objects are pairs $(I,X)$ of sets where $X \subseteq I$. Jacobs says "we consider $X$ as a predicate on a type $I$, and write $X(i)$ for $i \in X$ to emphasise that an element $i \in I$ may be understood as a free variable in $X$".

Although Jacobs is using the word "type" here, which I'm not sure I want to explore yet, this seems to suggest that a predicate distinguishes certain entities in a given context. (Possibly distinguishing entities that produce a true proposition when inserted into a statement with variables?) Beyond that, this description leaves me a bit confused when attempting to connect it to the above discussion on predicates referring to Wikipedia.

David Egolf (Apr 01 2023 at 15:16):

"Practical Foundations For Programming Languages" provides: "A judgment states that one or more abstract binding trees have a property or stand in some relation to one another. The property or relation itself is called a judgment form, and the judgment that an object or objects have that property or stand in that relation is said to be an instance of that judgment form. A judgment form is also called a predicate, and the objects constituting an instance are its subjects."
It seems here that a predicate (also called a "judgement form") describes some kind of property of or relation between "abstract binding trees", which I think are certain formal sentences that can include the introduction of variables. But this feels a bit vague!

David Egolf (Apr 01 2023 at 15:17):

Well, I feel a little bit like I'm swimming in a sea of different definitions with an unclear relationship to one another! And I don't feel like I understand any one of the definitions... It's possible that starting by trying to understand what "predicate" means isn't a fruitful approach. Perhaps I need to understand some simpler concepts first to better understand these descriptions provided by the above sources.

John Baez (Apr 01 2023 at 15:40):

Well, I feel a little bit like I'm swimming in a sea of different definitions with an unclear relationship to one another!

That's inevitable, because you're just beginning to learn logic - and in logic, like any other important subject, there are many different approaches, with different conventions. People have been working on logic at least since Aristotle, after all.

John Baez (Apr 01 2023 at 15:42):

So, instead of running around, reading a bit here and a bit there, and hoping that it all adds up to a coherent picture, it's probably better to get a really good textbook on first-order logic - something that doesn't cut any corners - and learn that approach. After you learn one approach you will be able to see how other approaches, which often different in only minor ways, map on to the approach you know.

John Baez (Apr 01 2023 at 15:45):

But other approaches are more dramatically different. Trying to read about modern categorical approaches like Categorical Logic and Type Theory at the same time as traditional approaches like in the Wikipedia article First-order logic sounds like a recipe for disaster to me.

John Baez (Apr 01 2023 at 15:47):

It's sort of like you're just starting to learn music theory and you're reading books on Indian ragas and classical counterpoint at the same time.

David Egolf (Apr 01 2023 at 15:48):

Picking one really good textbook sounds like a great approach to me! I'm all for avoiding disaster.. :upside_down:

Do you still recommend "Mathematical Introduction to Logic" by Enderton? I was also just now taking a look at a book by Carnap "Introduction to Symbolic Logic and its Applications".

John Baez (Apr 01 2023 at 16:00):

I recommend Enderton, which I know. I don't know Carnap's book, but as a philosopher he may be fun to read yet more confusing.

David Egolf (Apr 01 2023 at 16:12):

John Baez said:

I recommend Enderton, which I know. I don't know Carnap's book, but as a philosopher he may be fun to read yet more confusing.

Awesome, I will give Enderton a try!

John Baez (Apr 01 2023 at 16:30):

When I was in high school in Virginia I took some math courses at George Washington University in DC, and one was on logic. We used Mathematical Logic by Kleene. I just took at look at the book again, and I still think it's good.

John Baez (Apr 01 2023 at 16:30):

So I recommend that, but I've also looked at Enderton's book and that seems good too.

John Baez (Apr 01 2023 at 16:37):

David Egolf said:

Figuring out what a "predicate" is seems like a place to start.

Yes, and their treatment of predicates might be a good way to judge different books on classical first-order logic.

The Wikipedia article says "A predicate takes an entity or entities in the domain of discourse and evaluates to true or false."

That of course is just preliminary chat, sort of like when a piano player noodles around a bit before the actual tune. It's important throughout math, but especially in foundations of mathematics, to distinguish between chat designed to give you the rough feel of a concept, and the actual serious stuff.

Since this article hadn't already rigorously defined "entity", "domain of discourse", "true", or "false", this can be nothing but chat. Don't take it too seriously.

However, further on, it says that "If P is an n-ary predicate symbol and $t_1, ..., t_n$ are terms then $P(t_1,...,t_n)$ is a formula." So, maybe predicates actually generate "formulas", not truth values.

This is more like serious stuff. But I do recommend a textbook written by an licensed logician, rather than a Wikipedia article written by a team of random people. The former is more likely to present a single well-thought-out framework.

John Baez (Apr 01 2023 at 16:39):

I'm unsure, though, if the term "predicate symbol" refers to predicates or to something different - like a variable $P$ that stands for an arbitrary unspecified predicate.

Here's some preliminary chat that may help:

In traditional mathematical logic we often start out with syntax - symbols written on the page. So, in first-order logic a predicate is an actual letter like this:

$P$

John Baez (Apr 01 2023 at 16:40):

We can call it a "predicate symbol" if we want to thump our fist on the table and get you to stop asking what it "means" - it's just a symbol.

John Baez (Apr 01 2023 at 16:42):

In first-order logic we tend to assume we have a countably infinite list of 1-ary predicates at our disposal, maybe

$A, A', A'', A''', \dots$

and then a countably infinite list of 2-ary predicates, maybe

$B, B', B'', B''', \dots$

and so on for 3-ary and 4-ary etc. forever. It doesn't really matter what they're called as long as we're completely clear about our choice!

John Baez (Apr 01 2023 at 16:45):

So those are predicates, and then comes the question of what you're allowed to do with them... I will let a textbook explain that, but you've probably already seen that we have a countably infinite list of 'variables', say

$x, x', x'', x''', \dots$

and if we have a 5-ary predicate $E'''$ we're allowed to write an expression involving it and 5 variables, like

$E'''(x'',x'',x''''',x',x)$

John Baez (Apr 01 2023 at 16:48):

So for example when I wrote something above like

$X \subseteq X'$

in the setup I'm talking about now, the symbol $\subseteq$ is really short for some 2-ary predicate, maybe $B'''''$ for all I know, and $X$ and $Y$ are 2 variables: maybe a fun shorthand for $x$ and $x'$. If so, the above expression $X \subseteq Y$ is just a user-friendly way of writing

$B'''''(x,x')$

John Baez (Apr 01 2023 at 16:50):

This sort of thing $B'''''(x,x')$ is an example of a 'formula', but there are many other ways to build up formulas, like

$A(x'''') \vee (B(x,x') \implies B'(x',x))$

John Baez (Apr 01 2023 at 16:51):

I'm just telling you a bit of a story that goes on for pages; when it's done you know what a 'sentence' is, and what's a 'proof' of a sentence from a list of sentences called 'axioms'.

John Baez (Apr 01 2023 at 16:52):

This is handy to know, because if you ask traditional mathematicians what they're doing when they're writing a proof in English, they will often say they're writing some stuff that could in principle be translated into a proof in first-order logic.

John Baez (Apr 01 2023 at 16:53):

Whether they could actually do it is open to question, and whether they even should be able to do it is also controversial. But anyway, that's a common attitude, so it's good to know what the game actually is, here.

John Baez (Apr 01 2023 at 16:54):

Since this is a category theory discussion forum, some people must be thinking it's weird that I'm urging you to learn this 'traditional' approach to logic, called first-order logic, and in particular classical first-order logic.

John Baez (Apr 01 2023 at 16:55):

It's sort of like I'm telling you to learn common practice harmony from a textbook that treats Bach as an exemplar, when the cool kids are all playing jazz.... or creating electropop on their digital audio workstations using MIDI.

John Baez (Apr 01 2023 at 16:57):

But since you and especially @Jacob Zelko are wanting to learn a lot of math, much of it written by 'traditional' mathematicians rather than category theorists, I think it's good to understand the approach to logic that implicitly underlies their writing - even if they only nod to it without deeply understanding it.

John Baez (Apr 01 2023 at 16:59):

It may not be worth getting too deep into classical first-order logic, but I'm really glad that I did early on. It's not very complicaed, and after I learned it I knew one carefully designed formal setup that was precise enough to program into a computer (if I wanted to, but I didn't) and also expressive enough to handle most of the math I ran into.

John Baez (Apr 01 2023 at 17:00):

These days there are slicker approaches - but folks like Whitehead and Hilbert and Goedel and von Neumann and lots of logicians even now use classical first-order logic.

David Egolf (Apr 01 2023 at 17:34):

Thanks for writing that all out! It is interesting and helpful!

Nathanael Arkor (Apr 01 2023 at 20:49):

John Baez said:

But since you and especially Nathanael Arkor are wanting to learn a lot of math, much of it written by 'traditional' mathematicians rather than category theorists, I think it's good to understand the approach to logic that implicitly underlies their writing - even if they only nod to it without deeply understanding it.

I think perhaps you meant to tag someone else (though I certainly have much to learn mathematically :grinning_face_with_smiling_eyes:).

John Baez (Apr 01 2023 at 21:05):

Ulp. I'm terrible at names, which is why I named my kids $x, y$ and $z$.

John Baez (Apr 01 2023 at 21:06):

I meant @Jacob Zelko. Almost the same thing, right? Zelko, Arkor? :blushing:

Jacob Zelko (Apr 01 2023 at 21:09):

Hehe, thanks for the ping and yea! Both have 5 letters, share an "o" and and "k", and are great sounding! :wink: Thanks for looping me back into the conversation -- will get caught up here!

John Baez (Apr 01 2023 at 21:10):

You two should team up - you could cover mathematics from A to Z!