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: logic

Topic: for all x implies exists x?

John Baez (Jan 14 2021 at 16:56):

One rule that some logicians use, which I hate, is

$\forall x P(x) \implies \exists x P(x)$

John Baez (Jan 14 2021 at 16:58):

This rules out empty models of your theory, and thus often kills off the possibility of having an initial object in the category of models.

More fundamentally, it's not something you can prove using ideas about quantifiers as adjoints.

Morgan Rogers (he/him) (Jan 14 2021 at 17:01):

Sounds like a classic case of forgetting about the empty set :sad:

Fawzi Hreiki (Jan 14 2021 at 17:02):

You might want to take a look at this introduction.

Fawzi Hreiki (Jan 14 2021 at 17:03):

On the second page this exact problem is mentioned

Fawzi Hreiki (Jan 14 2021 at 17:04):

The problem is that most people interpret 'is' as a monomorphism when in fact that need not be the case.

John Baez (Jan 14 2021 at 17:04):

I've often wondered about the history of this. I just learned that Abū Naṣr al-Fārābī (Iraq, c. 870–c. 950) noticed this issue when explaining Aristotle's syllogisms. Aristotle's syllogisms have funny names like "Barbara", and it turns out "Darapti" is a bad one:

All squares are rectangles.
All squares are rhombuses.
∴ Some rhombuses are rectangles.

According to the Stanford Encyclopedia of Philosophy:

Aristotle’s justification of Darapti relies on the conversion implication: from “Every B is an A” infer “Some A is a B” (cf. [Syllogism] 30.3). This implication fails to hold if we allow “Every B is an A” to be true when there are no Bs. Accordingly al-Fārābī declares that “Every B is an A” is false unless there is at least one B ([Categories] 124.14). Though he sometimes seems to forget he said this, he is the earliest logician on record as having spelled out this implication of “Every B is an A”.

So Al-Farabi at least made it explicit that he was ruling out the empty set, though I don't like this solution to the problem!

Oscar Cunningham (Jan 14 2021 at 17:06):

I've heard logicians say that this simplifies the statement of some theorems, but I've never actually seen an example.

John Baez (Jan 14 2021 at 17:16):

Thanks for that reference to Lawvere, @Fawzi Hreiki. I seem to remember some place where Lawvere complained at great length about the "banishment" of empty models.

John Baez (Jan 14 2021 at 17:21):

I think logicians are still fighting about this issue, but I think $\forall x P(x) \Rightarrow \exist x P(x)$ is losing the fight.

In

• Harry Gensler, Introduction to Logic, 2nd edition, 2010, page 32.

there's a nice simple explanation of why Aristotle's approach is not so good.

Historically, “Aristotelian” and “modern” logicians disagree about the validity of some syllogism forms. They disagree because of differing policies about allowing empty terms (general terms that don’t refer to any existing beings).

Compare these two arguments:

• All cats are animals. Therefore : Some animals are cats.

• All unicorns are animals. Therefore : Some animals are unicorns.

The first seems valid while the second seems invalid. Yet both have the same form [...]. What’s going on here?

When we read the first argument, we tend to presuppose that there’s at least one cat. Given this as an assumed additional premise, it follows validly that some animals are cats. When we read the second argument, we don’t assume that there’s at least one unicorn. Without this additional assumption, it doesn’t follow that some animals are unicorns.

The Aristotelian view, which assumes that each general term in a syllogism refers to at least one existing being, calls the argument “valid.” The modern view, which allows empty terms like “unicorn” that don’t refer to existing beings, calls the argument “invalid.”

Consider this pair of arguments with the same form (a form that’s valid on the Aristotelian view but invalid on the modern view):

• All cats are mammals. All cats are furry. Therefore : Some mammals are furry.

• All square circles are squares. All square circles are circles. Therefore : Some squares are circles.

The first inference is sensible, because there are cats. The second inference isn’t sensible, because there are no square circles. Some logic books use the Aristotelian view, but most use the modern view. It makes a difference in very few cases.

John Baez (Jan 14 2021 at 17:27):

Of course "it makes a difference in very few cases" is not the sort of excuse that should satisfy a logician.

Fawzi Hreiki (Jan 14 2021 at 17:40):

I would think that elegance and continuity with the rest of mathematics should matter. The analogy between propositions in a context and bundles over a space is quite nice and in the bundle case there is no analogous map from the section space to the total space.

Fawzi Hreiki (Jan 14 2021 at 17:40):

Since for example there may be a bundle with nonempty total space but with no global sections.

John Baez (Jan 14 2021 at 17:44):

Traditional logicians are not very concerned with getting their ideas to nicely match ideas about "bundles" and "sections" - most of them don't know what a bundle is, and if you told them, they'd say "but that's not logic".

John Baez (Jan 14 2021 at 17:45):

However, I agree with you, Fawzi. Our ideas of logic should connect nicely to our ideas involving the concept of space. So, I think the insights of Lawvere are fundamental.

John Baez (Jan 14 2021 at 17:50):

I'm mainly interested in the history of $\forall x P(x) \implies \exists x P(x)$ because it's part of the long slow history of our acceptance of the number 0, the empty set, and things like that.

It's very slow; for example topologists still argue about whether the empty set is a connected topological space (which is analogous to the question of whether 1 is prime).

John Baez (Jan 14 2021 at 17:51):

Puzzle 1. How many partitions does the empty set have?

Fawzi Hreiki (Jan 14 2021 at 17:54):

One

John Baez (Jan 14 2021 at 17:55):

Maybe you can correct the comment in reply to this question:

https://math.stackexchange.com/questions/3383713/what-is-the-partition-of-an-empty-set

John Baez (Jan 14 2021 at 17:55):

Puzzle 2. How many open covers does the empty topological space have?

Oscar Cunningham (Jan 14 2021 at 17:58):

