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 answer is free for anyone to use


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*}


Question title: Can we name every object in every model of a first order theory?

Is it possible to name every object in every model of any first order (FO) theory? I would like this question to be answered using Tarskian semantics, where names refer to objects external to the logic.

This is a self answer question.

Self answer:

Consider that we have a name for every object, in every model of any first order theory.

Since we have a name for every object, consider an infinite set of formulae comprising of a property for every name in the language $(1)$:

\begin{equation}\tag{1}\{\lnot P_1,\lnot P_2,\lnot P_3\dots\}\end{equation}

Then consider those same formula in a theory $T$, which also contains the sentence $(2)$.

\begin{equation}\tag{2}\exists x \lnot P_x\end{equation}

Now each propositional atom cannot be satisfied unless that atom is false, so it cannot be the case that $\exists x \lnot P_x$ is true.

However, by compactness, since each finite subset is satisfiable, the whole thing is.

This is a contradiction, so it must not be the case that for any particular first order theory, that we can have a name for every object, in every model of it.

A question I want to ask: What is the recursive definition of $\vDash$?

When reasoning about FOL, satisfaction is often brought up. If a sentence $X$ is satisfiable (written by some authors as $X\nvDash$), then there is at least one interpretation where it is true. If $A$ satisfies $B$ ($A\vDash B$), then an interpretation which satisfies $A$ is also one which satisfies $B$.

After a conversation in the logic chat room, I was made aware of a recursive definition of $\vDash$. However I cannot find this definition after searching for it on Math S.E. or Google.

I am asking for a reference where this recursive definition is given, or an explanation of what it is and how it works in an answer.

What is precisely the logical problem which Karnaugh map solves?

In propositional logic, what is precisely the logical problem which Karnaugh map method solves?

K-maps do not solve any particular problem in propositional logic. They are used for circuit design. Propositional logic is distinct from the logic of Boolean circuits, because there is the added structure of a formal proof system.

K-maps are a visual aid used to simplify formulas. You circle the sections of the map you think will make the formula simpler, which usually involves circling the most objects at once.

They do not guarantee the simplest formula.

Specifically, what are the inputs and outputs of K-map method?

The input is any formula in Boolean algebra. The output is another formula in Boolean algebra.

Specifically can K-map simplify all formulas, or just some? What kinds of formulas can K-map simplify?

A K-map cannot simplify formulas which are already as simple as possible. For instance, it cannot simplify the formula $A$.

Does K-map guarantee that the resulted formula must be logically equivalent to the input formula?


What (normal) form does K-map simplify a formula into?

It doesn't have one. A k-map can 'simplify' into anything at all, so long as you know what the connectives mean. The output of a k-map for a given input is not unique.

Usually though, a people use k-maps to make Boolean circuits different.

Does K-map guarantee that the resulted formula must be completely in terms of some complete set of connectives? (e.g. any of {¬,∨},{¬,∧},{¬,∨,∧},…

No it doesn't. Placing $A$ on a k-map could result in $A$, which contains none of the connectives you mentioned. It is still possible to write $A\land(A\lor\lnot A)$ from the same k-map, but this isn't guaranteed.

K-map is said to convert a formula into some minimal or least complicated form. What is the criterion for measuring complexity of a formula?

A k-map doesn't necessarily convert to the simplest form.


First I will define the metric on Iso(M)

Let $M$ be a finite dimensional Riemannian manifold and $\operatorname{Iso}(M)$ be its set of isometries. It can be shown that $\operatorname{Iso}(M)$ is a finite dimensional manifold with a metric as defined below:

Consider $(n + 1)$ points on $M$ so close together that $n$ of them lie in an normal neighborhood of the other, and if the points are linearly independent (i.e. not in the same $(n-1)$-dimensional geodesic hypersurface). Then the distance $d(f, \tilde f)$ between two isometries $f$ and $\tilde f$ will be defined as the maximum of the distance $d_i[f(x), \tilde f(x)]$ as $x$ ranges over the given set of $n+1$ points. This distance can be shown to satisfy the usual metric axioms. Here $d_i$ is of course the induced metric on $M$ (Riemannian distance fucntion)

Given $\operatorname{Iso}(M)$ is now a metric space with metric $d$ as defined, we thus get a natural metric topology for $\operatorname{Iso}(M)$. That is open sets are all subsets that can be realized as the unions of open balls of form $B(f_0, r) = \{f \in \operatorname{Iso}(M): d(f_0,f)< r\}$ where $f_0 \in \operatorname{Iso}(M)$ and $r>0$.

$\ $

Q) I am trying to prove that $$\mathscr M: \operatorname{Iso}(M) \times \operatorname{Iso}(M) \rightarrow \operatorname{Iso}(M), \, (f,g) \mapsto f \circ g$$ is continuous in the metric topology of $\operatorname{Iso}(M)$.

$\ $

