Bases for Structures and Theories II
- PDF / 415,764 Bytes
- 19 Pages / 439.37 x 666.142 pts Page_size
- 69 Downloads / 190 Views
Logica Universalis
Bases for Structures and Theories II Jeffrey Ketland Abstract. In Part I of this paper (Ketland in Logica Universalis 14:357– 381, 2020), I assumed we begin with a (relational) signature P = {Pi } and the corresponding language LP , and introduced the following notions: a definition system dΦ for a set of new predicate symbols Qi , given by a set Φ = {φi } of defining LP -formulas (these definitions have the form: ∀x(Qi (x) ↔ φi )); a corresponding translation function τΦ : LQ → LP ; the corresponding definitional image operator DΦ , applicable to LP structures and LP -theories; and the notion of definitional equivalence itself: for structures A + dΦ ≡ B + dΘ ; for theories, T1 + dΦ ≡ T2 + dΘ . Some results relating these notions were given, ending with two characterizations for definitional equivalence. In this second part, we explain the notion of a representation basis. Suppose a set Φ = {φi } of LP -formulas is given, and Θ = {θi } is a set of LQ -formulas. Then the original set Φ is called a representation basis for an LP -structure A with inverse Θ iff an inverse explicit definition ∀x(Pi (x) ↔ θi ) is true in A + dΦ , for each Pi . Similarly, the set Φ is called a representation basis for a LP -theory T with inverse Θ iff each explicit definition ∀x(Pi (x) ↔ θi ) is provable in T + dΦ . Some results about representation bases, the mappings they induce and their relationship with the notion of definitional equivalence are given. In particular, we show that T1 (in LP ) is definitionally equivalent to T2 (in LQ ), with respect to Φ and Θ, if and only if Φ is a representation basis for T1 with inverse Θ and T2 ≡ DΦ T1 . Mathematics Subject Classification. Primary 03C07; Secondary 03C95. Keywords. Definitional equivalence, Theories, Definability.
1. Introduction Sometimes theories are formulated with different sets of non-logical primitives and yet are definitionally equivalent. There are many examples of theories— often involving formalized systems of arithmetic and set theory—formulated with rather different sets of primitives (aka signatures), which are nonetheless “equivalent”.
J. Ketland
Log. Univers.
2. Summary of Part I In Part I ([4]), we considered a starting language LP over a relational signature P = {Pi }i∈IP , and a set Φ = {φi }i∈I of LP -formulas. Given Φ, introduce a disjoint set Q = {Qi }i∈I of new relation symbols, with card Q = card Φ, and with the arity of Qi matching the arity of φi . The extended language is denoted LP,Q and the language built from the new signature Q (with the implicitly induced arities) is denoted LQ .1 Definition 1. Given Φ = {φi }, the definition system over Φ, which we write as, dΦ is the set of explicit definitions, ∀x1 . . . xni (Qi (x1 , . . . , xni ) ↔ φi ) where {x1 , . . . xni } = FV(φi ), and ni = card FV(φi ) (the “arity” of φi ). These define the new symbols Qi in terms of the defining LP -formulas φi . We shall sometimes write ∀x(Qi (x) ↔ φi ) instead of ∀x1 . . . xn (Qi (x1 , . . . , xn ) ↔ φi ).2 Definition 2. Let A be an LP -structure. Then A+dΦ is th
Data Loading...
