Category Archives: Uncategorized

Complexity to Simplicity and Back Again

Generalizing a problem can make the solution simpler or more complicated, and it’s often hard to predict which beforehand. Here’s a mini-example of a puzzle and four generalizations which alternately make it simpler or more complicated.
Continue reading


Filed under Uncategorized

Generating Functions as Cardinality of Set Maps

There is a class of all cardinalities \mathbf{Card}, and it
has elements 0, 1 and operations +, \cdot, and so forth defined on it. Furthermore, there is a map
\mathrm{card}\colon\mathbf{Set}\to\mathbf{Card} which takes
sets to cardinalities such that \mathrm{card}(A\times  B)=\mathrm{card}(A)\cdot\mathrm{card}(B) (and so on).

Ordinary generating functions can be thought of entirely analogously
with set maps \mathbf{Set}\to\mathbf{Set} replacing sets:
There is a class \mathbf{GenFunc} with elements 0,
1, and operations +, \cdot. Furthermore,
there is a (partial) map \mathrm{genFunc}\colon (\mathbf{Set}\to\mathbf{Set})\to\mathbf{GenFunc} such that \mathrm{genFunc}(F\times G)=\mathrm{genFunc}(F)\cdot\mathrm{genFunc}(G) (and so on). Here, F\times G is defined by (F\times G)(S)=F(S)\times G(S). Other operations on set maps (like disjoint union) are similarly defined pointwise.

(This is probably obvious and trivial to anyone who actually works
with generating functions, but it only occurred to me recently, so I
thought I’d write a blog post about it.)

The class \mathbf{GenFunc} is in fact a set, and is just the set of formal power series \{\sum_{i\geq 0} a_i z^i\mid a_i\in\mathbb{N}\}. The partial map \mathrm{genFunc} takes F to \sum_{i\geq 0} a_i z^i just in case F is “canonically isomorphic” (a notion I’ll leave slippery and undefined but that can be made precise) to the map Z\mapsto \coprod_{i\geq 0} \{1,2,\ldots,a_i\}\times Z^i, where \coprod indicates disjoint union.

That provides a semantics for ordinary generating functions. Furthermore, this semantics has a number of features beyond those of cardinality. For example, in addition to respecting \coprod and \times, \mathrm{genFunc} represents composition.

A similar semantics can be provided for exponential generating functions, but it takes a little more work. In particular, we have to single out \lbrack0,1\rbrack as a distinguished set. Let \mathbf{Meas} be the smallest set containing all measurable subsets of \lbrack0,1\rbrack^n for any finite n and which is closed under finite products, countable disjoint unions, and products with sets \{1,\ldots,n\} for finite n\geq 1.

We can define the measure \mu of all sets in \mathbf{Meas} by extending Lebesgue measure in the obvious way (taking the product of a set with \{1,\ldots,n\} will multiply the measure by n). Furthermore, notice that, by construction, every element of every set M in \mathbf{Meas} is a tuple which (after flattening) has all of its elements either natural numbers or elements of \lbrack 0,1\rbrack and has at least one element of \lbrack 0,1\rbrack. Therefore, we can define a pre-ordering on M by comparing the corresponding first elements that are in \lbrack 0,1\rbrack.

The point of all that is that, for M\in\mathbf{Meas}, we can form the set M^n_{<}=\{\langle m_1,\ldots,m_n\rangle\mid m_1 < \cdots < m_n\} which will again be in \mathbf{Meas} and its measure will be \mu(M)^n/n!. The corresponding statement with cardinality is not true since you have to worry about the case when elements in the tuple are equal (\mathrm{card}(X^n_{<}) = \mathrm{card}(X)(\mathrm{card}(X)-1)\cdots(\mathrm{card}(X)-n+1)/n!) but the set of tuples that have duplicates has measure 0, so by working with measure, we can get the equality we want.

Finally, let \mathbf{ExpGenFunc} be the set of formal power series \{\sum_{i\geq 0} a_i/i! z^i\mid a_i\in\mathbb{N}\}. The partial map \mathrm{expGenFunc} takes F to \sum_{i\geq 0} a_i/i! z_i just in case F is “canonically isomorphic” to the map Z\mapsto \coprod_{i\geq 0} \{1,2,\ldots,a_i\}\times Z^i_{<} for all Z in \mathbf{Meas}. Just as before, this map respects +, \cdot, composition, etc.

Note that the exponential generating functions are usually explained via labeled objects and some sort of relabeling operation. This approach weasels out of that by observing that the event that there was a label collision has probability 0, so you can just ignore it.

1 Comment

Filed under Uncategorized

Mathematica and Quantifier Elimination

In 1931, Alfred Tarski proved that the real ordered field (\mathbb{R}, 0, 1, +,\times, <) allows quantifier elimination: i.e., every first-order formula is equivalent to one with no quantifiers.  This is implemented in Mathematica’s “Resolve” function.

The Resolve function is called like Resolve[formula,domain] where domain gives the domain for the quantifiers in formula.  Since we’ll always be working over \mathbb{R} in this blog post, let’s set that to be the default at the start.

In[1]:= Unprotect[Resolve]; Resolve[expr_] := Resolve[expr, Reals]; Protect[Resolve];

Now let’s see what quantifier elimination lets you do!

