Same Same But Different: An Alphabetically Innocent Compositional Predicate Logic

Appendices

Appendix 1: de Bruijn’s indices

DeBruijn indices [1] are a way of representing (primarily) bound variables by using integer indices instead of variable names. The basic idea is that the index [n] refers to a variable bound by the n-th binding expression counting outward from the occurrence of [n]. For example, to represent the expression λ x ₃.λ x ₅.x ₅ by means of de Bruijn indices, we first remove the occurrences of x ₃ and x ₅ immediately following λ (getting λ.λ.x ₅), and then we replace x ₅ by the corresponding de Bruijn index. Since (the last occurrence of) x ₅ in λ x ₃.λ x ₅.x ₅ is bound by λ x ₅, which is the first λ binder having scope over x ₅, we replace x ₅ by the deBruijn index [1], resulting in λ.λ.[1]. On the other hand, the term λ x ₃.λ x ₅.x ₃ is represented by λ.λ.[2], because x ₃ is bound by λ x ₃, which is the second λ-binder having scope over x ₃. Importantly, note that the terms λ x ₃.λ x ₅.x ₅ and λ x ₃.λ x ₇.x ₇ are represented by the same term λ.λ.[1].

DeBruijn indices can also be used to represent free variables. For example, the term λ x ₃.x ₁ can be represented by the term λ.[2]. So, by convention, a deBruijn index [n] stands for a free variable if it is bigger than the number of binders in whose scope it is. In addition, one can stipulate that if a deBrujn index [n] is bigger than the number b of binders having scope over it, then [n] stands for the free variable x _{n − b} . So in the term λ.λ.[4] the number of binders is 2, the deBrujn index is bigger than 2, and therefore it stands for the free variable x ₄₋₂, ie. x ₂, whereas in λ.λ.[3] the deBrujn index stands for the free variable x ₁.

Note, importantly, that the terms λ.λ.[4] and λ.λ.[3] are not alphabetically innocent: prefixing another λ binder to λ.λ.[4] results in λ.λ.λ.[4] where, according to our convention [4] stands for the free variable x ₁, whereas prefixing λ.λ.[3] results in λ.λ.λ.[3] where [3] is bound by outermost λ binder, showing that λ.λ.[4] and λ.λ.[3] are not alphabetically innocent.

We therefore conclude that deBruijn indices do not provide a solution to the problem addressed in this paper, namely how to define an alphabetically innocent and compositional predicate logic.

Appendix 2: Proof of Lemma 1

Let T ₁(A) = π ₁(T(A)) and T ₂(A) = π ₂(T(A)). Let [[T ₁(A)]] = π ₁([[T ₁(A)]]) and [[T ₂(A)]] = π ₂([[T ₂(A)]]). Recall:

• (60) G t o S(A) := {s : there is a g ∈ [[A]] and s = g(T ₂(A))}

• (61) Lemma 1: $GtoS(A) = \pi _{1}([\![ T(A)]\!]) \cap \pi _{2}([\![ T(A)]\!])$

Proof of Lemma one by induction over the complexity of formulas.

1.1 Atomic Formulas

Let A be an atomic formua P(x ₁,…x _n ). Then

