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: learning: questions

Topic: understanding "dual" statements

David Egolf (Dec 07 2023 at 19:10):

I'm trying to understand this idea: "If a statement $\Sigma$ is true for a partial order $P$, then the 'dual' of that statement $\Sigma^*$ is true in the dual partial order $P^*$. (For context, I'm reading "Introduction to lattices and order" by Davey and Priestley. I'm also referencing this webpage).

By the dual $P^*$ of a partial order $P$, I mean that $P^*$ and $P$ have the same elements, and $a \leq b$ in $P^*$ exactly if $b \leq a$ in $P$. By the dual of a statement, I mean the same statement where every occurrence of $\leq$ is replaced by $\geq$.

David Egolf (Dec 07 2023 at 19:10):

For example, assume that the following statement $\Sigma$ is true in $P$: "there is an element $a$ so that $a \leq b$ for all $b$". Then the dual statement $\Sigma^*$ I think is: "there is an element $a$ so that $a \geq b$ for all $b$." I think that $\Sigma^*$ is true in $P^*$. We know that $a \leq b$ for all $b$ in $P$. Thus $b \leq a$ for all $b$ in $P^*$. So this works out!

David Egolf (Dec 07 2023 at 19:12):

I would like to prove in general that if $\Sigma$ is true in $P$, then $\Sigma^*$ is true in $P^*$. But I don't know where to start! I feel like I don't even really know what a "statement" is, or exactly what it means for a statement $\Sigma$ to be "true for a partial order $P$".

Any thoughts are appreciated!

Todd Trimble (Dec 07 2023 at 19:18):

What you have is basically correct, but it should be added that if the statement includes operations on a partial order, such as $\wedge$ and $\vee$, then those have to be dualized as well. Let's talk about this.

Todd Trimble (Dec 07 2023 at 19:21):

So one very categorically minded definition of $\wedge$ is that it is the cartesian product in a poset. When you spell this out, it means:

$x \leq a \wedge b \qquad \text{iff} \qquad x \leq a\; \text{and}\; x \leq b$

(Note: this is a very "Yoneda-esque" description: it uniquely characterizes $a \wedge b$ in terms of "maps", i.e., instances of $\leq$, coming out of arbitrary objects/elements $x$.)

Todd Trimble (Dec 07 2023 at 19:24):

Similarly, or rather dually, the characterization of joins $\vee$ is:

$x \geq a \vee b \qquad \text{iff} \qquad x \geq a\; \text{and}\; x \geq b$

or (of course)

$a \vee b \leq x \qquad \text{iff} \qquad a \leq x\; \text{and}\; b \leq x.$

David Egolf (Dec 07 2023 at 19:25):

Thanks for pointing this out!

And I think I see that the first bijection you have provided is a particular component of the natural isomorphism which declares $a \land b$ to be a product: $\alpha:P(-, a \land b) \cong P(-, a) \times P(-,b)$. So, $\alpha_x: P(x, a \land b) \cong P(x,a) \times P(x,b)$

Todd Trimble (Dec 07 2023 at 19:26):

That's right.

So $\vee, \wedge$ can be expressed in the core language of posets, where they emerge as concepts dual to one another, and therefore when you dualize statements which involve them, you have to interchange them.

Todd Trimble (Dec 07 2023 at 19:32):