(A couple of caveats first though: First, many of these algorithms are extremely inefficient. Second, I had some trouble exporting the Mathematica notebook, so I basically just copy-and-pasted the text. Apologies if it’s unreadable.)

How many solutions?

Let’s start with just existential formulas.  By eliminating quantifiers from \exists x\, \phi(x,a), we can tell what the conditions are on a such that there’s at least one solution x.  For example:

In[2]:= Resolve[Exists[x, x^2 + b x + c == 0]]
Out[2]= -b^2 + 4 c <= 0

This just tells you that there’s a solution to the quadratic if the discriminant is non-negative.  Let’s turn this into a function:

In[3]:= atLeastOneSolution[formula_, variable_] := Resolve[Exists[variable, formula]]

Now we can verify that cubics always have solutions:

In[4]:= atLeastOneSolution[x^3 + b x^2 + c x + d == 0, x]
Out[4]= True

Now suppose we wanted to find when something has at least two solutions.  Just like resolving \exists x\,\phi(x) told us when there was at least one, \exists x_1,x_2\,x_1\ne x_2\wedge \phi(x_1)\wedge\phi(x_2) will be true exactly when there are at least two.

This is just as easy to program as atLeastOneSolution was, except that when we create the variables x_1 and x_2 we have to be careful to avoid capture (what if one of those two already appeared in \phi?).  Mathematica provides a function called Unique where if you call Unique[], you’re guaranteed to get back a variable that’s never been used before.  With that we can define atLeastTwoSolutions correctly (edit: actually, this isn’t right if the passed-in variable is also bound in the passed-in formula):

In[5]:= atLeastTwoSolutions[formula_, v_] :=
With[{s1 = Unique[], s2 = Unique[]},
Exists[{s1, s2},
s1 != s2 && (formula /. v -> s1) && (formula /. v -> s2)]]]

We can check this by verifying that quadratics have two solutions when the discriminant is strictly positive:

In[6]:= atLeastTwoSolutions[x^2 + b x + c == 0, x]
Out[6]= -b^2 + 4 c < 0

Here’s the condition for the cubic to have at least two solutions:

In[7]:= atLeastTwoSolutions[x^3 + b x^2 + c x + d == 0, x]
Out[7]= c < b^2/3 &&
1/27 (-2 b^3 + 9 b c) - 2/27 Sqrt[b^6 - 9 b^4 c + 27 b^2 c^2 - 27 c^3] <=
d <= 1/27 (-2 b^3 + 9 b c) + 2/27 Sqrt[b^6 - 9 b^4 c + 27 b^2 c^2 - 27 c^3]

Note that (and I believe Resolve always does this) the c<b^2/3 condition given first is sufficient that the later square root is well-defined:
In[8]:= Resolve[ForAll[{b, c}, c < b^2/3 ⇒ b^6 - 9 b^4 c + 27 b^2 c^2 - 27 c^3 > 0]]
Out[8]= True

It’s clear that we can determine when there at least n solutions by a very similar trick: just resolve \exists x_1,\ldots,x_n (x_i\ne x_j,i\ne j)\wedge (\phi(x_i),\forall i).

We’ll first write a helper function to produce the conjunction of inequalities we’ll need:

In[9]:= noneEqual[vars_] :=
And @@ Flatten[Table[If[s1 === s2, True, s1 != s2], {s1, vars}, {s2, vars}]]
In[10]:= noneEqual[{x, y, z}]
Out[10]= x != y && x != z && y != x && y != z && z != x && z != y

And now we’ll write atLeastNSolutions:

In[11]:= atLeastNSolutions[formula_, v_, n_] := With[{sList = Array[Unique[] &, n]},
noneEqual[sList] && (And @@ Table[formula /. v -> s, {s, sList}])]]]

Given atLeastNSolutions, we can easily write exactlyNSolutions:

In[12]:= exactlyNSolutions[formula_, v_, n_] :=
atLeastNSolutions[formula, v, n] && ! atLeastNSolutions[formula, v, n + 1]]

I used BooleanConvert instead of Resolve since there won’t be any quantifiers left in the formula, so we just have to do Boolean simplifications.

In[13]:= exactlyNSolutions[x^3 + b x^2 + c x + d == 0, x, 2]
Out[13]= ! 1/27 (-2 b^3 + 9 b c) - 2/27 Sqrt[b^6 - 9 b^4 c + 27 b^2 c^2 - 27 c^3] < d <
1/27 (-2 b^3 + 9 b c) + 2/27 Sqrt[b^6 - 9 b^4 c + 27 b^2 c^2 - 27 c^3] &&
1/27 (-2 b^3 + 9 b c) - 2/27 Sqrt[b^6 - 9 b^4 c + 27 b^2 c^2 - 27 c^3] <=
d <= 1/27 (-2 b^3 + 9 b c) +
2/27 Sqrt[b^6 - 9 b^4 c + 27 b^2 c^2 - 27 c^3] && c < b^2/3
In[14]:= exactlyNSolutions[x^2 + b x + c == 0, x, 1]
Out[14]= -b^2 + 4 c <= 0 && -b^2 + 4 c >= 0