Two or infinitely many, depending on whether you allow the same set to appear more than once in an open cover. I say you do.

Fawzi Hreiki (Jan 14 2021 at 18:00):

Just one open cover, namely $\{\empty\}$.

John Baez (Jan 14 2021 at 18:03):

Okay, so the answer is either 1, 2, or $\infty$. That narrows it down. :upside_down:

Fawzi Hreiki (Jan 14 2021 at 18:04):

An open cover is a family of open sets. So the empty set itself is not an open cover with this definition.

John Baez (Jan 14 2021 at 18:04):

So you're claiming the empty set is not a family of open sets?

Fawzi Hreiki (Jan 14 2021 at 18:04):

Ah you're right actually. Caught me out

John Baez (Jan 14 2021 at 18:05):

:upside_down: The empty set is a tricky thing!

Fawzi Hreiki (Jan 14 2021 at 18:06):

Yeah so Oscar was right. I guess the infinity option is just if we define families as indexed open sets in which case we can repeat the same open set in the family.

Oscar Cunningham (Jan 14 2021 at 18:31):

John Baez said:

Maybe you can correct the comment in reply to this question:

https://math.stackexchange.com/questions/3383713/what-is-the-partition-of-an-empty-set

The definition given there is

Let $I$ be a bounded interval. A partition of $I$ is a finite set $P$ of bounded intervals contained in $I$, such that every $x$ in $I$ lies in exactly one of the bounded intervals $J$ in $P$.

I think with that exact definition we either say that the empty set is a 'bounded interval' in which case it does have two partitions, or it isn't in which case the definition of partition doesn't apply to it. But this isn't how I would define 'partition'.

John Baez (Jan 14 2021 at 19:41):

Okay. I didn't even notice that they were talking about partitions of bounded intervals.

Todd Trimble (Jan 14 2021 at 20:09):

I only spent a few seconds skimming this. But it seems patently stupid to me to have $\forall_x\; P(x) \Rightarrow \exists_x\; P(x)$. To even speak of quantifying, you have to have a domain or type you're quantifying over. Suppose the domain is the set of odd perfect numbers (and make up something for $P(x)$, like $x >100$). Where does that put you at, Jack?

John Baez (Jan 14 2021 at 21:00):

I don't think Aristotle was patently stupid.

John Baez (Jan 14 2021 at 21:02):

He probably just wasn't thinking about empty domains.

John Baez (Jan 14 2021 at 21:04):

So, I posted this because I just learned that around 900 AD al-Fārābī noticed that Aristotle's reasoning implicitly assumed a nonempty domain. I never knew before who spotted this.

John Baez (Jan 14 2021 at 21:04):

More recent authors who still haven't caught on may indeed be patently stupid.

Eric Forgy (Jan 14 2021 at 21:05):

John Baez said:

I don't think Aristotle was patently stupid.

Quote of the day :blush:

Todd Trimble (Jan 14 2021 at 21:22):

Yeah, but I didn't say "was stupid". It is certainly stupid today, after all we've learned.

And to be clear, it's merely something that would be stupid to subscribe to, today -- not that particular people are "stupid". People are teachable, once a really simple example is shoved in their faces.

Crucially in the example I gave, we don't know the domain is empty. The fact it might be is all we need to reject this as a principle of logic.

John Baez (Jan 14 2021 at 21:24):

Okay, Todd, I wasn't really accusing you of beating up on Aristotle. A lot of people do.... blaming a guy who died in 322 BC for all the mistakes later people didn't catch.

Todd Trimble (Jan 14 2021 at 21:26):

I've never studied Aristotle in the first place. My rough history is that quantification took quite some time to get ironed out -- maybe with Frege. Or Peirce.

John Baez (Jan 14 2021 at 21:31):

To beat Aristotle on his own ground, I think it's good to go after his syllogism of the form "Darapti" - I just cottoned on to this.

It goes like this:

All squares are rectangles.
All squares are rhombuses.
∴ Some rhombuses are rectangles.

but equally well you could have

All even primes > 2 are composite numbers.
All even primes > 2 are prime.
∴ Some composite numbers are prime.

and he could have caught this... but I guess he just didn't think of saying a silly sentence like "all even primes > 2 are composite numbers", i.e. there was an implicit premise of existence when he said "for all".

John Baez (Jan 14 2021 at 21:34):

Wikipedia says:

It is claimed Aristotle's logic system does not cover cases where there are no instances. Aristotle's goal was to develop "a companion-logic for science. He relegates fictions, such as mermaids and unicorns, to the realms of poetry and literature. In his mind, they exist outside the ambit of science. This is why he leaves no room for such non-existent entities in his logic. This is a thoughtful choice, not an inadvertent omission. Technically, Aristotelian science is a search for definitions, where a definition is 'a phrase signifying a thing's essence.'... Because non-existent entities cannot be anything, they do not, in Aristotle's mind, possess an essence... This is why he leaves no place for fictional entities like goat-stags (or unicorns)" [Louis Groarke]. However, many logic systems developed since do consider the case where there may be no instances.

However, medieval logicians were aware of the problem of existential import and maintained that negative propositions do not carry existential import, and that positive propositions with subjects that do not supposit are false.

Fawzi Hreiki (Jan 14 2021 at 21:35):

Is there any modern mathematical logic book which has this rule as one of the deduction rules?

John Baez (Jan 14 2021 at 21:42):

I don't know - I hope no mathematical logic book would use this rule, but it would be interesting to see who still uses this rule.

John Baez (Jan 14 2021 at 21:43):

Here's a webpage on the subject, that doesn't completely answer your question:

• Existential import

