This sandbox is intended for saving drafts of long, complex posts, especially posts whose composition takes a long time. It serves to localize to one thread the front-page "bumps" caused by edits to drafts of such posts, so that they may be easily ignored. Also, it helps to guard against losing longly-composed posts due to system crashes.

When you are happy with your draft here, you may simply copy the code and paste it to the desired location.

Proper Use of the Sandbox

  1. Do not post a new answer! We wish all the answers on this page to be owned by the Community user (so that only a non-sentient bot is informed of edits to these answers). Posting a new answer will make you the owner, meaning that you will be notified whenever another user makes an edit to that answer.

    The sandbox has been "wiki locked" to prevent the creation of new answers. There are more than enough existing answers for users to edit over, and this will greatly reduce the frequency at which we request that the answers be disassociated from specific users.

  2. Do not delete answers! Deleting seems like a reasonable option, but there are no "hard deletions" on Stack Exchange, and users with sufficient privileges will still see your supposedly deleted postings. Deleted answers will be undeleted and cleared for the use of others.

  3. Do look for an answer which indicates that it is free and then edit it to your heart's content. If none appears available, take over the one that has been left unchanged the longest (which will appear at the bottom of the page if you order answers by "activity").

  4. Do not expect your draft to remain untouched for days. There are no guarantees that your draft will be the latest revision if you return days later. While users will try not to step over others' toes, it may happen that an unfinished draft is edited out. Your draft will, however, still exist as a revision of the answer it was made in. If your drafting is expected to take place over a longer period of time, either

    • take note of the URL of the answer provided by clicking the share button, or
    • save a copy of your draft locally (or even "in the cloud").
  5. Do clear your draft when you are finished. This includes removing all $\LaTeX$ from your answers. Replacing all code with a simple statement like

    This answer is free for anyone to use

    is sufficient. Periodically users may go through and free up answer slots that have not been edited in, say, over one month. But you can aid in the smooth running of this sandbox by clearing away your drafts when you are finished with them.

  6. Do not "claim" multiple answers concurrently. Since this post is closed, the answers are a limited resource. If you really must compose several long, complex posts at the same time, you can still use a single answer, separating the different drafts using Markup: horizontal rules (---) and/or headings (# Header 1 #) are natural choices.

  7. Do not create new such sandboxes. The point of having a unique such sandbox is that it minimizes the noise on the front page when the sandbox is edited. If there were multiple sandboxes they will frequently occupy numerous front page slots, pushing other topics off the front page, and increasing noise.

  • 8
    $\begingroup$ I have added a [sandbox] tag to allow people ignore it more easily (via software support of ignoring tags), and since it seems that we have two sandboxes now, a tag may seem a bit more in place here. $\endgroup$ – Asaf Karagila Jul 18 '12 at 8:35
  • 21
    $\begingroup$ (+1) For thinking outside the (sand)box. $\endgroup$ – cardinal Jul 18 '12 at 19:40
  • 14
    $\begingroup$ At the suggestion of the moderators, I have gone and changed the associated owners of all the answers here to the Community user. This way, the original owners will not receive excess pings for each time another user uses the draft space for their work. Enjoy! $\endgroup$ – Grace Note Oct 5 '12 at 14:45
  • 3
    $\begingroup$ To prevent crashes I've found the "Bookmarks to disable/enable MathJax", provided in here, pretty useful. $\endgroup$ – leo Dec 17 '12 at 18:03
  • 3
    $\begingroup$ PSA: Between the creation of this sandbox (in July 2012) and today (December 2015), technology has advanced. Something like StackEdit (or others, it's simply the only one I know) essentially solves all the limitations of this sandbox. You can have multiple concurrent drafts, you don't have to worry about polluting meta's front page, you can leave your draft untouched for days and expect it to still be there, you don't have to explicitly clear up your draft when you're done... Maybe someday we can get rid of this outdated crutch. $\endgroup$ – Najib Idrissi Dec 2 '15 at 14:07

17 Answers 17


This question is free for all to use


$$ b= {ra + s \over 2^A} \\ c= {rb + s \over 2^B} = a\\ $$ $$ b\cdot a = {ra + s \over 2^A}\cdot {rb + s \over 2^B} \\ 2^S = (r+{s \over a})\cdot (r+{ s \over b} ) \\ {2^S\over r^N} = (1+{s \over ra})\cdot (1+{ s \over rb} ) $$ $$ S \log2-N \log r = \log(1+{s \over ra})+\log(1+{ s \over rb}) \\ S \log2-N \log r \lt {s \over ra}+{ s \over rb} = {s\over r}({1 \over a}+{1 \over b}) $$ let $a_h$ be the harmonic mean of $a$ and $b$, then one of the values $a$ and $b$ must be smaller than $a_h$ and one larger. Let $a \lt a_h$ then $a_h$ is an upper bound for $a$ and we have $$ (a \lt ) \qquad a_h \lt {s\over r}{1 \over S \log2-N \log r} \\ $$ Because the denominator on the rhs is not "small" the value for $a_h$ and $a$ on the lhs cannot be "large", and indeed it is possible to find an upper bound for $a_h$ depending on $N$, $s$, and $r$ using the known results of Baker and the improvements of the lower bounds for $S \log 2 - N \log r$ found so far.


This answer is available for anyone to use.


This question is free for all to use


Question title: Infinite disjunction in FOL

In the language of first order logic (FOL), is it possible to include an infinitely long disjunction, such as (1)?

\begin{equation}\tag{1}a_1\lor a_2\lor a_3\lor\dots\end{equation}

Self answer:

Suppose that an infinitely long disjunction (1) exists.

\begin{equation}\tag{1}a_1\lor a_2\lor a_3\lor\dots\end{equation}

Then consider an infinite collection of formulae (2), consisting of the negation of each instance of the disjunction.

\begin{equation}\tag{2}\{\lnot a_1,\lnot a_2,\lnot a_3,\dots\}\end{equation}

A theory $T$ consisting of (1) and all the formulae in (2) will necessarily be unsatisfiable, as each negated propositional atom $a_i$, cannot be satisfied unless the atom is false, which implies that the infinite disjunction is false.

However, every finite subset of formulae in $T$ will be satisfiable, (e.g. $\lnot a_1\land(a_1\lor a_2\lor a_3\lor\dots)$), so by compactness, the set comprising all formulae in the theory will be satisfiable.

This is a contradiction, so it is not the case that an infinite disjunction can be defined in FOL.

Regarding our previous discussion, I have one more question. I was able to show that there is no infinite disjunction by using the concept of an infinite set of formulae. However, I now have a problem with said infinite set of formula.

Consider that there exists an infinite set of formula comprising of the negation of a property for every name in the language, and that we have a name for every object in the language: $\{\lnot P_1,\lnot P_2,\dots\}$ (1 of 6).

Then consider those same formula in a theory $T$, which also contains the sentence $\exists x P_x$. (2 of 6).

Now each propositional atom cannot be satisfied unless that atom is false, so it cannot be the case that $\exists x P_x$ is true (3 of 6).

However, by compactness, since each finite subset is satisfiable, the whole thing is. (4 of 6).

This is a contradiction, so it must not be the case that we can consider an infinite set of formulae comprising of the negation of a property for every name in the language (5 of 6).

My question regarding this is, is the proof correct, and if so, why was an infinite set of formulae considered in the proof of inexpressibility? (6 of 6)


Since $P$ is a quadratic polynomial and $P(0) = 0$, one can write $$ P(q) = aq+ bq^2$$ for some real numbers $a, b$. The conditions $$P'(\bar{q}_P)+\bar{q}_P=1, \frac{P(\hat{q}_P)}{\hat{q}_P}+\hat{q}_P=1$$ translates to \begin{align*}\tag{1} a + (2b+1) \bar q_P &= 1, \\ a+ (b+1) \hat q_P &= 1 \end{align*} or $$ \bar q_P = \frac{1-a}{2b+1}, \ \ \hat q_P = \frac{1-a}{b+1}.$$ We will assume that our conditions are that $\bar q_P ,\hat q_P>0$ instead of $\ge 0$ (when one of them is zero, $J(P) = 0$. Thus it suffices to check that the maximum of $J$ is positive, which we will do later).

The above conditions together with (1) imply that $b\neq -1$ and $b\neq -1/2$.

Next, note that $\bar q_P = \hat q_P$ only when $a=1$. The lines $$ a=1, \ \ b=-1, \ \ b = -1/2$$ split the $a-b$ plane into six region. Only two of them $$R_1 = \{a<1, b>-1/2\}, \ \ R_2 = \{ a>1, b<-1\}$$ gives BOTH positive $\bar q_P, \hat q_P$.

In each region either $q^*_P = \bar q_P$ or $\hat q_P$. For example, in $R_1$ we have $\hat q_P > \bar q_P$, giving $q^*_P = \bar q_P$.

Then one can check in each region: For example in $R_1$,

\begin{align*} J(aq+ bq^2) &= \int_0^{\frac{1-a}{2b+1}} (a+2bq-c)(1+q-\lambda (a+bq)-(1-\lambda)(a+2bq))dq \\ &=\int_0^{\frac{1-a}{2b+1}} (a+2bq-c)(1+q-(a+bq)+\lambda bq)dq \\ &=\int_0^{\frac{1-a}{2b+1}} (a-c+2bq)(1-a +(1 +(\lambda -1)b)q) dq \\ &=\int_0^{\frac{1-a}{2b+1}} \bigg(a(1-a) + \big(2(1-a)b +a(1 +(\lambda -1)b) \big)q + 2b(1 +(\lambda -1)b)q^2\bigg) dq\\ &= \frac{a(1-a)^2}{2b+1} + \frac{2(1-a)b +a(1 +(\lambda -1)b)}{2(2b+1)^2} \end{align*}


This space is available for anyone


This answer is available for anyone to use.


this box is free for anyone to use


This slot is available for anyone


this slot is available for anyone


Let's prove, without using any set theory, that the natural numbers are the natural numbers!

Specifically, we're going to show that the natural numbers, defined as the inductive data type generated by one constant and one unary operation, are the natural numbers, defined as the free monoid with one generator. We'll do this by sheer symbol manipulation, without recourse to any underlying foundational theory.

Starting definitions

Define a general presentation as an algebraic theory. When we talk about general presentations, we are interested in the initial algebra of the underlying theory, and we call it the algebra presented by that presentation. Given two general presentations $P$ and $Q$, we say that $Q$ is a conservative extension of $P$ if every axiom (that is, every term (generator) and every equation) of $P$ is also an axiom of $Q$, and the algebras generated by $P$ and $Q$ are isomorphic (when considered as algebras for the underlying theory of $P$).

$\newcommand{Nat}{\mathbb{N}}\newcommand{Nind}{\Nat_\mathrm{ind}}\newcommand{Nmon}{\Nat_\mathrm{mon}}$In order to show that "the natural numbers are the natural numbers", we will consider two general presentations $\Nind$, representing the first definition of the natural numbers, and $\Nmon$, representing the second, and we will show that there is a third general presentation, $\Nat_\mathrm{ind+mon}$, which is a conservative extension of both.

First, here is $\Nind$:

  • $\newcommand{Zero}{\mathrm{Zero}}\Zero : \Nat$
  • $\newcommand{PlusOne}{\mathrm{PlusOne}}\PlusOne : \Nat \to \Nat$

In other words, $\Nind$ consists of a generator (or term) called $\Zero$ of arity zero; a generator called $\PlusOne$ of arity one; and no equations.

The general presentation $\Nmon$ is more complex. Here it is:

  • $\Zero : \Nat$
  • $\newcommand{Plus}{\mathrm{Plus}}\Plus : \Nat \times \Nat \to \Nat$
  • $\newcommand{One}{\mathrm{One}}\One : \Nat$
  • $\Plus(\Zero, x) = x$
  • $\Plus(x, \Zero) = x$
  • $\Plus(x, \Plus(y, z)) = \Plus(\Plus(x, y), z)$

The general presentation $\Nmon$ consists of three generators (two of arity 0, one of arity 2) and three equations. Notice that the axioms of $\Nmon$, aside from $\One$, are simply the axioms of a monoid. Adding $\Nmon$ to the general presentation turns it into a presentation of a monoid with one generator.

How can we prove things?

Now, before we continue, here's a question: how can we identify conservative extensions of $\mathbb{N}_\mathrm{ind}$ without recourse to an underlying foundational theory?

Well, the Tietze transformations are a collection of rules for transforming a group presentation into another equivalent group presentation. The new group presentation is equivalent in the sense that the group generated by the new presentation is isomorphic to the group generated by the old presentation, and, furthermore, the isomorphism preserves any generators which were not affected by the transformation.

There are four Tietze transformations:

  • Adding a generator: You may add a generator, along with an equation asserting that the new generator equals some term.
  • Removing a generator: If an equation asserts that some generator equals some term, and that generator does not appear in the right-hand side of that equation, or anywhere in any other equation, then you may remove that generator and that equation.
  • Adding an equation: You may add an equation, if you can prove that equation from the other equations.
  • Removing an equation: You may remove an equation, if you can prove that equation from the other equations.

For the purposes of adding and removing an equation, a proof is not allowed to refer to outside axioms, or even to use first-order logic; the proof must be performed entirely using the substitution and reflexive properties of equality.

The Tietze transformations work just fine for general presentations, too. Specifically, if one applies the "add a generator" or "add an equation" transformation to a general presentation, the new presentation will be a conservative extension of the old one. If one applies the "remove a generator" or "remove an equation" transformation, the converse happens: the new presentation will be conservatively extended by the old one.

Given an underlying theory such as ZFC, hopefully the assertions I made in the above paragraph would not be too difficult to prove. For now, we simply take the four transformations as axioms.

The Tietze transformations will get us part of the way where we want to go, but in order to go the entire way, we will need to use two additional transformations:

  • Adding a function: You may add a function, along with a collection of equations which constitute a primitive recursive definition of that function.
  • Removing a function: You may perform the reverse of adding a function.

There will be an example of just what I mean by this below.

In addition, inductive proofs of equality will be permitted. I apologize for not giving a definition of what constitutes an inductive proof of equality.

The proof

We now have all we need to show that there is a general presentation $\Nat_{\mathrm{ind+mon}}$ which is a conservative extension of both $\Nind$ and $\Nmon$.

We start with $\Nind$, which consists of only these two axioms:

  1. $\Zero : \Nat$
  2. $\PlusOne : \Nat \to \Nat$

We will now apply the "adding a function" transformation. We add a function symbol and two equations:

  1. $\Plus : \Nat \times \Nat \to \Nat$
  2. $\Plus(\Zero, y) = y$
  3. $\Plus(\PlusOne(x), y) = \PlusOne(\Plus(x, y))$

Notice that the definition of $\Plus$ is by cases, and the cases are perfectly exhaustive: every possible pair of terms of $\Nind$ fits exactly one of the cases. Furthermore, although the definition of $\Plus$ is recursive, the recursion is primitive recursion.

We now desire to apply the "adding an equation" transformation:

  1. $\Plus(x, \Zero) = x$

This can be proven inductively by noting that $\Plus(\Zero, \Zero) = \Zero$ and $\Plus(\PlusOne(x), \Zero = \PlusOne(\Plus(x, \Zero)) = \PlusOne(x)$.

We apply the "adding an equation" transformation again:

  1. $\Plus(x, \Plus(y, z)) = \Plus(\Plus(x, y), z)$

Once again, we can do a proof by induction, noting that $\Plus(\Zero, \Plus(y, z)) = \Plus(y, z) = \Plus(\Plus(\Zero, y), z)$ and that

$$\Plus(\PlusOne(x), \Plus(y, z)) = \PlusOne(\Plus(x, \Plus(y, z))) = \PlusOne(\Plus(\Plus(x, y), z)) = \Plus(\PlusOne(\Plus(x, y)), z) = \Plus(\Plus(\PlusOne(x), y), z).$$

Next, we apply the "adding a generator" transformation:

  1. $\One : \Nat$
  2. $\One = \PlusOne(\Zero)$

Finally, we apply the "adding an equation" transformation again:

  1. $\PlusOne(x) = \Plus(\One, x)$

We have created a general presentation with 10 axioms which is a conservative extension of $\Nind$. This general presentation is called $\Nat_\mathrm{ind + mon}$.

Next, it only remains to show that $\Nat_\mathrm{ind + mon}$ is a conservative extension of $\Nmon$ as well. In order to do this, we will start by listing the axioms of $\Nat_\mathrm{ind + mon}$ again, but in a different order:

  1. $\Zero : \Nat$
  2. $\Plus : \Nat \times \Nat \to \Nat$
  3. $\One : \Nat$
  4. $\Plus(\Zero, y) = y$
  5. $\Plus(x, \Zero) = x$
  6. $\Plus(x, \Plus(y, z)) = \Plus(\Plus(x, y), z)$
  7. $\PlusOne : \Nat \to \Nat$
  8. $\PlusOne(x) = \Plus(\One, x)$
  9. $\Plus(\PlusOne(x), y) = \PlusOne(\Plus(x, y))$
  10. $\One = \PlusOne(\Zero)$

Equation 10 can be proven from the other equations: $\One = \Plus(\One, \Zero) = \PlusOne(\Zero)$. So we may remove it.

Next, equation 9 can also be proven from the other equations: $\Plus(\PlusOne(x), y) = \Plus(\Plus(\One, x), y) = \Plus(\One, \Plus(x, y)) = \PlusOne(\Plus(x, y))$. So we may remove it as well.

At this point, only axioms 1 through 8 remain. We can use the "removing a function" rule to remove axioms 7 and 8, leaving only axioms 1 through 6. These axioms are $\Nmon$.

This completes the proof that both $\Nind$ and $\Nmon$ are both conservatively extended by a single presentation $\Nat_\mathrm{ind + mon}$.

To restate, we have shown that the natural numbers, defined as the inductive data type generated by one constant and one unary operation, are the natural numbers, defined as the free monoid with one generator.

The question

Surely I'm not the first person to think of all this.

Has anyone studied these "generalized Tietze transformations" before? How powerful are they? Are they sufficiently powerful to prove, say, the fundamental theorem of arithmetic? (We would do that by showing that the positive integers, as usually defined, are isomorphic to the free monoid on countably infinitely many generators, with the monoid operation being multiplication.)


This answer is available for anyone to use.


This answer is available for anyone to use.


This slot is available for anyone


This slot is available for anyone


$$2^S-3^N =3^{N-1}(1/a+1/b+...+1/h) +.... \geq 2^S/ 2^{S/10/l2} \\ 1- 3^N/2^S \geq e^{-S/10} \\ 1-e^{-S/10} \geq 3^N/2^S \\ \log(1-e^{-S/10}) \geq N \log(3) - S \log(2) $$

$$2^S-3^N \geq 2^S e^{-S/10} \\ 1- 3^N/2^S \geq e^{-S/10} \\ 1-e^{-S/10} \geq 3^N/2^S \\ \log(1-e^{-S/10}) \geq N \log(3) - S \log(2) $$ $$|2^S-3^N| \geq 2^S e^{-S/10}= 1.808^{S}$$

You can use Ellison’s estimate, $$|2^S-3^N| \geq 2^S e^{-S/10}= 1.808^{S}$$, which holds for $S \geq 12$ with $ S \neq 13, 14, 16, 19, 27$ and all $N$.
This is based on results by Pillai and Baker. Reference: “WJ Ellison, On a theorem of S. Sivasankaranarayana Pillai, S´eminaire de th´eorie des nombres de Bordeaux, 1970 (1971), pp. 1–10.”


You must log in to answer this question.