Now: the language of posets is (depending on terminological conventions) the collection of all first-order formulas that you can build up using any core relations of the theory (for posets, there's only one such predicate, which is $\leq$) and constants of the theory (there are no primitive constants for the language of posets per se, although for some extensions of the language, you might bring in constant symbols like $0$ (bottom) and $1$ (top), which by the way are dual to one another as well, being the initial/terminal elements), and finally any primitive operations (again, for the core language of posets, there are no primitive operations per se, but again, some extensions may include operations like $\vee$ and $\wedge$, and there may be others besides depending on the language extension).

Todd Trimble (Dec 07 2023 at 19:33):

So to make use of this, you have to understand "first-order formulas", but that's a recursive matter, much like algebraic expressions are built up recursively.

Todd Trimble (Dec 07 2023 at 19:33):

A "statement" is a first-order formula in which every variable is quantified, either universally or existentially.

Todd Trimble (Dec 07 2023 at 19:34):

Finally, to take the dual of a statement (in the core language), you reverse all instances of $\leq$ in your statement, but otherwise leave its logical structure unchanged.

Todd Trimble (Dec 07 2023 at 19:41):

Duality is an absolutely fundamental theme in category theory, and this was recognized from the very beginning by Eilenberg and Mac Lane: I think they might have mentioned the analogy with duality in projective geometry, or duality in the theory of Boolean algebras, but I don't remember for sure. Anyway, like the theory of posets, the theory of categories is "self-dual". In essence this means that if, in the core language which specifies function symbols $\text{dom}$ and $\text{cod}$, identity function symbols, and the composition symbol, the "dual" of a statement in this language is obtained by swapping $\text{dom}$ and $\text{cod}$, swapping instances of $f \circ g$ with $g \circ f$, and leaving everything else unchanged, then the dual of any theorem in the theory of categories is again a theorem. This is because the dual of an axiom in the theory of categories is again an axiom in this theory.

Todd Trimble (Dec 07 2023 at 19:43):

I think I will stop there for now.

David Egolf (Dec 07 2023 at 19:45):

Thanks, that is all quite helpful! That gives me a lot of things to look up and review. (I looked at "first-order formulas" a while ago, but I've forgotten most of the details! This gives me a good reason to review that.)

Todd Trimble said:

This is because the dual of an axiom in the theory of categories is again an axiom in this theory.

I bet an analogous statement is important for proving what I want to prove for partial orders!

Todd Trimble (Dec 07 2023 at 19:45):

Absolutely. The theory of posets is also self-dual (exercise!).

Todd Trimble (Dec 07 2023 at 19:51):

Some of this can be confusing at times. When we teach Boolean algebra, for example, and dualize a statement, the symbols $\wedge$ and $\vee$ which belong to the object language are interchanged, but not the words "and" and "or" in the meta-language that we use to talk about logical formulas in the theory!

Todd Trimble (Dec 07 2023 at 19:52):

Those meta-usages are unchanged in the process of dualizing.

David Egolf (Dec 07 2023 at 20:09):

Todd Trimble said:

Those meta-usages are unchanged in the process of dualizing.

That makes sense! I was just thinking about this, trying to imagine an inductive procedure to show that more and more statements stay true when dualized. We might first show that if $a$ is true in $P$ then $a^*$ is true in $P^*$, and if $b$ is true in $P$ then $b^*$ is true in $P^*$.

David Egolf (Dec 07 2023 at 20:09):

Then we might assume that "$a$ and $b$" is true in $P$ and ask if "$a^*$ and $b^*$" is true in $P^*$. Since "$a$ and $b$" is true, then $a$ is true and $b$ is true (all in $P$) therefore $a^*$ is true and $b^*$ is true (in $P^*$) and hence "$a^*$ and $b^*$" is true in $P^*$.

David Egolf (Dec 07 2023 at 20:11):

So the "and" didn't need to get changed as we moved from $P$ to $P^*$.

Todd Trimble (Dec 07 2023 at 20:25):

Yes, exactly.

Leopold Schlicht (Dec 07 2023 at 21:17):

Todd Trimble said:

A "statement" is a first-order formula

Why first-order?

Todd Trimble (Dec 07 2023 at 21:33):

Doesn't have to be, necessarily. But typical texts on logic often stop at this point, for a variety of reasons, so it's a useful stopgap that seems appropriate for this level of conversation. Did you want to say something more on this?

John Baez (Dec 07 2023 at 22:06):

@David Egolf wrote:

I would like to prove in general that if $\Sigma$ is true in $P$, then $\Sigma^*$ is true in $P^*$. But I don't know where to start! I feel like I don't even really know what a "statement" is, or exactly what it means for a statement $\Sigma$ to be "true for a partial order $P$".

There are lots of levels of generality for what we can take a "statement" to be, and the precise details of how we dualize a statement depends on what framework we use to define "statements".

John Baez (Dec 07 2023 at 22:08):

I was going to recommend starting with the approach of first-order logic, since this is a classic approach to working with "statements", but I see now that Todd Trimble beat me to it:

A "statement" is a first-order formula in which every variable is quantified, either universally or existentially.

John Baez (Dec 07 2023 at 22:09):

where "first-order formula" needs to be defined inductively. I'm actually glad Todd beat me to it, because it takes a fair amount of work.

John Baez (Dec 07 2023 at 22:14):

We could then move on to second-order logic, etcetera, but many of the classic results in logic (like Godel's completeness theorem, soundness, compactness, etc.) work nicely for first-order logic, so I think it's good to get comfy with first-order logic before moving on.

Leopold Schlicht (Dec 07 2023 at 22:36):

John Baez said:

We could then move on to second-order logic, etcetera, but many of the classic results in logic (like Godel's completeness theorem, soundness, compactness, etc.) work nicely for first-order logic

These results are completely unrelated to the duality principle under discussion.

John Baez (Dec 07 2023 at 22:37):

I know. I'm just trying to explain to David Egolf why it's good to learn first-order logic.

John Baez (Dec 07 2023 at 22:40):

Actually I think it's going too far to say anything in logic is completely unrelated to anything else: I feel confident that with a little work I could find a fun application of soundness or completeness to the first-order theory of posets, and how this theory is "self-dual".

But I was really just trying to get David more interested in logic.

Leopold Schlicht (Dec 07 2023 at 22:42):

Todd Trimble said:

Doesn't have to be, necessarily. But typical texts on logic often stop at this point, for a variety of reasons, so it's a useful stopgap that seems appropriate for this level of conversation. Did you want to say something more on this?

I just wondered why stop at first-order when discussing the duality principle David mentioned. Many properties of partial orders like "well-ordered" are higher-order.

John Baez (Dec 07 2023 at 22:43):

If you're teaching someone first-order logic, as Todd just did, maybe you'd want to wait a few days before explaining second-order logic.

David Egolf (Dec 07 2023 at 22:50):

John Baez said:

We could then move on to second-order logic, etcetera, but many of the classic results in logic (like Godel's completeness theorem, soundness, compactness, etc.) work nicely for first-order logic, so I think it's good to get comfy with first-order logic before moving on.

Yes, I hope to get a bit more comfortable with some first-order logic by thinking about the topic of this thread. I am hopeful that having a specific question I want to answer (as described above) will be helpful motivation!

David Egolf (Dec 07 2023 at 22:52):

One thing that I'm noticing right away is that we have two "layers" going on:

• we can form expressions "inside" a partial order, like $a \leq b$ or $a \land b$
• we can form expressions "one level up" like "$a \leq b$ and $c \leq d$"

David Egolf (Dec 07 2023 at 22:54):

Referencing the below definition of an alphabet of a first-order language, I am wondering if the "inside the poset" expressions need to be our variables. Or maybe instead our variables are the elements of the poset and we have a "relation symbol" $\leq$ in our first-order alphabet. Probably this second approach is simpler!

alphabet of a first-order language

Leopold Schlicht (Dec 07 2023 at 23:05):

David Egolf said:

I would like to prove in general that if $\Sigma$ is true in $P$, then $\Sigma^*$ is true in $P^*$. But I don't know where to start!

I don't think you will be able to formulate such a theorem in the first place! Here is a related MathOverflow question.

Leopold Schlicht (Dec 07 2023 at 23:19):

I wonder how people would use the duality principle in a proof assistant. Is that what "metaprogramming" is?

John Baez (Dec 07 2023 at 23:21):

David Egolf said:

One thing that I'm noticing right away is that we have two "layers" going on:

• we can form expressions "inside" a partial order, like $a \leq b$ or $a \land b$
• we can form expressions "one level up" like "$a \leq b$ and $c \leq d$"

This is because you're studying the theory of a poset using first-order logic, which has its own poset structure (called implication).

That's a bit more confusing than if you were studying, say, the theory of a group using first-order logic.

John Baez (Dec 07 2023 at 23:22):

If you were studying that, the concept you'd be studying would not be so similar to the framework you were studying it in.

But if you want to study duality, the theory of posets is a nice example. (The theory of projective planes also has a nice duality, of a rather different sort.)

John Baez (Dec 07 2023 at 23:25):

Leopold Schlicht said:

David Egolf said:

I would like to prove in general that if $\Sigma$ is true in $P$, then $\Sigma^*$ is true in $P^*$. But I don't know where to start!

I don't think you will be able to formulate such a theorem in the first place!

Of course he can formulate such a theorem. Todd Trimble began outlining how. There are many such theorems along these lines, but Todd is leading him to a nice simple one.

Leopold Schlicht (Dec 07 2023 at 23:32):

Note that David in his question didn't mention that the "statements" he is talking about are first-order. First-order sentences almost surely don't capture what he meant by "statement" (since, for instance, the duality principle should apply to the property of being well-ordered).

David Egolf (Dec 07 2023 at 23:40):

Leopold Schlicht said:

Note that David in his question didn't mention that the "statements" he is talking about are first-order. First-order sentences almost surely don't capture what he meant by "statement" (since, for instance, the duality principle should apply to the property of being well-ordered).

I'm happy to start with simpler statements, like first-order sentences! If I can understand how those behave with respect to "duality" maybe I can start thinking about more complex ones. But I appreciate you pointing out that more complex statements are important!

Leopold Schlicht (Dec 07 2023 at 23:52):

That's a nice exercise if you want to familiarize yourself with first-order logic! I didn't know that that's what you are interested in from reading your question.

However, if you are interested in making precise the duality principle you mentioned, I claim that no formal logic captures what you mean by "statement", though. So the only way I see to make the duality principle precise would be to investigate how such a situation is handled in a proof assistant.

Mike Shulman (Dec 08 2023 at 00:17):

If we're just talking about duality of a single poset (or category), then it seems to me that any sort of statement you like should be captured by saying there is an involution on the syntax of the theory "T + a poset", where T is whatever foundational theory of mathematics you like (ZFC, MLTT, HoTT, etc.), which intertwines with the duality construction on models of that theory. The MO question you linked to is about duality statements involving multiple categories and functors between them, which is somewhat more complicated, but is probably still captured by involutions of a theory like "T + a diagram of posets/categories, functors, and natural transformations between them".

Ralph Sarkis (Dec 08 2023 at 06:18):

I really like to rephrase statements about partial orders in the calculus of relations. It is a language without variables (which to me makes it feel more categorical), and it makes duality very easy to see (almost too trivial) because there is an converse operation changing $\leq$ into $\geq$. One caveat is that it is not as expressive as FO logic.

Ralph Sarkis (Dec 08 2023 at 06:18):

Here is a simple example (first in FO logic) (EDIT: ok I wrote these right after waking up and I didn't realize any poset is dense and reflexive so the properties are not that interesting...).
Def: We say a poset $(X,\leq)$ is dense if

$$\forall x. \forall y. x\leq y \implies \exists z. x\leq z \wedge z \leq y.$$

In words, you can always find an element between two others like inside the real or rational numbers ($\mathbb{Q}$ and $\R$ with the strict orders $<$ are dense).

Ralph Sarkis (Dec 08 2023 at 06:18):

Def: We say a poset $(X,\leq)$ is reflexive if

$$\forall x. x \leq x.$$

In words, every element is related to itself in the order.

Ralph Sarkis (Dec 08 2023 at 06:18):

Thm: If $(X,\leq)$ is reflexive, then it is dense.
Proof: For any $x \leq y \in X$, let $z =x$ (or $z = y)$ and by reflexivity, we have $x\leq z \leq y$.

Ralph Sarkis (Dec 08 2023 at 06:19):

Now the same example with the calculus of relations (I can go into the details of why these are equivalent formulations).
Def: We say that a poset $(X,\leq)$ is dense if ${\leq} \subseteq {\leq} ; {\leq}$.
Def: We say that a poset $(X,\leq)$ is reflexive if $\mathrm{id}_X \subseteq {\leq}$.
Proof of Thm: ${\leq} \subseteq \mathrm{id}_X ; {\leq} \subseteq {\leq};{\leq}$.

Morgan Rogers (he/him) (Dec 08 2023 at 09:27):

Leopold Schlicht said:

However, if you are interested in making precise the duality principle you mentioned, I claim that no formal logic captures what you mean by "statement", though. So the only way I see to make the duality principle precise would be to investigate how such a situation is handled in a proof assistant.

In order to formally discuss statements, you need to fix a language (you need to decide whether you allow joins and meets in your statements, say). Once you've made that choice, I would argue that you in fact can prove a duality meta-theorem by arguing by substitution into proofs. That is, let $\pi$ be a proof that $P$ satisfies $\Sigma$; then the proof $\pi^*$ obtained by substituting every formula by its syntactic dual is a proof that $P^*$ satisfies $\Sigma^*$. The only requirement here is that of invariance of deduction rules under dualization; you don't need to have decided in advance what your deduction rules are (i.e. which fragment of logic you're working in).

David Egolf (Dec 08 2023 at 18:46):

I've just learned about induction in the calculus of formulas for a first order language. I think this will be a helpful tool for proving that if $\Sigma$ is any formula in the first order language for a poset $P$, then $\Sigma^*$ is true in $P^*$ exactly when $\Sigma$ is true in $P$.

To do this, we first need to define what the formulas are for the poset $P$. To do that, we first define what terms are. And to define what terms are, we need to first define the alphabet for $P$. The alphabet for $P$ is a set of symbols containing exactly the following:

• the variables, which are exactly the elements of $P$
• these logical symbols: $\neg, \iff, \implies, \land, \lor$
• the equality symbol $\equiv$
• parentheses: $($ and $)$
• a 2-ary relation symbol $\leq$

David Egolf (Dec 08 2023 at 18:51):

The terms for the poset $P$ are exactly the variables of our alphabet, the elements of $P$.

The formulas for $P$ are exactly the strings obtained by finitely many applications of the following rules:

• If $a$ and $b$ are terms (elements of $P$) then $a \equiv b$ is a formula.
• If $a$ and $b$ are terms (elements of $P$) then $\leq a b$ is a formula. I will write this kind of formula more conveniently as $a \leq b$.

David Egolf (Dec 08 2023 at 18:51):

• If $s$ is a formula, then $\neg s$ is a formula
• If $s$ and $t$ are formulas, then $(s \land t)$, $(s \lor t)$, $(s \implies t)$, $(s \iff t)$ are also formulas
• If $s$ is a formula and $x$ is a variable (an element of $P$) then $\forall xs$ and $\exists xs$ are also formulas

Todd Trimble (Dec 08 2023 at 20:39):

I had begun writing a long response, but everything got screwed up because one of the comments was "too long" for this stupid zulip to handle -- and then everything got fouled up.

If I have the time and energy, then I'll reconstruct the series of messages. But maybe someone else would like to intervene (I hope so -- that would save me from having to do it all over again).

David Egolf (Dec 08 2023 at 20:51):

Todd Trimble said:

I had begun writing a long response, but everything got screwed up because one of the comments was "too long" for this stupid zulip to handle -- and then everything got fouled up.

If I have the time and energy, then I'll reconstruct the series of messages. But maybe someone else would like to intervene (I hope so -- that would save me from having to do it all over again).

I have been struggling a lot with this problem! I noticed that long messages tend to (thankfully) still get saved to "drafts", which might help in your case too, depending on what exactly went wrong.

Todd Trimble (Dec 08 2023 at 20:57):

No, there are no drafts of mine, alas.

John Baez (Dec 09 2023 at 11:22):

David Egolf said:

I've just learned about induction in the calculus of formulas for a first order language. I think this will be a helpful tool for proving that if $\Sigma$ is any formula in the first order language for a poset $P$, then $\Sigma^*$ is true in $P^*$ exactly when $\Sigma$ is true in $P$.

I agree with your main point here: since formulae are defined inductively, to prove a claim about all formulae it's very natural (and maybe even inevitable?) that you'll use induction.

John Baez (Dec 09 2023 at 11:23):

But I have a nitpick to point out:

Note that a formula can have free variables, while a statement is a formula with no free variables. It makes plenty of sense to say a statement is true in a poset $P$, but not that a formula is true in a poset $P$. Here's a formula:

$x \le y$

Is this true in the poset $(\mathbb{N}, \le)$? Is it false? Not really either. It does however define a function from $\mathbb{N}^2$ to truth values, sending each pair $(x,y) \in \mathbb{N}$ to the truth value of $x \le y$. Or in other words, it defines a binary relation on $\mathbb{N}$.

John Baez (Dec 09 2023 at 11:23):

So, instead of saying

if $\Sigma$ is any formula in the first order language for a poset $P$, then $\Sigma^*$ is true in $P^*$ exactly when $\Sigma$ is true in $P$.

it might be better to say it a bit differently.

Of course, it's possible you meant exactly what I'm trying to make explicit here! And in fact I don't even know the standard jargon for what I'm trying to say.

John Baez (Dec 09 2023 at 11:29):

But anyway, an induction over formulae should make it really easy to prove what you're trying to prove.

John Baez (Dec 09 2023 at 14:05):

So here's how I might rather clumsily state what you're trying to prove:

If $\Sigma$ is a formula with $n$ free variables in the first-order language of posets, for any poset $P$ it defines a subset $S(\Sigma, P) \subseteq P^n$, namely the set of $n$-tuples for which the formula holds. There is a "dual" formula $\Sigma^\ast$, defined inductively, and also a dual poset $P^\ast$ (usually called the opposite poset), and

$S(\Sigma^\ast, P^\ast) = S(\Sigma, P) \subseteq P^n$

where I'm using the fact that the underlying set of $P^\ast$ equals that of $P$.

Todd Trimble (Dec 09 2023 at 15:03):

Yesterday I had started a series of comments regarding the use of variables in logic, with some appropriate categorical glosses on the subject, because "variables, which are exactly the elements of $P$" (back here) had triggered me. But then Zulip punished me by carping about a too-long comment, and I couldn't put my comments back in order, and I gave up.

Todd Trimble (Dec 09 2023 at 15:04):

Variables, which are usually introduced to kids starting around middle school age, are usually explained not too well in that time period, and can cause a lot of puzzlement (in what sense does a letter "vary"?). In later courses before a more sophisticated audience, a certain amount of wind has to be expended on the syntax of free variables, bound variables, and so on. The notion of a truth set of a formula (which John denoted as $S(\Sigma, P)$), a semantic concept, becomes pretty important around this point.

Todd Trimble (Dec 09 2023 at 15:04):

For someone who likes category theory, I think one can get a lot of explanation-mileage by talking about the uses of free structures in mathematics and the role that so-called "variables" play there. At some point the yoga of "quantifiers as adjoints" also comes into play, rather beautifully.

John Baez (Dec 09 2023 at 15:42):

Yes, @Todd Trimble, I can easily imagine you getting lured into a quite precise account of how variables in first-order logic are connected to - but certainly not the same as! - elements in a specific model of a specific theory! Getting this right indeed requires "expending a certain amount of wind" - yet it's worthwhile, because it's part of the whole story about syntax versus semantics... a story that's key to understanding mathematical logic. There are old-fashioned versions of this story still worth hearing, and also modern versions that use category theory.

So it's a pity you were punished by Zulip, the goddess of brevity.

Mike Shulman (Dec 09 2023 at 16:11):

John Baez said:

Note that a formula can have free variables, while a statement is a formula with no free variables.

A formula can definitely have free variables, but I'm more used to the word "sentence" for a formula with no free variables. I'm not very familiar with "statement" being given a formal meaning at all, and the Internet didn't help me find examples. Do you have a reference?

John Baez (Dec 09 2023 at 16:17):

No, I just assumed that when @David Egolf said "statement" he meant "sentence", so I went along with his terminology.

John Baez (Dec 09 2023 at 16:19):

If by "statement" he meant "formula", then a lot of my comments were a bit off the mark. But he said stuff like "a statement is true in $P$", which made me think he was talking about a sentence being satisfied in some model of the theory of posets.

Todd Trimble (Dec 09 2023 at 17:19):

Some introductory textbooks use "statement" to mean a sentence (i.e., a grammatical form with nouns and verbs) that has a definite truth value (when interpreted in a model), and I've gotten used to that usage.

Mike Shulman (Dec 09 2023 at 20:00):

Ah, I think I've seen that before too.

David Egolf (Dec 10 2023 at 06:13):

John Baez said:

But I have a nitpick to point out:

Note that a formula can have free variables, while a statement is a formula with no free variables. It makes plenty of sense to say a statement is true in a poset $P$, but not that a formula is true in a poset $P$. Here's a formula:

$x \le y$

Is this true in the poset $(\mathbb{N}, \le)$? Is it false? Not really either. It does however define a subset of $\mathbb{N}^2$, the set of pairs $(x,y)$ for which $x \le y$.

Thanks for raising this point! Let me look back at what I said: "if $\Sigma$ is any formula in the first order language for a poset $P$, then $\Sigma^*$ is true in $P^*$ exactly when $\Sigma$ is true in $P$".

I think what I meant is this: if the formula $\Sigma$ has a truth value in the context of $P$, and that truth value is "true", then the formula $\Sigma^*$ also is assigned the truth value of "true" in the context of $P^*$. So I was trying to keep in mind the idea that some formulas don't necessarily have a truth value assigned to them.

David Egolf (Dec 10 2023 at 06:13):

On a related note, I haven't said how I'm assigning truth values to a formula. That seems like something important I should try to understand! Considering your example $x \leq y$, if $x$ and $y$ are both variables, that means that (by my definition above for the variables in the alphabet for $P$) both $x$ and $y$ are specific elements of $P$. [I now realize that this definition is not consistent with the definition of "alphabet" I am referencing.] So it seems like $x \leq y$ is the sort of formula I would want to assign a truth value to: it should be true if in the poset $P$ we really have $x \leq y$ (and it should be false otherwise).

Interestingly, your discussion of the formula $x \leq y$ seems to indicate that this formula specifies something that can be true or false, and only takes on a particular truth value once we assign specific poset elements to $x$ and $y$. We then end up having some subset of $P^2$ for which $x \leq y$ is true. So it seems like we are considering how to assign a truth value to $x \leq y$ in quite different ways! Upon reflection, I think this is because I was confused about how to use "variables".

David Egolf (Dec 10 2023 at 06:17):

I think my (incorrect) understanding of "variables" was that they are a set of symbols that one is free to define as one wishes. I was employing this freedom to define the set of variables in terms of the set of elements in $P$. But I think now that I actually don't have this freedom according to the definition of an alphabet I am trying to use. Instead, I believe that "variables" are supposed to be a fixed set of symbols that I don't get to choose, and in particular I don't get to define this set in terms of the elements of a chosen poset.

David Egolf (Dec 10 2023 at 06:24):

Here's the definition of an alphabet for a first-order language that I want to use:
alphabet

I see that the set of variables $v_0, v_1, v_2, \dots$ is fixed in this definition. So, I was not working with this definition correctly when I defined the set of variables to be the set of elements of the poset $P$!

In summary, I think your comments helped me realize that I was confused about what a "variable" is in the context of the above definition for an alphabet of a first-order language. That should help me as I continue to think about this!

Mike Shulman (Dec 10 2023 at 07:03):

Fundamentally, a variable (in mathematics) is a placeholder, like $\underline{\;\;}$ or $\Box$, that can be filled with anything (of the appropriate type). So if I ask you what the value of $x^2+y^2$ is, you can't answer (with a number) until I tell you what numbers to plug in for $x$ and $y$. Similarly, if I ask you whether $x\le y$, you can't answer until I tell you what elements of the poset to plug in for $x$ and $y$.

Mike Shulman (Dec 10 2023 at 07:05):

By contrast with variables, a formal language can also contain constants, which are symbols that have a particular fixed meaning (once a particular model is chosen). So for instance in the theory of the real numbers, there are constants like $0$ and $1$ and $\pi$ and so on. So if you start from some poset and are constructing a first-order theory for it, you could choose to include constants corresponding to some or all of the elements of that poset.

John Onstead (Dec 10 2023 at 08:40):

I'm not sure if this is relevant at all, and I know almost no categorical logic, but I wanted to mention it as it involves logic, statements, and posets. What if there was a category where the objects were true statements and morphisms were a form of implication? For instance, if statement A is true implies that statement B is true, then there is a morphism A -> B. And if you need statements A, B, and C to show that D is true, then you can have some sort of product (like a tensor product) A x B x C -> D. I believe this would form a poset? Please correct me if I'm wrong!

Mike Shulman (Dec 10 2023 at 08:50):

If you change "the objects are true statements" to "the objects are all statements", then what you have is the [[Lindenbaum algebra]] of the theory. This is the "0-categorical" version of the [[syntactic category]] that plays an essential role in categorical logic.

Mike Shulman (Dec 10 2023 at 08:52):

Hmm, the nLab page [[Lindenbaum algebra]] redirects to [[propositional theory]], which is not very helpful. But [[Lindenbaum-Tarski algebra]] is not much better, nor is the wikipedia page on Lindenbaum-Tarski algebra. Someone should improve the situation...

John Onstead (Dec 10 2023 at 09:17):

True, the actually relevant information I found under "type theory" of all places: [[type theory]]

David Egolf (Dec 10 2023 at 20:31):

With my better understanding of variables, I now define the alphabet for our first order language to be:

• the variable symbols $v_0, v_1, \dots$
• these logical symbols: $\neg, \iff, \implies, \land, \lor$
• the equality symbol $\equiv$
• parentheses: $($ and $)$
• a 2-ary relation symbol $\leq$
• a set of constant symbols, having one symbol for each element of our poset $P$

The terms are then the variables and the constants.
The formulas are then defined inductively essentially as before (except now our terms are different).

David Egolf (Dec 10 2023 at 20:34):

Next, to start to interpret these formulas, we can define a "structure" consisting of:

• the set $A$ of elements of our poset $P$
• an 2-ary relation $\leq^P$ on $A$, given by the ordering in our poset $P$
• for each constant symbol $a$, the corresponding element $a^P$ in $P$

This structure will help us interpret formulas in $P$, and I think will help us talk about whether formulas (or sentences in particular) are true or false.

Mike Shulman (Dec 10 2023 at 20:38):

That's looking good! However, it's a bit archaic to describe formulas as untyped strings involving explicit parentheses and so on. When one is actually implementing a proof assistant, there is of course a parsing step that has to take an untyped string of characters as input and know how to reject malformed strings like $\le)x\neg\wedge y$, but when doing mathematics it's generally better to leave that step for the programmers and work with abstract syntax trees.

Todd Trimble (Dec 10 2023 at 20:42):

Building a language (or theory) based on a given fixed poset $P$, in particular positing a constant term for each element of $P$, is something you can do, and it's also a maneuver that is used for certain purposes in model theory, but I'm not quite clear on why you feel a need for this move here.

(If it were me doing the exercise, I think I'd work with the language of posets plain and simple, and not deal with all these constants running around. The language of posets doesn't have constants.)

Mike Shulman (Dec 10 2023 at 20:44):

An AST is a rooted tree where each vertex is labeled by a symbol of the alphabet (now without parentheses) and has the correct number of children for that operator, labeled by things of the correct type. So a node labeled $\le$ has two children labeled by terms and is itself a formula, a node labeled $\wedge$ has two children labeled by formulas and is itself another formula, a node labeled by a variable has no children and is a term, etc.

David Egolf (Dec 10 2023 at 23:57):

Todd Trimble said:

Building a language (or theory) based on a given fixed poset $P$, in particular positing a constant term for each element of $P$, is something you can do, and it's also a maneuver that is used for certain purposes in model theory, but I'm not quite clear on why you feel a need for this move here.

(If it were me doing the exercise, I think I'd work with the language of posets plain and simple, and not deal with all these constants running around. The language of posets doesn't have constants.)

I think I want to be able to consider formulas where we are comparing (using $\leq$) a specific element of the poset to a variable that can range over different elements in the poset. I thought that introducing these constants would make it easy to consider such formulas. But maybe these constants aren't needed to achieve this! I can try proceeding without the constants, and see what happens...

David Egolf (Dec 11 2023 at 00:02):

Mike Shulman said:

An AST is a rooted tree where each vertex is labeled by a symbol of the alphabet (now without parentheses) and has the correct number of children for that operator, labeled by things of the correct type. So a node labeled $\le$ has two children labeled by terms and is itself a formula, a node labeled $\wedge$ has two children labeled by formulas and is itself another formula, a node labeled by a variable has no children and is a term, etc.

Thanks for telling me about abstract syntax trees! If we were to define formulas using these trees instead of strings of symbols, I am guessing the process is similar? We presumably define some small "basic" trees (that correspond to certain simple formulas) and then describe some operations that assemble smaller trees into bigger trees (presumably using a symbol like $\land$ as the root of the new tree). So we'll again end up with an inductive definition for formulas, but now in terms of trees.

Todd Trimble (Dec 11 2023 at 00:31):

David Egolf said:

Todd Trimble said:

Building a language (or theory) based on a given fixed poset $P$, in particular positing a constant term for each element of $P$, is something you can do, and it's also a maneuver that is used for certain purposes in model theory, but I'm not quite clear on why you feel a need for this move here.

(If it were me doing the exercise, I think I'd work with the language of posets plain and simple, and not deal with all these constants running around. The language of posets doesn't have constants.)

I think I want to be able to consider formulas where we are comparing (using $\leq$) a specific element of the poset to a variable that can range over different elements in the poset. I thought that introducing these constants would make it easy to consider such formulas. But maybe these constants aren't needed to achieve this! I can try proceeding without the constants, and see what happens...

There's nothing (that I can see) that is particularly wrong doing what you are doing, so don't worry about my comment too much. Whatever sees the problem through to completion is fine. I was just wondering what you had in mind, and you've explained, so go ahead and carry on.

John Baez (Dec 11 2023 at 10:01):

There's a conceptual difference, of course, in using "the language of posets", which is essentally the bare minimum version of first-order logic needed to write down the axioms for posets, and a language that also has a constant for each element of a specific poset $P$. In the first there's a standard way to get any $n$-ary relation on any poset from a formula with $n$ free variables, where in the latter it's only reasonable to hope for such relations on a single poset, namely $P$. So the former allows for some tricks that the latter does not.

For example, we can check that given an isomorphism of posets $f: P \to P'$, any sentence holds in $P$ iff the same sentence holds in $P'$. (Remember, sentences are formulae with no free variables.)

John Baez (Dec 11 2023 at 10:07):

But for the question you're considering, you are lucky: $P$ and $P^\ast$ have the same underlying set, so you'll give each one the same language even if your language includes a constant for each element of your poset.

Mike Shulman (Dec 11 2023 at 16:41):

John Baez said:

$P$ and $P^\ast$ have the same underlying set, so you'll give each one the same language even if your language includes a constant for each element of your poset.

Well, you'll have the same set of formulas, but not the same set of axioms: the axiom $a\le b$ for $P$ becomes the axiom $b\le a$ for $P^\ast$. So yes if by "language" you mean the set of formulas, but I think usually the whole phrase "internal language" refers to the whole theory, including the axioms.

John Baez (Dec 11 2023 at 17:36):

I was using "language" in the sense of (old-fashioned?) first-order classical logic, e.g.:

• Encyclopedia Brittanica, First-order language.

John Baez (Dec 11 2023 at 17:39):

That's the sense I grew up with: first you choose a language, which specifies "what you can say", and then you choose axioms, which specify "what's true".

John Baez (Dec 11 2023 at 17:41):

I think "internal language" is a later concept - I don't know who started talking about that, but maybe it came along after the "Mitchell-Benabou language of a topos"?

David Egolf (Dec 11 2023 at 19:03):

Now that I've defined a structure (although I probably want to change it, because I suspect I don't need the constants I introduced!), we can introduce the concept of an "assignment". An assignment $\beta$ is a function from the set of variables $\{v_0, v_1, \dots, \}$ to the "domain" set in our structure. In this case, $\beta: \{v_0, v_1, \dots, \} \to A$, where $A$ is the underlying set of the poset $P$.

David Egolf (Dec 11 2023 at 19:03):

Then, an "interpretation" $J$ of our terms and formulas is given by a pair: a structure and an assignment in that structure. For a formula $\phi$, we say that $J \models \phi$ if applying our structure and assignment to $\phi$ yields a true statement in the context of our structure. (The definition in the book I'm following is much longer, but I hope this is the basic idea).

David Egolf (Dec 11 2023 at 19:04):

I hope I can state the thing I want to prove this way:

• let $U_P$ be the structure for the poset $P$, which specifies the underlying set $A$ of $P$ and the relation $\leq^P$ (from the poset $P$) on $A$
• let $U_{P^*}$ be the structure for the poset $P^*$, which specifies the underlying set $A$ of $P^*$ and the relation $\geq^{P^*}$ on $A$. We have $a \leq^{P^*} b \iff b \geq^{P^*} a$, where $\leq^{P^*}$ is the relation from the poset $P^*$.

David Egolf (Dec 11 2023 at 19:04):

• then let $J = (U_P, \beta)$ and $J^* = (U_{P^*}, \beta)$ be interpretations, where $\beta$ is an assignment
• then I think this is what I want to prove: for all $J$ (we have multiple possible $J$ because there are multiple possible $\beta$), if $J \models \phi$, then $J^* \models \phi$, where $\phi$ is any formula in our first-order language

David Egolf (Dec 11 2023 at 19:16):

To give an example, if our original formula is $v_0 \leq v_1$, our structure is the underlying set of $P$ and the $\leq^P$ from $P$, and our assignment is $\beta: v_0 \mapsto a$ and $\beta: v_1 \mapsto b$ for $a,b \in P$, then this formula becomes $a \leq^P b$. If $J$ is the interpretation we just used, then $J \models v_0 \leq v_1$ exactly if $a \leq^P b$ is true.

David Egolf (Dec 11 2023 at 19:24):

To finish this example, let $J^*$ be the same as $J$ except it uses the structure which contains $\geq^{P^*}$ instead of $\leq^P$. The the interpretation of $v_0 \leq v_1$ under $J^*$ is $a \geq^{P^*} b$, which is true exactly if $b \leq^{P*} a$, which is true exactly if $a \leq^P b$.

So, if $J \models v_0 \leq v_1$, then $J^* \models v_0 \leq v_1$.

John Onstead (Dec 12 2023 at 02:42):

As I am learning categorical logic, I find it immensely helpful to always keep what I believe to be the central concept of categorical logic in mind: the syntax-semantics duality. IE, the adjunctions between categories of theories (like type theories) and certain category of categories that assigns a type theory to the syntactic category and a category its internal or "underlying" type theory, which then corresponds to its internal logic. My main question relative to dual posets and more generally opposite categories is where the internal logic functor within this adjunction maps opposite categories to in the category of type theories. My conjecture is that there exists an isomorphism (or at least an equivalence if isomorphism is too strong) between the corresponding underlying type theories of opposite categories within that category of type theories. If this is the case, it would perfectly explain why proving something in one category automatically proves the dual case in the opposite category. As an alternative conjecture, if it isn't true that there exists such an isomorphism or equivalence, there should at the very least be some relationship between these underlying type theories that could explain this, right? So, is my "conjecture" or its alternatives true? Thanks!

John Baez (Dec 12 2023 at 09:23):

David Egolf said:

I hope I can state the thing I want to prove this way:

• let $U_P$ be the structure for the poset $P$, which specifies the underlying set $A$ of $P$ and the relation $\leq^P$ (from the poset $P$) on $A$
• let $U_{P^*}$ be the structure for the poset $P^*$, which specifies the underlying set $A$ of $P^*$ and the relation $\geq^{P^*}$ on $A$. We have $a \leq^{P^*} b \iff b \geq^{P^*} a$, where $\leq^{P^*}$ is the relation from the poset $P^*$.

John Baez (Dec 12 2023 at 09:24):

So you're saying the relation $\geq^{P^*}$ is the same as the relation $\le^P$?

John Baez (Dec 12 2023 at 09:27):

If so, what's the difference between $U_P$ and $U_{P^\ast}$? If I understand you correctly, they have the same underlying set $A$ and the same relation on it.

David Egolf (Dec 12 2023 at 18:18):

Yes, @John Baez, I think $\geq^{P^*}$ and $\leq^P$ specify the same relationship on $A$. I think that makes sense because $a \leq b$ in $P$ exactly when $a \geq b$ in $P^*$ (by the definition of the dual of a partial order).

So, I suppose the only difference between $U_P$ and $U_{P^*}$ is that they use a different symbol for the specified relation on $A$.

David Egolf (Dec 12 2023 at 18:28):

I notice that $J \models$ is defined inductively on formulas in "Mathematical Logic" (by Ebbinghaus):
definition

So if we can show that $J \models t_1 \equiv t_2$ iff $J^* \models t_1 \equiv t_2$, and that $J \models \leq t_1, t_2$ iff $J^* \models \leq t_1, t_2$, then I am guessing that implies that $J \models \phi$ iff $J^* \models \phi$. (In our case the only $n$-ary relationship $R$ is the 2-ary relationship $\leq$).

David Egolf (Dec 12 2023 at 18:32):

And since $J$ and $J^*$ are extremely similar - they just use a different symbol for the same relationship on $A$ in their structures - it seems that we should be able to show this quickly. Since the assignment $\beta$ is the same in $J$ and $J^*$, we immediately have that $J \models t_1 \equiv t_2$ iff $J^* \models t_1 \equiv t_2$. That is because $J \models t_1 \equiv t_2$ iff $J(t_1) = J(t_2)$ and in our case $J(t_1) = \beta(t_1)$ and $J(t_2) = \beta(t_2)$ for variables $t_1$ and $t_2$.

David Egolf (Dec 12 2023 at 18:37):

Further, $J \models \leq t_1 t_2$ iff $\leq^P J(t_1) J(t_2)$ which in our case can be rewritten as $\beta(t_1) \leq^P \beta(t_2)$. Similarly, $J^* \models \leq t_1 t_2$ iff $\beta(t_1) \geq^{P^*} \beta(t_2)$. Since $\leq^P$ and $\geq^{P^*}$ specify the same relationship, we have $J \models \leq t_1 t_2 \iff J^* \models \leq t_1 t_2$.

Because of how $J \models$ is defined inductively on formulas, I am hoping this means that $J \models \phi \iff J^* \models \phi$ for any formula $\phi$ in our first order language.

David Egolf (Dec 12 2023 at 18:45):

Reflecting on this process:

• This was a fun way to start learning a little bit about logic. I enjoyed learning about things like terms, formulas and sentences, free and bound variables, induction on terms and formulas, structures and assignments, and interpretations. In particular the mysterious $\models$ symbol now starts to make a bit more sense.
• Regarding my original goal (showing that if $\Sigma$ is a true "statement" in $P$, then $\Sigma^*$ is a true "statement" in $P^*$), I feel like this process has shed some light on this for me. Namely, it helped me realize that $\leq$ in $P$ is exactly same the relationship on the same underlying set as $\geq$ is in $P^*$. So when we build up statements using $\leq$ in $P$, we can build up equivalent statements using $\geq$ in $P^*$ instead. That helps me intuitively understand this concept of a "dual" statement in the dual partial order, I think.

John Baez (Dec 12 2023 at 21:06):

At the end you claimed, or at least hoped to show, that

$J \models \phi \iff J^* \models \phi$

for any formula $\phi$. This would be automatic if we had $J = J^*$. But as far as I can tell you're not claiming $J = J^\ast$; instead you say "$J$ and $J^*$ are extremely similar - they just use a different symbol for the same relationship on $A$ in their structures". If this is what's going on, a formula $\phi$ that contains the first symbol ($\le^P$) will not contain the second symbol ($\ge^{P^*}$), so I don't think

$J^* \models \phi$

literally makes sense.

John Baez (Dec 12 2023 at 21:10):

Personally I would go about this a bit differently. For example, I might define a way of transforming the formula $\phi$ into a formula $\phi^\ast$ by replacing every instance of the symbol $\le^P$ with the symbol $\ge^{P^\ast}$, and then show

$J \models \phi \iff J^* \models \phi^\ast$

John Baez (Dec 12 2023 at 21:12):

Or, I might try something else: I might define a "language for posets" with a symbol $\le$ that doesn't mention the name of the poset, and define a way of transforming any formula $\phi$ in this language into a formula $\phi^\dagger$ by replacing every expression of the form $x \le y$ with an expression of the form $y \le$, and then show

$J \models \phi \iff J^\dagger \models \phi^\dagger$

John Baez (Dec 12 2023 at 21:15):

for some suitable $J^\dagger$. The slight advantage here is that $\phi$ and $\phi^\dagger$ are in the same language, and this language applies to all posets.

John Baez (Dec 12 2023 at 21:18):

It's possible I'm not understanding you or your setup exactly, so take everything I say with suitable grains of salt.

David Egolf (Dec 12 2023 at 21:23):

John Baez said:

At the end you claimed, or at least hoped to show, that

$J \models \phi \iff J^* \models \phi$

for any formula $\phi$. This would be automatic if we had $J = J^*$. But as far as I can tell you're not claiming $J = J^\ast$; instead you say "$J$ and $J^*$ are extremely similar - they just use a different symbol for the same relationship on $A$ in their structures". If this is what's going on, a formula $\phi$ that contains the first symbol ($\le^P$) will not contain the second symbol ($\ge^{P^*}$), so I don't think

$J^* \models \phi$

literally makes sense.

A formula in our first order language doesn't contain either $\le^P$ or $\ge^{P^*}$. It might contain $\leq$, though. This symbol gets swapped out for the appropriate symbol once we pick a particular structure though, and interpret that formula using that structure.

David Egolf (Dec 12 2023 at 21:25):

For example, once we pick a structure and an assignment, the formula $\leq t_1 t_2$ gets turned into something like $\leq^P ab$, for some $a,b \in A$. If we pick a different structure (but the same assignment), interpreting the same formula could yield $\geq^{P^*} ab$. (I prefer to write these expressions more intuitively as $a \leq^P b$ and $a \geq^{P^*} b$.)

David Egolf (Dec 12 2023 at 21:28):

John Baez said:

for some suitable $J^\dagger$. The slight advantage here is that $\phi$ and $\phi^\dagger$ are in the same language, and this language applies to all posets.

I like the idea of having only one language. I think there is only one language (for formulas) in the approach that I am describing, as well.

David Egolf (Dec 12 2023 at 21:33):

In case having another example would be useful, here is an example (from the book I'm referencing) of using a structure and an assignment to interpret a formula:
example

In this example, the fancy $U$ is the structure and $\beta$ is the assignment. We start with the formula $v_2 \cdot (v_1 + v_2) \equiv v_4$, and by making use of the specified structure and assignment we end up with $4 \cdot (2 + 4) = 8$. Somewhat confusingly, the $+$ in the original formula is just a function symbol, while the $+$ in $4 \cdot (2 + 4) = 8$ is referring to the addition function $+: \mathbb{N} \times \mathbb{N} \to \mathbb{N}$.

David Egolf (Dec 12 2023 at 21:39):

Similarly, returning to the main example we care about, this "interpretation" process moves us from formulas with the relation symbol $\leq$ to expressions involving a relation on $A$ (either $\leq^P$ or $\geq^{P^*}$).

(I hope I explained this correctly! I just read about these concepts a couple days ago, and it's possible I'm misunderstanding something.)

David Egolf (Dec 13 2023 at 00:01):

John Baez said:

But as far as I can tell you're not claiming $J = J^\ast$; instead you say "$J$ and $J^*$ are extremely similar - they just use a different symbol for the same relationship on $A$ in their structures".

I was reflecting on this a bit more. I've realized that I'm not 100% sure what it means for two interpretations (say $J$ and $J^*$) to be equal. $J$ and $J^*$ are the same in the sense that they contain all the same sets, functions, and relations. But they are not the same in the sense that $J$ and $J^*$ yield syntactically different expressions when used to interpret a formula. So if we view $J$ and $J^*$ as specifying functions from formulas (like $\leq t_1 t_2$) to expressions (like $\leq^P a b$ with $a,b \in A$), then the resulting functions are not equal.

David Egolf (Dec 13 2023 at 00:26):

My current guess is that $J$ and $J^*$ are equal, but the "interpretation functions" they induce are not equal.

I don't know a formal definition of what it means for two things like $J$ and $J^*$ to be equal though, so I'm not sure about this. (Is a tuple of things equal to another tuple if (1) the two tuples have the same number of elements and (2) the $i_{th}$ element in one tuple is equal to the $i_{th}$ element in the other tuple, for all $i$? If that is true, then I think $J = J^*$.)

John Baez (Dec 13 2023 at 13:58):

David Egolf said:

A formula in our first order language doesn't contain either $\le^P$ or $\ge^{P^*}$. It might contain $\leq$, though. This symbol gets swapped out for the appropriate symbol once we pick a particular structure though, and interpret that formula using that structure.

Okay. I guess I don't completely understand your attitude toward syntax and semantics. The traditional approach to model theory in first-order logic doesn't think of an interpretation as "swapping out one symbol for another": instead, it maps each formula (which is a syntactic entity, a thing built from symbols) to a subset of $X^N$, where $X$ is some set (a semantic entity, not just the letter $X$) and $N$ is the set of free variables in the formula.

John Baez (Dec 13 2023 at 14:00):

I suppose if you are taking an ultra-syntactic approach, basically denying that semantics has a separate life from syntax, you may think of this subset of $X^N$ as itself described by symbols! This is a coherent viewpoint, and I've actually advocated it at times, but it's not the traditional one I learned in school. I figure if you're going to be radical, you should at least know you're being radical. :upside_down:

John Baez (Dec 13 2023 at 14:01):

Returning to your example, here's a more traditional way to say what's going on. We have a formula in the language of posets. To keep things simple, take the formula

$x \le y$

John Baez (Dec 13 2023 at 14:02):

A model of the theory of posets is a set - let me call it $P$ instead of $X$, just to be friendly - together with a recipe for assigning a subset of $P^N$ to each formula in the language of posets whose set of free variables is $N$. This recipe needs to obey some rules.

In the end, a model of the theory of poset amounts to a poset: a set $P$ together with a binary relation which I'll call $x \le^P y$. Note: the symbol $\le^P$ is part of my meta-mathematical chat here. I'm giving it a symbol just because I need symbols to talk to you: we say it's part of the metalanguage. It exists on a different plane than our friend $\le$.

John Baez (Dec 13 2023 at 14:04):

In our example formula, $N = \{x,y\}$.

John Baez (Dec 13 2023 at 14:11):

So, a model of the formula

$x \le y$

John Baez (Dec 13 2023 at 14:12):

is a subset of $P^N \cong P^2$ consisting of pairs $a, b \in P$ such that $a \le^P b$.

John Baez (Dec 13 2023 at 14:13):

So, you see, the model is sending a formula to a certain subset of a certain set, not another formula with different symbols in it.

John Baez (Dec 13 2023 at 14:14):

The difference may seem a petty one, and indeed I'm starting to feel petty writing so much about this. But logicians argue endlessly about nuances like this - one reason I'm not a logician. :upside_down:

John Baez (Dec 13 2023 at 14:15):

David Egolf said:

Is a tuple of things equal to another tuple if (1) the two tuples have the same number of elements and (2) the $i_{th}$ element in one tuple is equal to the $i_{th}$ element in the other tuple, for all $i$? If that is true, then I think $J = J^*$.)

Yes, that's the usual definition of equality for tuples.

John Baez (Dec 13 2023 at 14:17):

So my (mild) complaint was that in your discussion of duality, you wound up giving a rather elaborate discussion leading up to a proof that

$J \models \phi \iff J^* \models \phi$

followed ultimately by an admission that $J = J^*$, which makes the proof exceedingly easy: you are just proving that

$J \models \phi \iff J \models \phi$

John Baez (Dec 13 2023 at 14:18):

I was offering a way to think about duality where duality changes a formula $\phi$, say

$x \le y$

into a different formula, say $\phi^\dagger$, namely

$y \le x$

John Baez (Dec 13 2023 at 14:20):

In my approach duality also changes the interpretation $J$ to a different interpretation, say $J^\dagger$. And then we can show

$J \models \phi \iff J^\dagger \models \phi^\dagger$

John Baez (Dec 13 2023 at 14:21):

This seems a bit more exciting to me than showing

$J \models \phi \iff J \models \phi$

John Baez (Dec 13 2023 at 14:22):

By the way, I'm using daggers instead of stars just so we can talk about your approach and mine together without fighting over what notation means. Secretly I use stars too. :upside_down:

David Egolf (Dec 13 2023 at 17:07):

Awesome, thanks for explaining that @John Baez ! I was not appreciating that a structure (and apparently a "model" as well) is really about specifying certain functions and relations. And although we use new symbols in the resulting interpreted formulas, these symbols can be viewed as shorthand (I think) for the full ordered-pair information of the functions and relations. From this perspective, $a \leq^P b$ and $a \geq^{P^*} b$ specify the exact same thing: the claim that $(a,b)$ is in the subset of $A^2$ specified by both $\leq^P$ and $\geq^{P^*}$.

David Egolf (Dec 13 2023 at 17:08):

John Baez said:

This seems a bit more exciting to me than showing

$J \models \phi \iff J \models \phi$

Now that I understand that my $J$ and $J^*$ are equal, I agree! I will plan to give your approach a try, hopefully later today.

David Egolf (Dec 15 2023 at 17:14):

I now begin again, with a different approach. (I'm trying to follow the approach John Baez sketched above, although I'm not sure I'll actually manage to do so right away!)
These things stay the same:

• our alphabet is as before (it includes the 2-ary $\leq$ symbol, and it does not include any constant symbols)
• our terms and formulas are defined as before

But we now define our two structures in a different way:

• $(A, \leq)$ where $A$ is the underlying set of our poset $P$, and $\leq$ is the 2-ary relationship on $A$ corresponding to $P$
• $(A, \leq^\dagger)$ where $\leq^\dagger$ is the relationship on $A$ satisfying $a \leq^\dagger b \iff b \leq a$. Note that $\leq^\dagger$ is the relationship corresponding to the dual order $P^\dagger$ of $P$.

David Egolf (Dec 15 2023 at 17:16):

Notice that $\leq$ and $\leq^\dagger$ are different relationships in general.

Then, for each assignment $\beta$, we get two different interpretations:

• $J = ((A, \leq), \beta)$
• $J^\dagger = ((A, \leq^\dagger), \beta)$

David Egolf (Dec 15 2023 at 17:25):

Next, we wish to define a function $f$ on formulas that intuitively "swaps" the variables provided to our 2-ary relationship symbol $\leq$. If we start with the formula $v_0 \leq v_1$, then $f(v_0 \leq v_1) = v_1 \leq v_0$.

We want to define what $f$ does for any formula $\phi$. Once we have done so, we will then denote $f(\phi)$ by $\phi^\dagger$.

David Egolf (Dec 15 2023 at 17:35):

I will now attempt to define $f$ on all formulas:

• if $\phi$ is equal to $t_1 \equiv t_2$ for terms $t_1$ and $t_2$ then $f(\phi) = \phi$
• if $\phi$ is equal to $v_i \leq v_j$ for some variables $v_i, v_j$, then $f(\phi) = v_j \leq v_i$

David Egolf (Dec 15 2023 at 17:35):

• if $\phi$ is equal to $\neg \psi$ for a formula $\psi$, then $f(\phi) = \neg f(\psi)$
• if $\phi$ is equal to $(\alpha \land \beta)$ for formulas $\alpha$ and $\beta$, then $f(\phi) = (f(\alpha) \land f(\beta))$
• if $\phi$ is equal to $(\alpha \lor \beta)$, then $f(\phi) = (f(\alpha) \lor f(\beta))$

David Egolf (Dec 15 2023 at 17:38):

• if $\phi$ is equal to $(\alpha \implies \beta)$, then $f(\phi) = (f(\alpha) \implies f(\beta))$
• if $\phi$ is equal to $(\alpha \iff\beta)$, then $f(\phi) = (f(\alpha) \iff f(\beta))$

David Egolf (Dec 15 2023 at 17:38):

• if $\phi$ is equal to $\forall x \psi$ for a variable $x$ and a formula $\psi$, then $f(\phi) = \forall x f(\psi)$
• if $\phi$ is equal to $\exists x \psi$ for a variable $x$ and a formula $\psi$, then $f(\phi) = \exists x f(\psi)$

David Egolf (Dec 15 2023 at 17:44):

Denoting $f(\phi)$ by $\phi^\dagger$, we now wish to show that $J \models \phi \iff J^\dagger \models \phi^\dagger$.

As a small check on this setup, I first try this out for the formula $\phi$ equal to $v_0 \leq v_1$. Let $\beta$ be the assignment that sends $v_0$ to $a \in A$ and $v_1$ to $b \in A$. Then $J \models \phi$ is true exactly if $a \leq b$ in $P$.

David Egolf (Dec 15 2023 at 17:44):

Since $\phi^\dagger = v_1 \leq v_0$, we have that $J^\dagger \models \phi^\dagger$ is true exactly if $b \leq^\dagger a$. Since $a \leq b \iff b \leq ^\dagger a$ we see that $J \models \phi \iff J^\dagger \models \phi^\dagger$ for this particular $\phi$.

I think the next step is probably to do a kind of induction over formulas to show that $J \models \phi \iff J^\dagger \models \phi^\dagger$ for any formula $\phi$ in our first-order language.

John Baez (Dec 16 2023 at 11:29):

This looks great to me! You'll need to do the induction for formulae, not just sentences (= formulae without free variables), since sentences are made of formulae, not just sentences. Thus, in the induction you'll need to talk about something other than just

$J \models \phi$

since this makes sense only when $\phi$ is a formula. I think you'll need to talk, for each formula with a set $N$ of free variables, about the subset of $P^N$ that it defines.

John Baez (Dec 16 2023 at 11:31):

For a sentence $\phi$, $N = \emptyset$ so $P^N$ has one element, so a subset of it has either 0 or 1 elements, which correspond to the two options: $J \models \phi$ is either true or false.

David Egolf (Dec 16 2023 at 17:35):

That's great to hear!

I think that $J \models \phi$ makes sense for any formula $\phi$, not just when $\phi$ is a sentence. That's because an interpretation $J$ includes an assignment $\beta$, which assigns particular values (in $A$) to all free variables.

At any rate, I hope to give some version of the induction a try in the next few days!

David Egolf (Dec 17 2023 at 19:41):

I'm going to be busy spending time with family for probably the next couple weeks. So, it may be a while before I get back to this! But I do look forward to finishing this up.

John Baez (Dec 17 2023 at 20:49):

David Egolf said:

That's great to hear!

I think that $J \models \phi$ makes sense for any formula $\phi$, not just when $\phi$ is a sentence. That's because an interpretation $J$ includes an assignment $\beta$, which assigns particular values (in $A$) to all free variables.

Okay, if that's how it works you can induct over formulae, not just sentences.