A proposition is said to have existential import if the truth of the proposition requires a belief in the existence of members of the subject class. I and O propositions have existential import; they assert that the classes designated by their subject terms are not empty. But in Aristotelian logic, I and O propositions follow validly from A and E propositions by sub-alternation. As a result, Aristotelian logic requires A and E propositions to have existential import, because a proposition with existential import cannot be derived from a proposition without existential import. Thus, for Aristotle, if we believe it is that "All unicorns have one horn" then we are committed to believing that unicorns exist. For the modern logician or mathematician, this is an unacceptable result because modern mathematics and logic often deal with empty or null sets or with imaginary objects. A modern mathematician might, for example, wish to make a true claim about all irrational prime numbers. Since there are no irrational prime numbers, Aristotle would say that any claim about them is necessarily false.

George Boole developed an interpretation of categorical propositions solves the dilemma by denying that universal propositions have existential import. Modern logic accepts the Boolean interpretation of categorical propositions.

John Baez (Jan 14 2021 at 21:43):

The page goes on further, long enough to suggest someone still cares about this.

John Baez (Jan 14 2021 at 21:43):

It's interesting to hear we can thank Boole for straightening this out!

Fawzi Hreiki (Jan 14 2021 at 21:48):

There's a nice SEP article on 'the algebra of logic tradition' although unfortunately it stops short of category theory. It seems that Boole was the first to really try and understand the semantics behind the symbols.

Todd Trimble (Jan 14 2021 at 21:54):

I started teaching again in January 2019, and for the fall semester that year I was the instructor for the Proofs course. In the spring, two senior department members came to my office and recommended using the book How to Think Like a Mathematician by Kevin Houston. So I wound up using it (which I would not do again, by the way, although I thought some of his advice was good). I do remember that one of his exercises was exactly whether this implication holds, and I always wondered what he thought the answer was.

