ファイル置き場 Sendai Logic Homepage speaker19

Interpretation between weak theories of

concatenation and arithmetic

Osam Yoshida and Yoshihiro Horihata

(Tohoku university)

Feb 23, 2012

Workshop on Proof Theory and Computability Theory 2012

Fundamental human abilities

読み（ _yomi ） 書き（ _kaki ） そろばん（ _soroban ）

Fundamental human abilities

読み（ _yomi ） 書き（ _kaki ） そろばん（ _soroban ）

|| || ||

Reading Writing Abacus (Arithmetic)

Figure 1: Reading and Writing Figure 2: Abacus

Fundamental human abilities

Reading Writing Arithmetic

↑

Well-studied !

Example

PA, IΣ

, Q, R,

second-order arithmetic, etc

Fundamental human abilities

Reading Writing Arithmetic

1930’s Tarski

1940’s Quine

Fundamental human abilities

Reading Writing Arithmetic

1930’s Tarski

1940’s Quine

↓

2005 Grzegorczyk’s TC

A Theory of Concatenation

babababababababababababababab

Back ground and known results

C

^{⊲ ⊳ PA}

▽ ▽

TC _{⊲ ⊳} Q

TC : Theory of Concatenation

In A. Grzegorczyk’s paper “Undecidability without arith- metization”(2005), he defined a (^⌢,_ε,_α,_β)-theory TC of con- catenation, whose axioms are:

(TC1) _∀x(x

_{ε = ε}

x _{= x)}

(TC2) _{∀x∀y∀z(x}

_(y

z _{) = (x}

y ₎

z ₎

(TC3) Editors Axiom:

∀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= β}

About (TC3); editors axiom

If x

y _{= u}

v,

x ^y

u ^v

About (TC3); editors axiom

If x

y _{= u}

v,

x ^y

u ^v

About (TC3); editors axiom

If x

y _{= u}

v,

x ^y

u ^v

w

w

TC : Theory of Concatenation

Definition

✓ ✏

• ^x ⊑ y ≡ ∃k∃l(kxl = y)

• ^x ⊑

^y ≡ ∃l(xl = y)

• ^x ⊑

^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(xα = yα ∨α^x = α^y → x = y) Weak cancellation

✒ ✑

Proposition

✓ ✏

TC cannot prove the following assertions:

• ∀x∀y∀z(xz = yz → x = y) cancellation

✒ ✑

TC and undecidability

Theorem [Grzegorczyk, 2005]

✓ ✏

TC is undecidable.

✒ ✑

Moreover,

Theorem [Grzegorczyk and Zdanowski, 2007]

✓ ✏

TC is essentially undecidable.

✒ ✑

Before this, Yaegashi proved this fact in 2006 in his

master’s thesis, by interpreting arithmetic R in TC.

Grzegorczyk and Zdanowski conjectured that TC

and Q are mutually interpretable.

Definition of interpretation

L₁,L₂ : languages of first order logic.

A relative translation _τ : L₁ → L₂ is a pair h_δ,Fi such that

• δ ^{is an L}2-formula with one free variable.

• F maps each relation-symbol R of L₁ to an L₂-formula F(R).

We translate L₁-formulas to L₂-formulas as follows:

• (R(x₁^,· · · , x_n))^τ := F(R)(x₁^,· · · , x_n);

• (·)^τ commutes with the propositional connectives;

• (∀xϕ(x))^{τ :}= ∀x(δ(x) → ϕ^τ);

• (∃xϕ(x))^{τ :}= ∃x(δ(x) ∧ ϕ^τ).

Definition of interpretation

Definition (relative interpretation)

✓ ✏

L₁-theory T is (relatively) interpretable in L₂-theory S, de- noted by S ⊲ T , iff

there exists a relative translation _τ : L_{1 → L2} such that for each axiom _σ of T , S ⊢ _σ^τ.

✒ ✑

Proposition

✓ ✏

Let S be a consistent theory.

If S ⊲ T and T is essentially undecidable, then S is also es- sentially undecidable.

✒ ✑

That is, the interpretability conserves the essential undecid- ability.

TC and Q

In 2009, the following results were proved by three ways independently:

Visser and Sterken, ˇSvejdar, and Ganea. Theorem [2009]

✓ ✏

TC interprets Q. (Hence TC ✄ ✁ Q.)

✒ ✑

Here, Q is Robinson’s arithmetic, whose language is (+, ·, 0, S) (Q1) ∀x∀y(S(x) = S(y) → x = y) (Q2) ∀x(S(x) 6= 0)

(Q3) ∀x(x + 0 = x) (Q4) ∀x∀y(x + S(y) = S(x + y)) (Q5) ∀x(x · 0 = 0) (Q6) ∀x∀y(x · S(y) = x · y + x) (Q7) ∀x(x 6= 0 → ∃y(x = S(y)))

Q is essentially undecidable and finitely axiomatizable.

Theory C

and Peano arithmetic PA

The theory C

of concatenation consists of TC

plus the following notation induction:

ϕ ⁽ ε ^{) ∧ ∀x (} ϕ ^{(x) →} ϕ ^(x

α ^{) ∧} ϕ ^(x

β ^{)) → ∀x} ϕ ^(x).

