Weak theories of concatenation and
undecidability
HORIHATA Yoshihiro
May 7, 2010
Tohoku university logic seminar
Main results
We define a new theory of concatenation WTC such that:
Q ⊲ ⊳ TC
▽ ▽
R ⊲⊳ WTC
Contents
• Preliminary
• TC, Q, and undecidablity
• WTC, R, and undecidablity
• (Appendix)
babababababababababababababab
Preliminary:
interpretability and undecidability
Definition of interpretation
Σ,Ξ : languages of first order logic.
T, S : Σ-theory and Ξ-theory respectively.
A relative translation τ : Σ → Ξ is a pair hδ,Fi such that - δ is Ξ-formula with one free variable.
- F is a mapping from relation-symbol R of Σ to a Ξ-formula F(R).
We translate Σ-formulas to Ξ-formulas as follows:
• (R(x1,· · · , xn))τ := F(R)(x1,· · · , xn);
• (·)τ commutes with the propositional connectives;
• (∀xϕ(x))τ := ∀x(δ(x) → ϕτ);
• (∃xϕ(x))τ := ∃x(δ(x) ∧ ϕτ).
Definition of interpretation
Definition (relative interpretation)
✓ ✏
Σ-theory T is (relatively) interpretable in Ξ-theory S, de- noted by S ⊲ T , iff
there exists a relative translation τ : Σ → Ξ such that T ⊢ ϕ ⇒ S ⊢ ϕτ.
T is faithfully interpretable in S, denoted by S D T , iff there exists a relative translation τ : Σ → Ξ such that
T ⊢ ϕ ⇔ S ⊢ ϕτ.
✒ ✑
Properties of interpretation Proposition
✓ ✏
(1) S ⊲ T and T is essentially undecidable ⇒ S is also essentially undecidable.
(2) S ⊲ T and S is consistent ⇒ T is consistent. (3) S D T and T is undecidable ⇒ S is undec.
✒ ✑
Remark: –Interpretability can be taken as a measure of strength of axiomatic theories.
– We can’t replace “D” into ⊲, since the undecidable thoery of groups is interpretable in the decidable theory of Abelian groups.
TC : Theory of Concatenation
In his paper “Undecidablity without arithmetization”,
A. Grzegorczyk defined the (⌢,ε,α,β,γ)-theory of concate- nation TC with the following axioms:
(TC1) ∀x(x⌢ε = ε⌢x = x)
(TC2) ∀x∀y∀z(x⌢(y⌢z) = (x⌢y)⌢z) (TC3) ∀x∀y∀u∀v(x⌢y = u⌢v →
∃w((x⌢w = u∧y = w⌢v)∨(x = u⌢w∧w⌢y = v))) (TC4) α 6= ε ∧ ∀x∀y(x⌢y = α → x = ε ∨ y = ε)
(TC5) β 6= ε ∧ ∀x∀y(x⌢y = β → x = ε ∨ y = ε) (TC6) γ 6= ε ∧ ∀x∀y(x⌢y = γ → x = ε ∨ y = ε) (TC7) α 6= β ∧ β 6= γ ∧ γ 6= α
About (TC3); editors axiom
x y
u v
About (TC3); editors axiom
x y
u v
About (TC3); editors axiom
x y
u v
w w
TC : Theory of Concatenation Definition
✓ ✏
• x ⊑ y ≡ ∃k∃l(kxl = y)
• x ⊑ini y ≡ ∃l(xl = y)
• x ⊑end y ≡ ∃k(kx = y)
✒ ✑
What can TC prove? Proposition
✓ ✏
TC proves the following assertions: (1) ∀x(xα 6= ε ∧ αx 6= ε)
(2) ∀x∀y(xy = ε → x = ε ∧ y = ε)
(3) ∀x∀y(α ⊑end xy → y = ε ∨ α ⊑end y)) (4) ∀x∀y(xα = yα ∨ αx = αy → x = y) (5) ∀x∀y(α ⊑ xy → α ⊑ x ∨ α ⊑ y)
✒ ✑
What cannot TC prove? Proposition
✓ ✏
TC cannot prove the following assertions: (1) ∀x¬(∃y(y 6= ε ∧ xy = x))
(2) ∀x∀y∀z(xz = yz → x = y)
✒ ✑
TC and undecidablity
In 2005’s, Grzegorczyk proved that TC is unde- cidable.
And he left the following conjectures: Grzegorczyk’s conjecture
✓ ✏
He conjectured that:
(A)TC is essentially undecidable;
(B)TC is essentially weaker than the Robinson’s arithmetic Q.
(B’)(In formally) TC cannot interpret Q.
✒ ✑
TC and undecidablity
• For the conjecture (A), in 2008’s, Grzegorczyk and Zdanowski solved positively, that is, TC is essentially undecidable.
• For the conjecture (B), in 2009’s, Visser and Rachel, Svejdar, and Ganea independently solved negatively, that is, TC interprets Q.
Remark: It is well known that Q interprets TC, since Q interprets I∆0.
Hence, TC and Q are mutually interpretable.
TC and Q
The difficulty of the interpretation of Q in TC is to translate the product totally.
Another translation of Q in TC is as follows:
• 0 ⇒ ε;
• 1 ⇒ α;
• x + y ⇒ x⌢y.
For example, 3 ⇒ ααα, 4 + 2 ⇒ (αααα)⌢(αα) = αααααα
TC and Q
We see the idea of translation of the product. (Example)4 × 3
Let α4 = αααα. We make the witnessing of product as follows:
(ε,ε) → (α, α4) → (αα,α4α4) → (ααα,α4α4α4) In TC, it is not possible to prove that a witnessing exists for each choice of x, y. It is also not possible to prove that if we can find the witnessing of the prod- uct x × y, it is uniquely determined.
To overcome this problem, there are two ways; (i)Visser and Rachel’s method, (ii)Svejdar or Ganea’s method.
TC ⊲ Q; Visser and Rachel’s proof
First, in 2008’s, Rachel defined the new theory TCQ of concatenation and proved TCQ ⊲ Q. Sec- ondly, in 2009’s, Visser proved TC ⊲ TCQ. Hence, TC interprets Q. Here, the theory TCQ has the fol- lowing axioms:
(TCQ1) Sα(x) 6= ε; (TCQ2) Sβ (x) 6= ε;
(TCQ3) Sα(x) 6= Sβ (x);
(TCQ4) Sα(x) = Sα(y) → x = y; (TCQ5) Sβ (x) = Sβ(y) → x = y; (TCQ6) c⌢ε = x;
(TCQ7) x⌢Sα(y) = Sα(x⌢y); (TCQ8) x⌢Sβ (y) = Sβ(x⌢y);
(TCQ9) x = ε ∨ ∃y(x = Sα(y) ∨ x = Sβ(y)).
TC ⊲ Q; Svejdar or Ganea’s proof
First, in 2008’s, Svejdar proved that Q− inter- prets Q.
Then, in 2009’s, Svejdar and Ganea independently proved that TC interprets Q−.
Q− is (0, S, A, M)-theory with the following axioms:
(A) A(x, y, z1) ∧ A(s, y, z2) → z1 = z2; (M) M(x, y, z1) ∧ M(s, y, z2) → z1 = z2; (Q1) S(x) = S(y) → x = y;
(Q2) S(x) 6= 0;
(Q3) x 6= 0 → ∃y(x = S(y)); (G4) A(x, 0, x);
(G5) (∃zA(x, y, z) ∧ u = S(z)) → A(x, S(y), u); (G6) M(z, 0, 0);
(G7) (∃zM(x, y, z) ∧ A(z, x, u)) → A(x, S(y), u).
(∗)Historical issue
In Ganea’s paper, he also proved that F interprets Q and hence F is essentially undecidable. But F was introduced by
Tarski at 1953’s and he stated in Tarski, Robinson and Mostowski’s book “Undecidable theories”, but without proof, that F is es-
sentially undecidable since F interprets Q. There is a histor- ical problem: We can easily find the interpretation of TC in F. In other hand, in both proofs of the interpretabilities of Q in Q− (by Svejdar) and Q in TCQ (by Rachel), the Solovay’s method of shortening cuts is used essentially. But this method was inspired by Solovay at 1976’s. So, the issue is what is the Tarski’s original proof of the interpretability of Q in F?
TC and F
The Tarski’s theory F has the following axioms: (F1) ∀x(xε = εx = x);
(F2) ∀x∀y∀z(x(yz) = (xy)z);
(F3) ∀x∀y∀z(xz = yz ∨ zx = zy → x = y); (F4) ∀x∀y(xα 6= yβ);
(F5) ∀x(x 6= ε → (∃u(x = uα ∨ x = uβ))) Facts
✓ ✏
– Theories F and TC are incomparable. – F and TC are mutually interpretable.
✒ ✑
babababababababababababababab
Our new theories of concatenation
and
mutuall interpretability with R
WTC and R
Our main result is as follows: Theorem
✓ ✏
• WTC interprets Robinson’s very weak arith- metic R.
• As a corollary of the above, WTC is essen- tially undecidable.
• R interprets WTC.
• As a corollary of the above, TC is not inter- pretable in WTC.
✒ ✑
Why the target theory is R?
Arithmetic R has the following axioms: for each n, m ∈ ω,
(R1) n + m = n + m; (R2) n · m = n · m;
(R3) n 6= m (if n 6= m); (R4) ∀x(x ≤ n → _
m≤n
x = m).
Here, we define x ≤ y ≡ ∃z(x + z = y).
Why the target theory is R? Reason 1
✓ ✏
Since R is locally finitely satisfiable, R cannot in- terpret Q. Hence, R is much weaker than Q, but still essentially undecidable.
Moreover, Jones and Shepherdson proved the following theorems:
• R is minimal essentially undecidable which satisfies Σ1-completeness.
• R − (R1) is minimal essentially undecidable.
✒ ✑
Why the target theory is R? Reason 2
✓ ✏
In 2009’s, Visser proved the following theorem:
• If a theory T is locally finitely satisfiable, then, T is interpretable in R.
Here, a theory T is locally finitely satisfiable if each finite subtheory of T has a finite model.
✒ ✑
WTC: Weak Theoy of Concatenation
WTC has the following axioms: for each u ∈ {a, b, c}+ (WTC1) ∀x ⊑ u(x⌢ε = ε⌢x = x);
(WTC2) ∀x∀y∀z[[x⌢(y⌢z) ⊑ u ∨ (x⌢y)⌢z ⊑ u] → x⌢(y⌢z) = (x⌢y)⌢z];
(WTC3) ∀x∀y∀s∀t[(x⌢y = s⌢t ∧ x⌢y ⊑ u) →
∃w((x⌢w = s ∧ y = w⌢t) ∨ (x = s⌢w ∧ w⌢y = t))]; (WTC4) α 6= ε ∧ ∀x∀y(x⌢y = α → x = ε ∨ y = ε); (WTC5) β 6= ε ∧ ∀x∀y(x⌢y = β → x = ε ∨ y = ε); (WTC6) γ 6= ε ∧ ∀x∀y(x⌢y = γ → x = ε ∨ y = ε); (WTC7) α 6= β ∧ β 6= γ ∧ γ 6= α.
WTC: Weak Theoy of Concatenation Definition
✓ ✏
• x ⊑ y ≡ (x = y) ∨ ∃k∃l[kx = y ∨ xl = y ∨ (kx)l = y ∨ k(xl) = y]
• x ⊑ini y ≡ ∃l(xl = y)
• x ⊑end y ≡ ∃k(kx = y)
✒ ✑
Σ1-completeness of WTC Lemma
✓ ✏
WTC proves the following assertion:
∀x(x ⊑ u ↔ _
v⊑u
x = v).
✒ ✑
Theorem
✓ ✏
WTC is Σ1-complete, that is, for each Σ1-formula ϕ, if {a, b, c}+ ϕ then WTC ⊢ ϕ.
✒ ✑
WTC interprets R
translation of 0, 1,+
✓ ✏
We translate 0, 1,+ as follows:
• 0 ⇒ ε;
• 1 ⇒ α;
• x + y ⇒ x⌢y.
✒ ✑
To translate the product, we have to make it total on ω.
To do this, we define a notion “good string”.
WTC interprets R
Definition of “Good”
✓ ✏
We define the formula Good(x) as follows:
Good(x) ≡ ID(x) ∧ AS(x) ∧ EA(x), where
• ID(x) ≡ ∀s ⊑ x(s⌢ε = ε⌢s = s);
• AS(x) ≡ ∀s0∀s1∀s2[[s0⌢(s1⌢s2) ⊑ x ∨ (s0⌢s1)⌢s2 ⊑ x] → s0⌢(s1⌢s2) = (s0⌢s1)⌢s2]
• EA(x) ≡ ∀s0∀s1∀t0∀t1[(s0⌢s1 = t0⌢t1 ∧ s0⌢s1 ⊑ x) →
∃w((s0⌢w = t0 ∧ s1 = w⌢t1) ∨ (s0 = t0⌢w ∧ w⌢s1 = t1))]
✒ ✑
WTC interprets R Properties of Good
✓ ✏
(1) For each u ∈ {a, b, c}+, WTC ⊢ Good(u); WTC proves the following assertions:
(2) ∀x[Good(x) → ∀y(y ⊑ x ↔ ∃k∃l[(ky)l = x])]; (3) ∀x(Good(x) → TR⊑(x)), where
TR⊑(x) ≡ ∀y∀z(y ⊑ x ∧ z ⊑ y → z ⊑ x); (4) ∀x(Good(x) → ∀y ⊑ x Good(y)).
✒ ✑
WTC interprets R
To translate the product, we define the witnessing for product.
First, we define a notion “number strings” as fol- lows:
Definition of “Num”
✓ ✏
We define the formula Num(x) as follows:
Num(x) ≡ ∀y((y ⊑ x ∧ y 6= ε) → α ⊑end y).
✒ ✑
✓Fact ✏
For each u ∈ {a}+, WTC ⊢ Num(u).
✒ ✑
Definition of PWitn
✓ ✏
We define a formula PWitn(x, y, w) as follows: (i) Num(x) ∧ Num(y) ∧ Good(w);
(ii) βγβ ⊑ini w;
(iii) ∃z(Num(z) ∧ βyγzβ ⊑end w);
(iv) ∀p∀z(Num(z) ∧ pβyγzβ = w → ∀z′(Num(z′) →
¬(βyγz′β ⊑ pβ));
(v) ∀p∀q∀s2∀t2[(Num(s2) ∧ Num(t2) ∧ pβs2γt2βq = w ∧ p 6= ε)
→ (∃s1∃t1(Num(s1) ∧ Num(t1) ∧ s2 = s1α ∧ t2 = t1x ∧ βs1γt1β ⊑end pβ))];
(vi) ∀p∀q∀s∀t((Num(s1) ∧ Num(t1) ∧ pβsγtβq = w ∧ q 6= ε) → βsαγtxβ ⊑ini βq).
✒ ✑
WTC interprets R Example
✓ ✏
Witnessing w for 2 × 3 is as follows:
w = βγβαγααβααγ(αα)(αα)βαααγ(αα)(αα)(αα)β
This is from
(0, 0) → (1, 2) → (2, 2 + 2) → (3, 2 + 2 + 2).
✒ ✑
WTC interprets R
Teanslation of product
✓ ✏
We translate the multiplication “x × y = z” into the formula M(x, y, z) as follows:
M(x, y, z) ≡ (∃!wPWitn(x, y, w) ∧ γzβ ⊑end w)∨ (¬(∃!wPWitn(x, y, w))) ∧ z = 0.
✒ ✑
WTC interprets R Main theorem
✓ ✏
For each u, v ∈ {a}+, there exists w ∈ {a, b, c}+ such that WTC proves
PWitn(u, v, w) ∧ ∀w′(PWitn(u, v, w′) → w = w′).
✒ ✑
In what follows, we see the each steps of the proof of this main theorem.
Proof of the main theorem Lemma
✓ ✏
WTC proves the following assertions:
(1) Good(xβs) ∧ xβs = yβt ∧ ¬(β ⊑ s) ∧ ¬(β ⊑ t)
→ (x = y ∧ s = t).
(2) Good(xβsβ p) ∧ xβsβ p = yβtβ ∧ ¬(β ⊑ s) ∧ ¬(β ⊑ t)
→
((y ∧ s = t ∧ p = ε)∨
∃w(xβsβw = yβ ∧ wtβ = p).
✒ ✑
Proof of the main theorem Fix u ∈ {a}+.
Existence of the witnessing
✓ ✏
We can prove the existence of the witnessing
w ∈ {a, b, c}+ by the meta-induction on the length of v ∈ {a}+.
✒ ✑
Proof of the main theorem
To prove the uniqueness of the witnessing, we prove the following two lemmas: Fix u, v ∈ {a}+ and let w ∈ {a, b, c}+ be some witnessing for u, v. In WTC, let w′ be such that PWitn(u, v, w′). Then,
Lemma.1
✓ ✏
(1) For each k, l ∈ {a}+,
WTC ⊢ ∀p(pβ kγlβ ⊑ini w → pβ kγlβ ⊑ini w′); (2) WTC ⊢ w ⊑ini w′.
✒ ✑
Proof of the main theorem
w′ w
β γβ β γβ
Proof of the main theorem
w′ w
β γβ β γβ β γβ
Proof of the main theorem
w′
w β αγuβ
Proof of the main theorem
w′
w β αγuβ
β αγuβ
Proof of the main theorem
w′
w β ααγuuβ
Proof of the main theorem
w′
w β ααγuuβ
β ααγuuβ
Proof of the main theorem
w′ w
Proof of the main theorem
Finally, to prove w = w′ by way of contradiction, let us assume that ∃q(wq = w′ ∧ q 6= ε).
Proof of the main theorem
Finally, to prove w = w′ by way of contradiction, let us assume that ∃q(wq = w′ ∧ q 6= ε).
Then,
w′ w
q (6= ε)
Proof of the main theorem
Finally, to prove w = w′ by way of contradiction, let us assume that ∃q(wq = w′ ∧ q 6= ε).
Then,
w′
w β vγz0β
Proof of the main theorem
Finally, to prove w = w′ by way of contradiction, let us assume that ∃q(wq = w′ ∧ q 6= ε).
Then,
w′
w β vγz0β
β vγz1β
Proof of the main theorem
Finally, to prove w = w′ by way of contradiction, let us assume that ∃q(wq = w′ ∧ q 6= ε).
Then,
w′
w β vγz0β
β vγz1β β vγz0β
Proof of the main theorem
Finally, to prove w = w′ by way of contradiction, let us assume that ∃q(wq = w′ ∧ q 6= ε).
Then,
w′ w
β vγz1β β vγz0β
contradict to the def. of PWitn
R interprets WTC
Conversly, we can prove that R interprets WTC, by applying the Visser’s following theorem:
Visser’s theorem (2009’s)
✓ ✏
If a theory T is locally finitely satisfiable, then, T is interpretable in R.
✒ ✑
Since WTC is locally finitely satisfiable, we can get the following result:
Theorem
✓ ✏
R interprets WTC.
✒ ✑
Conclusion
We proved following results: Theorem
✓ ✏
• WTC and R are mutually interpretable.
• WTC is essentially undecidable.
• WTC cannot interpret TC.
✒ ✑
Qustions Theorem
✓ ✏
• Is there some theory T such that R ⋫ T and T ⋫ Q?
• Is there some theory T such that
T ⋫ Q and T and R are incompatible, in the sense of interpretability?
✒ ✑
References
[1] V. Cacic, P. Pudlak, G. Restall, A. Urquhart, and A. Visser. Decorated linear order types and the theory of concatenation. October 4, 2007.
[2] M. Ganea. Arithmetic on semigroups. The Journal of Symbolic Logic, 74(1):265–278, 2009.
[3] A. Grzegorczyk. Undecidability without arithmetization. Studia Logica, 79(1):163–230, 2005.
[4] A. Grzegorczyk and K. Zdanowski. Undecidability and concatenation. In V. W. Marek A. Ehrenfeucht and M. Srebrny, editors, Andrzej Mostowski and foudational studies, pages 72–91. IOS Press, 2008.
[5] J. P. Jones and J. C. Shepherdson. Variants of robinson’s essentially undecid- able theory R. Archive for Math. Logic, 23:65–77, 1983.
[6] W. V. Quine. Concatenation as a basis for arithmetic. J. Symbolic Logic, 11:105–114, 1946.
[7] Sterken Rachel. Concatenation as a basis for Q and the intuitionistic varient of Nelson’s classic result. Master’s thesis, Universiteit van Amsterdam, October 2008.
[8] R. M. Solovay. Interpretability in set theories. August 1976. unpublished letter to P. H´ajek, http://www.cs.cas.cz/hajek/RSolovayZFGB.pdf.
[9] V. Svejdar. An interpretation of Robinson arithmetic in its Grzegorczyk’s weaker varient. Fundamenta Informaticae, 81:347–354, 2007.
[10] V. Svejdar. On interpretability in the theory of concatenation. Nortre Dame Journal of Formal Logic, 50(1):87–95, 2009.
[11] V. Svejdar. Relatives of Robinson arithmetic. In The Logica Yearbook 2008: Proceedings of the Logica 08 International Conference. 2009.
[12] A. Tarski, A. Mostowski, and R. M. Robinson. Undecidable theories. North- Holland, 1953.
[13] R. L. Vaught. On a theorem of cobham concerning undecidable theories. In E. Negel, P. Suppes, and A. Tarski, editors, Logic, Methodology, and Philoso- phy of Science. Stanford University Press, 1962.
[14] A. Visser. Growing commas – a study of sequentiality and concatenation. Nortre Dame Journal of Formal Logic, 50(1):61–85, 2009.
[15] A. Visser. Why the theory R is special. August 10, 2009.
Appendix
Let us think the next arithmetical statement: (R6) ∀x∀y(x · y = n ∧ y 6= 0 → x ≤ n)
✓Fact ✏
• R ( R + (R6) and R + (R6) ( Q.
• R and R + (R6) are mutually interpretable.
✒ ✑
Another weak theory TCH of concatenation (H1) u⌢ε = ε⌢u = u
(H2) u0⌢(u1⌢u2) = (u0⌢u1)⌢u2
(H3) ∀x∀y∀s∀t(x⌢y = s⌢t ∧ s⌢t ⊑ u →
∃w((x⌢w = s ∧ y = w⌢t) ∨ (x = s⌢w∧ w⌢y = t))) (H4) α 6= ε ∧ (u⌢v = α → u = ε ∨ v = ε)
(H5) β 6= ε ∧ (u⌢v = β → u = ε ∨ v = ε) (H6) γ 6= ε ∧ (u⌢v = γ → u = ε ∨ v = ε) (H7) α 6= β ∧ β 6= γ ∧ γ 6= α
(H8) ∀x(x ⊑ u → _
v⊑u
x = v)
Another weak theory TCH of concatenation
✓Fact ✏
Th(WTC) = Th(TCH)
✒ ✑