I would almost bet money that you could find last-century textbooks that have this principle (I have a vague memory of seeing one, but I wouldn't be able to cough up a title).

Cool about Boole!

James Wood (Jan 14 2021 at 22:11):

If your first order logic exists primarily because you're going to build a material set theory on top of it, then there's only one sort you ever formally quantify over (the universe of sets), and it's not empty. That's the pragmatic modern motivation I can come up with: basically, you don't really want to be doing logic, so you don't care about models, or indeed proofs.

James Wood (Jan 14 2021 at 22:15):

From this point of view, it's only strange pedagogically that quantification over the universe and quantification over a general set obey different laws.

Morgan Rogers (he/him) (Jan 14 2021 at 22:52):

Fawzi Hreiki said:

Yeah so Oscar was right. I guess the infinity option is just if we define families as indexed open sets in which case we can repeat the same open set in the family.

But just as partitions involve non-empty subsets, so should open covers, no? Since the motivation is to consider connectedness, it's only covers by non-trivial opens that matter. At which point there are no inhabited open covers of the initial topological space, so $\emptyset$ is the only option.

Morgan Rogers (he/him) (Jan 14 2021 at 22:58):

Oscar Cunningham said:

John Baez said:

Maybe you can correct the comment in reply to this question:

https://math.stackexchange.com/questions/3383713/what-is-the-partition-of-an-empty-set

The definition given there is

Let $I$ be a bounded interval. A partition of $I$ is a finite set $P$ of bounded intervals contained in $I$, such that every $x$ in $I$ lies in exactly one of the bounded intervals $J$ in $P$.

I think with that exact definition we either say that the empty set is a 'bounded interval' in which case it does have two partitions, or it isn't in which case the definition of partition doesn't apply to it. But this isn't how I would define 'partition'.

I'm going to write this up as an answer there if you don't mind. :wink:

Martti Karvonen (Jan 15 2021 at 00:20):

John Baez said:

I don't know - I hope no mathematical logic book would use this rule, but it would be interesting to see who still uses this rule.

I believe this rule is still relatively standard in textbooks in mathematical logic. For instance, both van Dalen's logic and structure (which I'm currently using to teach an intro to mathematical logic, as it's the book they've usually used here) and wikipedia (see e.g. https://en.wikipedia.org/wiki/First-order_logic#Semantics and https://en.wikipedia.org/wiki/First-order_logic#Empty_domains ) seem to require structures to be non-empty by definition. Given that they then prove the completeness theorem, the rule $\forall x P(x)\to\exists x P(x)$ needs to be deducible as it is valid for all structures (in this restricted sense).

Martti Karvonen (Jan 15 2021 at 00:36):

In fact, I'm tempted to pose the opposite challenge (and happy to lose it): find a modern introductory/intermediate textbook on classical mathematical logic that doesn't have this convention and is happy to call their system FOL instead of explicitly calling it with an alternative title like "free logic" or "inclusive logic".

Todd Trimble (Jan 15 2021 at 00:58):

It seems to me the debate is a pretty good advertisement for a typing discipline, where entailment comes equipped with an explicit declaration of which variables are free in a sequent judgment. This point was pretty well explained by Lambek in a BAMS review, and I think it saves the day for the completeness theorem.

As in the example I gave before, it's sometimes not at all clear whether a definable structure is empty or not. So this sort of exception-barring (in the sense of Lakatos) is highly problematic.

Martti Karvonen (Jan 15 2021 at 01:59):

I agree, I'm just making the empirical/sociological claim that logicians of a non-categorical bent tend to exclude empty structures and then wanting the completeness theorem commits them to $\forall x P(x)\to\exists x P(x)$.

Martti Karvonen (Jan 15 2021 at 02:05):

Ok I missed Gensler's book above. Anyway, van Dalen still excludes empty structures in the 2013, and it's not obvious to me that most recent books for a similar target audience do differently, so the switch in conventions (to allow empty domains) is not yet complete.

John Baez (Jan 15 2021 at 02:05):

Martti Karvonen said:

John Baez said:

I don't know - I hope no mathematical logic book would use this rule, but it would be interesting to see who still uses this rule.

I believe this rule is still relatively standard in textbooks in mathematical logic. For instance, both van Dalen's logic and structure (which I'm currently using to teach an intro to mathematical logic, as it's the book they've usually used here) and wikipedia (see e.g. https://en.wikipedia.org/wiki/First-order_logic#Semantics and https://en.wikipedia.org/wiki/First-order_logic#Empty_domains ) seem to require structures to be non-empty by definition. Given that they then prove the completeness theorem, the rule $\forall x P(x)\to\exists x P(x)$ needs to be deducible as it is valid for all structures (in this restricted sense).

Interesting! By the way, that's a clever use of a fancy theorem to deduce what the axioms must be.

Martti Karvonen (Jan 15 2021 at 02:09):

One can still have a completeness theorem when empty models are allowed, you just need to change the rules. So I guess it mostly boils down to logicians not caring about the empty model and having it around making some stuff a bit harder to do (truth defs with an assignment function for variables, prenex normal forms).

John Baez (Jan 15 2021 at 02:11):

But I'd hope that van Dalen's logic actually states the axioms of first-order logic that they're using.

John Baez (Jan 15 2021 at 02:17):

It turns out Wikipedia has a whole article on this:

• Empty domain.

Logics whose theorems are valid in every, including the empty, domain were first considered by Jaskowski 1934, Mostowski 1951, Hailperin 1953, Quine 1954, Leonard 1956, and Hintikka 1959. While Quine called such logics "inclusive" logic they are now referred to as free logic.

And the link goes to an even longer article on this issue.

John Baez (Jan 15 2021 at 02:20):

The latter article makes it sound like axioms that rule out the empty model are still the norm!

In classical logic there are theorems that clearly presuppose that there is something in the domain of discourse. Consider the following classically valid theorems.

1. $\forall xA \Rightarrow \exists xA$
2. $\forall x \forall rA(x) \Rightarrow \forall rA(r)$
3. $\forall rA(r) \Rightarrow \exists xA(x)$

Martti Karvonen (Jan 15 2021 at 03:31):

John Baez said:

But I'd hope that van Dalen's logic actually states the axioms of first-order logic that they're using.

Yeah on the semantics side the domain of discourse of a model is explicitly declared to be non-empty, and on the syntax/deduction side elim rule for $\forall$ and the intro rule for $\exists$ lets you derive $\exists x\varphi(x)$ from $\forall x\varphi(x)$.

Martti Karvonen (Jan 15 2021 at 03:32):

John Baez said:

The latter article makes it sound like axioms that rule out the empty model are still the norm!

I suspect they are.

John Baez (Jan 15 2021 at 04:31):

Martti Karvonen said:

Yeah on the semantics side the domain of discourse of a model is explicitly declared to be non-empty, and on the syntax/deduction side elim rule for $\forall$ and the intro rule for $\exists$ lets you derive $\exists x\varphi(x)$ from $\forall x\varphi(x)$.

Oh, I see. Yes, Wikipedia's description of the rules of the classical predicate calculus also lets you derive $\exists x\varphi(x)$ from $\forall x\varphi(x)$ that way.

So, everyone who learns logic from Wikipedia is going to believe

$\forall x\varphi(x) \implies \exists x\varphi(x)$

:cry:

John Baez (Jan 15 2021 at 04:35):

I suppose there are also people who believe

$\prod_{i=1}^n 0 = 0$

for all $n \ge 0$.

Todd Trimble (Jan 15 2021 at 05:16):

See however this post by Mike Shulman and the comment by Joel David Hamkins, where he expresses surprise that acceptance of empty structures as domains of discourse isn't by now standard.

Since it got no traction last time I pointed to it, I'll bring it more out into the open: this is Lambek explaining how the device of declaring free variables in sequent deductions circumvents the undesired consequence $\forall x P(x) \Rightarrow \exists x P(x)$: Screen-Shot-2021-01-14-at-11.42.22-PM.png Screen-Shot-2021-01-14-at-11.43.04-PM.png

Matteo Capucci (he/him) (Jan 15 2021 at 08:29):

John Baez said:

All squares are rectangles.
All squares are rhombuses.
∴ Some rhombuses are rectangles.

Well, this works because squares exist :)

Matteo Capucci (he/him) (Jan 15 2021 at 08:32):

John Baez said:

I suppose there are also people who believe

$\prod_{i=1}^n 0 = 0$

for all $n \ge 0$.

Sad...

Morgan Rogers (he/him) (Jan 15 2021 at 10:28):

John Baez said:

The latter article makes it sound like axioms that rule out the empty model are still the norm!

In classical logic there are theorems that clearly presuppose that there is something in the domain of discourse. Consider the following classically valid theorems.

1. $\forall xA \Rightarrow \exists xA$
2. $\forall x \forall rA(x) \Rightarrow \forall rA(r)$
3. $\forall rA(r) \Rightarrow \exists xA(x)$
   

This becomes so much more problematic when we consider structures in categories (eg toposes) other than $\mathbf{Set}$, where there might be many non-trivial objects failing to have global elements, as we've discussed elsewhere in the "empty group" discussion.

Javier Prieto (Jan 15 2021 at 11:40):

John Baez said:

I suppose there are also people who believe

$\prod_{i=1}^n 0 = 0$

for all $n \ge 0$.

I think I believe that... what is $n$ supposed to be ranging over tho?

Morgan Rogers (he/him) (Jan 15 2021 at 11:44):

The non-negative integers

Javier Prieto (Jan 15 2021 at 12:13):

Ah, I see the catch now. I don' believe it anymore :laughter_tears:

Chris Barrett (Jan 15 2021 at 12:39):

Todd Trimble said:

