February 25, 2015

Concepts of Sameness (Part 3)

Posted by John Baez

Now I’d like to switch to pondering different approaches to equality. (Eventually I’ll have put all these pieces together into a coherent essay, but not yet.)

We tend to think of $x = x$ as a fundamental property of equality, perhaps the most fundamental of all. But what is it actually used for? I don’t really know. I sometimes joke that equations of the form $x = x$ are the only really true ones — since any other equation says that different things are equal — but they’re also completely useless.

But maybe I’m wrong. Maybe equations of the form $x = x$ are useful in some way. I can imagine one coming in handy at the end of a proof by contradiction where you show some assumptions imply $x \ne x$. But I don’t remember ever doing such a proof… and I have trouble imagining that you ever need to use a proof of this style.

If you’ve used the equation $x = x$ in your own work, please let me know.

To explain my question a bit more precisely, it will help to choose a specific formalism: first-order classical logic with equality. We can get the rules for this system by taking first-order classical logic with function symbols and adding a binary predicate “$=$” together with three axiom schemas:

1. Reflexivity: for each variable $x$,

$x = x$

2. Substitution for functions: for any variables $x, y$ and any function symbol $f$,

$x = y \; \implies\; f(\dots, x, \dots) = f(\dots, y, \dots)$

3. Substitution for formulas: For any variables $x, y$ and any formula $\phi$, if $\phi'$ is obtained by replacing any number of free occurrences of $x$ in $\phi$ with $y$, such that these remain free occurrences of $y$, then