Here, _ϕ is a ₍

, _ε , _α , _{β )-formula.}

Then, Ganea proved that

Theorem [Ganea, 2009]

✓ ✏

C

and PA are mutually interpretable.

✒ ✑

This is a positive answer for Yaegashi’s question

raised in his master thesis.

babababababababababababababab

Part I

A weak theory WTC of concatenation

and

mutual interpretability with R

Arithmetic R (MRT, 1953)

(+, ·, 0, 1, ≤)-theory R

✓ ✏

For each n, m _{∈ ω} , ( n represents 1 + · · · + 1

| {z }

n

)

(R1) n + m = n + m

(R2) n · m = n · m

(R3) n 6= m (if n 6= m)

(R4) ∀x x ≤ n → x = 0 ∨ x = 1 ∨ · · · ∨ x = n

(R5) ∀x(x ≤ n ∨ n ≤ x)

✒ ✑

* R is _Σ

-complete and essentially undecidable.

* R _{6 ✄} Q, since Q is finitely axiomatizable.

Arithmetic R

(Cobham, 1960’s)

(+, ·, 0, 1, ≤)-theory R

✓ ✏

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↔} x = 0 ∨ x = 1 ∨ · · · ∨ x = n

✒ ✑

* R₀ interprets R by translating ‘ ≤ ’ by ‘ ⋖ ’ as follows: x ⋖ y ≡ [0 ≤ y ∧ ∀u (u ≤ y ∧ u 6= y → u + 1 ≤ y)] → x ≤ y.

* R₀ is minimal theory which is _Σ1-complete and essentially undecidable.

WTC : Weak Theory of Concatenation

(

^, _ε ^, _α ^, _β )-theory WTC has the following

axioms: for each u _{∈ { α} , _{β }}

,

(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= β} .

WTC: Weak Theory of Concatenation

Here, {_α^,_β}^∗ is a set of finite strings over {_α^,_β}, including empty string _ε. Let _{α,_β}⁺ :_{= {α},_β}^∗ _{\ {ε}.}

For each u ∈ {_α^,_β}^∗, we represent u in theories as u by adding parentheses from left. For example, _ααβα = ((_αα)_β)_α. We call each u (∈ {_α^,_β}^∗) standard string.

Definition

✓ ✏

• ^x ⊑ y ≡ (x = y) ∨ ∃k ∃l [kx = y ∨ xl = y ∨ (kx)l = y ∨ k(xl) = y]

• x ⊑ⁱⁿⁱ y ≡ (x = y) ∨ ∃l (xl = y)

• x ⊑^end y ≡ (x = y) ∨ ∃k (kx = y)

✒ ✑

Σ

-completeness of WTC

Lemma

✓ ✏

WTC proves the following assertion:

∀x (x ⊑ u ↔ ^_

v⊑u

x _{= v).}

✒ ✑

Theorem

✓ ✏

WTC is _Σ

-complete, that is, for each

Σ

^-sentence ϕ ^{, if {} α ^, β ^}

_ ϕ ^{then WTC ⊢} ϕ ^.

✒ ✑

{ α ^, β }

is a standard model of TC.

WTC interprets R

From now on, we consider the translation of R into WTC. translation of 0, 1,+

✓ ✏

We translate 0, 1,+ as follows:

• 0 ⇒ _ε;

• ¹ ⇒ α^;

• ^x+ y ⇒ x^⌢y;

• ^x ≤ y ⇒ ∃z (x^⌢z = y).

✒ ✑

To translate the product, we have to make it total

on _ω . To do this, we consider notion, “witness for

product”.

WTC interprets R

An idea for the definition of witness

✓ ✏

Witness w for 2× 3 is as follows:

w = βββββαβααββααβ(αα)(αα)ββαααβ(αα)(αα)(αα)ββ

This is from the following interpretation of 2_{× 3:} (0, 0) → (1, 2) → (2, 2 + 2) → (3, 2 + 2 + 2). That is, 2× 3 is interpreted as adding 2 three times.

✒ ✑

