Treffer: Interpreting LAp into V ⊕L and V #L

This document’s goal is to interpret Soltys ’ theory LAp [SK01, SC04] two times. Once over the field F2 into the theory V ⊕L, and once over the integral domain Z into the theory V #L [Fon09]. Both theories capture basic arithmetic and include a function expressing matrix powering. Each interpretation is a mapping from LAp to V ⊕L (respectively, V #L) of terms and formulas such that provability is preserved. That is, theorems in LAp are mapped to theorems of V ⊕L (V #L). Such an interpretation has two uses. First, it allows for a shortcut when working in V ⊕L (V #L): no duplication of Soltys ’ work must be done in order to show that theorems proved in LAp are also provable in V ⊕L (V #L). Second, it fits Soltys ’ otherwise standalone hierarchy of theories LA ⊂ LAp ⊂ ∀LAp into the hierarchy of theories established in [CN10]. LAp has three sorts – indices (N), field elements, and matrices, which we think of semantically as having field elements as entries. V ⊕L (V #L) has only two sorts, numbers (N) and binary strings, which are used to encode matrices, lists, and other data structures, as required. The technical details of interpreting LAp into V ⊕L (V #L) arise from this difference in number of sorts. The number sort of LAp can be directly interpreted as the number sort of V ⊕L (V #L), but the field sort and the matrix sort present a non-obvious technical point. This document motivates, explains, and proves