$x = y \;\implies\; (\phi \;\implies\; \phi')$

Where did symmetry and transitivity of equality go? They can actually be derived!

For transitivity, use ‘substitution for formulas’ and take $\phi$ to be $x = z$, so that $\phi'$ is $y = z$. Then we get

$x=y \;\implies\; (x = z \;\implies\; y = z)$

This is almost transitivity. From this we can derive

$(x = y \;\&\; x = z) \;\implies\; y = z$

and from this we can derive the usual statement of transitivity

$(x = y\; \& \; y = z) \;\implies\; x = z$

by choosing different names of variables and using symmetry of equality.

But how do we get symmetry? We can derive this using reflexivity and substitution for formulas. Take $\phi$ to be $x = x$ and take $\phi'$ be the result of substituting the first instance of $x$ with $y$: that is, $y = x$. Then we get

$x = y \;\implies \;(x = x \;\implies \;y = x)$

Using $x = x$, we can derive

$x = y \;\implies\; y = x$

This is the only time I remember using $x = x$ to derive something! So maybe this equation is good for something. But if proving symmetry and transitivity of equality is the only thing it’s good for, I’m not very impressed. I would have been happy to take both of these as axioms, if necessary. After all, people often do.

So, just to get the conversation started, I’ll conjecture that reflexivity of equality is completely useless if we include symmetry of equality in our axioms. Namely:

Conjecture. Any theorem in classical first-order logic with equality that does not include a subformula of the form $x = x$ for any variable $x$ can also be derived from a variant where we drop reflexivity, keep substitution for functions and substitution for formulas, and add this axiom schema:

1’. Symmetry: for any variables $x$ and $y$,

$x = y \; \implies \; y = x$

Proof theorists: can you show this is true, or find a counterexample? We’ve seen that we can get transitivity from this setup, and then I don’t really see how it hurts to omit $x = x$. I may be forgetting something, though!

Posted at February 25, 2015 1:20 AM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2808

Re: Concepts of Sameness (Part 3)

You definitely want reflexivity in the list of conditions for an equivalence relation. Let $\sim$ be an equivalence relation without reflexivity on $X$. Then, if $x \in X$ is equivalent to anything, we can deduce that $x \sim x$. However, we can’t rule out the possibility that $x$ is equivalent to nothing, not even itself.

Therefore, we don’t get a map from $X$ to $X/\sim$. To me, one of the main purposes of equivalence relations is forming quotients, so this is definitely a problem.

Posted by: David Speyer on February 25, 2015 7:17 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

More specifically, here is a true statement if we assume $x=x$ that I don’t see any way to prove without it: “there is a bijection between isomorphism classes of surjections with domain $A$ and equivalence relations on $A$”. That’s not quite a counterexample to your conjecture as stated, since it involves higher-order constructions, but I would argue that it’s an important part of mathematics.

Posted by: Mike Shulman on February 25, 2015 8:36 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

Mike wrote:

More specifically, here is a true statement if we assume $x=x$ that I don’t see any way to prove without it: “there is a bijection between isomorphism classes of surjections with domain $A$ and equivalence relations on $A$”.

Nice. Here is a simpler statement that also requires $x = x$: “the identity function $id: X \to X$ is a surjection”.

Or, using that other idea: “for any set $X$ there exists a surjection $f : Y \to X$.” If we can find $f$ and $y$ with $f(y) = x$ then something equals $x$, so by symmetry and transitivity $x = x$.

Puzzle. What about proving that identity functions are really functions?

(I’m being a bit loose about what formalism I’m working in here, so this is a bit open-ended…)

Posted by: John Baez on February 26, 2015 4:33 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

Haha, so reflexivity of equality is a sort of ultra-weak presentation axiom: every set admits a surjection from something.

Posted by: Mike Shulman on February 26, 2015 10:50 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

It seems plausible that there’s no need to use “because $x = x$” as a step in a proof in the most straightforward manner, since it can’t help you deduce (in the most straightforward manner) any equalities you didn’t already know. But as you know, in category theory the natural categorification of $x = x$ is very important, namely identity morphisms $\text{id}_x : x \to x$ (e.g. in the Yoneda lemma, as universal bundles, etc.). Here one upshot is that if you have a description of a representable functor $F(-) = Hom(x, -)$, it’s usually still interesting to ask what $\text{id}_x$ looks like hiding inside $F(x) = Hom(x, x)$.

Posted by: Qiaochu Yuan on February 25, 2015 7:24 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

Qiaochu wrote:

It seems plausible that there’s no need to use “because $x = x$” as a step in a proof in the most straightforward manner, since it can’t help you deduce (in the most straightforward manner) any equalities you didn’t already know.

Right, that’s the intuition behind my conjecture. My intuition was shaken when I learned on Wikipedia that in a certain formalism you can use $x = x$ to prove

$x=y \; \implies \; y=x$

and then use that to prove

$(x=y \; \& \; y=z) \; \implies \; x=z$

But that’s because I’d never thought of a setup where symmetry and transitivity weren’t axioms along with reflexivity!

So, I’m still hoping that my conjecture, corrected to take this into account, can be proved by someone who either knows more proof theory or is more patient than me.

But as you know, in category theory the natural categorification of $x = x$ is very important, namely identity morphisms $\text{id}_x : x \to x$ (e.g. in the Yoneda lemma, as universal bundles, etc.)

For me the most fundamental reason for including identity morphisms in category theory is that if we leave them out, the resulting gadgets can be thought of as categories of a special kind, by formally adjoining identity morphisms. And what we get are categories with no invertible morphisms except for the identity.

In other words: if we leave out identity morphisms it becomes impossible — or at least tricky — to define isomorphisms.

And this is somewhat interesting. If you think equations between objects in a category theory are evil, you might say “so let’s leave out identity morphisms, which are a way of expressing equations between objects: let’s only work with isomorphisms”. But without identity morphisms, the usual definition of isomorphism makes no sense!

It’s as if you need a bit of evil to avoid evil.

Posted by: John Baez on February 25, 2015 7:41 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

Perhaps of some relevance, at least to the intuition behind the Conjecture, there’s an old proof of Hintikka’s which takes up a suggestion thrown out (but of course not worked through) in the Tractatus. Hintikka distinguishes the usual ‘inclusive’ reading of the variables (i.e. we are allowed to assign the same object to distinct variables) from the ‘exclusive’ reading, and then proves the key theorem that everything expressible in terms of the inclusive quantifiers and identity may also be expressed by means of the weakly exclusive quantifiers without using a special symbol for identity at all.

There’s a bit more in this blogpost: http://www.logicmatters.net/2013/04/25/an-old-result-of-hintikkas/

Posted by: Peter Smith on February 25, 2015 8:14 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

Of course, in homotopy type theory we frequently finish our proofs with reflexivity, having used path-induction to reduce to that case. So in that sense, I use $x=x$ all the time. Path induction is a type-theoretic version of your “substitution for functions” and “substitution for formulas”; in type theory, the role of reflexivity is that “equality is freely generated by reflexivity”.

Posted by: Mike Shulman on February 25, 2015 8:33 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

I would argue that this is really the essence of the importance of reflexivity, even outside HoTT. It is the only axiom that actually requires the relation to be inhabited at all, let alone to be inhabited at all values.

Intuitively, it’s the only non-recursive constructor of an inductively defined object. So while you may not actually use the axiom often, if at all, in practice, you can’t conclude anything at all about your relation without including it in the definition (or something else to serve that purpose).

Posted by: James Cook on March 25, 2015 7:51 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

Concerning your conjecture, how about this formula: $\forall x \exists y, x = y$ This doesn’t contain an exact subformula of the form “$x=x$”, although it’s rather close to. I don’t see how you could possibly prove this without using reflexivity. But I also feel like I’m missing something here and just being dense ;)