By the help of above idea, we can represent the re-

lation “ w is a witness for product of x and y ” by a

formula PWitn _{(x, y, w).}

WTC interprets R

Translation of product

✓ ✏

We translate the multiplication “x× y = z” by (∃!w PWitn(x, y, w) ∧_ββz_β ⊑end w)∨

(¬(∃!w PWitn(x, y, w))) ∧ z = 0.

✒ ✑

Lemma (uniqueness of the witness on _ω)

✓ ✏

For each u, v _{∈ {α}}^∗, there exists w _{∈ {α},_β}^∗ such that WTC proves

PWitn(u, v, w) ∧ ∀w^′(PWitn(u, v, w^′) → w = w^′).

✒ ✑

Theorem

✓ ✏

WTC interprets R.

✒ ✑

R interprets WTC

Conversely, we can prove that R interprets WTC, by apply- ing the Visser’s following theorem:

Visser’s theorem (2009)

✓ ✏

T is interpretable in R iff T is locally finitely satisfiable

✒ ✑

Here, a theory T is locally finitely satisfiable iff any finite sub- theory of T has a finite model.

Since WTC is locally finitely satisfiable, we can get the follow- ing result:

Corollary

✓ ✏

R interprets WTC.

✒ ✑

Conclusion of part I Theorem

✓ ✏

WTC and R are mutually interpretable.

✒ ✑

Corollary

✓ ✏

(1) WTC is essentially undecidable.

(2) WTC interprets T iff T is locally finitely satisfiable. (3) ^{WTC cannot} interpret TC.

(4) ^WTC₂ ^{and WTC}_n (n ≥ 2) are mutually interpretable.

✒ ✑

Here, WTC_n is WTC with n-th single-letters. (4) is from WTC₂ ^✄R ✄ WTC_n ^✄WTC_2.

babababababababababababababab

Part II

Minimal essential undecidability

and

variations of WTC

Minimal essential undecidability Question

✓ ✏

Is WTC minimal essentially undecidable ?

✒ ✑

Here, minimal essentially undecidable means if one omits one axiom from WTC, then the resulting theory is no longer essen- tially undecidable. Again, WTC is: for each u ∈ {_α^,_β}^∗

(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= _β.

Minimal essential undecidability Proposition

✓ ✏

WTC−(WTC k) (k = 3, 4, 5, 6) is not essentially undecid- able.

✒ ✑

We can find a decidable consistent extension of each WTC_{−(WTC k)} (k = 3, 4, 5, 6). Hence remaining question is

WTC−(WTC k) (k = 1, 2) is essentially undecidable ? Recently, we proved the following:

Theorem

✓ ✏

WTC−(WTC1) can interpret WTC.

Hence, WTC−(WTC1) is still essentially undecidable.

✒ ✑

WTC−(WTC1) ✄ ✁ WTC This is proved as follows. Lemma

✓ ✏

For each u _{∈ {α},_β}^∗, WTC - (WTC1) proves u_{ε = ε}u _{= u.}

✒ ✑

⇒ Without (WTC1), axiom for identity, we can prove that the empty string works well, as an identity element, for at least all standard strings.

Main Lemma

✓ ✏

WTC - (WTC1) ⊢ ∀x (x ⊑ u∧∃x^′(x = (_εx^′)_ε) → ^W_v⊑ux = v).

✒ ✑

Although we do not know whether WTC−(WTC1) can prove

∀x (x ⊑ u → ^W_v⊑u^x = v) or not, the above corollary is strong enough to interpret WTC into WTC−(WTC1).

WTC−(WTC1) ✄ ✁ WTC

Then, we interpret WTC in WTC - (WTC1) as follows: Domain _δ(x) ≡ x = _α ∨ ∃x^′(x = (_βx^′)_ε).

Remark that if (_βx^′)_ε is standard, then (_βx^′)_ε = _β((_εx^′)_ε). Constants _ε ⇒ _β, _α ⇒ _βα, _β ⇒ _ββ.

x^⌢y = z Let _Ω(x, y) ≡ ∃!x^′ ∃!y^′(x = (_βx^′)_ε ∧ y = (_βy^′)_ε). Then we translate concatenation as Conc(x, y, z) ≡

x _{= α ∨ y = α → z = α}

∧Ω(x, y) → ∃x^′∃y^′ [x = (_βx^′)_ε ∧ y = (_βy^′)_ε ∧ z = (_β((x^′_ε)y^′))_ε]

∧ o.w. → z = _α. Lemma

✓ ✏

For each w ∈ {_α^,_β}^∗, WTC - (WTC1) can prove that if Conc_{(x, y,β}w), then x and y are also standard.

✒ ✑

WTC −(WTC1) ✄ ✁ WTC

By this lemma, we can prove WTC −(WTC1) ✄ WTC.

Question

✓ ✏

Is WTC −(WTC1) minimal essentially undecid-

able ?

✒ ✑

TC^−ε

On the other hand, we can consider the theory

of concatenation without empty string: ₍

, _α , _{β )-}