I only spent a few seconds skimming this. But it seems patently stupid to me to have $\forall_x\; P(x) \Rightarrow \exists_x\; P(x)$. To even speak of quantifying, you have to have a domain or type you're quantifying over. Suppose the domain is the set of odd perfect numbers (and make up something for $P(x)$, like $x >100$). Where does that put you at, Jack?

I may be being a bit slow here.. but you can reason about domains which may or may not be empty within ordinary classical logic. Specifically for the example there, you can talk about that in ordinary Peano arithmetic, just setting up a predicate P(x) which says that x is an "odd perfect number". This is completely tangential to the issue of your underlying domain (i.e. the numbers themselves) being nonempty. However, I suspect I may be missing your point?

Chris Barrett (Jan 15 2021 at 12:43):

More generally, I mentioned this discussion to my logic/proof theory research group. The general consensus is: 1. yes, we accept this rule as natural; 2. no, we don't really care if the CT turns out nicer without it

Fawzi Hreiki (Jan 15 2021 at 13:06):

But then you can’t really deal with models in other categories since emptiness vs nonemptiness is not as clear cut

Fawzi Hreiki (Jan 15 2021 at 13:08):

To rule out models in all non-Boolean categories just for this ‘convenience’ seems to be throwing out the baby with the bathwater (when there isn’t even bathwater to begin with)

Fawzi Hreiki (Jan 15 2021 at 13:18):

Also, studying models in other categories actually sheds light on set-valued models.

By analogy, even if some number theorist is only interested in $\mathbb{Z}$-valued solutions to some equation, studying solutions in other related rings is helpful to this end.

Morgan Rogers (he/him) (Jan 15 2021 at 13:33):

Chris Barrett said:

Todd Trimble said:

I only spent a few seconds skimming this. But it seems patently stupid to me to have $\forall_x\; P(x) \Rightarrow \exists_x\; P(x)$. To even speak of quantifying, you have to have a domain or type you're quantifying over. Suppose the domain is the set of odd perfect numbers (and make up something for $P(x)$, like $x >100$). Where does that put you at, Jack?

I may be being a bit slow here.. but you can reason about domains which may or may not be empty within ordinary classical logic. Specifically for the example there, you can talk about that in ordinary Peano arithmetic, just setting up a predicate P(x) which says that x is an "odd perfect number". This is completely tangential to the issue of your underlying domain (i.e. the numbers themselves) being nonempty. However, I suspect I may be missing your point?

I believe Todd's point is that if we take $S = \{ n \in \mathbb{N} \mid n \text{ is odd and perfect } \}$ and take $P(x)$ to be the statement $x > 100$, then $\forall_{x \in S} P(x) \Rightarrow \exists_{x \in S} P(x)$ is enough to deduce that an odd perfect number exists, since any $x \in S$ certainly satisfies $P(x)$... and I don't think anyone would consider that a satisfactory proof of the existence of odd perfect numbers!

Todd Trimble (Jan 15 2021 at 13:34):

@Chris Barrett The assumption $\forall_{x: D} \; P(x)$ of the implication, where $D$ is the domain of odd perfect numbers, is provable and hence true. Does that mean we may infer the consequence $\exists_{x: D}\; P(x)$, i.e., that there exists an odd perfect number greater than $100$?