Posted by: Tobias Fritz on February 25, 2015 8:58 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

In fact, by David’s remark above, if you assume symmetry and transitivity, then this formula is equivalent to reflexivity.

Posted by: Mike Shulman on February 25, 2015 9:17 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

Great— this sounds like progress!

So my conjecture is false unless you can derive $x = x$ from first-order logic with an $=$ predicate obeying reflexivity, symmetry, substitution for functions and substitution for formulas.

And I guess the quickest way to prove you can’t do that that is to use Gödel’s completeness theorem and find a model of the above theory in which

$\not{\forall x \, \exists y \; x = y}$

holds. Such a model should be easy to find.

If so, my conjecture is false.

And in this case, I need some subtler way to explain the sense in which $x = x$ is useless in first-order logic. You see, this defeat does not feel like much of a defeat. I claim that using $x = x$ to prove

$\forall x \, \exists y \; x = y$

is not truly interesting: it’s just ‘another way to say the same thing’.

Posted by: John Baez on February 25, 2015 10:00 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

How about a model in which $x=y$ is never true?

Posted by: Mike Shulman on February 25, 2015 10:33 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

How about taking the model given by any inhabited set $A$ and interpreting $=$ as the empty relation? This makes the axiom schemas for substitution vacuously true, since their premises are always false.

But since $A$ is inhabited, we have both $\exists x, \not(x=x)$ and $\not\forall x \exists y, x = y$. (We already knew these two to be equivalent by Mike’s observation.)

How is the completeness theorem relevant here?

I claim that using $x=x$ to prove $\forall x \, \exists y \; x = y$ is not truly interesting: it’s just ‘another way to say the same thing’.

I agree, and that’s probably why my previous comment felt like I was cheating. Let me try to make the sentiment that it’s ‘another way to say the same thing’ a bit more precise.

I suspect that any true first-order formula that only involves variable symbols and “=” can be proven using reflexivity and classical logic only. And conversely, that it implies reflexivity unless it is a tautology. I’ve been trying to show this, but after some failed initial attempts I’m not quite sure.

(My model theory is not very firm, so I hope that at least some of my reasoning makes sense.)

Posted by: Tobias Fritz on February 25, 2015 10:37 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

Tobias wrote:

How about taking the model given by any inhabited set $A$ and interpreting $=$ as the empty relation? This makes the axiom schemas for substitution vacuously true, since their premises are always false.

Yes, that should do the job!

How is the completeness theorem relevant here?

I asked a question about provability, but using Gödel’s completeness theorem we can convert that into a question about what holds in all models. In first-order logic, a sentence is unprovable from some axioms iff there’s a model of the axioms in which it fails to hold.