Ans) It is easy to show that $\operatorname{Iso}(M)$ is a group (which I have shown before) and I am assuming the continuity of the inversion $$\iota: \operatorname{Iso}(M) \to \operatorname{Iso}(M), \, f \mapsto f^{-1},$$ so I will use these two facts in the following answer. Now let $S$ denote the set of the $n+1$ points defining the metric on $\operatorname{Iso}(M)$. For $g, f, \tilde{f} \in \operatorname{Iso}(M)$ we have $$d(g \circ f, g \circ \tilde{f}) = \max_{x \in S} d_i(g(f(x)), g(\tilde{f}(x))) = \max_{x \in S} d_i(f(x), \tilde{f}(x)) = d(f, \tilde{f})$$ since $g$ is an isometry, so the map $$\mathscr{M}(g, -): \operatorname{Iso}(M) \to \operatorname{Iso}(M), \, f \mapsto g \circ f$$ is a $d$-isometry and in particular continuous for any $g \in \operatorname{Iso}(M).$ Furthermore $$f \circ g = \left((f \circ g)^{-1}\right)^{-1} = (g^{-1} \circ f^{-1})^{-1}, \text{ i.e. } \mathscr{M}(f,g) = \iota(\mathscr{M}(g^{-1}, \iota(f)),$$ so the continuity of the inversion and the above shows that $$\mathscr{M}(-,g): \operatorname{Iso}(M) \to \operatorname{Iso}(M), \, f \mapsto f \circ g$$ is continuous for $g \in \operatorname{Iso}(M)$ since $\mathscr{M}(-,g) = \iota \circ \mathscr{M}(g^{-1}, -) \circ \iota$.

Now let $(f_n)_{n \in \mathbb{N}}, (g_n)_{n \in \mathbb{N}}$ be sequences in $\operatorname{Iso}(M)$ and $f,g \in \operatorname{Iso}(M)$ such that $$\lim_{n \to \infty} d(f_n, f) = \lim_{n \to \infty} d(g_n, g) = 0.$$ Then the continuity of $\mathscr{M}(-,g)$ implies $\lim_{n \to \infty} d(f_n \circ g, f \circ g) = 0$. Furthermore we can use the triangle inequality of $d$ and the fact that $\mathscr{M}(f_n, -)$ is a $d$-isometry for any $n \in \mathbb{N}$ to obtain $$d(f_n \circ g_n, f \circ g) \leq d(f_n \circ g_n, f_n \circ g) + d(f_n \circ g, f \circ g) = d(g_n, g) + d(f_n \circ g, f \circ g),$$ so $\lim_{n \to \infty} d(f_n \circ g_n, f \circ g) = 0$. Hence $$\mathscr{M}: \operatorname{Iso}(M) \times \operatorname{Iso}(M) \to \operatorname{Iso}(M), \, (f,g) \mapsto f \circ g$$ is sequentially continuous and therefore continuous on the metric space $\operatorname{Iso}(M) \times \operatorname{Iso}(M)$.

$\ $

$\ $

Q) So now the only thing left to do would be to prove the assumption. That is I need to show that the inversion map $$\iota: \operatorname{Iso}(M) \to \operatorname{Iso}(M), \, f \mapsto f^{-1},$$ is indeed continuous in the metric topology of Iso(M)

That is I need a proof that if {$f_k$} $\rightarrow$ $f$ then {$f_k^{-1}$} $\rightarrow$ $f^{-1}$

$\ $

$\ $


This slot is available for anyone


This answer is available for anyone to use


This slot is available for anyone to use


$\mathcal{Y}\sim \mathcal{N}(\mu=\frac{X}{X+K_m}, \sigma^2) \Rightarrow $

In this answer I assume $V_{max}$ is known to be (without loss of generality) 1. As confirmed in the comments you are using the following model:

$\mathcal{Y}\sim \mathcal{N}(\mu=\frac{X}{X+K_m}, \sigma^2)$

The corresponding likelihood function is

$L(K_m, \sigma) = p_{\mathcal{Y^N}}(Y^N|K_m, \sigma, X^N) = \prod_{i=1}^Np_{\mathcal{N}}(Y^N|\mu=\frac{X^N_i}{X^N_i+K_m}, \sigma^2)$,

where $p_\mathcal{N}$ is the density of the normal distribution.

Now, you would like to know the distribution of a random variable $\mathcal{\hat{K_m}}$ that is the maximum likelihood estimate,

$ML_{\hat{K_m}}(X^N,Y^N) = \operatorname*{argmax}\limits_{K_m} \operatorname*{max}\limits_{\sigma} p_{\mathcal{Y^N}}(Y^N|K_m, \sigma, X^N)$ $ = \operatorname*{argmax}\limits_{K_m} \operatorname*{max}\limits_{\sigma} \prod_{i=1}^Np_{\mathcal{N}}(Y^N_i|\mu=\frac{X^N_i}{X^N_i+K_m}, \sigma^2)$

$ = \operatorname*{argmax}\limits_{K_m} \operatorname*{max}\limits_{\sigma} \sum_{i=1}^N\log(p_{\mathcal{N}}(Y^N_i|\mu=\frac{X^N_i}{X^N_i+K_m}, \sigma^2))$