(Again, we simply don't know whether the domain is empty or not.)

Morgan Rogers (he/him) (Jan 15 2021 at 13:37):

One should be able to reason about mathematical objects from their formal definitions without having to provide a model (empty or otherwise) and hence verify the consistency of the definition beforehand.

Chris Barrett (Jan 15 2021 at 15:48):

Fawzi Hreiki said:

But then you can’t really deal with models in other categories since emptiness vs nonemptiness is not as clear cut

What models of FOL do you have in mind?

Chris Barrett (Jan 15 2021 at 16:08):

Todd Trimble said:

Chris Barrett The assumption $\forall_{x: D} \; P(x)$ of the implication, where $D$ is the domain of odd perfect numbers, is provable and hence true. Does that mean we may infer the consequence $\exists_{x: D}\; P(x)$, i.e., that there exists an odd perfect number greater than $100$?

(Again, we simply don't know whether the domain is empty or not.)

Forgive me for being obtuse. Suppose D is the set of odd perfect numbers. In your example, if D is empty, the proof isn't well-formed, if D is non-empty, the proof is valid. I'm still unsure why you'd want to allow D to be empty.

Morgan Rogers (he/him) said:

One should be able to reason about mathematical objects from their formal definitions without having to provide a model (empty or otherwise) and hence verify the consistency of the definition beforehand.

So you can reason about mathematical objects without having to provide a model (in the way I stated in my previous post). The model theory of FOL only comes into play if you're actually treating D as part of your model

Morgan Rogers (he/him) (Jan 15 2021 at 16:16):

Chris Barrett said:

In your example, if D is empty, the proof isn't well-formed, if D is non-empty, the proof is valid. I'm still unsure why you'd want to allow D to be empty.

Are you saying that whether or not a proof is well-formed can depend on something non-syntactic? Why would you build your logic that way?

John Baez (Jan 15 2021 at 16:18):

Yeah, I don't want the well-formedness of my proofs to depend on whether there exist odd perfect numbers - that would make it very painful, perhaps impossible, to check their well-formedness.

A good system of logic should have a decision procedure for the well-formedness of proofs. If we have to check that a set of natural numbers described by PA is empty or not then no decision procedure exist: that question is undecidable.

John Baez (Jan 15 2021 at 16:21):

Thanks for that material by Lambek, @Todd Trimble!

Todd Trimble (Jan 15 2021 at 16:31):

Morgan Rogers (he/him) said:

Chris Barrett said:

In your example, if D is empty, the proof isn't well-formed, if D is non-empty, the proof is valid. I'm still unsure why you'd want to allow D to be empty.

Are you saying that whether or not a proof is well-formed can depend on something non-syntactic? Why would you build your logic that way?

I'm not getting this either. Checking validity or "well-formedness" of a proof is a formal, syntactic matter which we can train computers to do. And all the proposition is saying is, "Let $x$ be an odd perfect number. Then $x > 100$." This is certainly something you can prove! It's completely ordinary mathematics, just like some theorem saying that something would have to be true about nontrivial zeta zeroes off the critical line.

Morgan Rogers (he/him) (Jan 15 2021 at 16:34):

Chris Barrett said:

Morgan Rogers (he/him) said:

One should be able to reason about mathematical objects from their formal definitions without having to provide a model (empty or otherwise) and hence verify the consistency of the definition beforehand.

So you can reason about mathematical objects without having to provide a model (in the way I stated in my previous post). The model theory of FOL only comes into play if you're actually treating D as part of your model

I guess we're talking across purposes here. If you've already decided that something only counts as a model if it contains at least one element, and the quantification $\forall_x$ is forced to refer to the full set of elements of any model, which makes sense for FOL, then $\forall_x P(x) \Rightarrow \exists_x P(x)$ will hold, since we avoid quantifying over anything potentially empty.

Morgan Rogers (he/him) (Jan 15 2021 at 16:38):

But my question then is... why?
Chris Barrett said:

1. yes, we accept this rule as natural; 2. no, we don't really care if the CT turns out nicer without it

What do you do in model theory if you don't care about the categories of models of the theories you're studying? (This is a genuine, sincere question; I am curious what kinds of questions you tackle in your research group!)

Chris Barrett (Jan 15 2021 at 16:43):

Morgan Rogers (he/him) said:

Chris Barrett said:

In your example, if D is empty, the proof isn't well-formed, if D is non-empty, the proof is valid. I'm still unsure why you'd want to allow D to be empty.

Are you saying that whether or not a proof is well-formed can depend on something non-syntactic? Why would you build your logic that way?

Excuse me. You're right to pick up on this, it was inaccurate phrasing on my part. Let my try to wriggle out of this. The problem isn't that the proof is syntactically not well-formed in the case D is empty. But rather that, in the case D is empty; well, the logic you're using was never meant to deal with this case. So the proof doesn't apply.

EDIT: I think @Morgan Rogers (he/him) addressed the point I was trying (and failing) to make. But at this point we are both just asking each other "why?". I can have a go at answering this later.

Chris Barrett (Jan 15 2021 at 16:49):

Morgan Rogers (he/him) said:

But my question then is... why?
Chris Barrett said:

1. yes, we accept this rule as natural; 2. no, we don't really care if the CT turns out nicer without it

What do you do in model theory if you don't care about the categories of models of the theories you're studying? (This is a genuine, sincere question; I am curious what kinds of questions you tackle in your research group!)

We don't really do model theory per se. We (or at least, I) mostly do structural proof theory; linear logic and its models, sequent calculus and natural deduction, curry-howard and the lambda calculus, cut elimination, a bit of CT, that kind of stuff. I honestly know very little model theory so it's very possible there's a motivation from that area that I just don't understand.

Morgan Rogers (he/him) (Jan 15 2021 at 16:56):

Chris Barrett said:

But at this point we are both just asking each other "why?". I can have a go at answering this later.

The CT reasons for this are easy. For example, take the empty theory, which is surely the simplest case you'd want FOL to handle. In a formalism with the axiom scheme $\forall_x P(x) \Rightarrow \exists_x P(x)$ built in, the category of models is the category of non-empty sets, which lacks not only an initial objects, but pullbacks and equalizers as a result. We gain a lot, categorically speaking, by just declaring the empty model to be valid. As @John Baez was saying earlier, it's another instance of granting 'zero' validity which makes the overall structure more tractable.
So we just want to know what convenience is gained by excluding it :wink: .

Morgan Rogers (he/him) (Jan 15 2021 at 16:59):

Chris Barrett said:

I honestly know very little model theory so it's very possible there's a motivation from that area that I just don't understand.

That's fine! Why do you and your team accept this rule as natural, though?

Todd Trimble (Jan 15 2021 at 22:59):

Chris Barrett said:

More generally, I mentioned this discussion to my logic/proof theory research group. The general consensus is: 1. yes, we accept this rule as natural; 2. no, we don't really care if the CT turns out nicer without it

This 2. makes me uncomfortable: it's as if suggesting category theory is referring to some outré or fancy-shmancy thing that need not concern us. To the contrary, CT is a powerful guide to what is natural, and that's what it was invented for.

I'd like to indicate how CT suggests the natural way forward in this particular topic. Out of sheer laziness, I had linked to some stuff written by Lambek, but now I'll stop being lazy and explain how it comes straight out of Lawvere's ideas about quantification as adjoints to "substitution". Lawvere invented hyperdoctrines to help give precise expression to this general idea, and they're a nice framework, but I can probably merely allude to that framework in what appears below.

Todd Trimble (Jan 15 2021 at 23:00):

So here's the deal. In a traditional sequent-based presentation of deductive systems, one has a pair of rules

$\forall_x P(x) \vdash P(x), \qquad P(x) \vdash \exists_x P(x)$

where the turnstyle $\vdash$ denotes logical entailment, and of course something like these rules occur in the categorical language as well (but let me come to that in a moment). By transitivity of entailment, we are apparently led to $\forall_x P(x) \vdash \exists_x P(x)$. So what could be the problem?

Todd Trimble (Jan 15 2021 at 23:00):

The problem is that the rules involves a tacit conventional shorthand which is brushing some details under the carpet. Let's back up a minute. A free variable $x$ in an expression $P(x)$ is attached to a type or domain $D$ where the variable is considered as taking values. In conventional language, we associate to an expression $P(x)$ a truth set of values $v$ in $D$ where $P(v)$ is true. The interpretation of $P(x) \vdash Q(x)$, where $P, Q$ share a free variable $x$, is that we have a corresponding inclusion between truth sets, both being subsets of $D$. In other words, if $P(v)$ is true for an element $v$ in $D$, then so is $Q(v)$.

Todd Trimble (Jan 15 2021 at 23:01):

Now, $\forall_x P(x)$ is a closed expression (i.e., is closed if $x$ is the only free variable of $P(x)$). What is its truth set? Well, for such a proposition with 0 free variables, we wouldn't normally refer to its truth set, but rather to its truth value. But we could think of it as a truth set, namely as a subset of a 1-element set $1$, where it's all of $1$ if true and the empty subset if false.

Todd Trimble (Jan 15 2021 at 23:01):

Armed with these understandings, we can come back and examine the sequent $\forall_x P(x) \vdash P(x)$. As it stands, this doesn't have a coherent interpretation! The truth set of the left side is a subset of $1$; the truth set of the right side is a subset of $D$. There's a mismatch. To speak of an entailment relation $P \vdash Q$ between formulae $P, Q$, we should insist that their truth sets be subsets of the same domain $D$, so that we can compare them. In other words, that the formulas $P$ and $Q$ be of the same type.

Todd Trimble (Jan 15 2021 at 23:02):

So what ought we have said instead of $\forall_x P(x) \vdash P(x)$? The main thing to say is that if we have a proposition $c$ of empty type $1$ (for example, if $c$ is a closed term), then we can "pull back" to a formula of the same type as $P(x)$, e.g., we can consider the expression $c \wedge [x = x]$. (At the truth set level, this corresponds to the set-theoretic pullback of a subset of $1$ along the unique function $D \to 1$.) Category theorists like to denote this pullback formula by something like $D^\ast c$. Anyway, we pull back the formula $\forall_x P(x)$ to $D^\ast \forall_x P(x)$, and this can now be compared with $P(x)$. Our rule becomes

$D^\ast \forall_x P(x) \vdash P(x)$

or, if we really wanted to be hygienic about it, we should just admit that quantification is always relative to some domain $D$, and declare that domain, instead of just leaving it implicit. Thus, we should rather write

$D^\ast \forall_{x: D} P(x) \vdash P(x) \qquad (1)$.

Todd Trimble (Jan 15 2021 at 23:02):

Category theorists will recognize here a counit of an adjunction. In the language of Lawvere, universal quantification along a domain $D$ is right adjoint to pulling back along $D \to 1$. In the semantic language of truth sets, letting $[P]$ denote the truth set of a formula $P$, this means we ought to have $[D^\ast c] \subseteq [P]$ if and only if $[c] \subseteq [\forall_{x: D} P(x)]$. If we want the syntactic language to match up, we ought to arrange our deductive system so that from a sequent $D^\ast c \vdash P(x)$ we can derive the sequent $c \vdash \forall_{x: D} P(x)$, and vice-versa. But that will follow from (1) above together with the unit of the adjunction

$c \vdash \forall_{x: D} D^\ast c$

(together with other very standard rules).

Todd Trimble (Jan 15 2021 at 23:02):

(Actually, Lawvere generalizes this considerably: it doesn't have to be a function $D \to 1$ with codomain $1$. In principle one could pull back a formula $Q$ of type $Y$ along any function $f: X \to Y$ (or a morphism in the domain of a hyperdoctrine) to get a formula $f^\ast Q$ of type $X$, and likewise there is a universal quantification operator $\forall_f$ taking a formula $P$ of type $X$ to a formula $\forall_f P$ of type $Y$, enjoying the same type of adjunction relationship as above. But now is not the time to go into the significance of this powerful generalization of Lawvere.)

Todd Trimble (Jan 15 2021 at 23:03):

The sequent $P(x) \vdash \exists_x P(x)$ (I ought to write $P(x) \vdash \exists_{x: D} P(x)$) undergoes a similar treatment. Here existential quantification is left adjoint to pulling back, and so we ought to write this sequent as

$P(x) \vdash D^\ast \exists_{x: D} P(x) \qquad (3)$

which is a unit for an adjunction $\exists_{x: D} \dashv D^\ast$ (where the categories involved are, at the semantic level, posets of truth sets and inclusions between them; at the syntactic level, posets of formulae of the same type partially ordered by provable/derivable entailment).

Todd Trimble (Jan 15 2021 at 23:03):

Composing (1) and (3), we get the "corrected" form of the sequent we are debating, which takes the form

$D^\ast \forall_{x: D} P(x) \vdash D^\ast \exists_{x: D} P(x)$

where now all the types match up correctly.

Todd Trimble (Jan 15 2021 at 23:04):

Now, it may be felt that the notation is a bit heavy at this point. It's clear at this point that some obeisance to a typing discipline is required to make sense of entailments, but that modulo that, mathematicians are accustomed to validating $\forall_{x: D} P(x) \vdash P(x)$ by mentally inserting some dummy free variables if need be to put the antecedent and succedent on the same footing. What's the expression the type theorists use? I think it's coercion: we subconsciously apply implicit coercions to get expressions to match and make sense.

Todd Trimble (Jan 15 2021 at 23:04):

But the main takeaway is not to conflate different contexts for entailments. The type discipline strongly suggests that we consider entailments in context, i.e., a separate entailment $\vdash_D$ for each domain $D$, writing for example $\forall_{x: D} P(x) \vdash_D P(x)$, or even just

$\forall_x P(x) \vdash_D P(x)$.

This is the device Lambek (and Scott) use, rather than smushing all the entailments together into a single symbol $\vdash$, which potentially conflates contexts and leads to confusion.

Todd Trimble (Jan 15 2021 at 23:05):

Thus, we can assert (modulo these coercions) that $\forall_x P(x) \vdash_D \exists_x P(x)$ is universally valid -- just so long as we're clear what that means exactly and where we are in context!

And we can write $\vdash_1$, entailment between truth values, simply as $\vdash$ if we want to.

Todd Trimble (Jan 15 2021 at 23:05):

So,

$\forall_{x: D} P(x) \vdash_D \exists_{x: D} P(x) \qquad (4)$

is universally valid. The entailment

$\forall_{x: D} P(x) \vdash \exists_{x: D} P(x) \qquad (5)$,

where $\vdash = \vdash_1$, is not universally valid.

Todd Trimble (Jan 15 2021 at 23:06):

But, if we can produce a term $a: 1 \to D$, then we can derive that last sequent by hitting (4) on both sides with the pullback operator $a^\ast$. In language closer to hyperdoctrines, we have a composite

$1 \stackrel{a}{\to} D \stackrel{!}{\to} 1$

which is the identity on $1$. Correspondingly, $a^\ast \circ D^\ast$, by which we really mean $a^\ast \circ !^\ast$, behaves as an identity pullback operator. Hence if we apply $a^\ast$ to both sides of the correctly written entailment

$D^\ast \forall_{x: D} P(x) \vdash_D D^\ast \exists_{x: D} P(x)$,

we get

$a^\ast D^\ast \forall_{x: D} P(x) \vdash_1 a^\ast D^\ast \exists_{x: D} P(x)$

which reduces to

$\forall_{x: D} P(x) \vdash_1 \exists_{x: D} P(x)$.

(That's if we have a term $a: 1 \to D$ to work with.) And all is well.

Todd Trimble (Jan 15 2021 at 23:06):

This, I am convinced, is the proper and principled way of looking at things, and completely explains what is going on. No exception-barring, just clean careful algebra.

Fabrizio Genovese (Jan 15 2021 at 23:29):

That was neat.

James Wood (Jan 15 2021 at 23:54):

Todd Trimble said:

So here's the deal. In a traditional sequent-based presentation of deductive systems, one has a pair of rules

$\forall_x P(x) \vdash P(x), \qquad P(x) \vdash \exists_x P(x)$

Where did the function symbols go?

Todd Trimble (Jan 16 2021 at 00:00):

James, I don't understand the question. What function symbols?

James Wood (Jan 16 2021 at 00:02):

Todd Trimble said:

The type discipline strongly suggests that we consider entailments in context, i.e., a separate entailment $\vdash_D$ for each domain $D$, writing for example $\forall_{x: D} P(x) \vdash_D P(x)$, or even just

$\forall_x P(x) \vdash_D P(x)$.

I suppose, if you're more syntactically minded, you'd go for some notation like $x : D; \forall_x P(x) \vdash P(x)$.

Todd Trimble (Jan 16 2021 at 00:05):

Sure, there are even more annotated and careful notations. But I was trying not to depart too far from the notation that had arisen in the discussion (or from the notation Lambek uses in the link I provided).

James Wood (Jan 16 2021 at 00:05):

Todd Trimble said:

James, I don't understand the question. What function symbols?

I mean, I'd normally expect a more general entailment $\forall_xP(x) \vdash P(t)$, where $t$ is some term made up of function symbols applied to whatever free term variables happen to be around. But maybe this comes from the substitution.

Todd Trimble (Jan 16 2021 at 00:06):

Please see the link to Lambek's thing to see the context I'm referring to. You're actually referring to something other than what I was talking about (what you wrote was correct -- it's just referring to something slightly different than what I had in mind).

Todd Trimble (Jan 16 2021 at 00:08):

I can show how that would be derived in the hyperdoctrine-y mechanism that I'm secretly alluding to, if that would be of interest. (Although maybe not right away.)

Todd Trimble (Jan 16 2021 at 00:27):

Well, I may as well describe it now. Let $t: 1 \to D$ be a term of type $D$ (formed say from function symbols, etc., in whatever theory one happens to be working in). Starting with the counit sequent

$D^\ast \forall_{x: D} P(x) \vdash_D P(x)$

one pulls back this sequent along $t$, i.e., one applies a preorder map $t^\ast: \textsf{Form}(D) \to \textsf{Form}(1)$ to both sides, to get

$t^\ast D^\ast \forall_{x: D} P(x) \vdash_1 t^\ast P(x)$.

Now we have $t^\ast P(x) \equiv P(t)$ (the pullback map is also called a substitution map: syntactically, it here involves substituting a term $t$ of type $D$ for a variable of type $D$). On the left side of the sequent, the composite $t^\ast D^\ast$ is the identity map, as explained at the end of my long series of posts. Thus we derive

$\forall_{x: D} P(x) \vdash_1 P(t)$

as you were saying.

Jason Erbele (Feb 26 2021 at 19:04):

John Baez said:

I don't know - I hope no mathematical logic book would use this rule, but it would be interesting to see who still uses this rule.

I came across the difference between Aristotelian logic and the logic of possibly non-existent things in a lower-division logic course in the philosophy department. Both logics were introduced and then compared/contrasted. Unfortunately, I do not recall what book we used 20 years ago.

Something else this thread reminds me of is the definition of $\mathbb{N}$: is the number 0 included or not? Every undergrad or intro text I have seen that defines $\mathbb N$ (a nonempty set of books, incidentally) will say that 0 is not a member of $\mathbb{N}$, and refers to the set that does include 0 as the "whole" numbers instead of the "natural" numbers. So this revolution is lagging behind even the revolution that rejects $\forall_x P(x) \implies \exists_x P(x)$ hold universally.

John Baez (Feb 26 2021 at 19:12):

Interesting!

How long will it take for people to understand nothing?

Mike Shulman (Feb 27 2021 at 02:39):

I've seen some more modern undergrad and intro texts that include 0 in $\mathbb{N}$, like Velleman's How to Prove it and Hamkins's Proof and the Art of Mathematics.