Posted by: John Baez on February 25, 2015 10:57 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

In first-order logic, a sentence is unprovable from some axioms iff there’s a model of the axioms in which it fails to hold.

Although in this case, we were only using the “if” direction, which requires only the (much easier) soundness theorem.

Posted by: Mike Shulman on February 25, 2015 11:36 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

Right; sorry.

Posted by: John Baez on February 26, 2015 2:07 AM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

Mike wrote:

How about a model in which $x = y$ is never true?

Yes, I guess that satisfies all the axioms I listed, in a nicely trivial way!

On the one hand I think a model like this deeply violates my heart-felt, cherished intuitions about equality in first-order logic. I instinctively want to rule out such models!

On the other hand, I’m wondering what really interesting theorems we lose if we allow such models. (You started making progress on that question…)

Posted by: John Baez on February 25, 2015 10:37 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

It’s hard to think of interesting examples in first-order theories because so many of the interesting first-order theories have the property that their axioms imply reflexivity, or at least Tobias’s equivalent axiom $\forall x \exists y (x=y)$. For example, in first-order ZFC, the axiom of extensionality implies reflexivity, and in the first-order theory of a monoid, we have $x=x \cdot e$ for all $x$.

Posted by: Mike Shulman on February 25, 2015 11:42 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

To extend Mike’s point a little, with the risk of stating the obvious, in a relation which is symmetric and transitive, any element which is related to something is related to itself. This is why they are called partial equivalence relation (they’re like equivalence relation on a subset).

So, any theorem of the form $\forall x\ldots.\,\exists\ldots.\,x=t$ entails reflexivity (in particular, induction principles).

Now, partial equivalence relations are useful in their own right, but when proving things about them, one finds himself often relativising the quantifier to elements to which reflexivity applies. A testimony to the role of reflexivity in proofs about equality.

Posted by: Arnaud Spiwack on February 26, 2015 12:34 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

John wrote:

I can imagine one coming in handy at the end of a proof by contradiction where you show some assumptions imply $x \neq x$. But I don’t remember ever doing such a proof… and I have trouble imagining that you ever need to use a proof of this style.

I’ve often done proofs by contradiction that finish with a line of the form $x \leq y \leq \cdots \lt x.$ And although I wouldn’t literally follow this with “and therefore $x \neq x$, a contradiction”, it seems to me that this is an example of what you’re talking about.

I’m sure I’ve included proofs like this in my teaching over the last few months (topology — including metric spaces — and Fourier analysis).

Posted by: Tom Leinster on February 26, 2015 5:42 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

Hmm, I’ve taught analysis and never done a proof by contradiction like this!

What I have often done is show

$x \le y \le x$

and conclude that $x = y$. So apparently I believe the real numbers are totally ordered and therefore obey $x = x$.

(Why are you doing so many proofs by contradiction, anyway? Don’t you know it promotes tooth decay?)

Posted by: John Baez on February 26, 2015 5:47 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

I know, I know, I try to bring my students up to be good constructivists with confident smiles. But sometimes it’s not easy.

Let’s see. According to a search of the PDF of my Fourier analysis notes this semester, I’ve only done one proof by contradiction so far, and it wasn’t of the form I mentioned. (For what it’s worth: it was to prove that if $I$ is a real interval and $f, g \colon I \to \mathbb{C}$ are equal almost everywhere, then $f(x) = g(x)$ for all points $x$ at which both $f$ and $g$ are continuous.)

Now for last semester’s topology notes. And here’s a proof of the form I mentioned! Verbatim:

Lemma Every metrizable space is Hausdorff.

Proof Let $(X, d)$ be a metric space and let $x, y$ be distinct points of $X$. Put $r = d(x, y)/2$. Then $B(x, r)$ is an open subset of $X$ containing $x$, and similarly $B(y, r)$ is an open subset of $X$ containing $y$, so it suffices to show that $B(x, r)$ and $B(y, r)$ are disjoint. This follows from the triangle inequality, as if there exists a point $z \in B(x, r) \cap B(y, r)$ then $d(x, y) \leq d(x, z) + d(z, y) \lt r + r = d(x, y),$ a contradiction.

