How to express “b is a power of 10” – Typographical Number Theory in Gödel Escher Bach
up vote
11
down vote
favorite
The book Gödel, Escher, Bach (GEB) by Douglas R. Hofstadter introduces a formal system called “Typographical Number Theory” (TNT). It's essentially first order predicate logic over the universe of natural numbers, with addition and multiplication but no exponentiation. Numbers are encoded using zero and the successor function $S$.
In one excercise, explicitely described as hard, one is asked to formalize the condition that a given number is a power of $10$.
My solution seems too simple, and GEB has been my first introduction to TNT, so I am doubtful that I have gotten this problem correct. Of course, due to my position on the learning curve, I think the Dunning-Kruger effect limits me from noticing my own flaw in this solution. Can anyone tell me how this is wrong, or if it is somehow miraculously correct?
$d$ is a power of $10$ iff:
$$exists! a: exists! b: exists c: exists d: (((a = SS0) land (b = SSSSS0)) land (((a cdot c) cdot (b cdot c)) = d)) \
$$
number-theory elementary-number-theory logic puzzle peano-axioms
add a comment |
up vote
11
down vote
favorite
The book Gödel, Escher, Bach (GEB) by Douglas R. Hofstadter introduces a formal system called “Typographical Number Theory” (TNT). It's essentially first order predicate logic over the universe of natural numbers, with addition and multiplication but no exponentiation. Numbers are encoded using zero and the successor function $S$.
In one excercise, explicitely described as hard, one is asked to formalize the condition that a given number is a power of $10$.
My solution seems too simple, and GEB has been my first introduction to TNT, so I am doubtful that I have gotten this problem correct. Of course, due to my position on the learning curve, I think the Dunning-Kruger effect limits me from noticing my own flaw in this solution. Can anyone tell me how this is wrong, or if it is somehow miraculously correct?
$d$ is a power of $10$ iff:
$$exists! a: exists! b: exists c: exists d: (((a = SS0) land (b = SSSSS0)) land (((a cdot c) cdot (b cdot c)) = d)) \
$$
number-theory elementary-number-theory logic puzzle peano-axioms
This post by Anders Kaseorg has a nice write-up of how to express that condition. I'm thinking about turning that into an answer, but I'm not yet satsified with the way I'm adding my own touch to it.
– MvG
May 14 '15 at 18:46
See also this other question for yet another failed attempt at formulating this predicate, also cross-posted to MathOverflow (and closed there). How is exponentiation defined in Peano arithmetic? deals with the core question here in a more general setup, and has some nice answers.
– MvG
May 14 '15 at 22:02
add a comment |
up vote
11
down vote
favorite
up vote
11
down vote
favorite
The book Gödel, Escher, Bach (GEB) by Douglas R. Hofstadter introduces a formal system called “Typographical Number Theory” (TNT). It's essentially first order predicate logic over the universe of natural numbers, with addition and multiplication but no exponentiation. Numbers are encoded using zero and the successor function $S$.
In one excercise, explicitely described as hard, one is asked to formalize the condition that a given number is a power of $10$.
My solution seems too simple, and GEB has been my first introduction to TNT, so I am doubtful that I have gotten this problem correct. Of course, due to my position on the learning curve, I think the Dunning-Kruger effect limits me from noticing my own flaw in this solution. Can anyone tell me how this is wrong, or if it is somehow miraculously correct?
$d$ is a power of $10$ iff:
$$exists! a: exists! b: exists c: exists d: (((a = SS0) land (b = SSSSS0)) land (((a cdot c) cdot (b cdot c)) = d)) \
$$
number-theory elementary-number-theory logic puzzle peano-axioms
The book Gödel, Escher, Bach (GEB) by Douglas R. Hofstadter introduces a formal system called “Typographical Number Theory” (TNT). It's essentially first order predicate logic over the universe of natural numbers, with addition and multiplication but no exponentiation. Numbers are encoded using zero and the successor function $S$.
In one excercise, explicitely described as hard, one is asked to formalize the condition that a given number is a power of $10$.
My solution seems too simple, and GEB has been my first introduction to TNT, so I am doubtful that I have gotten this problem correct. Of course, due to my position on the learning curve, I think the Dunning-Kruger effect limits me from noticing my own flaw in this solution. Can anyone tell me how this is wrong, or if it is somehow miraculously correct?
$d$ is a power of $10$ iff:
$$exists! a: exists! b: exists c: exists d: (((a = SS0) land (b = SSSSS0)) land (((a cdot c) cdot (b cdot c)) = d)) \
$$
number-theory elementary-number-theory logic puzzle peano-axioms
number-theory elementary-number-theory logic puzzle peano-axioms
edited May 14 '15 at 21:55
MvG
30.6k449101
30.6k449101
asked Aug 10 '14 at 23:54
Speleo
636
636
This post by Anders Kaseorg has a nice write-up of how to express that condition. I'm thinking about turning that into an answer, but I'm not yet satsified with the way I'm adding my own touch to it.
– MvG
May 14 '15 at 18:46
See also this other question for yet another failed attempt at formulating this predicate, also cross-posted to MathOverflow (and closed there). How is exponentiation defined in Peano arithmetic? deals with the core question here in a more general setup, and has some nice answers.
– MvG
May 14 '15 at 22:02
add a comment |
This post by Anders Kaseorg has a nice write-up of how to express that condition. I'm thinking about turning that into an answer, but I'm not yet satsified with the way I'm adding my own touch to it.
– MvG
May 14 '15 at 18:46
See also this other question for yet another failed attempt at formulating this predicate, also cross-posted to MathOverflow (and closed there). How is exponentiation defined in Peano arithmetic? deals with the core question here in a more general setup, and has some nice answers.
– MvG
May 14 '15 at 22:02
This post by Anders Kaseorg has a nice write-up of how to express that condition. I'm thinking about turning that into an answer, but I'm not yet satsified with the way I'm adding my own touch to it.
– MvG
May 14 '15 at 18:46
This post by Anders Kaseorg has a nice write-up of how to express that condition. I'm thinking about turning that into an answer, but I'm not yet satsified with the way I'm adding my own touch to it.
– MvG
May 14 '15 at 18:46
See also this other question for yet another failed attempt at formulating this predicate, also cross-posted to MathOverflow (and closed there). How is exponentiation defined in Peano arithmetic? deals with the core question here in a more general setup, and has some nice answers.
– MvG
May 14 '15 at 22:02
See also this other question for yet another failed attempt at formulating this predicate, also cross-posted to MathOverflow (and closed there). How is exponentiation defined in Peano arithmetic? deals with the core question here in a more general setup, and has some nice answers.
– MvG
May 14 '15 at 22:02
add a comment |
3 Answers
3
active
oldest
votes
up vote
8
down vote
accepted
You should spell out your abbreviations, since they are not universal. I assume you mean "Typographical Number Theory" in the book "Gödel, Escher, Bach" by Douglas R. Hofstadter.
Your TNT statement is wrong. First, you want your formula to be about $d$, but you bound $d$ in an existence quantifier. So, remove the $exists d:$ to get a statement about $d$.
Also, your formula just says that $a=2$, $b=5$, $c$ is a natural number, and the equation basically says $d=10c^2$.
I also worked on this problem a bit when I read (the first half of) Gödel, Escher, Bach, and the answer will be much more complicated than you have set out here. I got some ideas but I never finished the answer: too much time involved. I never even got to the second half of the book!
ADDED
If I recall correctly, I was able to get a statement for "b is a power of 2" by saying something like "2 is the only prime divisor of b," and similarly for "b is a power of 5." I could then say "b is a power of 2 times a power of 5" but I never did find a way to ensure that the exponents of 2 and of 5 are the same.
Very well, this does command a much higher grasp of Number Theory than I currently possess. I think I might be able to attempt the "b is a factor of 2" problem by stating something along the lines of " it is not the case that a is a factor of b except for a is equal to 1 or 2", adding variables where needed of course.
– Speleo
Aug 11 '14 at 2:53
add a comment |
up vote
12
down vote
how do you express “b is a power of 10”.
Since Rory already covered the problems with your approach, I'll tackle the question of finding a different solution.
In my first attempt to do so, I have made a mistake, so I'm completely rewriting my answer. It is now inspired by this post by Anders Kaseorg, although the wording is mine.
All powers at once
The main problem is that you can't simply write down a recursive definition. You can't have the formula build on itself. One way to tackle this is by speaking about all powers of ten, at least up to the given number, simultaneously. Lacking sets, we have to represent this as a single number. We can't do digit shifting in base 10 yet, but we can express powers of ten in some prime base.
Some nomenclature up front. I'll use $a$ to denote the free variable, the input, the thing we want to check the predicate for. $p$ will be a prime number used as number base, $t$ the base-$p$ number used to encode our powers of ten. $d$ will often be a digit or element of that set of powers of ten.
To keep things understandible, I'll define abbreviations for semantic units. But note that every such abbreviation only builds on those I have defined before, not itself or the ones coming afterwards. Therefore you could expand the abbreviations level by level to get back to the strict notation of TNT. I'll do so towards the end of this post.
Step by step
isPrime(p)
When is a number prime? If it itself is not less than $2$ and not the product of two integers greater or equal to $2$. (I write $neg$ instead of $sim$ for negation.)
$$text{isPrime}(p):=;;langleexists i:p=textsf{SS}i;wedge;neg;exists j:exists k:p=textsf{SS}jcdottextsf{SS}krangle$$
primePower(p, q)
To write digit operations in a base-$p$ number, we'll need to talk about powers of $p$. When is some $q$ a power of $p$? If $q$ is non-zero and contains no other prime factors. (I prefer to write implication as $rightarrow$ not $supset$.)
begin{align*}
text{primePower}(p,q):=;;&Bigllangleneg;q=textsf 0;wedge\&forall g:forall h:biglangle q=textsf{SS}gcdottextsf{SS}h;rightarrow;langleneg;text{isPrime}(textsf{SS}g);vee;textsf{SS}g=pranglebigrangleBigrrangle
end{align*}
digitOf(p, t, d)
When is $d$ a digit of a base-$p$ number $t$? If $t=(ecdot p+d)cdot p^k+f$ for some $e,f,k$ with $d<p$ and $f<p^k$.
begin{align*}
text{digitOf}(p,t,d):=;;&exists e:exists f:exists q:biglangle
langleexists c:p=d+textsf{S}c;wedge;exists c:q=f+textsf{S}crangle;wedge\&langle t=(ecdot p+d)cdot q+f;wedge;text{primePower}(p,q)ranglebigrangleend{align*}
contains(p, t, d)
Having base-$p$ numbers represent sets is a beautiful idea, but one has to be careful about zeros: every integer contains an infinite number of leading zeros. But we don't want any zeros in our set of powers of ten, so we can exclude zeros.
$$text{contains}(p, t, d):=;;langleneg;d=0;wedge;text{digitOf}(p, t, d)rangle$$
powersOfTen(p, t)
Now we can start talking about powers of ten. When does a base-$p$ number $t$ describe sufficiently many powers of ten? Originally I'd start this by saying it must contain $1=10^0$ and for every $d$ it must contain $10cdot d$, and no other numbers except for these. But we'll eventually quantify this number as $exists t$, so all requirement about what it must contain can be avoided. The only important thing is writing down what it must not contain, i.e. expressing that it should contain nothing but powers of ten.
For every number it contains, there must be a lower power of ten which it also contains, with one as the obvious exception.
begin{align*}
text{powersOfTen}(p,t):=;;&forall d:Biglangletext{contains}(p,t,d);rightarrow;biglangle d=textsf{S0};vee\&exists b:langle d=textsf{SSSSSSSSSS0}cdot b;wedge;text{contains}(p,t,b)ranglebigrangleBigrangle
end{align*}
powerOfTen(a)
So when is a number a power of ten? If it contained in the powers of ten number, for some suitable prime $p$.
begin{align*}
text{powerOfTen}(a):=;;&exists p:bigllangletext{isPrime}(p);wedge\&
exists t:langletext{powersOfTen}(p,t);wedge;text{contains}(p,t,a)ranglebigrrangleend{align*}
We didn't require $p>a$, but the existential quantification of $t$ takes care of that. Likewise, we at no point made any statement about the order of digits inside $t$. Any order will do, and repetitions are fine as well.
The formulation is not optimized for brevity. Instead, I tried to make each definition capture a mathematical idea as precisely as possible, even if that meant covering corner cases which are irrelevant for the application at hand. For example, if in the $text{digitOf}$ formulation I had written $textsf Sq$ for $p^k$ instead of $q$, then the case of $q=0$ in $text{primePower}$ would become irrelevant.
All together
If you plug everything together, you get the following pretty unreadable expression:
$$
exists p:langle
\
langleexists i:p=textsf{SS}i;wedge;neg;exists j:exists k:p=textsf{SS}jcdottextsf{SS}krangle
\
;wedge;exists t:langle
forall d:langle
\
langleneg;d=0;wedge;
\
exists e:exists f:exists q:langlelangleexists c:p=d+textsf Sc;wedge;exists c:q=f+textsf Scrangle;wedge;langle t=(ecdot p+d)cdot q+f;wedge;
\
langleneg;q=textsf 0;wedge;forall g:forall h:langle q=textsf{SS}gcdottextsf{SS}h;rightarrow;langleneg;
\
langleexists i:textsf{SS}g=textsf{SS}i;wedge;neg;exists j:exists k:textsf{SS}g=textsf{SS}jcdottextsf{SS}krangle
\
;vee;textsf{SS}g=prangleranglerangle
ranglerangle
rangle
\
;rightarrow;langle d=textsf{S0};vee;exists b:langle d=textsf{SSSSSSSSSS0}cdot b;wedge;
\
langleneg;b=0;wedge;
\
exists e:exists f:exists q:langlelangleexists c:p=b+textsf Sc;wedge;exists c:q=f+textsf Scrangle;wedge;langle t=(ecdot p+b)cdot q+f;wedge;
\
langleneg;q=textsf 0;wedge;forall g:forall h:langle q=textsf{SS}gcdottextsf{SS}h;rightarrow;langleneg;
\
langleexists i:textsf{SS}g=textsf{SS}i;wedge;neg;exists j:exists k:textsf{SS}g=textsf{SS}jcdottextsf{SS}krangle
\
;vee;textsf{SS}g=prangleranglerangle
ranglerangle
rangle
rangleranglerangle
\
;wedge;
langleneg;a=0;wedge;
\
exists e:exists f:exists q:langlelangleexists c:p=a+textsf Sc;wedge;exists c:q=f+textsf Scrangle;wedge;langle t=(ecdot p+a)cdot q+f;wedge;
\
langleneg;q=textsf 0;wedge;forall g:forall h:langle q=textsf{SS}gcdottextsf{SS}h;rightarrow;langleneg;
\
langleexists i:textsf{SS}g=textsf{SS}i;wedge;neg;exists j:exists k:textsf{SS}g=textsf{SS}jcdottextsf{SS}krangle
\
;vee;textsf{SS}g=prangleranglerangle
ranglerangle
rangle
ranglerangle
$$
If you look closely, you can recognize three similar block, corresponding to the three $text{contains}$ instances. That might help you find your bearings.
Alternatives
The above is one possible formulation, but there are many others. The post by Anders Kaseorg formulated $text{primePower}$ not in terms of “every prime factor must be equal to $p$” but instead “every factor must be divisible by $p$”. In the expanded form this is certainly shorter, but since my formulation is what first came to my mind, I'll keep it the way it is.
Instead of writing $t$ as a set of all powers of ten, one could also make it a sequence of such powers. In that case you'd say that every pair of subsequent digits has a power of ten between them. But since we still need the $text{contains}$ predicate to eventually check whether $a$ is contained, working exclusively on sets makes things simpler.
How is exponentiation defined in Peano arithmetic? is a more general variant of this question here. The answers there don't use base-$p$ numbers, but instead the Chinese remainder theorem to express a sequence in a single number. The great benefit there is that the index into the sequence is only a factor in some product in the accompanying formulas. In my approach, it's the exponent of the prime, so I need extra predicates to formulate that. So indexing is easier with the Chinese remainder theorem. On the other hand, seeing how the data is stored in the number is harder. Even if you're rationally perfectly convinced that the theorem works as advertised, I still think it's harder to establish a kind of gut understanding for how the single number (or rather pair of numbers, in my case $t$ and $p$) represents a sequence. That's the reason I prefer the base-$p$ numbers. Their approach is however better suited if you not only want to establish that $a$ is a power of ten, but also characterize the exponent, like check whether $a=10^b$ for $a,b$ given as free variables. The use of a sequence with easy indexing pays off in that setup.
Another common tool to represent sequences as single numbers is by using a pairing function to denote the sequence. The first element of the pair would be an element of the list, the second the remaining list except for that first element. But this is a recursive data structure, and we had enough trouble expressing the simpler recursive concepts above, so I'd not follow that approach here.
The same goes for the idea of representing a set by writing down as many distinct primes as the set has elements, and then using the set elements as exponents for the primes. To decode this, you again have to not only recognize powers of primes, but also to identify the exponent. Once you can express such things, the answer to this problem here is a pretty trivial application of that.
1
In digitOf, you probably also want to require that f is less than q.
– Alex Kruckman
May 14 '15 at 21:26
add a comment |
up vote
3
down vote
Step 1: We can encode any finite sequence in just a few numbers
Any finite sequence $a_0,a_2,ldots,a_n$ of (natural) numbers can be encoded as a predicate
$$begin{align}P(x,k,alpha,beta,n)&iff xtext{ is the $k$th term of thes given equence $a_0,ldots,a_n$}\&iff kle nland x=alphabmod{((k+1)beta+1)}\&iffexists tcolon n=k+tland exists tcolon alphacdot x+tcdot S(betacdot Sk)land exists tcolon x+t=betacdot Skend{align}$$
where the existence of suitable $alpha,beta$ is guaranteed by the Chinese Remainder Theorem. All we need is that the numbers $beta+1,2beta+1,ldots,(n+1)beta+1$ are coprime and $>a_k$, which can be achieved by letting $beta$ a multiple of $(n+1)!$.
Example: $alpha=1981297324554360860$, $beta=2016$ can be used to encode (any inital seqgment of) the sequence $1,10,100,1000,10000,7101,6944,15819,ldots$; especially, the first few terms happen to coincide with the first few powers of ten.
Step 2: We can talk about recursive sequences by using finite sequences
Assume we define a sequence by its initial term $a_0$ and a recursion $a_n=f(a_{n-1})$ (where we can express $f$ in TNT). Then we can encode the property that $x$ equals $a_n$ as
$$begin{align}R(x,n)iffexists alphaexistsbetacolon &quad P(a_0,0,alpha,beta,n)\&land P(x,n,alpha,beta,n)\&landforall kforall ycolonbigl(( k<nland P(y,k,alpha,beta,n))to P(f(y),Sk,alpha,beta,n)bigr)\ end{align}$$
Example: If $f(y)=10cdot y$ and $a_0=1$, then the numbers $alpha,beta$ from the previous example make the statement $R(10000,4)$ true.
Step 3: We can encode "$b$ is a power of $10$"
This is just $$exists ncolon R(b,n) $$
where $R$ is defined as in step 2 using $f(y)=10y$ and $a_0=1$.
Exercise: Recognize the methods of the two steps just described in the following:
∃n:∃a:∃c:∃d:∃e: ∀p:∀q:∀r:∀s:∀t: ∃f:∃g: 〈〈S(a· SSc)=(b+ (d· S(Sc· Sn))) ∧ (b+ e)=(Sc· Sn)〉 ∧ 〈〈〈¬S(p+ r)=n ∨ ¬S(a· SSc)=(q+ (s· S(Sc· Sp)))〉 ∨ ¬(q+ t)=(Sc· Sp) 〉 ∨ 〈S(a· SSc)=((SSSSSSSSSS0· q)+ (f· S(Sc· SSp))) ∧ ((SSSSSSSSSS0· q)+ g)=(Sc· SSp)〉〉〉
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
return StackExchange.using("mathjaxEditing", function () {
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
});
});
}, "mathjax-editing");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "69"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f893526%2fhow-to-express-b-is-a-power-of-10-typographical-number-theory-in-g%25c3%25b6del-esche%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
3 Answers
3
active
oldest
votes
3 Answers
3
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
8
down vote
accepted
You should spell out your abbreviations, since they are not universal. I assume you mean "Typographical Number Theory" in the book "Gödel, Escher, Bach" by Douglas R. Hofstadter.
Your TNT statement is wrong. First, you want your formula to be about $d$, but you bound $d$ in an existence quantifier. So, remove the $exists d:$ to get a statement about $d$.
Also, your formula just says that $a=2$, $b=5$, $c$ is a natural number, and the equation basically says $d=10c^2$.
I also worked on this problem a bit when I read (the first half of) Gödel, Escher, Bach, and the answer will be much more complicated than you have set out here. I got some ideas but I never finished the answer: too much time involved. I never even got to the second half of the book!
ADDED
If I recall correctly, I was able to get a statement for "b is a power of 2" by saying something like "2 is the only prime divisor of b," and similarly for "b is a power of 5." I could then say "b is a power of 2 times a power of 5" but I never did find a way to ensure that the exponents of 2 and of 5 are the same.
Very well, this does command a much higher grasp of Number Theory than I currently possess. I think I might be able to attempt the "b is a factor of 2" problem by stating something along the lines of " it is not the case that a is a factor of b except for a is equal to 1 or 2", adding variables where needed of course.
– Speleo
Aug 11 '14 at 2:53
add a comment |
up vote
8
down vote
accepted
You should spell out your abbreviations, since they are not universal. I assume you mean "Typographical Number Theory" in the book "Gödel, Escher, Bach" by Douglas R. Hofstadter.
Your TNT statement is wrong. First, you want your formula to be about $d$, but you bound $d$ in an existence quantifier. So, remove the $exists d:$ to get a statement about $d$.
Also, your formula just says that $a=2$, $b=5$, $c$ is a natural number, and the equation basically says $d=10c^2$.
I also worked on this problem a bit when I read (the first half of) Gödel, Escher, Bach, and the answer will be much more complicated than you have set out here. I got some ideas but I never finished the answer: too much time involved. I never even got to the second half of the book!
ADDED
If I recall correctly, I was able to get a statement for "b is a power of 2" by saying something like "2 is the only prime divisor of b," and similarly for "b is a power of 5." I could then say "b is a power of 2 times a power of 5" but I never did find a way to ensure that the exponents of 2 and of 5 are the same.
Very well, this does command a much higher grasp of Number Theory than I currently possess. I think I might be able to attempt the "b is a factor of 2" problem by stating something along the lines of " it is not the case that a is a factor of b except for a is equal to 1 or 2", adding variables where needed of course.
– Speleo
Aug 11 '14 at 2:53
add a comment |
up vote
8
down vote
accepted
up vote
8
down vote
accepted
You should spell out your abbreviations, since they are not universal. I assume you mean "Typographical Number Theory" in the book "Gödel, Escher, Bach" by Douglas R. Hofstadter.
Your TNT statement is wrong. First, you want your formula to be about $d$, but you bound $d$ in an existence quantifier. So, remove the $exists d:$ to get a statement about $d$.
Also, your formula just says that $a=2$, $b=5$, $c$ is a natural number, and the equation basically says $d=10c^2$.
I also worked on this problem a bit when I read (the first half of) Gödel, Escher, Bach, and the answer will be much more complicated than you have set out here. I got some ideas but I never finished the answer: too much time involved. I never even got to the second half of the book!
ADDED
If I recall correctly, I was able to get a statement for "b is a power of 2" by saying something like "2 is the only prime divisor of b," and similarly for "b is a power of 5." I could then say "b is a power of 2 times a power of 5" but I never did find a way to ensure that the exponents of 2 and of 5 are the same.
You should spell out your abbreviations, since they are not universal. I assume you mean "Typographical Number Theory" in the book "Gödel, Escher, Bach" by Douglas R. Hofstadter.
Your TNT statement is wrong. First, you want your formula to be about $d$, but you bound $d$ in an existence quantifier. So, remove the $exists d:$ to get a statement about $d$.
Also, your formula just says that $a=2$, $b=5$, $c$ is a natural number, and the equation basically says $d=10c^2$.
I also worked on this problem a bit when I read (the first half of) Gödel, Escher, Bach, and the answer will be much more complicated than you have set out here. I got some ideas but I never finished the answer: too much time involved. I never even got to the second half of the book!
ADDED
If I recall correctly, I was able to get a statement for "b is a power of 2" by saying something like "2 is the only prime divisor of b," and similarly for "b is a power of 5." I could then say "b is a power of 2 times a power of 5" but I never did find a way to ensure that the exponents of 2 and of 5 are the same.
edited Aug 11 '14 at 11:02
answered Aug 11 '14 at 0:00
Rory Daulton
29.3k53254
29.3k53254
Very well, this does command a much higher grasp of Number Theory than I currently possess. I think I might be able to attempt the "b is a factor of 2" problem by stating something along the lines of " it is not the case that a is a factor of b except for a is equal to 1 or 2", adding variables where needed of course.
– Speleo
Aug 11 '14 at 2:53
add a comment |
Very well, this does command a much higher grasp of Number Theory than I currently possess. I think I might be able to attempt the "b is a factor of 2" problem by stating something along the lines of " it is not the case that a is a factor of b except for a is equal to 1 or 2", adding variables where needed of course.
– Speleo
Aug 11 '14 at 2:53
Very well, this does command a much higher grasp of Number Theory than I currently possess. I think I might be able to attempt the "b is a factor of 2" problem by stating something along the lines of " it is not the case that a is a factor of b except for a is equal to 1 or 2", adding variables where needed of course.
– Speleo
Aug 11 '14 at 2:53
Very well, this does command a much higher grasp of Number Theory than I currently possess. I think I might be able to attempt the "b is a factor of 2" problem by stating something along the lines of " it is not the case that a is a factor of b except for a is equal to 1 or 2", adding variables where needed of course.
– Speleo
Aug 11 '14 at 2:53
add a comment |
up vote
12
down vote
how do you express “b is a power of 10”.
Since Rory already covered the problems with your approach, I'll tackle the question of finding a different solution.
In my first attempt to do so, I have made a mistake, so I'm completely rewriting my answer. It is now inspired by this post by Anders Kaseorg, although the wording is mine.
All powers at once
The main problem is that you can't simply write down a recursive definition. You can't have the formula build on itself. One way to tackle this is by speaking about all powers of ten, at least up to the given number, simultaneously. Lacking sets, we have to represent this as a single number. We can't do digit shifting in base 10 yet, but we can express powers of ten in some prime base.
Some nomenclature up front. I'll use $a$ to denote the free variable, the input, the thing we want to check the predicate for. $p$ will be a prime number used as number base, $t$ the base-$p$ number used to encode our powers of ten. $d$ will often be a digit or element of that set of powers of ten.
To keep things understandible, I'll define abbreviations for semantic units. But note that every such abbreviation only builds on those I have defined before, not itself or the ones coming afterwards. Therefore you could expand the abbreviations level by level to get back to the strict notation of TNT. I'll do so towards the end of this post.
Step by step
isPrime(p)
When is a number prime? If it itself is not less than $2$ and not the product of two integers greater or equal to $2$. (I write $neg$ instead of $sim$ for negation.)
$$text{isPrime}(p):=;;langleexists i:p=textsf{SS}i;wedge;neg;exists j:exists k:p=textsf{SS}jcdottextsf{SS}krangle$$
primePower(p, q)
To write digit operations in a base-$p$ number, we'll need to talk about powers of $p$. When is some $q$ a power of $p$? If $q$ is non-zero and contains no other prime factors. (I prefer to write implication as $rightarrow$ not $supset$.)
begin{align*}
text{primePower}(p,q):=;;&Bigllangleneg;q=textsf 0;wedge\&forall g:forall h:biglangle q=textsf{SS}gcdottextsf{SS}h;rightarrow;langleneg;text{isPrime}(textsf{SS}g);vee;textsf{SS}g=pranglebigrangleBigrrangle
end{align*}
digitOf(p, t, d)
When is $d$ a digit of a base-$p$ number $t$? If $t=(ecdot p+d)cdot p^k+f$ for some $e,f,k$ with $d<p$ and $f<p^k$.
begin{align*}
text{digitOf}(p,t,d):=;;&exists e:exists f:exists q:biglangle
langleexists c:p=d+textsf{S}c;wedge;exists c:q=f+textsf{S}crangle;wedge\&langle t=(ecdot p+d)cdot q+f;wedge;text{primePower}(p,q)ranglebigrangleend{align*}
contains(p, t, d)
Having base-$p$ numbers represent sets is a beautiful idea, but one has to be careful about zeros: every integer contains an infinite number of leading zeros. But we don't want any zeros in our set of powers of ten, so we can exclude zeros.
$$text{contains}(p, t, d):=;;langleneg;d=0;wedge;text{digitOf}(p, t, d)rangle$$
powersOfTen(p, t)
Now we can start talking about powers of ten. When does a base-$p$ number $t$ describe sufficiently many powers of ten? Originally I'd start this by saying it must contain $1=10^0$ and for every $d$ it must contain $10cdot d$, and no other numbers except for these. But we'll eventually quantify this number as $exists t$, so all requirement about what it must contain can be avoided. The only important thing is writing down what it must not contain, i.e. expressing that it should contain nothing but powers of ten.
For every number it contains, there must be a lower power of ten which it also contains, with one as the obvious exception.
begin{align*}
text{powersOfTen}(p,t):=;;&forall d:Biglangletext{contains}(p,t,d);rightarrow;biglangle d=textsf{S0};vee\&exists b:langle d=textsf{SSSSSSSSSS0}cdot b;wedge;text{contains}(p,t,b)ranglebigrangleBigrangle
end{align*}
powerOfTen(a)
So when is a number a power of ten? If it contained in the powers of ten number, for some suitable prime $p$.
begin{align*}
text{powerOfTen}(a):=;;&exists p:bigllangletext{isPrime}(p);wedge\&
exists t:langletext{powersOfTen}(p,t);wedge;text{contains}(p,t,a)ranglebigrrangleend{align*}
We didn't require $p>a$, but the existential quantification of $t$ takes care of that. Likewise, we at no point made any statement about the order of digits inside $t$. Any order will do, and repetitions are fine as well.
The formulation is not optimized for brevity. Instead, I tried to make each definition capture a mathematical idea as precisely as possible, even if that meant covering corner cases which are irrelevant for the application at hand. For example, if in the $text{digitOf}$ formulation I had written $textsf Sq$ for $p^k$ instead of $q$, then the case of $q=0$ in $text{primePower}$ would become irrelevant.
All together
If you plug everything together, you get the following pretty unreadable expression:
$$
exists p:langle
\
langleexists i:p=textsf{SS}i;wedge;neg;exists j:exists k:p=textsf{SS}jcdottextsf{SS}krangle
\
;wedge;exists t:langle
forall d:langle
\
langleneg;d=0;wedge;
\
exists e:exists f:exists q:langlelangleexists c:p=d+textsf Sc;wedge;exists c:q=f+textsf Scrangle;wedge;langle t=(ecdot p+d)cdot q+f;wedge;
\
langleneg;q=textsf 0;wedge;forall g:forall h:langle q=textsf{SS}gcdottextsf{SS}h;rightarrow;langleneg;
\
langleexists i:textsf{SS}g=textsf{SS}i;wedge;neg;exists j:exists k:textsf{SS}g=textsf{SS}jcdottextsf{SS}krangle
\
;vee;textsf{SS}g=prangleranglerangle
ranglerangle
rangle
\
;rightarrow;langle d=textsf{S0};vee;exists b:langle d=textsf{SSSSSSSSSS0}cdot b;wedge;
\
langleneg;b=0;wedge;
\
exists e:exists f:exists q:langlelangleexists c:p=b+textsf Sc;wedge;exists c:q=f+textsf Scrangle;wedge;langle t=(ecdot p+b)cdot q+f;wedge;
\
langleneg;q=textsf 0;wedge;forall g:forall h:langle q=textsf{SS}gcdottextsf{SS}h;rightarrow;langleneg;
\
langleexists i:textsf{SS}g=textsf{SS}i;wedge;neg;exists j:exists k:textsf{SS}g=textsf{SS}jcdottextsf{SS}krangle
\
;vee;textsf{SS}g=prangleranglerangle
ranglerangle
rangle
rangleranglerangle
\
;wedge;
langleneg;a=0;wedge;
\
exists e:exists f:exists q:langlelangleexists c:p=a+textsf Sc;wedge;exists c:q=f+textsf Scrangle;wedge;langle t=(ecdot p+a)cdot q+f;wedge;
\
langleneg;q=textsf 0;wedge;forall g:forall h:langle q=textsf{SS}gcdottextsf{SS}h;rightarrow;langleneg;
\
langleexists i:textsf{SS}g=textsf{SS}i;wedge;neg;exists j:exists k:textsf{SS}g=textsf{SS}jcdottextsf{SS}krangle
\
;vee;textsf{SS}g=prangleranglerangle
ranglerangle
rangle
ranglerangle
$$
If you look closely, you can recognize three similar block, corresponding to the three $text{contains}$ instances. That might help you find your bearings.
Alternatives
The above is one possible formulation, but there are many others. The post by Anders Kaseorg formulated $text{primePower}$ not in terms of “every prime factor must be equal to $p$” but instead “every factor must be divisible by $p$”. In the expanded form this is certainly shorter, but since my formulation is what first came to my mind, I'll keep it the way it is.
Instead of writing $t$ as a set of all powers of ten, one could also make it a sequence of such powers. In that case you'd say that every pair of subsequent digits has a power of ten between them. But since we still need the $text{contains}$ predicate to eventually check whether $a$ is contained, working exclusively on sets makes things simpler.
How is exponentiation defined in Peano arithmetic? is a more general variant of this question here. The answers there don't use base-$p$ numbers, but instead the Chinese remainder theorem to express a sequence in a single number. The great benefit there is that the index into the sequence is only a factor in some product in the accompanying formulas. In my approach, it's the exponent of the prime, so I need extra predicates to formulate that. So indexing is easier with the Chinese remainder theorem. On the other hand, seeing how the data is stored in the number is harder. Even if you're rationally perfectly convinced that the theorem works as advertised, I still think it's harder to establish a kind of gut understanding for how the single number (or rather pair of numbers, in my case $t$ and $p$) represents a sequence. That's the reason I prefer the base-$p$ numbers. Their approach is however better suited if you not only want to establish that $a$ is a power of ten, but also characterize the exponent, like check whether $a=10^b$ for $a,b$ given as free variables. The use of a sequence with easy indexing pays off in that setup.
Another common tool to represent sequences as single numbers is by using a pairing function to denote the sequence. The first element of the pair would be an element of the list, the second the remaining list except for that first element. But this is a recursive data structure, and we had enough trouble expressing the simpler recursive concepts above, so I'd not follow that approach here.
The same goes for the idea of representing a set by writing down as many distinct primes as the set has elements, and then using the set elements as exponents for the primes. To decode this, you again have to not only recognize powers of primes, but also to identify the exponent. Once you can express such things, the answer to this problem here is a pretty trivial application of that.
1
In digitOf, you probably also want to require that f is less than q.
– Alex Kruckman
May 14 '15 at 21:26
add a comment |
up vote
12
down vote
how do you express “b is a power of 10”.
Since Rory already covered the problems with your approach, I'll tackle the question of finding a different solution.
In my first attempt to do so, I have made a mistake, so I'm completely rewriting my answer. It is now inspired by this post by Anders Kaseorg, although the wording is mine.
All powers at once
The main problem is that you can't simply write down a recursive definition. You can't have the formula build on itself. One way to tackle this is by speaking about all powers of ten, at least up to the given number, simultaneously. Lacking sets, we have to represent this as a single number. We can't do digit shifting in base 10 yet, but we can express powers of ten in some prime base.
Some nomenclature up front. I'll use $a$ to denote the free variable, the input, the thing we want to check the predicate for. $p$ will be a prime number used as number base, $t$ the base-$p$ number used to encode our powers of ten. $d$ will often be a digit or element of that set of powers of ten.
To keep things understandible, I'll define abbreviations for semantic units. But note that every such abbreviation only builds on those I have defined before, not itself or the ones coming afterwards. Therefore you could expand the abbreviations level by level to get back to the strict notation of TNT. I'll do so towards the end of this post.
Step by step
isPrime(p)
When is a number prime? If it itself is not less than $2$ and not the product of two integers greater or equal to $2$. (I write $neg$ instead of $sim$ for negation.)
$$text{isPrime}(p):=;;langleexists i:p=textsf{SS}i;wedge;neg;exists j:exists k:p=textsf{SS}jcdottextsf{SS}krangle$$
primePower(p, q)
To write digit operations in a base-$p$ number, we'll need to talk about powers of $p$. When is some $q$ a power of $p$? If $q$ is non-zero and contains no other prime factors. (I prefer to write implication as $rightarrow$ not $supset$.)
begin{align*}
text{primePower}(p,q):=;;&Bigllangleneg;q=textsf 0;wedge\&forall g:forall h:biglangle q=textsf{SS}gcdottextsf{SS}h;rightarrow;langleneg;text{isPrime}(textsf{SS}g);vee;textsf{SS}g=pranglebigrangleBigrrangle
end{align*}
digitOf(p, t, d)
When is $d$ a digit of a base-$p$ number $t$? If $t=(ecdot p+d)cdot p^k+f$ for some $e,f,k$ with $d<p$ and $f<p^k$.
begin{align*}
text{digitOf}(p,t,d):=;;&exists e:exists f:exists q:biglangle
langleexists c:p=d+textsf{S}c;wedge;exists c:q=f+textsf{S}crangle;wedge\&langle t=(ecdot p+d)cdot q+f;wedge;text{primePower}(p,q)ranglebigrangleend{align*}
contains(p, t, d)
Having base-$p$ numbers represent sets is a beautiful idea, but one has to be careful about zeros: every integer contains an infinite number of leading zeros. But we don't want any zeros in our set of powers of ten, so we can exclude zeros.
$$text{contains}(p, t, d):=;;langleneg;d=0;wedge;text{digitOf}(p, t, d)rangle$$
powersOfTen(p, t)
Now we can start talking about powers of ten. When does a base-$p$ number $t$ describe sufficiently many powers of ten? Originally I'd start this by saying it must contain $1=10^0$ and for every $d$ it must contain $10cdot d$, and no other numbers except for these. But we'll eventually quantify this number as $exists t$, so all requirement about what it must contain can be avoided. The only important thing is writing down what it must not contain, i.e. expressing that it should contain nothing but powers of ten.
For every number it contains, there must be a lower power of ten which it also contains, with one as the obvious exception.
begin{align*}
text{powersOfTen}(p,t):=;;&forall d:Biglangletext{contains}(p,t,d);rightarrow;biglangle d=textsf{S0};vee\&exists b:langle d=textsf{SSSSSSSSSS0}cdot b;wedge;text{contains}(p,t,b)ranglebigrangleBigrangle
end{align*}
powerOfTen(a)
So when is a number a power of ten? If it contained in the powers of ten number, for some suitable prime $p$.
begin{align*}
text{powerOfTen}(a):=;;&exists p:bigllangletext{isPrime}(p);wedge\&
exists t:langletext{powersOfTen}(p,t);wedge;text{contains}(p,t,a)ranglebigrrangleend{align*}
We didn't require $p>a$, but the existential quantification of $t$ takes care of that. Likewise, we at no point made any statement about the order of digits inside $t$. Any order will do, and repetitions are fine as well.
The formulation is not optimized for brevity. Instead, I tried to make each definition capture a mathematical idea as precisely as possible, even if that meant covering corner cases which are irrelevant for the application at hand. For example, if in the $text{digitOf}$ formulation I had written $textsf Sq$ for $p^k$ instead of $q$, then the case of $q=0$ in $text{primePower}$ would become irrelevant.
All together
If you plug everything together, you get the following pretty unreadable expression:
$$
exists p:langle
\
langleexists i:p=textsf{SS}i;wedge;neg;exists j:exists k:p=textsf{SS}jcdottextsf{SS}krangle
\
;wedge;exists t:langle
forall d:langle
\
langleneg;d=0;wedge;
\
exists e:exists f:exists q:langlelangleexists c:p=d+textsf Sc;wedge;exists c:q=f+textsf Scrangle;wedge;langle t=(ecdot p+d)cdot q+f;wedge;
\
langleneg;q=textsf 0;wedge;forall g:forall h:langle q=textsf{SS}gcdottextsf{SS}h;rightarrow;langleneg;
\
langleexists i:textsf{SS}g=textsf{SS}i;wedge;neg;exists j:exists k:textsf{SS}g=textsf{SS}jcdottextsf{SS}krangle
\
;vee;textsf{SS}g=prangleranglerangle
ranglerangle
rangle
\
;rightarrow;langle d=textsf{S0};vee;exists b:langle d=textsf{SSSSSSSSSS0}cdot b;wedge;
\
langleneg;b=0;wedge;
\
exists e:exists f:exists q:langlelangleexists c:p=b+textsf Sc;wedge;exists c:q=f+textsf Scrangle;wedge;langle t=(ecdot p+b)cdot q+f;wedge;
\
langleneg;q=textsf 0;wedge;forall g:forall h:langle q=textsf{SS}gcdottextsf{SS}h;rightarrow;langleneg;
\
langleexists i:textsf{SS}g=textsf{SS}i;wedge;neg;exists j:exists k:textsf{SS}g=textsf{SS}jcdottextsf{SS}krangle
\
;vee;textsf{SS}g=prangleranglerangle
ranglerangle
rangle
rangleranglerangle
\
;wedge;
langleneg;a=0;wedge;
\
exists e:exists f:exists q:langlelangleexists c:p=a+textsf Sc;wedge;exists c:q=f+textsf Scrangle;wedge;langle t=(ecdot p+a)cdot q+f;wedge;
\
langleneg;q=textsf 0;wedge;forall g:forall h:langle q=textsf{SS}gcdottextsf{SS}h;rightarrow;langleneg;
\
langleexists i:textsf{SS}g=textsf{SS}i;wedge;neg;exists j:exists k:textsf{SS}g=textsf{SS}jcdottextsf{SS}krangle
\
;vee;textsf{SS}g=prangleranglerangle
ranglerangle
rangle
ranglerangle
$$
If you look closely, you can recognize three similar block, corresponding to the three $text{contains}$ instances. That might help you find your bearings.
Alternatives
The above is one possible formulation, but there are many others. The post by Anders Kaseorg formulated $text{primePower}$ not in terms of “every prime factor must be equal to $p$” but instead “every factor must be divisible by $p$”. In the expanded form this is certainly shorter, but since my formulation is what first came to my mind, I'll keep it the way it is.
Instead of writing $t$ as a set of all powers of ten, one could also make it a sequence of such powers. In that case you'd say that every pair of subsequent digits has a power of ten between them. But since we still need the $text{contains}$ predicate to eventually check whether $a$ is contained, working exclusively on sets makes things simpler.
How is exponentiation defined in Peano arithmetic? is a more general variant of this question here. The answers there don't use base-$p$ numbers, but instead the Chinese remainder theorem to express a sequence in a single number. The great benefit there is that the index into the sequence is only a factor in some product in the accompanying formulas. In my approach, it's the exponent of the prime, so I need extra predicates to formulate that. So indexing is easier with the Chinese remainder theorem. On the other hand, seeing how the data is stored in the number is harder. Even if you're rationally perfectly convinced that the theorem works as advertised, I still think it's harder to establish a kind of gut understanding for how the single number (or rather pair of numbers, in my case $t$ and $p$) represents a sequence. That's the reason I prefer the base-$p$ numbers. Their approach is however better suited if you not only want to establish that $a$ is a power of ten, but also characterize the exponent, like check whether $a=10^b$ for $a,b$ given as free variables. The use of a sequence with easy indexing pays off in that setup.
Another common tool to represent sequences as single numbers is by using a pairing function to denote the sequence. The first element of the pair would be an element of the list, the second the remaining list except for that first element. But this is a recursive data structure, and we had enough trouble expressing the simpler recursive concepts above, so I'd not follow that approach here.
The same goes for the idea of representing a set by writing down as many distinct primes as the set has elements, and then using the set elements as exponents for the primes. To decode this, you again have to not only recognize powers of primes, but also to identify the exponent. Once you can express such things, the answer to this problem here is a pretty trivial application of that.
1
In digitOf, you probably also want to require that f is less than q.
– Alex Kruckman
May 14 '15 at 21:26
add a comment |
up vote
12
down vote
up vote
12
down vote
how do you express “b is a power of 10”.
Since Rory already covered the problems with your approach, I'll tackle the question of finding a different solution.
In my first attempt to do so, I have made a mistake, so I'm completely rewriting my answer. It is now inspired by this post by Anders Kaseorg, although the wording is mine.
All powers at once
The main problem is that you can't simply write down a recursive definition. You can't have the formula build on itself. One way to tackle this is by speaking about all powers of ten, at least up to the given number, simultaneously. Lacking sets, we have to represent this as a single number. We can't do digit shifting in base 10 yet, but we can express powers of ten in some prime base.
Some nomenclature up front. I'll use $a$ to denote the free variable, the input, the thing we want to check the predicate for. $p$ will be a prime number used as number base, $t$ the base-$p$ number used to encode our powers of ten. $d$ will often be a digit or element of that set of powers of ten.
To keep things understandible, I'll define abbreviations for semantic units. But note that every such abbreviation only builds on those I have defined before, not itself or the ones coming afterwards. Therefore you could expand the abbreviations level by level to get back to the strict notation of TNT. I'll do so towards the end of this post.
Step by step
isPrime(p)
When is a number prime? If it itself is not less than $2$ and not the product of two integers greater or equal to $2$. (I write $neg$ instead of $sim$ for negation.)
$$text{isPrime}(p):=;;langleexists i:p=textsf{SS}i;wedge;neg;exists j:exists k:p=textsf{SS}jcdottextsf{SS}krangle$$
primePower(p, q)
To write digit operations in a base-$p$ number, we'll need to talk about powers of $p$. When is some $q$ a power of $p$? If $q$ is non-zero and contains no other prime factors. (I prefer to write implication as $rightarrow$ not $supset$.)
begin{align*}
text{primePower}(p,q):=;;&Bigllangleneg;q=textsf 0;wedge\&forall g:forall h:biglangle q=textsf{SS}gcdottextsf{SS}h;rightarrow;langleneg;text{isPrime}(textsf{SS}g);vee;textsf{SS}g=pranglebigrangleBigrrangle
end{align*}
digitOf(p, t, d)
When is $d$ a digit of a base-$p$ number $t$? If $t=(ecdot p+d)cdot p^k+f$ for some $e,f,k$ with $d<p$ and $f<p^k$.
begin{align*}
text{digitOf}(p,t,d):=;;&exists e:exists f:exists q:biglangle
langleexists c:p=d+textsf{S}c;wedge;exists c:q=f+textsf{S}crangle;wedge\&langle t=(ecdot p+d)cdot q+f;wedge;text{primePower}(p,q)ranglebigrangleend{align*}
contains(p, t, d)
Having base-$p$ numbers represent sets is a beautiful idea, but one has to be careful about zeros: every integer contains an infinite number of leading zeros. But we don't want any zeros in our set of powers of ten, so we can exclude zeros.
$$text{contains}(p, t, d):=;;langleneg;d=0;wedge;text{digitOf}(p, t, d)rangle$$
powersOfTen(p, t)
Now we can start talking about powers of ten. When does a base-$p$ number $t$ describe sufficiently many powers of ten? Originally I'd start this by saying it must contain $1=10^0$ and for every $d$ it must contain $10cdot d$, and no other numbers except for these. But we'll eventually quantify this number as $exists t$, so all requirement about what it must contain can be avoided. The only important thing is writing down what it must not contain, i.e. expressing that it should contain nothing but powers of ten.
For every number it contains, there must be a lower power of ten which it also contains, with one as the obvious exception.
begin{align*}
text{powersOfTen}(p,t):=;;&forall d:Biglangletext{contains}(p,t,d);rightarrow;biglangle d=textsf{S0};vee\&exists b:langle d=textsf{SSSSSSSSSS0}cdot b;wedge;text{contains}(p,t,b)ranglebigrangleBigrangle
end{align*}
powerOfTen(a)
So when is a number a power of ten? If it contained in the powers of ten number, for some suitable prime $p$.
begin{align*}
text{powerOfTen}(a):=;;&exists p:bigllangletext{isPrime}(p);wedge\&
exists t:langletext{powersOfTen}(p,t);wedge;text{contains}(p,t,a)ranglebigrrangleend{align*}
We didn't require $p>a$, but the existential quantification of $t$ takes care of that. Likewise, we at no point made any statement about the order of digits inside $t$. Any order will do, and repetitions are fine as well.
The formulation is not optimized for brevity. Instead, I tried to make each definition capture a mathematical idea as precisely as possible, even if that meant covering corner cases which are irrelevant for the application at hand. For example, if in the $text{digitOf}$ formulation I had written $textsf Sq$ for $p^k$ instead of $q$, then the case of $q=0$ in $text{primePower}$ would become irrelevant.
All together
If you plug everything together, you get the following pretty unreadable expression:
$$
exists p:langle
\
langleexists i:p=textsf{SS}i;wedge;neg;exists j:exists k:p=textsf{SS}jcdottextsf{SS}krangle
\
;wedge;exists t:langle
forall d:langle
\
langleneg;d=0;wedge;
\
exists e:exists f:exists q:langlelangleexists c:p=d+textsf Sc;wedge;exists c:q=f+textsf Scrangle;wedge;langle t=(ecdot p+d)cdot q+f;wedge;
\
langleneg;q=textsf 0;wedge;forall g:forall h:langle q=textsf{SS}gcdottextsf{SS}h;rightarrow;langleneg;
\
langleexists i:textsf{SS}g=textsf{SS}i;wedge;neg;exists j:exists k:textsf{SS}g=textsf{SS}jcdottextsf{SS}krangle
\
;vee;textsf{SS}g=prangleranglerangle
ranglerangle
rangle
\
;rightarrow;langle d=textsf{S0};vee;exists b:langle d=textsf{SSSSSSSSSS0}cdot b;wedge;
\
langleneg;b=0;wedge;
\
exists e:exists f:exists q:langlelangleexists c:p=b+textsf Sc;wedge;exists c:q=f+textsf Scrangle;wedge;langle t=(ecdot p+b)cdot q+f;wedge;
\
langleneg;q=textsf 0;wedge;forall g:forall h:langle q=textsf{SS}gcdottextsf{SS}h;rightarrow;langleneg;
\
langleexists i:textsf{SS}g=textsf{SS}i;wedge;neg;exists j:exists k:textsf{SS}g=textsf{SS}jcdottextsf{SS}krangle
\
;vee;textsf{SS}g=prangleranglerangle
ranglerangle
rangle
rangleranglerangle
\
;wedge;
langleneg;a=0;wedge;
\
exists e:exists f:exists q:langlelangleexists c:p=a+textsf Sc;wedge;exists c:q=f+textsf Scrangle;wedge;langle t=(ecdot p+a)cdot q+f;wedge;
\
langleneg;q=textsf 0;wedge;forall g:forall h:langle q=textsf{SS}gcdottextsf{SS}h;rightarrow;langleneg;
\
langleexists i:textsf{SS}g=textsf{SS}i;wedge;neg;exists j:exists k:textsf{SS}g=textsf{SS}jcdottextsf{SS}krangle
\
;vee;textsf{SS}g=prangleranglerangle
ranglerangle
rangle
ranglerangle
$$
If you look closely, you can recognize three similar block, corresponding to the three $text{contains}$ instances. That might help you find your bearings.
Alternatives
The above is one possible formulation, but there are many others. The post by Anders Kaseorg formulated $text{primePower}$ not in terms of “every prime factor must be equal to $p$” but instead “every factor must be divisible by $p$”. In the expanded form this is certainly shorter, but since my formulation is what first came to my mind, I'll keep it the way it is.
Instead of writing $t$ as a set of all powers of ten, one could also make it a sequence of such powers. In that case you'd say that every pair of subsequent digits has a power of ten between them. But since we still need the $text{contains}$ predicate to eventually check whether $a$ is contained, working exclusively on sets makes things simpler.
How is exponentiation defined in Peano arithmetic? is a more general variant of this question here. The answers there don't use base-$p$ numbers, but instead the Chinese remainder theorem to express a sequence in a single number. The great benefit there is that the index into the sequence is only a factor in some product in the accompanying formulas. In my approach, it's the exponent of the prime, so I need extra predicates to formulate that. So indexing is easier with the Chinese remainder theorem. On the other hand, seeing how the data is stored in the number is harder. Even if you're rationally perfectly convinced that the theorem works as advertised, I still think it's harder to establish a kind of gut understanding for how the single number (or rather pair of numbers, in my case $t$ and $p$) represents a sequence. That's the reason I prefer the base-$p$ numbers. Their approach is however better suited if you not only want to establish that $a$ is a power of ten, but also characterize the exponent, like check whether $a=10^b$ for $a,b$ given as free variables. The use of a sequence with easy indexing pays off in that setup.
Another common tool to represent sequences as single numbers is by using a pairing function to denote the sequence. The first element of the pair would be an element of the list, the second the remaining list except for that first element. But this is a recursive data structure, and we had enough trouble expressing the simpler recursive concepts above, so I'd not follow that approach here.
The same goes for the idea of representing a set by writing down as many distinct primes as the set has elements, and then using the set elements as exponents for the primes. To decode this, you again have to not only recognize powers of primes, but also to identify the exponent. Once you can express such things, the answer to this problem here is a pretty trivial application of that.
how do you express “b is a power of 10”.
Since Rory already covered the problems with your approach, I'll tackle the question of finding a different solution.
In my first attempt to do so, I have made a mistake, so I'm completely rewriting my answer. It is now inspired by this post by Anders Kaseorg, although the wording is mine.
All powers at once
The main problem is that you can't simply write down a recursive definition. You can't have the formula build on itself. One way to tackle this is by speaking about all powers of ten, at least up to the given number, simultaneously. Lacking sets, we have to represent this as a single number. We can't do digit shifting in base 10 yet, but we can express powers of ten in some prime base.
Some nomenclature up front. I'll use $a$ to denote the free variable, the input, the thing we want to check the predicate for. $p$ will be a prime number used as number base, $t$ the base-$p$ number used to encode our powers of ten. $d$ will often be a digit or element of that set of powers of ten.
To keep things understandible, I'll define abbreviations for semantic units. But note that every such abbreviation only builds on those I have defined before, not itself or the ones coming afterwards. Therefore you could expand the abbreviations level by level to get back to the strict notation of TNT. I'll do so towards the end of this post.
Step by step
isPrime(p)
When is a number prime? If it itself is not less than $2$ and not the product of two integers greater or equal to $2$. (I write $neg$ instead of $sim$ for negation.)
$$text{isPrime}(p):=;;langleexists i:p=textsf{SS}i;wedge;neg;exists j:exists k:p=textsf{SS}jcdottextsf{SS}krangle$$
primePower(p, q)
To write digit operations in a base-$p$ number, we'll need to talk about powers of $p$. When is some $q$ a power of $p$? If $q$ is non-zero and contains no other prime factors. (I prefer to write implication as $rightarrow$ not $supset$.)
begin{align*}
text{primePower}(p,q):=;;&Bigllangleneg;q=textsf 0;wedge\&forall g:forall h:biglangle q=textsf{SS}gcdottextsf{SS}h;rightarrow;langleneg;text{isPrime}(textsf{SS}g);vee;textsf{SS}g=pranglebigrangleBigrrangle
end{align*}
digitOf(p, t, d)
When is $d$ a digit of a base-$p$ number $t$? If $t=(ecdot p+d)cdot p^k+f$ for some $e,f,k$ with $d<p$ and $f<p^k$.
begin{align*}
text{digitOf}(p,t,d):=;;&exists e:exists f:exists q:biglangle
langleexists c:p=d+textsf{S}c;wedge;exists c:q=f+textsf{S}crangle;wedge\&langle t=(ecdot p+d)cdot q+f;wedge;text{primePower}(p,q)ranglebigrangleend{align*}
contains(p, t, d)
Having base-$p$ numbers represent sets is a beautiful idea, but one has to be careful about zeros: every integer contains an infinite number of leading zeros. But we don't want any zeros in our set of powers of ten, so we can exclude zeros.
$$text{contains}(p, t, d):=;;langleneg;d=0;wedge;text{digitOf}(p, t, d)rangle$$
powersOfTen(p, t)
Now we can start talking about powers of ten. When does a base-$p$ number $t$ describe sufficiently many powers of ten? Originally I'd start this by saying it must contain $1=10^0$ and for every $d$ it must contain $10cdot d$, and no other numbers except for these. But we'll eventually quantify this number as $exists t$, so all requirement about what it must contain can be avoided. The only important thing is writing down what it must not contain, i.e. expressing that it should contain nothing but powers of ten.
For every number it contains, there must be a lower power of ten which it also contains, with one as the obvious exception.
begin{align*}
text{powersOfTen}(p,t):=;;&forall d:Biglangletext{contains}(p,t,d);rightarrow;biglangle d=textsf{S0};vee\&exists b:langle d=textsf{SSSSSSSSSS0}cdot b;wedge;text{contains}(p,t,b)ranglebigrangleBigrangle
end{align*}
powerOfTen(a)
So when is a number a power of ten? If it contained in the powers of ten number, for some suitable prime $p$.
begin{align*}
text{powerOfTen}(a):=;;&exists p:bigllangletext{isPrime}(p);wedge\&
exists t:langletext{powersOfTen}(p,t);wedge;text{contains}(p,t,a)ranglebigrrangleend{align*}
We didn't require $p>a$, but the existential quantification of $t$ takes care of that. Likewise, we at no point made any statement about the order of digits inside $t$. Any order will do, and repetitions are fine as well.
The formulation is not optimized for brevity. Instead, I tried to make each definition capture a mathematical idea as precisely as possible, even if that meant covering corner cases which are irrelevant for the application at hand. For example, if in the $text{digitOf}$ formulation I had written $textsf Sq$ for $p^k$ instead of $q$, then the case of $q=0$ in $text{primePower}$ would become irrelevant.
All together
If you plug everything together, you get the following pretty unreadable expression:
$$
exists p:langle
\
langleexists i:p=textsf{SS}i;wedge;neg;exists j:exists k:p=textsf{SS}jcdottextsf{SS}krangle
\
;wedge;exists t:langle
forall d:langle
\
langleneg;d=0;wedge;
\
exists e:exists f:exists q:langlelangleexists c:p=d+textsf Sc;wedge;exists c:q=f+textsf Scrangle;wedge;langle t=(ecdot p+d)cdot q+f;wedge;
\
langleneg;q=textsf 0;wedge;forall g:forall h:langle q=textsf{SS}gcdottextsf{SS}h;rightarrow;langleneg;
\
langleexists i:textsf{SS}g=textsf{SS}i;wedge;neg;exists j:exists k:textsf{SS}g=textsf{SS}jcdottextsf{SS}krangle
\
;vee;textsf{SS}g=prangleranglerangle
ranglerangle
rangle
\
;rightarrow;langle d=textsf{S0};vee;exists b:langle d=textsf{SSSSSSSSSS0}cdot b;wedge;
\
langleneg;b=0;wedge;
\
exists e:exists f:exists q:langlelangleexists c:p=b+textsf Sc;wedge;exists c:q=f+textsf Scrangle;wedge;langle t=(ecdot p+b)cdot q+f;wedge;
\
langleneg;q=textsf 0;wedge;forall g:forall h:langle q=textsf{SS}gcdottextsf{SS}h;rightarrow;langleneg;
\
langleexists i:textsf{SS}g=textsf{SS}i;wedge;neg;exists j:exists k:textsf{SS}g=textsf{SS}jcdottextsf{SS}krangle
\
;vee;textsf{SS}g=prangleranglerangle
ranglerangle
rangle
rangleranglerangle
\
;wedge;
langleneg;a=0;wedge;
\
exists e:exists f:exists q:langlelangleexists c:p=a+textsf Sc;wedge;exists c:q=f+textsf Scrangle;wedge;langle t=(ecdot p+a)cdot q+f;wedge;
\
langleneg;q=textsf 0;wedge;forall g:forall h:langle q=textsf{SS}gcdottextsf{SS}h;rightarrow;langleneg;
\
langleexists i:textsf{SS}g=textsf{SS}i;wedge;neg;exists j:exists k:textsf{SS}g=textsf{SS}jcdottextsf{SS}krangle
\
;vee;textsf{SS}g=prangleranglerangle
ranglerangle
rangle
ranglerangle
$$
If you look closely, you can recognize three similar block, corresponding to the three $text{contains}$ instances. That might help you find your bearings.
Alternatives
The above is one possible formulation, but there are many others. The post by Anders Kaseorg formulated $text{primePower}$ not in terms of “every prime factor must be equal to $p$” but instead “every factor must be divisible by $p$”. In the expanded form this is certainly shorter, but since my formulation is what first came to my mind, I'll keep it the way it is.
Instead of writing $t$ as a set of all powers of ten, one could also make it a sequence of such powers. In that case you'd say that every pair of subsequent digits has a power of ten between them. But since we still need the $text{contains}$ predicate to eventually check whether $a$ is contained, working exclusively on sets makes things simpler.
How is exponentiation defined in Peano arithmetic? is a more general variant of this question here. The answers there don't use base-$p$ numbers, but instead the Chinese remainder theorem to express a sequence in a single number. The great benefit there is that the index into the sequence is only a factor in some product in the accompanying formulas. In my approach, it's the exponent of the prime, so I need extra predicates to formulate that. So indexing is easier with the Chinese remainder theorem. On the other hand, seeing how the data is stored in the number is harder. Even if you're rationally perfectly convinced that the theorem works as advertised, I still think it's harder to establish a kind of gut understanding for how the single number (or rather pair of numbers, in my case $t$ and $p$) represents a sequence. That's the reason I prefer the base-$p$ numbers. Their approach is however better suited if you not only want to establish that $a$ is a power of ten, but also characterize the exponent, like check whether $a=10^b$ for $a,b$ given as free variables. The use of a sequence with easy indexing pays off in that setup.
Another common tool to represent sequences as single numbers is by using a pairing function to denote the sequence. The first element of the pair would be an element of the list, the second the remaining list except for that first element. But this is a recursive data structure, and we had enough trouble expressing the simpler recursive concepts above, so I'd not follow that approach here.
The same goes for the idea of representing a set by writing down as many distinct primes as the set has elements, and then using the set elements as exponents for the primes. To decode this, you again have to not only recognize powers of primes, but also to identify the exponent. Once you can express such things, the answer to this problem here is a pretty trivial application of that.
edited Nov 23 at 9:27
answered May 14 '15 at 17:58
MvG
30.6k449101
30.6k449101
1
In digitOf, you probably also want to require that f is less than q.
– Alex Kruckman
May 14 '15 at 21:26
add a comment |
1
In digitOf, you probably also want to require that f is less than q.
– Alex Kruckman
May 14 '15 at 21:26
1
1
In digitOf, you probably also want to require that f is less than q.
– Alex Kruckman
May 14 '15 at 21:26
In digitOf, you probably also want to require that f is less than q.
– Alex Kruckman
May 14 '15 at 21:26
add a comment |
up vote
3
down vote
Step 1: We can encode any finite sequence in just a few numbers
Any finite sequence $a_0,a_2,ldots,a_n$ of (natural) numbers can be encoded as a predicate
$$begin{align}P(x,k,alpha,beta,n)&iff xtext{ is the $k$th term of thes given equence $a_0,ldots,a_n$}\&iff kle nland x=alphabmod{((k+1)beta+1)}\&iffexists tcolon n=k+tland exists tcolon alphacdot x+tcdot S(betacdot Sk)land exists tcolon x+t=betacdot Skend{align}$$
where the existence of suitable $alpha,beta$ is guaranteed by the Chinese Remainder Theorem. All we need is that the numbers $beta+1,2beta+1,ldots,(n+1)beta+1$ are coprime and $>a_k$, which can be achieved by letting $beta$ a multiple of $(n+1)!$.
Example: $alpha=1981297324554360860$, $beta=2016$ can be used to encode (any inital seqgment of) the sequence $1,10,100,1000,10000,7101,6944,15819,ldots$; especially, the first few terms happen to coincide with the first few powers of ten.
Step 2: We can talk about recursive sequences by using finite sequences
Assume we define a sequence by its initial term $a_0$ and a recursion $a_n=f(a_{n-1})$ (where we can express $f$ in TNT). Then we can encode the property that $x$ equals $a_n$ as
$$begin{align}R(x,n)iffexists alphaexistsbetacolon &quad P(a_0,0,alpha,beta,n)\&land P(x,n,alpha,beta,n)\&landforall kforall ycolonbigl(( k<nland P(y,k,alpha,beta,n))to P(f(y),Sk,alpha,beta,n)bigr)\ end{align}$$
Example: If $f(y)=10cdot y$ and $a_0=1$, then the numbers $alpha,beta$ from the previous example make the statement $R(10000,4)$ true.
Step 3: We can encode "$b$ is a power of $10$"
This is just $$exists ncolon R(b,n) $$
where $R$ is defined as in step 2 using $f(y)=10y$ and $a_0=1$.
Exercise: Recognize the methods of the two steps just described in the following:
∃n:∃a:∃c:∃d:∃e: ∀p:∀q:∀r:∀s:∀t: ∃f:∃g: 〈〈S(a· SSc)=(b+ (d· S(Sc· Sn))) ∧ (b+ e)=(Sc· Sn)〉 ∧ 〈〈〈¬S(p+ r)=n ∨ ¬S(a· SSc)=(q+ (s· S(Sc· Sp)))〉 ∨ ¬(q+ t)=(Sc· Sp) 〉 ∨ 〈S(a· SSc)=((SSSSSSSSSS0· q)+ (f· S(Sc· SSp))) ∧ ((SSSSSSSSSS0· q)+ g)=(Sc· SSp)〉〉〉
add a comment |
up vote
3
down vote
Step 1: We can encode any finite sequence in just a few numbers
Any finite sequence $a_0,a_2,ldots,a_n$ of (natural) numbers can be encoded as a predicate
$$begin{align}P(x,k,alpha,beta,n)&iff xtext{ is the $k$th term of thes given equence $a_0,ldots,a_n$}\&iff kle nland x=alphabmod{((k+1)beta+1)}\&iffexists tcolon n=k+tland exists tcolon alphacdot x+tcdot S(betacdot Sk)land exists tcolon x+t=betacdot Skend{align}$$
where the existence of suitable $alpha,beta$ is guaranteed by the Chinese Remainder Theorem. All we need is that the numbers $beta+1,2beta+1,ldots,(n+1)beta+1$ are coprime and $>a_k$, which can be achieved by letting $beta$ a multiple of $(n+1)!$.
Example: $alpha=1981297324554360860$, $beta=2016$ can be used to encode (any inital seqgment of) the sequence $1,10,100,1000,10000,7101,6944,15819,ldots$; especially, the first few terms happen to coincide with the first few powers of ten.
Step 2: We can talk about recursive sequences by using finite sequences
Assume we define a sequence by its initial term $a_0$ and a recursion $a_n=f(a_{n-1})$ (where we can express $f$ in TNT). Then we can encode the property that $x$ equals $a_n$ as
$$begin{align}R(x,n)iffexists alphaexistsbetacolon &quad P(a_0,0,alpha,beta,n)\&land P(x,n,alpha,beta,n)\&landforall kforall ycolonbigl(( k<nland P(y,k,alpha,beta,n))to P(f(y),Sk,alpha,beta,n)bigr)\ end{align}$$
Example: If $f(y)=10cdot y$ and $a_0=1$, then the numbers $alpha,beta$ from the previous example make the statement $R(10000,4)$ true.
Step 3: We can encode "$b$ is a power of $10$"
This is just $$exists ncolon R(b,n) $$
where $R$ is defined as in step 2 using $f(y)=10y$ and $a_0=1$.
Exercise: Recognize the methods of the two steps just described in the following:
∃n:∃a:∃c:∃d:∃e: ∀p:∀q:∀r:∀s:∀t: ∃f:∃g: 〈〈S(a· SSc)=(b+ (d· S(Sc· Sn))) ∧ (b+ e)=(Sc· Sn)〉 ∧ 〈〈〈¬S(p+ r)=n ∨ ¬S(a· SSc)=(q+ (s· S(Sc· Sp)))〉 ∨ ¬(q+ t)=(Sc· Sp) 〉 ∨ 〈S(a· SSc)=((SSSSSSSSSS0· q)+ (f· S(Sc· SSp))) ∧ ((SSSSSSSSSS0· q)+ g)=(Sc· SSp)〉〉〉
add a comment |
up vote
3
down vote
up vote
3
down vote
Step 1: We can encode any finite sequence in just a few numbers
Any finite sequence $a_0,a_2,ldots,a_n$ of (natural) numbers can be encoded as a predicate
$$begin{align}P(x,k,alpha,beta,n)&iff xtext{ is the $k$th term of thes given equence $a_0,ldots,a_n$}\&iff kle nland x=alphabmod{((k+1)beta+1)}\&iffexists tcolon n=k+tland exists tcolon alphacdot x+tcdot S(betacdot Sk)land exists tcolon x+t=betacdot Skend{align}$$
where the existence of suitable $alpha,beta$ is guaranteed by the Chinese Remainder Theorem. All we need is that the numbers $beta+1,2beta+1,ldots,(n+1)beta+1$ are coprime and $>a_k$, which can be achieved by letting $beta$ a multiple of $(n+1)!$.
Example: $alpha=1981297324554360860$, $beta=2016$ can be used to encode (any inital seqgment of) the sequence $1,10,100,1000,10000,7101,6944,15819,ldots$; especially, the first few terms happen to coincide with the first few powers of ten.
Step 2: We can talk about recursive sequences by using finite sequences
Assume we define a sequence by its initial term $a_0$ and a recursion $a_n=f(a_{n-1})$ (where we can express $f$ in TNT). Then we can encode the property that $x$ equals $a_n$ as
$$begin{align}R(x,n)iffexists alphaexistsbetacolon &quad P(a_0,0,alpha,beta,n)\&land P(x,n,alpha,beta,n)\&landforall kforall ycolonbigl(( k<nland P(y,k,alpha,beta,n))to P(f(y),Sk,alpha,beta,n)bigr)\ end{align}$$
Example: If $f(y)=10cdot y$ and $a_0=1$, then the numbers $alpha,beta$ from the previous example make the statement $R(10000,4)$ true.
Step 3: We can encode "$b$ is a power of $10$"
This is just $$exists ncolon R(b,n) $$
where $R$ is defined as in step 2 using $f(y)=10y$ and $a_0=1$.
Exercise: Recognize the methods of the two steps just described in the following:
∃n:∃a:∃c:∃d:∃e: ∀p:∀q:∀r:∀s:∀t: ∃f:∃g: 〈〈S(a· SSc)=(b+ (d· S(Sc· Sn))) ∧ (b+ e)=(Sc· Sn)〉 ∧ 〈〈〈¬S(p+ r)=n ∨ ¬S(a· SSc)=(q+ (s· S(Sc· Sp)))〉 ∨ ¬(q+ t)=(Sc· Sp) 〉 ∨ 〈S(a· SSc)=((SSSSSSSSSS0· q)+ (f· S(Sc· SSp))) ∧ ((SSSSSSSSSS0· q)+ g)=(Sc· SSp)〉〉〉
Step 1: We can encode any finite sequence in just a few numbers
Any finite sequence $a_0,a_2,ldots,a_n$ of (natural) numbers can be encoded as a predicate
$$begin{align}P(x,k,alpha,beta,n)&iff xtext{ is the $k$th term of thes given equence $a_0,ldots,a_n$}\&iff kle nland x=alphabmod{((k+1)beta+1)}\&iffexists tcolon n=k+tland exists tcolon alphacdot x+tcdot S(betacdot Sk)land exists tcolon x+t=betacdot Skend{align}$$
where the existence of suitable $alpha,beta$ is guaranteed by the Chinese Remainder Theorem. All we need is that the numbers $beta+1,2beta+1,ldots,(n+1)beta+1$ are coprime and $>a_k$, which can be achieved by letting $beta$ a multiple of $(n+1)!$.
Example: $alpha=1981297324554360860$, $beta=2016$ can be used to encode (any inital seqgment of) the sequence $1,10,100,1000,10000,7101,6944,15819,ldots$; especially, the first few terms happen to coincide with the first few powers of ten.
Step 2: We can talk about recursive sequences by using finite sequences
Assume we define a sequence by its initial term $a_0$ and a recursion $a_n=f(a_{n-1})$ (where we can express $f$ in TNT). Then we can encode the property that $x$ equals $a_n$ as
$$begin{align}R(x,n)iffexists alphaexistsbetacolon &quad P(a_0,0,alpha,beta,n)\&land P(x,n,alpha,beta,n)\&landforall kforall ycolonbigl(( k<nland P(y,k,alpha,beta,n))to P(f(y),Sk,alpha,beta,n)bigr)\ end{align}$$
Example: If $f(y)=10cdot y$ and $a_0=1$, then the numbers $alpha,beta$ from the previous example make the statement $R(10000,4)$ true.
Step 3: We can encode "$b$ is a power of $10$"
This is just $$exists ncolon R(b,n) $$
where $R$ is defined as in step 2 using $f(y)=10y$ and $a_0=1$.
Exercise: Recognize the methods of the two steps just described in the following:
∃n:∃a:∃c:∃d:∃e: ∀p:∀q:∀r:∀s:∀t: ∃f:∃g: 〈〈S(a· SSc)=(b+ (d· S(Sc· Sn))) ∧ (b+ e)=(Sc· Sn)〉 ∧ 〈〈〈¬S(p+ r)=n ∨ ¬S(a· SSc)=(q+ (s· S(Sc· Sp)))〉 ∨ ¬(q+ t)=(Sc· Sp) 〉 ∨ 〈S(a· SSc)=((SSSSSSSSSS0· q)+ (f· S(Sc· SSp))) ∧ ((SSSSSSSSSS0· q)+ g)=(Sc· SSp)〉〉〉
edited May 15 '15 at 13:44
answered May 15 '15 at 13:25
Hagen von Eitzen
275k21268495
275k21268495
add a comment |
add a comment |
Thanks for contributing an answer to Mathematics Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Some of your past answers have not been well-received, and you're in danger of being blocked from answering.
Please pay close attention to the following guidance:
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f893526%2fhow-to-express-b-is-a-power-of-10-typographical-number-theory-in-g%25c3%25b6del-esche%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
This post by Anders Kaseorg has a nice write-up of how to express that condition. I'm thinking about turning that into an answer, but I'm not yet satsified with the way I'm adding my own touch to it.
– MvG
May 14 '15 at 18:46
See also this other question for yet another failed attempt at formulating this predicate, also cross-posted to MathOverflow (and closed there). How is exponentiation defined in Peano arithmetic? deals with the core question here in a more general setup, and has some nice answers.
– MvG
May 14 '15 at 22:02