Talk:Diagonal lemma/Proof with diagonal formula/Language base
Although we ofter refer to the “text” of object language as “finite sequences” over a set of “letters”, but sometimes we axiomatize this explicitly. A language base declares the set of “letters” axiomatizes sequencing operations. This mini-theory formalizes what we think of informally as as “finite sequences”. Language base talks almost nothing of the syntax of the object languege (althoght the letters may coincide with those of the object languge, but also this is not necessary): treatment of syntax must be built upon it. See the notion in [1], but also — with somewhat different terminology — at Tarski).
For better readability, let us denote the respective singleton sequences with underlining:
For better readability, let us denote the respective singleton sequences with underlining:
Axiomatizations
editNow we axiomatize the notion of sequence. Well-chosen axioms provide appropriate distinctions and indentifications, unambiguity, and exclude alien objects.
Let us use to denote empty sequence. Now we have more ways to step further. In some of them, I shall have to resort to many-sorted logic.
List-like
editOne approach uses a similar terminology as the concept of list in functional programming: we can use a : operation, making form a letter and an (already made) sequence (possibly also the empty one) a new sequence. We can begin the axiomatization like this:
we can define concatenation by recursion.
Concatenation and singletons
editIn another approach concatenation is a primitive (mainly denoted by ). Also a new operaration may be introduced: singleton sequece building, let us denote it here e.g. by . Axiomatization would begin than like this:
A specific care must be taken of concatenation:
- associativity
- unambiguity
must be declared by appropriate axioms. Unambiguity (see at Tarski):
I think let us add also
Single-sorted logic
editWe resorted many-sorted logic in the above things. Mybe this can be avoided. But then, each letter must be regarded as a standlone case at the axioms discussing distinctions:
Singletons are not empty
editSingletons are distinct from each other
editAxiom scheme
editmaybe better to regard them as if they would be generated by an axiom scheme:
Alternatives
editModelling sequences
editWe can skip this level: we can choose a more denotational approach, and refer to sequences as directly building their set-theoretic models. E.g. somethng like where
where
with sequencing operations defnied e.g. something like
where
Syntax tree
editAnother alternative way: to build syntax tree directly, not resorting to an underlying representation with sequences.
Notes
edit- ^ Ruzsa, Imre: Logikai szintaxis es szemantika