Is the issue that although the definition of Hausdorff is usually stated as “if $x \neq y$ then there exist disjoint neighbourhoods of $x$ and $y$”, it would be better to state it contrapositively as “if every neighbourhood of $x$ meets every neighbourhood of $y$ then $x = y$”?

On the more general point of avoiding proofs by contradiction: I see that my topology notes actually contain quite a few of them, and they almost all involve sequences. Assuming that the thing you want to prove is false, you construct (perhaps iteratively) a sequence with some bad property, and deduce a contradiction. Proving that a compact metric space is sequentially compact was one example of this.

There are also statements like “$[0, 1]$ is not homeomorphic to $\mathbb{R}$” where by design you’re trying to show that some assumption implies a falsehood. I guess that doesn’t count as a proof by contradiction.

Posted by: Tom Leinster on February 26, 2015 6:07 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

Thanks for the examples! I find that my undergraduate students fall in love with the power of proof by contradiction and get carried away. For example, sometimes they do proofs like this:

To prove $P$, let us assume $\not{P}$. [Then they prove $P$.] This contradicts $\not{P}$. Therefore, $P$.

Posted by: John Baez on February 26, 2015 6:32 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

Yes, I see that too! And not infrequently :-)

Posted by: Tom Leinster on February 26, 2015 6:39 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

On the subject of constructive proofs and compactness, you might be interested to look at this MathOverflow question, particularly godelian’s comment.

Posted by: Mark Meckes on February 26, 2015 7:37 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

Thanks; that’s interesting. It suggests that I’m not invoking too many unnecessary logical principles in my topological proofs.

Posted by: Tom Leinster on February 26, 2015 8:50 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

…where by design you’re trying to show that some assumption implies a falsehood. I guess that doesn’t count as a proof by contradiction.

Right; at least, not the sort of proof-by-contradiction that’s nonconstructive.

I don’t know offhand the “right” constructive definition of “Hausdorff”. If it’s “if $x \neq y$ then there exist disjoint neighbourhoods of $x$ and $y$”, then your proof is an instance of the above sort (since being disjoint is a negative statement), and hence perfectly constructive. If it’s the contrapositive, then your proof could be turned around as “to show $x=y$ we show $d(x,y)=0$, and for that we show $d(x,y)\lt\epsilon$ for all $\epsilon\gt 0$, which follows by the triangle inequality blah blah from the fact that $B(x,\epsilon/2)$ meets $B(y,\epsilon/2)$.”

Posted by: Mike Shulman on February 26, 2015 11:03 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

Naively I’d expect the contrapositive, “if every neighborhood of x meets every neighborhood of y then x = y” to be the constructive version, since the usual formulation tells us “there exist disjoint neighborhoods” but don’t tell us which ones, and also invokes disequality, which is awkward. So I guess you’d say something like

$Hauss: \left(\Pi_{U: neighborhood(x)}\Pi_{V: neighborhood(y)} U\cap V\right) \rightarrow (x = y)$

or some formalization of such.

Posted by: Layra on March 1, 2015 11:22 AM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

I might mention here C.S. Peirce’s concept of “teridentity”, involved in saying that three things are identical, or more precisely that three signs denote the same object. There is some discussion in my notes on Peirce’s 1870 Logic of Relatives.

Posted by: Jon Awbrey on March 6, 2015 12:10 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

john why is the contrapositive of a statement sometimes easier to prove than the original if they are logically the same?

Posted by: k on March 7, 2015 3:30 AM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

That’s a good question. In intuitionistic logic the contrapositive of a statement is not always equivalent to the original statement. This means that certain very nice methods of proving $\not{Q} \implies \not{P}$ do not always work to prove $P \to Q$. I believe this may be part of why proving the contrapositive can be easier sometimes.

Posted by: John Baez on March 7, 2015 5:05 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

Here’s a different way to use reflexivity: according to SEP, Frege defined ‘$0$’ to be the number of objects that are not equal to themselves.