This last calculation shows that a quadratic has exactly one solution exactly when the discriminant is both nonnegative and nonpositive (as you can see, there is no guarantee that the formula will be in it’s simplest form).
We now have a way to test whether a formula with one free variable has n solutions for specific values of n, since exactlyNSolutions will return either True or False if you quantify out the only variable.  For example:

In[15]:= p = x^4 - 3 x^3 + 1
Out[15]= 1 - 3 x^3 + x^4
In[16]:= Plot[Evaluate[p], {x, -3, 3}]

In[17]:= exactlyNSolutions[p == 0, x, 2]
Out[17]= True

It would be nice, however, to have a function which will just tell you how many solutions such a formula has.

In the single-variable polynomial case, we could just try exactlyNSolutions for n=0,1,2,\ldots until we find the right n.  However, there might not be finitely many solutions if the formula involves inequalities or higher-dimension polynomials (e.g., x^2 + y^2 = 1 has infinitely many solutions).

How can we tell if a formula has infinitely many solutions?  Well, the fact that \mathbb{R} has quantifier elimination implies that \{x\in\mathbb{R}\mid \phi(x)\} for \phi with just x free must be a finite union of points and open intervals (since the only quantifier free terms are t_1=t_2 and t_1<t_2. Therefore \{x\in\mathbb{R}\mid\phi(x)\} is infinite iff it contains a non-empty open interval, i.e., iff \exists a,b\,a<b\wedge\forall x\,(a<x<b\implies\phi(x)).

In[18]:= infinitelyManySolutions[formula_, v_] := With[{a = Unique[], b = Unique[]},
Resolve[Exists[{a, b}, a < b && ForAll[v, a < v < b ⇒ formula]]]]

To test:

In[19]:= infinitelyManySolutions[Exists[y, x^2 + y^2 == 1], x]
Out[19]= True

Now we can write numberOfSolutions and be assured that it will always (theoretically) terminate for any formula with a single free variable:

In[20]:= numberOfSolutions[formula_, v_] :=
If[infinitelyManySolutions[formula, v], Infinity,
Block[{n = 0},
While[! exactlyNSolutions[formula, v, n], n++];

A few examples:

In[21]:= numberOfSolutions[p == 0, x]
Out[21]= 2
In[22]:= numberOfSolutions[p > x^2, x]
Out[22]= ∞
In[23]:= numberOfSolutions[p > x^6 + 5, x]
Out[23]= ∞
In[24]:= numberOfSolutions[p > x^6 + 6, x]
Out[24]= 0
In[26]:= Plot[{p, x^6 + 5, x^6 + 6}, {x, -1.6, -1},
PlotLegend -> {HoldForm[p], x^6 + 5, x^6 + 6}, LegendPosition -> {1, 0},
ImageSize -> Large]

Up to now, all our functions have taken single variables, but we can accomodate tuples of variables as well.  First, we’ll define the analogue of noneEqual to produce the formula asserting that none of the given tuples are equal (recall that two tuples are unequal iff a pair of corresponding components is unequal):

In[27]:= noTuplesEqual[tuples_] := And @@ Flatten[Table[If[t1 === t2, True,
Or @@ MapThread[#1 != #2 &, {t1, t2}]], {t1, tuples}, {t2, tuples}]]
In[28]:= noTuplesEqual[{{x[1], y[1]}, {x[2], y[2]}}]
Out[28]= (x[1] != x[2] || y[1] != y[2]) && (x[2] != x[1] || y[2] != y[1])

Now we can add rules to our old function to deal with tuples of variables as well:

In[29]:= atLeastNSolutions[formula_, variables_List, n_] := With[
{sList = Array[Unique[] &, {n, Length[variables]}]},
noTuplesEqual[sList] &&

And @@
formula /. MapThread[Rule, {variables, tuple}], {tuple, sList}]]]];

We can extend infinitelyManySolutions by observing that a formula \phi(x_1,\ldots,x_n) has infinitely many solutions iff some projection \exists x_1,\ldots,x_{i-1},x_{i+1},\ldots,x_n \phi(x_1,\ldots,x_n) does.

In[30]:= infinitelyManySolutions[formula_, variables_List] := Or @@ Table[
infinitelyManySolutions[Exists[Select[variables, ! (# === v) &], formula],
v], {v, variables}]
In[33]:= ContourPlot[{x^2 + y^3 - 2, x^2 + y^2/4 - 2}, {x, -3, 3}, {y, -3, 3}]

In[34]:= exactlyNSolutions[x^2 + y^3 == 2 && x^2 + y^2/4 == 2, {x, y}, 2]
Out[34]= False

(There are actually four solutions. This example of a set equations for which it’s difficult to tell how many solutions there are by graphing is from Stan Wagon)

Solving Polynomial Equations

In the last section, we saw how to use quantifier elimination to find out how many roots there are.  But how can you actually find the roots?

In a certain sense, you’ve already found them just when you identified how many there are!  To “find” a root in this sense, you just introduce a new symbol for it, and have some means for answering questions about its properties.  Given some property \phi(x), if you want to determine if it holds of the 6th root of some polynomial p with 17 roots, then you just have to decide \exists x_1,\ldots,x_{17}\,(x_i<x_j,i<j)\wedge(p(x_i),\forall i)\wedge\phi(x_6).

We can implement this by a function withSpecificRoot, that takes a variable, the formula it’s supposed to be a solution to, which of the roots it’s a solution to, and a formula in which you want to use this root:

In[35]:= withSpecificRoot[variable_, rootFormula_, whichRoot_, totalRoots_, formula_] :=

With[{roots = Array[Unique[] &, totalRoots]},
Less[Sequence @@ roots] &&
variable ==
roots[[whichRoot]] &&
(And @@
Table[(rootFormula /. variable -> root), {root, roots}]) && formula]]]

We can tell where various roots are with respect to already-known real numbers:
In[36]:= withSpecificRoot[x, x^2 - 3 == 0, 1, 2, x < 3]
Out[36]= True
In[37]:= withSpecificRoot[x, p == 0, 1, 2, x < 1]
Out[37]= True
In[38]:= withSpecificRoot[x, p == 0, 2, 2, x < 1]
Out[38]= False

We can also compute relationships between roots like \sqrt{2}+\sqrt{3}=\sqrt{5+2\sqrt{6}}:

In[39]:= withSpecificRoot[sqrt6, sqrt6^2 == 6, 2, 2,
withSpecificRoot[lhs, lhs^2 == 5 + 2 sqrt6, 2, 2,
withSpecificRoot[sqrt3, sqrt3^2 == 3, 2, 2,
withSpecificRoot[sqrt2, sqrt2^2 == 2, 2, 2,
lhs == sqrt3 + sqrt2
Out[39]= True

That’s all I have time for now, but I hope to write another blog post on the subject soon!

Leave a comment

Filed under Uncategorized

A Logical Interpretation of Some Bits of Topology

Edit: These ideas are also discussed here and here (thanks to Qiaochu Yuan: I found out about those links by him linking back to this post).

Although topology is usually motivated as a study of spatial structures, you can interpret topological spaces as being a particular type of logic, and give a purely logical, non-spatial interpretation to a number of bits of topology.

This seems like one of those facts that was obvious to everyone else already, but I’ll write a quick blog post about it anyway.
Continue reading


Filed under Uncategorized

The Spectrum From Logic to Probability

Let \Omega be the set of propositions considered by some rational logician (call her Sue).  Further, suppose that \Omega is closed under the propositional connectives \vee, \wedge, \neg.  Here are two related but different preorders on \Omega:

  1. p\leq q if p logically entails q.
  2. p \preceq q if Sue considers q at least as likely to be true as p is.

Let \sim be the equivalence relation defined by p \sim q iff p \leq q \wedge q \leq p and let \approx similarly be defined by p \approx q iff p\preceq q\wedge q\preceq p.

Then we know what type of structure \Omega/{\sim} is: since we’re assuming classical logic in this article, it’s a Boolean algebra.  What type of structure is \Omega/{\approx}?

We can at least come up with a couple of examples.  Since Sue is a perfect logician, it must be that if p\leq q, then p\preceq q.  If Sue is extremely conservative, she may decline to offer opinions about whether one proposition is more likely to be true than another except when she’s forced to by logic.  In this case, \Omega/{\approx} is equal to \Omega/{\sim} and therefore again a Boolean algebra.

In the other extreme, Sue may have opinions about every pair of propositions, making \preceq a total ordering.  A principal example of this is where \Omega/{\approx} is isomorphic to a subset of [0,1] and Sue’s opinions about the propositions were generated by her assigning a probability P(p)\in [0,1] to every proposition p.

What’s in between on the spectrum from logic to probability?  Are there totally ordered structures not isomorphic to [0,1] or a subset? More ambitiously: every Boolean algebra has operations \vee, \wedge, \neg, while [0,1] has operations {+}, \times, (x\mapsto 1-x) which play similar roles in the computation of probabilities (note that + is partial on [0,1]).  How are these related and does every structure on the spectrum from logic to probability have analogous operations?

These structures (i.e., structures of the form \Omega/{\approx} for some acceptable \preceq in a sense to be defined below) were called scales and defined and explored in a very nice paper by Michael Hardy.

Continue reading


Filed under Uncategorized

Topology and First-Order Modal Logic

The normal square root function can be considered to be multi-valued.

Let’s momentarily accept the heresy of saying that the square root of a negative number is 0, so that our function will be total.

How can we represent the situation of this branching “function” topologically?

Continue reading

Leave a comment

Filed under Uncategorized

Two Interesting Observations about Voting I Hadn’t Seen Until Recently

By “voting”, I mean the following general problem:  Suppose there are n candidates and m voters.  Each voter produces a total ordering of all n candidates.  A voting procedure is a function which takes as input all m orderings, and produces an output ranking of all n candidates.  Arrow’s impossibility theorem states that there is really no satisfactory voting procedure when the number of candidates is greater than 2 (majority rule is a good voting procedure when there are two candidates).

Continue reading


Filed under Uncategorized

Quantish Physics: A Discrete Model of Quantum Physics

In the book Good and Real, author Gary Drescher, who received his PhD from MIT’s AI lab, defends the view that determinism is a consistent and coherent view of the world.   In doing so, he enters many different arenas: ethics, decision theory, and physics.

In his chapter on quantum mechanics, he defends the “many-worlds” interpretation (although he doesn’t think the term accurately describes the concept) versus the Copenhagen interpretation.  In the process of doing so, he does something I thought was extraordinary:  he comes up with a simple model of quantum mechanics in which all of the standard concepts you read about: the two-slit experiment, the Heisenberg uncertainty principle, etc., are represented.  This model requires no prerequisites from physics and actually uses almost totally discrete mathematics!

(Edit: I somehow missed this when originally writing this post, but Drescher also outlines quantish physics in an online paper.)

I’ll sketch it below.

Continue reading


Filed under Uncategorized

Functions with Very Low Symmetry and the Continuum Hypothesis

A function from \mathbb{R} to \mathbb{R} is called even if for all h\in\mathbb{R}, f(-h) = f(h).  We might call it even about the point x if, for all h\in\mathbb{R}, f(x-h) = f(x +h).

Conversely, we can call a function strongly non-even if for all x\in\mathbb{R}, h>0, f(x-h)\ne f(x+h).

Finding strongly non-even functions is easy, as any injective function provides a trivial example.  We can make things harder for ourselves by considering only functions from \mathbb{R} to \mathbb{N}.  But now, it is just as easy to show that there are no strongly non-even functions.

Therefore, let’s make the following definition: Let a function f\colon \mathbb{R}\to\mathbb{N} be non-even of order n if, for all x, |\{h>0\mid f(x-h) = f(x + h)\}|\leq n.  Thus, a strongly non-even function is non-even of order 0, and a function being non-even of order n implies that it’s non-even of order m for all m\geq n.

In this paper, the set theorists Peter Komjáth and Saharon Shelah proved:

The existence of a non-even function of order 1 is equivalent to the Continuum Hypothesis (i.e., the statement that 2^{\aleph_0} = \aleph_1).

Thus, if we assume that there is a non-even function of order 1, then we can conclude that 2^{\aleph_0} = \aleph_1.  Can we weaken the hypothesis and still conclude something interesting?  We can, as they also proved:

For any n, if there is a non-even function of order n, then 2^{\aleph_0}\leq \aleph_{\lceil\log_2{(n+1)}\rceil}.

Continue reading


Filed under Uncategorized

A Suite of Cool Logic Programs

You may have heard about the Tarski-Seidenberg theorem, which says that the first-order theory of the reals is decidable, that the first-order theory of the complex numbers is similarly decidable, or that the first order theory of the integers without multiplication is decidable.

In the course of John Harrison‘s logic textbook Handbook of Practical Logic and Automated Reasoning, all three of these algorithms (and many more) are implemented.  Furthermore, you can download and play with them for free.  (However, I still recommend checking out the book: especially if you are looking for a good textbook for a course on logic with a concrete, computational bent.)

Below, I’ll describe how to install the programs and try them out.  There are many more interesting functions in this suite that I haven’t described.

Continue reading


Filed under Uncategorized

An Interesting Puzzle in Propositional Logic

Suppose that you’re translating an ancient text, and in this text you come across three words whose meaning you are unsure of: \mathit{bal}, \mathit{kat}, and \mathit{lot}.  So, you head down to the ancient language department of your local university.

The first professor you come across, \hbox{Prof. Bal}, knows what \mathit{bal} means, the second professor you come across, \hbox{Prof. Kat}, knows what \mathit{kat} means, and the third professor you come across, \hbox{Prof. Lot}, knows what \mathit{lot} means.  So you have fortunately solved your problem.

But you’re now curious and decide to meet some other professors in the department.  The next professor you come across is named \hbox{Prof. }(\mathrm{Bal}\rightarrow\mathrm{Kat}).  He doesn’t know what \mathit{bal} means or what \mathit{kat} means, but if you told him what \mathit{bal} meant, he would be able to tell you what \mathit{kat} means (for example, maybe he knows that \mathit{kat} is the noun form of \mathit{bal}).

The next professor you meet is named \hbox{Prof. }(\mathrm{Bal}\rightarrow(\mathrm{Kat}\rightarrow\mathrm{Lot})).  If you told him what \mathit{bal} meant and what \mathit{kat} meant, he would be able to tell you what \mathit{lot} means.

The next professor you meet is named \hbox{Prof. }((\mathrm{Bal}\rightarrow\mathrm{Kat})\rightarrow\mathrm{Lot}).  If you told him a method for finding out the meaning of \mathit{kat} given the meaning of \mathit{bal}, he would be able to tell you the meaning of \mathit{lot}.

In general, for any two professors \hbox{Prof. }P and \hbox{Prof. }Q, there is a professor \hbox{Prof. }P\rightarrow Q with the property that if you told him what \hbox{Prof. }P knew, he would be able to tell you what \hbox{Prof. }Q knows (but \hbox{Prof. }P\rightarrow Q doesn’t know any more than that).

Notice that some professors have essentially the same state of knowledge.  For example, \hbox{Prof. Bal} and \hbox{Prof. }((\mathrm{Kat}\rightarrow\mathrm{Kat})\rightarrow\mathrm{Bal}) have essentially the same knowledge, since to get the meaning of \mathit{bal} out of \hbox{Prof. }((\mathrm{Kat}\rightarrow\mathrm{Kat})\rightarrow\mathrm{Bal}) you only have to tell him a method for finding out the meaning of \mathit{kat} given the meaning of \mathit{kat}, which is something that you can do without any particular special knowledge concerning \mathit{bal}, \mathit{kat} and \mathit{lot}.

A more nontrivial example is that \hbox{Prof. }(((\mathrm{Bal}\rightarrow\mathrm{Kat})\rightarrow\mathrm{Bal})\rightarrow\mathrm{Kat}) has the same state of knowledge as \hbox{Prof. }(\mathrm{Bal}\rightarrow\mathrm{Kat}).  This is because each can “simulate” the other.  In one direction, suppose somebody told \hbox{Prof. }(((\mathrm{Bal}\rightarrow\mathrm{Kat})\rightarrow\mathrm{Bal})\rightarrow\mathrm{Kat}) the meaning of \mathit{bal}.  He therefore knows a trivial “method” for getting the meaning of \mathit{bal} given any inputs, and so he knows the meaning of \mathit{kat}.  In the other direction, suppose we told \hbox{Prof. }(\mathrm{Bal}\rightarrow\mathrm{Kat}) a method for turning (methods for turning the meaning of \mathit{bal} into the meaning of \mathit{kat}) into the meaning of \mathit{bal}.  Well, \hbox{Prof. }(\mathrm{Bal}\rightarrow\mathrm{Kat}) knows a method for turning the meaning of \mathit{bal} into the meaning of \mathit{kat}, so he can use that find the meaning of \mathit{bal}.  He can then use his method a second time to turn that into the meaning of \mathit{kat}.

The puzzle is then to prove that there are only finitely many professors with different states of knowledge.

This puzzle is equivalent to showing that intuitionistic implicational propositional logic over three variables has only finitely many logically inequivalent formulas.  Another formulation is: Let \mathbb{C}_n be the free cartesian closed category over n objects.  Given objects A and B\in \mathbb{C}_n, say that A and B are equivalent if there is an arrow from A to B and an arrow from B to A.  Then there are only finitely many equivalence classes in \mathbb{C}_3.  (The corresponding statements are also true with 3 replaced by n.)

Continue reading

Leave a comment

Filed under Uncategorized

What Happens When You Iterate Gödel’s Theorem?

Let \mathrm{PA} be Peano Arithmetic.  Gödel’s Second Incompleteness Theorem says that no consistent theory T extending \mathrm{PA} can prove its own consistency. (I’ll write \mathrm{Con}(T) for the statement asserting T‘s consistency; more on this later.)

In particular, \mathrm{PA} + \mathrm{Con}(\mathrm{PA}) is stronger than \mathrm{PA}.  But certainly, given that we believe that everything \mathrm{PA} proves is true, we believe that \mathrm{PA} does not prove a contradiction, and hence is consistent.  Thus, we believe that everything that (\mathrm{PA} + \mathrm{Con}(\mathrm{PA})) proves is true.  But by a similar argument, we believe that everything that (\mathrm{PA} + \mathrm{Con}(\mathrm{PA} + \mathrm{Con}(\mathrm{PA}))) proves is true.  Where does this stop?  Once we believe that everything \mathrm{PA} proves is true, what, exactly, are we committed to believing?

Continue reading


Filed under Uncategorized

Trigonometric Series and the Beginnings of Set Theory

Let f\colon\mathbb{R}\to\mathbb{R} be a 2\pi-periodic function. It may or may not have a representation as a trigonometric series

\displaystyle{a_0+\sum_{n=1}^\infty a_n\sin(nx) + b_n\cos(nx)}

A natural question to ask is whether or not the representation of f as a trigonometric series is unique, if it has one. It was the consideration of this question that led Cantor to the invention of set theory.

There is a nice writeup of this story in the first part of this article by Alexander Kechris. I’ll give part of the story below.

Continue reading


Filed under Uncategorized

A Simple Introduction to Quantum Groups

In the course of reading some background material for an article by James Worthington on using bialgebraic structures in automata theory, I was led to finally reading up on what a Hopf algebra (sometimes called a “quantum group“) is.

Although it is not strictly related to logic, I’ll write up what I learned here.

Continue reading

1 Comment

Filed under Uncategorized

Doing Calculus on the Rationals (with the help of Nonstandard Analysis)

Nonstandard Analysis is usually used to introduce infinitesimals into the real numbers in an attempt to make arguments in analysis more intuitive.

The idea is that you construct a superset \mathbb{R}^* which contains the reals and also some infinitesimals, prove that some statement holds of \mathbb{R}^*, and then use a general “transfer principle” to conclude that the same statement holds of \mathbb{R}.

Implicit in this procedure is the idea that \mathbb{R} is the real world, and therefore the goal is to prove things about it. We construct a field \mathbb{R}^* with infinitesimals, but only as a method for eventually proving something about \mathbb{R}.

We can do precisely the same thing with \mathbb{Q} instead of with \mathbb{R}. But, in Weak Theories of Nonstandard Arithmetic and Analysis, Jeremy Avigad observed that if we don’t care about transferring the results back down to \mathbb{Q}, then we can get all the basic results of calculus and elementary real analysis just by working with \mathbb{Q}^*, and without ever having to construct the reals.

Continue reading


Filed under Uncategorized

Games Which are Impossible to Analyze

In the last post, I mentioned the computational complexity of various games. To be explicit, we consider each “game” G to actually be a sequence of games \{G_n\} for n\in \mathbb{N}. For example, \text{checkers}_n would be checkers played on an n\times n board. The problem was then to analyze the computational complexity of the function which takes n and tells you which player has a winning strategy and what the winning strategy is. I’ll call that function the analysis function of G.

Are there any games which can actually be played in the real world with an undecidable analysis function? Robern Hearn, in the same thesis that I linked to last time, showed that the answer is yes.

Continue reading

Leave a comment

Filed under Uncategorized

How to Show that Games are Hard

Peg Solitaire is a pretty popular game, often found in restaurants (including Cracker Barrel, if I remember correctly). It’s also NP-complete (by which I mean determining a winning strategy given the initial set-up is an NP-complete problem). You may have also heard of computational complexity results for Minesweeper (see here, for example). There are a number of other results showing that various popular games are complete for some complexity class.

But what if you come across a new game, which no computer scientist has heard of yet? Well, you’re in luck, as Robert Hearn, in his thesis, formulated a framework called Constraint Logic intended to make it easy to prove complexity results for games.

Continue reading


Filed under Uncategorized

When are the Real Numbers Necessary?

The natural numbers can all be finitely represented, as can the rational numbers. The real numbers, however, cannot be so represented and require some notion of “infinity” to define. This makes it both computationally and philosophically interesting to determine for what purposes you need the real numbers, and for what purposes you need only the rationals.

It’s pretty clear that spatial concepts having to do with distances and rotation require the real numbers. For example, if we took \mathbb{Q}^2 as our model of the plane, the distance from (0,0) to (1,1) would not be rational, and we would not be able to rotate the point (1,0) about the point (0,0) by most angles.

But I always implicitly thought that spatial notions not depending on distances or angles required only the rationals. It turns out that I was wrong: there are spatial notions not depending on distances or angles which differ depending on whether you take space to be \mathbb{Q}^n or \mathbb{R}^n. The fact that I was wrong follows from a theorem of Micha Perles which is very famous in combinatorics, but which I only found out about recently.

Continue reading


Filed under Uncategorized

Playing Games in the Transfinite: An Introduction to “Ordinal Chomp”

Chomp is a two-player game which is played as follows: The two players, A and B, start with a “board” which is a chocolate bar divided into n \times m small squares. With Player A starting, they take turns choosing a square and eating it together with all squares above and to the right. The catch is that the square at the lower left-hand corner is poisonous, and the player who is forced to eat it loses.

This image from the Wikipedia article shows a typical sequence of moves for a 5\times 3 chocolate bar:

At this point, Player A is forced to eat the poisoned square and hence loses the game.

Although the question of what the winning strategies are for this game is very much an open problem, the question of who has a winning strategy is not: On the 1\times 1 board, Player B wins (since Player A must eat the poison piece on his first move). But for any other board, Player A has a winning strategy.

To see why, suppose not. Then if Player A’s first move is to eat just the one square in the top right-hand corner, Player B must have a winning response (since we are supposing that Player B has a winning response to any move that Player A makes). But if Player B’s response is winning, then Player A could have simply made that move to start with.

However, suppose we play Chomp not just on n\times m boards, but on \alpha\times\beta boards, where \alpha and \beta are arbitrary ordinals. The game still makes sense just as before, and will always end in finite time, but Player A no longer wins all of the time (there will no longer be a top right-hand corner square if either \alpha or \beta is a limit ordinal).

Scott Huddleston and Jerry Shurman investigated Ordinal Chomp in this paper, and showed that it has a number of interesting properties. I’ll describe a few of them below.

Continue reading


Filed under Uncategorized

Avoiding Set-Theoretic Paradoxes using Symmetry

Intuitively, for any property P(x) of sets, there should be a set \{x \mid P(x)\} which has as its members all and only those sets x such that P(x) holds. But this can’t actually work, due to Russell’s Paradox: Let b = \{x\mid x\notin x\}, and then you can derive a contradiction from both b\in b and b\notin b.

The standard solution to this is essentially to forbid the construction of any set which is too big. This solves the problem since you can prove that there are many sets which are not members of themselves, making b too big to be a set. But you also end up throwing out many sets which you might want to have: for example, the set of all sets, the set of all groups, etc.

Randall Holmes recently published a paper espousing another solution: instead of forbidding the construction of sets which are too big, forbid the construction of sets which are too asymmetric. Details below.

Continue reading

1 Comment

Filed under Uncategorized

The Undecidability of Identities Involving Sine, Exponentiation, and Absolute Value

In the book A=B, the authors point out that while the identity

\displaystyle{\sin^2(|10 + \pi x|) + \cos^2(|10 + \pi x|) = 1}

is provable (by a very simple proof!), it’s not possible to prove the truth or falsity of all such identities. This is because Daniel Richardson proved the following:

Let \mathcal{R} denote the class of expressions generated by

  1. The rational numbers, and \pi.
  2. The variable x
  3. The operations of addition, multiplication, and composition.
  4. The sine, exponential, and absolute value functions.

Then the problem of deciding whether or not an expression E in \mathcal{R} is identically zero is undecidable. This means as well that the problem of deciding whether or not two expressions E_1, E_2\in \mathcal{R} are always equal is also undecidable, since this is equivalent to deciding if E_1 - E_2 = E_1 + (-1)\cdot E_2 is identically zero.

A summary of Richardson’s proof (mostly from Richardson’s paper itself) is below.

Continue reading


Filed under Uncategorized

A Geometrically Natural Uncomputable Function

There are many functions from \mathbb{N} to \mathbb{N} that cannot be computed by any algorithm or computer program. For example, a famous one is the halting problem, defined by f(n) = 0 if the nth Turing machine halts and f(n) = 1 if the nth Turing machine does not halt. Another one in the same spirit is the busy beaver function.

We also know a priori that there must be uncomputable functions, since there are 2^{\aleph_0} functions from \mathbb{N} to \mathbb{N} but only \aleph_0 computer programs. But that is nonconstructive, and the two examples I gave above seem a bit like they’re cheating since their definitions refer to the concept of computability. Is there a natural example of an uncomputable function that does not refer to computability?

In this paper, Alex Nabutovsky found what I think is a great example of such a function from geometry. Details below.

Continue reading


Filed under Uncategorized

Integrability Conditions (Guest Post!)

Please enjoy the following guest post on differential geometry by Tim Goldberg.

A symplectic structure on a manifold M is a differential 2-form \omega satisfying two conditions:

  1. \omega is non-degenerate, i.e. for each p \in M and tangent vector \vec{u} based at p, if \omega_p(\vec{u},\vec{v}) = 0 for all tangent vectors \vec{v} based at p, then \vec{u} is the zero vector;
  2. \omega is closed, i.e. the exterior derivative of \omega is zero, i.e. \mathrm{d} \omega = 0.

In trying to come up with answers to questions like “what do you do?” and “what is symplectic geometry?” that would be accessible to an advanced undergraduate or beginning graduate student, I’ve tried to come up with fairly intuitive descriptions of what the two symplectic structure conditions really mean.

Non-degeneracy is pretty easy, because my intended audience is certainly familiar with the dot product in Euclidean space, and probably familiar with more general machinery like inner products and bilinear forms. A bilinear form on a vector space over a field \mathbb{F} is just an assignment of a number in \mathbb{F} to each pair of vectors, in such a way that the assignment is linear in each vector in the pair. A bilinear form is called non-degenerate if the only thing that pairs to zero with every single vector is the zero vector. A 2-form on M is a collection \omega = \{ \omega_p \mid p \in M \} of skew-symmetric bilinear forms, one for each tangent space of M. Saying that \omega is non-degenerate is saying that each of these bilinear forms is non-degenerate.

It’s much less clear how to describe to the uninitiated what the closed condition means. It’s even a bit unclear why this condition is required in the first place. A pretty nice answer came up yesterday, in a reading group I attend that is trying to learn about generalized complex structure. We are going through the PhD thesis of Marco Gualtieri, titled “Generalized Complex Geometry”. It is available at the following websites:

This was the first meeting, and Tomoo Matsumura was the speaker. He suggested that the requirement that \mathrm{d} \omega = 0 is an integrability condition. I had never thought of it this way, but I probably will from now on.
Continue reading

Leave a comment

Filed under Uncategorized

Lots of Fun Math Papers

In the course of looking up a link for my last blog entry, I discovered the MAA Writing Awards site, which collects many pdfs of articles that have won MAA writing awards.  From browsing it a bit, it seems to be a goldmine of fun math articles.

Leave a comment

Filed under Uncategorized

Non-Rigorous Arguments 1: Two Formulas For e

I’m a big fan of non-rigorous arguments, especially in calculus and analysis. I think there should be a book cataloging all the beautiful, morally-true-but-not-actually-true proofs that mathematicians have advanced, but until that time I’ll try to at least catalog a few of them on my blog.

This first one is Euler’s original argument for the equality of two expressions (both of which happen to define e):

\displaystyle{\sum_{n=0}^\infty \frac{1}{n!} = \lim_{n\to\infty}\left(1 + \frac{1}{n}\right)^n}

I’ll also sketch how this can be made rigorous in non-standard analysis.

Continue reading


Filed under Uncategorized

A Curious Application of Ambiguity with Respect to the Possessive Form

Why did the chicken cross the island on Lost?

Continue reading

Leave a comment

Filed under Uncategorized

Almost a Number-Theoretic Miracle

An arithmetic statement is one made up of quantifiers “\forall n\in\mathbb{N},” “\exists n\in \mathbb{N},” the logical connectives “and,” “or,” “not”, function symbols \times, +, constants {0}, 1, and variables n which are bound by the aforementioned quantifiers.

It is known that there is no algorithm which will decide whether or not an arithmetic statement is true or not. This shouldn’t be surprising, since if there were such an algorithm, it would be able to automatically prove Fermat’s Last Theorem, settle Goldbach’s Conjecture and the Twin Prime Conjecture, etc.

However, if we call a quasi-arithmetic statement one which uses the quantifiers “for all but finitely many n \in\mathbb{N}” (denoted “\forall^\infty n\in\mathbb{N}”) and “there exists infinitely many n\in\mathbb{N}” (denoted “\exists^\infty n\in\mathbb{N}”) instead of “\forall n\in\mathbb{N}” and “\exists n\in\mathbb{N}”, then we do have an algorithm for deciding whether a quasi-arithmetic statement is true or not!

Continue reading


Filed under Uncategorized