• (62) G t o S(P(x ₁,…x _n ))= {s : there is a g ∈ [[P(x ₁,…x _n )]] such that s = g(T ₂(P((x ₁,…x _n )))}= {s : there is a g ∈ [[P(x ₁,…x _n )]] such that s = 〈g(x ₁),…, g(x _n )〉}= {s : there is a g, 〈g(x ₁),…, g(x _n )〉 ∈ I(P) and s = 〈g(x ₁),…, g(x _n )〉}= { s:s ∈ I(P) and s ∈ [[x ₁…x _n ]] _D }=$I(P) \cap [\![ x_{1} \ldots , x_{n}]\!]_{D}\\=$ $\pi _{1}([\![ T(P(x_{1}, \ldots , x_{n}))]\!]) \cap \pi _{2}([\![ T(P(x_{1}, \ldots , x_{n}))]\!])$

1.2 Negation

Recall that T ₂(¬A) = T ₂(A) and that π ₁[[¬A]] = D∖π ₁[[¬A]].

• (63) $s \in (\pi _{1}([\![ T(\neg A)]\!]) \cap \pi _{2}([\![ T(\neg A)]\!])$

  • a. iff $s \in D^{n} \backslash [\![ T_{1}(A)]\!] \cap [\![ T_{2}(A)]\!]$

  • b. iff $s \in D^{n} \backslash ([\![ T_{1}(A)]\!]\cap [\![ T_{2}(A)]\!]) \cap [\![ T_{2}(\neg A)]\!]$

  • c. iff $s \in D^{n} \backslash GtoS(A) \cap [\![ T_{2}(\neg A)]\!]$

  • d. iff $s \in D^{n} \backslash \{s^{\prime } :$ there is a $g \in [\![ A]\!]\textrm { such that} s^{\prime }=g(T_{2}(A))$ and s conforms to the free variables of ¬A

  • e. iff there is no g, g ∈ [[A]] such thats = g(T ₂(A))} and s conforms to the free variables of ¬A

  • f. iff for all g, if s = g(T ₂(A)) then g∉[[A]], and s conforms to the free variables of ¬A

  • g. iff there is a g ∈ [[¬A]] such that s = g(T ₂(¬A))

  • h. iff s ∈ G t o S(¬A)

Comments: In (63-b) we duplicate the condition that s conforms to the free variables; as can be seen at the end of the derivation the second condition becomes redundant and is elimated in the step from f. to g.

1.3 Conjunction

• (64) s ∈ G t o S(A∧B)

  • a. iff there is a g, g ∈ [[A∧B]] and s = g(T ₂(A∧B))

  • b. iff s = s ₁ s ₂ and there is a g, g ∈ [[A]], g ∈ [[B]], and $\left .s_{1}s_{2}=g(T_{2}(A \wedge B))=g(T_{2}(A))+g(T_{2}(B))\right \}$

  • c. iff there is a g, g ∈ [[A]], g ∈ [[B]], and s ₁ = g(T ₂(A)), s ₂ = g(T ₂(B)) and s ₁ s ₂∈[[T ₂(A∧B)]] _D

  • d. iff there is a h, h ∈ [[A]], s ₁ = g(T ₂(A)) and there is an f, f ∈ [[B]], s ₂ = f(T ₂(B)) and s ₁ s ₂∈[[T ₂(A∧B)]] _D

  • e. iff s ₁∈G t o S(A), s ₂∈G t o S(B) and s ₁ s ₂∈[[T ₂(A∧B)]] _D

  • f. iff $s_{1}\in [\![ T_{1}(A)]\!] \cap [\![ T_{2}(A)]\!]$, $s_{2}\in [\![ T_{1}(B)]\!] \cap [\![ T_{2}(B)]\!]$ and s ₁ s ₂∈[[T ₂(A∧B)]] _D

  • g. iff s ₁∈[[T ₁(A)]], s ₂∈[[T ₁(B)]] and s ₁ s ₂∈[[T ₂(A∧B)]] _D

  • h. iff s ₁ s ₂ : s ₁ s ₂∈[[T ₁(A)]]⊗[[T ₁(B)]] and s ₁ s ₂∈[[T ₂(A∧B)]] _D

  • i. iff s ₁ s ₂∈[[T ₁(A∧B)]] and s ₁ s ₂∈[[T ₂(A∧B)]] _D

  • j. iff $s\in [\![ T_{1}(A\wedge B)]\!] \cap [\![ T_{2}(A\wedge B)]\!]_{D}$

  • k. iff $s\in \pi _{1}([\![ T(A\wedge B)]\!]) \cap \pi _{2}([\![ T(A\wedge B)]\!])$

Comments: Most equivalences follow by definition. Ad (64-d) upwards from right to left: assume that h and f assign different values to some variable that occurs both in A and B. Then it would be impossible for s ₁ s ₂ to conform to T ₂(A∧B). Therefore these values must be identical and we can combine h and f into the g of (64-c).

1.4 Quantification

• (65) s ∈ G t o S(∃x A)

  • a. iff $s \in [\![ T_{1}(\exists x A)]\!] \cap [\![ T_{2}(\exists x A)]\!]$

  • b. iff s ∈ [[T ₁(∃x A)]] and s conforms to the free variables of ∃x A

  • c. iff there is an $s^{\prime } \in D \otimes [\![ T_{1}(A)]\!]$ such that $s = r_{[\![ \sigma ]\!]}(s^{\prime })$, $s^{\prime }$ conforms to x, and s conforms to the free variables of ∃x A

  • d. iff there is an $s^{\prime } \in D \otimes [\![ T_{1}(A)]\!]$ such that $s = r_{[\![ \sigma ]\!]}(s^{\prime })$, and $s^{\prime }$ conforms to the free variables of A

  • e. iff there is an $s^{\prime \prime }$ and an a ∈ D such that $s^{\prime \prime } \in [\![ T_{1}(A)]\!]$, $s = r_{[\![ \sigma ]\!]}(as^{\prime \prime })$, and $s^{\prime \prime }$ conforms to the free variables of A

  • f. iff there is an $s^{\prime \prime }$ and an a such that $s^{\prime \prime } \in [\![ T_{1}(A)]\!] \cap [\![ T_{2}(A)]\!]$, $s = r_{[\![ \sigma ]\!]}(as^{\prime \prime })$

  • g. iff there is an $s^{\prime \prime }$ and an a such that $s^{\prime \prime } \in GtoS(A)$, $s = r_{[\![ \sigma ]\!]}(as^{\prime \prime })$

  • h. iff there is an $s^{\prime \prime }$, an a, and a g such that g ∈ [[A]], $s^{\prime \prime }=g(T_{2}(A))$, and $s = r_{[\![ \sigma ]\!]}(as^{\prime \prime })$

  • i. iff there is an a and a g such that g ∈ [[A]], and s = r _[[σ]](a + g(T ₂(A)))

  • j. iff there is an a, a g and a $g^{\prime }$ such that $g^{\prime } \in [\![ \exists x A]\!]$, g and $g^{\prime }$ possibly differ only for values for x, and s = r _[[σ]](a + g(T ₂(A))).

  • k. iff for some $g^{\prime }$, $g^{\prime } \in [\![\exists x A]\!]$, $s=g^{\prime }(T_{2}(\exists x A))$

  • l. iff s ∈ G t o S(∃x A)

Comments on (65-k): $g^{\prime }(T_{2}(\exists x A)) = r_{[\![ \sigma ]\!]}(a+g(T_{2}(A)))$, because the reduction of g(T ₂(A)) yields exactly the values for the free variables of T ₂(∃x A); moreover, it ignores only the values for x of g, which is exactly what $g^{\prime }$ does.