Posted by: Mike Shulman on March 10, 2015 7:12 AM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

Wow, that’s wild! And what’s ‘1’ — the number of objects that are equal to any fixed object?

Posted by: John Baez on March 10, 2015 4:51 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

It’s really the same as how the empty set is standardly defined in ZF via the separation axiom: given an axiom that ensures the existence of a set, the empty set can be defined as the subset of elements not equal to themselves. By extensionality, the result is independent of the set whose existence is assumed.

Posted by: Todd Trimble on March 10, 2015 9:20 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

It seems like a needless flourish to define the empty set as consisting of elements $x$ of some fixed set for which $x \ne x$, when you could have defined it to consist of elements for which $FALSE$ holds… or whatever is the quickest way you have at your disposal to say ‘$FALSE$’. But what the heck: let’s enjoy ourselves.

Posted by: John Baez on March 10, 2015 10:44 PM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

This “flourish” is probably an artifact of how $FALSE$ wasn’t considered part of the language of set theory. Boolean logic and truth tables were still rather new-fangled things at the time.

This is not to say that $FALSE$ was positively considered to be foreign to set theory either, merely that truth and falsity were optimistically expected to be properties of formulas in a sufficiently complete and explicit theory, rather than The Propositions of a Very Small theory… and then Gödel his notorious thing.

(I might muse that truth tables finally got their due respect when Gödel invented model theory, in which they became a small model of a particular theory; but for the actual history one should look for books instead of me…)

Posted by: Jesse C. McKeown on March 11, 2015 12:33 AM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

What’s FALSE? :-) Is it a logical formula?

I’m being slightly facetious here; there are all kinds of ways to set things up. I think most modern logicians would have no qualms admitting “true” and “false” as logical constants, but they could also be introduced in terms of other logical operators, via the formulae $\forall_x x = x$ (“true”) and $\exists_x \neg (x = x)$ (“false”). I’m not sure of the history, but I think maybe at some point those propositional constants were often not explicitly introduced; instead one had binary propositional operators $\vee, \wedge, \to$ and an unary operator $\neg$, and one represented “false” in a Boolean algebra as $p \wedge \neg p$ or some such thing. (Maybe Jesse was saying something like that earlier.) I’d have to check up on that.

I have maybe a slightly more serious point, having to do with the syntax of “pulling back” formulas. If $P(y)$ is a formula with one free variable $y$ of type $Y$, we would like to interpret it as a predicate on $Y$ or subtype of $Y$. Similarly, if $x_1, \ldots, x_n$ are the free variables of a formula $P = P(x_1, \ldots, x_n)$, with $x_i$ of type $X_i$, then the default interpretation would be as a predicate on or subtype of a product type $X_1 \times \ldots \times X_n$. In this way, we use the free variables of a formula to furnish its default context. Of course we might want to “pull back” to a different context – in fact we do this all the time – so that $P(y)$ could also be interpreted as a predicate on $X \times Y$ where $X$ is some given type, e.g., we might typically write $\{(x, y): P(y)\}$. One elegant way to do that, if we want to retain this idea of using free variables to declare the context, is to define the pullback formula $X^\ast P$ to be $P(y) \wedge [x = x]$ where $x$ is a variable of type $X$ not already in use.

So if we take your idea of starting with $FALSE$ (where the context is presumably the empty context) and we pull this proposition back to a predicate on some already introduced type $X$, we would represent it by the formula $FALSE \wedge [x = x]$, which is equivalent to $\neg [x = x]$ if you’ve set up your deductive system right. In that sense this “flourish” actually seems very natural to me (and it looks even better to me when reformulated in terms of Peircean string diagrams).

Posted by: Todd Trimble on March 11, 2015 2:42 AM | Permalink | Reply to this

Re: Concepts of Sameness (Part 3)

In other words, if you slight the empty set by excluding the nullary logical operations from your system, then you can make amends by appealing to reflexivity.

Posted by: Mike Shulman on March 11, 2015 4:01 AM | Permalink | Reply to this

Post a New Comment