$ = \operatorname*{argmax}\limits_{K_m} \operatorname*{max}\limits_{\sigma} \sum_{i=1}^N\log(\frac{1}{\sqrt{2\pi\sigma^2}}) - \frac{\left(Y^N_i-\frac{X^N_i}{X^N_i+K_m}\right)^2}{2\sigma^2}$

$ = \operatorname*{argmin}\limits_{K_m} \sum_{i=1}^N \left(Y^N_i-\frac{X^N_i}{X^N_i+K_m}\right)^2$,

obtained for draws of draws of size $N$ from $\mathcal{Y}$, $\mathcal{Y^N}$, for any $N$, $X^N$, $\sigma$.

You then sampled $K_m$ for some fixed $K$, $X^N$, $K_m$ and $\sigma$ by first sampling $\mathcal{Y^N}$ accordingly and then applying above ML estimator. Based on this, you think that $\mathcal{K_m}$ follows a log normal distribution.

It is known that, for any differentiable function $f: \mathbb{R}^N \to \mathbb{R}$ and $\mathcal{Y} = f(\mathcal{X})$,
$p_\mathcal{Y}(y) = \int_x \delta(f(x)-y) p_\mathcal{X}(x)\mathrm{d}x$ , where $\delta$ is the Dirac delta.

And that for any monotonic function $g: \mathbb{R} \to \mathbb{R}$ and $\mathcal{Y} = f(\mathcal{X})$,
$p_\mathcal{Y}(y) = p_\mathcal{X}(g^{-1}(y)) \left|\frac{\mathrm{d}}{\mathrm{d}y} g^{-1}(y) \right|$

We can use this to try to derive a closed form for the density of the distribution of $\mathcal{\hat{K_m}}$:

$p_{\mathcal{\hat{K_m}}}(\hat{K_m})=\int \delta (\hat{K_m}-ML_{\hat{K_m}}(X^N,Y^N)) p_{\mathcal{Y^N}}(Y^N) \mathrm{d} Y^N$

$\overset{\tiny{\text{if i'm lucky}}}{=}\int \delta(\frac{\mathrm{d}}{\mathrm{d} \hat{K_m}} \sum_{i=1}^N \left(Y^N_i-\frac{X^N_i}{X^N_i+\hat{K_m}}\right)^2) p_{\mathcal{Y^N}}(Y^N) \mathrm{d} Y^N$

$=\int \delta(\sum_{i=1}^N \frac{X^N_i(\hat{K_m}Y^N_i+X^N_i(Y^N_i-1))}{(\hat{K_m}+X^N_i)^3}) p_{\mathcal{Y^N}}(Y^N) \mathrm{d} Y^N$

But I don't how to find a simpler form for that.

For $N=1$ this is a bit simpler:

$p_{\mathcal{\hat{K_m}}}(\hat{K_m})=p_\mathcal{Y}(g^{-1}(\hat{K_m})) \left|\frac{\mathrm{d}}{\mathrm{d}\hat{K_m}} g^{-1}(\hat{K_m}) \right| = p_\mathcal{Y}(\frac{X}{X+\hat{K_m}}) \left|\frac{\mathrm{d}}{\mathrm{d}\hat{K_m}} \frac{X}{X+\hat{K_m}} \right|= p_\mathcal{Y}(\frac{X}{X+\hat{K_m}}) \left|- \frac{X}{(X+\hat{K_m})^2} \right|= p_{\mathcal{N}}(\frac{X}{X+\hat{K_m}}|\mu=\frac{X^N_i}{X^N_i+K_m}, \sigma^2) \frac{X}{(X+\hat{K_m})^2} $

This contains $ML_{\hat{K_m}}(X^N,Y^N)$ for which we might be able to find and algebraic expression for: $ML_{\hat{K_m}}(X^N,Y^N)

$ 0 = \left.\frac{\mathrm{d}}{\mathrm{d} K_m} \sum_{i=1}^N \left(Y^N_i-\frac{X^N_i}{X^N_i+K_m}\right)^2\right|_\hat{K_m}$ $ = \sum_{i=1}^N \left.\frac{\mathrm{d}}{\mathrm{d} K_m} \left(Y^N_i-\frac{X^N_i}{X^N_i+K_m}\right)^2\right|_\hat{K_m}$ $ = \sum_{i=1}^N \frac{X^N_i(\hat{K_m}Y^N_i+X^N_i(Y^N_i-1))}{(\hat{K_m}+X^N_i)^3}$

For $N=1$, $0=\frac{x(\hat{K_m}y+x(y-1))}{(\hat{K_m}+x)^3}$ solves $\hat{K_m}=x(\frac{1}{y}-1)$ whereas the solution for $N=2$ has a few more terms From where I don't know how to continue.


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 slot is available for anyone


This answer is free for anyone to use.


This answer is free for anyone to use.


$$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.