theory TC

has the following axioms:

(TC

1) _{∀x∀y∀z(x}

_(y

z _{) = (x}

y ₎

z ₎

(TC

2) Editors Axiom:

∀x ∀y ∀s ∀t (x

^y = s

^t → (x = s ∧ y = t)∨

∃w ((x

^w = s ∧ y = w

^t ) ∨ (x = s

^w ∧ w

^y = t)))

(TC

3) _{∀x ∀y ( α 6= x}

y ₎

(TC

4) _{∀x ∀y ( β 6= x}

y ₎

(TC

5) _{α 6= β}

WTC^−ε

A weak version WTC^−ε of TC^−ε has the following axioms: for each u ∈ {_α,_β}⁺,

(WTC^−ε1) ∀x ∀y ∀z [[x^⌢(y^⌢z)⊑ u∨ (x^⌢y)^⌢z⊑ u]

→ x^⌢(y^⌢z) = (x^⌢y)^⌢z];

(WTC^−ε2) ∀x ∀y ∀s ∀t [(x^⌢y = s^⌢t ∧ x^⌢y⊑ u) → (x = y) ∧ (s = t)∨

∃w ((x^⌢w = s ∧ y = w^⌢t) ∨ (x = s^⌢w∧ w^⌢y = t))]; (WTC^−ε3) ∀x ∀y (x^⌢y 6= _α);

(WTC^−ε4) _{∀x ∀y (x}^⌢y _{6= β);} (WTC^−ε5) _α 6= _β.

For this theory, we proved the following:

WTC^{−ε ✄ ✁}WTC Proposition

✓ ✏

WTC^−ε and WTC are mutually interpretable. Hence WTC^−ε is essentially undecidable.

✒ ✑

WTC ✄ WTC^−ε is easy. We interpret WTC in WTC^−ε as: Domain _{δ(x) ≡ x = α ∨ x = β ∨ ∃x}^′_{(x = β}x^′_).

Constants _ε ⇒ _β, _α ⇒ _βα, _β ⇒ _ββ.

x^⌢y _{= z Let} Ω(x, y) ≡ ∃!x^′ ∃!y^′ (x = β^x′ ∧ y = β^y′), and trans- late the concatenation by Conc(x, y, z) ≡

[x = _α ∨ y = _α → z = _α] ∧ [x = _β → z = y] ∧ [y = _β → z = x]∧ [_Ω(x, y) → ∃x^′ ∃y^′(x = _βx^′ ∧ y = _βy^′ ∧ z = _β(x^′y^′))]∧

[o.w. → z = _α].

WTC^−ε is minimal essentially undecidable Theorem

✓ ✏

WTC

_{is minimal} essentially undecidable.

✒ ✑

The essential part of the above theorem is to prove

“WTC^−ε−(WTC^−ε1) is not essentially undecidable”. This is proved by showing the followings (the proof is due to K. Higuchi):

Theorem (K. Higuchi)

✓ ✏

WTC^−ε_−(WTC^−ε1) is interpretable in S2S.

✒ ✑

Here, S2S is a monadic second-order logic whose language is L _{= {S0},S₁,_{(Pa)a∈A}. S0},S₁ are two successors and P_a’s are unary predicates. Then, S2S := {_ϕ | _ϕ is an L-sentence & {0, 1}^∗ _ ϕ}. S2S is proved to be decidable by M. O. Rabin (1969).

Minimal essential undecidability

This result partially contributes the following ques-

tion by Grzegorczyk and Zdanowski:

Question

✓ ✏

Is TC

minimal essentially undecidable ?

✒ ✑

The remaining part of the question is the essential

undecidability of TC

_−(TC

1), that is, TC with-

out associative law. We can easily find an decidable

extension of each TC

_−(TC

k), (k = 2, 3, 4, 5).

Variations of WTC: WTC+(TC1) + (TC2) ✄ ✁ WTC Recall that

(TC1) _{∀x (x}^⌢_{ε = ε}^⌢x _{= x)}

(TC2) ∀x ∀y ∀z (x^⌢(y^⌢z) = x^⌢(y^⌢z)) (TC3) ∀x∀y∀s∀t[(x^⌢y = s^⌢t) →

∃w((x^⌢w = s ∧ y = w^⌢t) ∨ (x = s^⌢w∧ w^⌢y = t))] Proposition

✓ ✏

WTC interprets WTC+(TC1) + (TC2)

✒ ✑

Because WTC+(TC1) + (TC2) is locally finitely satisfiable. Proposition

✓ ✏

WTC _{can not} interpret WTC+(TC3).

✒ ✑

Because WTC+(TC3) is not locally finitely satisfiable.

Conclusion of Part II

The following are mutually interpretable (n _{≥ 2):}

WTC

+ (Identity) + (Assoc)

WTC

+ (Identity)

WTC

_{+ (Assoc)} WTC

_{+ (Assoc)}

WTC

WTC

WTC

−(Identity)

Theorem

✓ ✏

WTC

is minimal essentially undecidable.

✒ ✑

Questions

(1) Is WTC-(Identity)-(Assoc) essentially undecid-

able ?

⇒ Our conjecture is ^NO.

(2) Is WTC-(Identity) _Σ

-complete ?

⇒ Our conjecture is ^NO.

(3) ^WTC + (Editors Axiom) ⊲ TC ?

⇒ Our conjecture is ^YES.

(4) Are there some natural theory T such that

TC ✄ T ✄ WTC and WTC 6 ✄T and T 6 ✄TC ?

References

[1] M. Ganea. Arithmetic on semigroups. The Journal of Symbolic Logic, 74(1):265–278, 2009.

[2] A. Grzegorczyk. Undecidability without arithmetization. Studia Log- ica, 79(1):163–230, 2005.

[3] A. Grzegorczyk and K. Zdanowski. Undecidability and concatena- tion. In V. W. Marek A. Ehrenfeucht and M. Srebrny, editors, Andrzej Mostowski and foudational studies, pages 72–91. IOS Press, 2008.

[4] Y. Horihata. Weak theories of concatenation and arithmetic. to appear in Notre Dame Journal of Formal Logic.

[5] A. Tarski, A. Mostowski, and R. M. Robinson. Undecidable theories. North-Holland, 1953.

[6] A. Visser. Why the theory R is special. August 10, 2009.

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) ≡ ∀s₀∀s₁∀s₂[[s₀^⌢(s₁^⌢s₂) ⊑ x ∨ (s₀^⌢s₁)^⌢s₂ ⊑ x_{] → s0}^⌢_(s1^⌢s_{2) = (s0}^⌢s₁₎^⌢s_2]

• ^EA(x) ≡ ∀s₀∀s₁∀t₀∀t₁[(s₀^⌢s₁ = t₀^⌢t₁ ∧ s₀^⌢s₁ ⊑ x) →

∃w((s₀^⌢w = t₀ ∧ s₁ = w^⌢t₁) ∨ (s₀ = t₀^⌢w ∧ w^⌢s₁ = t_1))]

✒ ✑

WTC interprets R

Properties of Good

✓ ✏

(1) ^{For each u} ∈ { _α ^, _β ^, _γ }

^{, WTC} ⊢ Good(u);

WTC proves the following assertions:

(2) ∀x(Good(x) → ∀y ⊑ x Good(y)), that is

Good is closed under taking substrings.

✒ ✑

WTC interprets R

To translate the product, we define “witness 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= _ε ) → _α ⊑

^y ).

✒ ✑

✓

Fact

For each u _{∈ { α }}

, WTC _{⊢ Num(u).}

✒ ✑

Definition of PWitn

✓ ✏

We define a formula PWitn(x, y, w) as follows: (i) Num(x) ∧ Num(y) ∧ Good(w);

(ii) _βγβ ⊑ⁱⁿⁱ 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∀s₂∀t₂[(Num(s₂) ∧ Num(t₂) ∧ p_βs_2γt_2βq = w ∧ p 6= _ε)

→ (∃s₁∃t₁(Num(s₁) ∧ Num(t₁) ∧ s₂ = s_1α ∧ t₂ = t₁^x ∧ β^s1γ^t1β ^{⊑end p}β^))];

(vi) ∀p∀q∀s∀t((Num(s₁) ∧ Num(t₁) ∧ p_βs_γt_βq = w ∧ q 6= ε^{) →} β αγ β ^⊑ β ^).

WTC interprets R

PWitn _{(x, y, w)}

w

WTC interprets R

PWitn _{(x, y, w)}

β γ β

condition (ii)

w

WTC interprets R

PWitn _{(x, y, w)}

β ^y γ ^z β

w

condition (iii)

WTC interprets R

PWitn _{(x, y, w)}

β ^y γ ^z β

w

condition (iv)

β ^y γ does not appear