Douglas Hofstader による Godel, Escher, Bach の第 8 章で、読者はこれら 2 つのステートメントを TNT に翻訳するように求められます。
「b は 2 の累乗です」
と
「b は 10 のべき乗です」
次の答えは正しいですか?:
(「∃」が「数値が存在する」という意味であると仮定すると):
∃x:(xx = b)
つまり、「x に x を掛けると b に等しい数 'x' が存在する」
それが正しければ、次のものも同様に簡単です。
∃x:(xxxxxxxxxx = b)
著者は、それらはトリッキーであり、2 つ目の問題は解決に数時間かかると述べているため、私は混乱しています。ここで明らかな何かを見逃したに違いありませんが、見えません!
In general, I would say "b is a power of 2" is equivalent to "every divisor of b except 1 is a multiple of 2". That is:
∀x((∃y(y*x=b & ¬(x=S0))) → ∃z(SS0*z=x))
EDIT: This doesnt work for 10 (thanks for the comments). But at least it works for all primes. Sorry. I think you have to use some sort of encoding sequences after all. I suggest "Gödel's Incompleteness Theorems" by Raymond Smullyan, if you want a detailed and more general approach to this.
Or you can encode Sequences of Numbers using the Chinese Remainder Theorem, and then encode recursive definitions, such that you can define Exponentiation. In fact, that is basically how you can prove that Peano Arithmetic is turing complete.
Try this:
D(x,y)=∃a(a*x=y)
Prime(x)=¬x=1&∀yD(y,x)→y=x|y=1
a=b mod c = ∃k a=c*k+b
Then
∃y ∃k(
∀x(D(x,y)&Prime(x)→¬D(x*x,y)) &
∀x(D(x,y)&Prime(x)&∀z(Prime(z)&z<x→¬D(z,y))→(k=1 mod x)) &
∀x∀z(D(x,y)&Prime(x)&D(z,y)&Prime(z)&z<x&∀t(z<t<x→¬(Prime(t)&D(t,y)))→
∀a<x ∀c<z ((k=a mod x)&(k=c mod z)-> a=c*10))&
∀x(D(x,y)&Prime(x)&∀z(Prime(z)&z>x→¬D(z,y))→(b<x & (k=b mod x))))
should state "b is Power of 10", actually saying "there is a number y and a number k such that y is product of distinct primes, and the sequence encoded by k throug these primes begins with 1, has the property that the following element c of a is 10*a, and ends with b"
あなたの式は、それぞれ「bは平方数です」および「bは数値の10乗です」というステートメントと同等です。「power of」ステートメントを TNT に変換するのは、かなりトリッキーです。
懐疑的な科学者の投稿のネタバレボタンの背後にある「b は 10 のべき乗」の問題に対する解決策があります。これは、数論からの中国の剰余定理と、素数の任意の長さの算術シーケンスの存在に依存します。Hofstadter が指摘したように、たとえ適切な定理を知っていたとしても、思いつくのは簡単ではありません。
「b は 10 の累乗です」と表現する場合、実際には中国剰余定理や有限数列のコーディングは必要ありません。別の方法として、次のように作業することもできます (ここでは、明白な意味を持つ式/用語のショートカットとして、|、>、cd などの通常の記号を使用します)。
素数 p に対して、「p は素数であり、a は p の冪乗である」という TNT の式を EXP(p,a) とします。作成方法はすでにわかっています。(技術的な理由から、S0 は p の累乗とは見なされないため、~EXP(p,S0) になります。)
p が素数の場合、EXP p (c,a) ≖ ⟨EXP(p,a) ∧ (c-1)|(a-1)⟩ を定義します。ここで、記号 | は、1 つの存在量指定子と乗算を使用して TNT で簡単に定義できる「除算」のショートカットです。同じことが c-1 (a-1、それぞれ) にも当てはまります。これは、「Sd=c となるような d」(Sd=a、それぞれ) を意味します。
EXP(p,c) が成立する (つまり、c が p のべき乗である) 場合、式 EXP p (c,a) は、a ≡ 1 (mod c-1) であるため、「a は c のべき乗である」と言います。
数値 (つまり、非負の整数) のプロパティ P を持つため、TNT では、このプロパティを持つ最小の数値を参照する方法があります: ⟨P(a) ∧ ∀c:⟨a>c → ~P(a) ⟩⟩.
「b は 10 のべき乗です」という式を表すことができます (読みやすくするために、記号 ⟨ と ⟩ を省略し、SS0 と SSSSS0 の代わりに 2 と 5 を書きます):
∃a:∃c:∃d: ( EXP(2,a) ∧ EXP(5,c) ∧ EXP(5,d) ∧ d > b ∧ a⋅c=b ∧ ∀e:(e>5 ∧ e|c ∧ EXP 5 (e, c) → ~EXP 5 (e,d)) ∧ ∀e:("e は EXP 5 (c,e) ∧ EXP 5 (d,e) となる最小のもの" → (d-2)|(ea))) .
説明: b = a⋅c = 2 x ⋅5 y (x,y>0) と書き、z と y が互いに素になるようにd=5 z >b を選択します (たとえば、z は素数である可能性があります)。その場合、「最小の e...」は (5 z ) y = d y ≡ 2 y (mod d-2) に等しく、(d-2)|(ea) は a = 2 x = e mod (d -2) = 2 y ('d-2 > 2 y ' と 'd-2 > a' もあります)、つまり x = y です。
注意:このアプローチは、固定分解 a 1 a 2 ...a kを使用して、任意の数 n に対して「b は n のべき乗」を定義するために簡単に適用できます。ここで、各 a iは素数 p iおよび pのべき乗です。 i = p j → i=j.
どうですか：
∀x: ∀y: (SSx･y = b → ∃z: z･SS0 = SSx)
(英語では、2 以上の b の約数は、それ自体が 2 で割り切れる必要があります。文字通り、すべての自然数 x と y について、(2+x) * y = b の場合、これは、次のような自然数 z が存在することを意味します。 z * 2 = (2+x). )
これがTNTと命題計算の構文で許可されていることを 100% 確信しているわけではありません。GEB を熟読してからしばらく経ちました。
(編集:少なくともb = 2 nの問題について; 10 は素数ではないため、10 nがより難しい理由がわかります。しかし、11 nは、1 つの用語「SS0」を「SSSSSSSSSSSS0」に置き換えることを除いて同じです。 .)
これが私が思いついたものです：
∀c：∃d：<（c * d = b）→＆lt;（c = SO）v∃e：（d = e * SSO）>>
これは次のように解釈されます。
すべての数cに対して、c x dがbに等しい場合はcが1であるか、dがex2に等しい数eが存在するような数dが存在します。
または
すべての数cに対して、数dが存在します。たとえば、bがcの因数であり、dの場合、cは1であるか、dは2の因数です。
または
2つの数値の積がbの場合、そのうちの1つは1であるか、1つは2で割り切れる
または
bのすべての除数は1であるか、2で割り切れる
または
bは2の累乗です
bが2の累乗であることを意味するオープン式の場合、次のようになります。∀a:~∃c:(S(Sa ∙ SS0) ∙ Sc) = b
これは事実上、すべてのaについて、S（Sa∙SS0）はbの係数ではないことを示しています。しかし、通常、S（Sa∙SS0）は1 + ((a + 1) * 2)または3 + 2aです。これで、ステートメントを「少なくとも3である奇数はbの因数ではない」と言い換えることができます。これは、bが2の累乗である場合にのみ当てはまります。
私はまだbに取り組んでいます10の累乗の問題です。
これが、「b は 2 の累乗である」というステートメントについて私が思いついたものです。
∃b: ∀a: ~∃c: ((a * ss0) + sss0) * c = b
これは、「すべての数 a に対して、(a * 2) + 3 (つまり、2 より大きい奇数) に c を掛けた数 c が存在しないような数 b が存在し、あなたにbを与えます。」では、b が存在し、ゼロにすることができず、2 より大きい奇数約数がない場合、b は必ずしも 1、2、または別の 2 の累乗ではないでしょうか?
上記のほとんどは、b が 4 の倍数でなければならないことを示しているだけだと思います。これはどうですか: ∃b:∀c:<<∀e:(c∙e) = b & ~∃c':∃c' ':(ssc'∙ssc'') = c> → c = 2>
フォーマットは完璧ではないと思いますが、次のように書かれています。
すべての c に対して、c が b の因数であり、c が素数である場合、c が 2 に等しいような b が存在します。
b の私の解は 2 の累乗です: ∀x: ∃y xy=b ( isprime(x) => x = SS0 )
isprime() を書くのは難しくありません。