Research output: Contribution to Journal/Magazine › Journal article › peer-review
Research output: Contribution to Journal/Magazine › Journal article › peer-review
}
TY - JOUR
T1 - Definition of first order language with arbitrary alphabet. Syntax of terms, atomic formulas and their subterms
AU - Caminati, Marco
PY - 2011/9/30
Y1 - 2011/9/30
N2 - Second of a series of articles laying down the bases for classicalfirst order model theory. A language is defined basically as a tuple made of aninteger-valued function (adicity), a symbol of equality and a symbol for the NORlogical connective. The only requests for this tuple to be a language is that thevalue of the adicity in = is -2 and that its preimage (i.e. the variables set) in 0is infinite. Existential quantification will be rendered (see [11]) by mere prefixinga formula with a letter. Then the hierarchy among symbols according to theiradicity is introduced, taking advantage of attributes and clusters.The strings of symbols of a language are depth-recursively classified as termsusing the standard approach (see for example [16], definition 1.1.2); technically,this is done here by deploying the ‘-multiCat’ functor and the ‘unambiguous’ at-tribute previously introduced in [10], and the set of atomic formulas is introduced.The set of all terms is shown to be unambiguous with respect to concatenation;we say that it is a prefix set. This fact is exploited to uniquely define the subtermsboth of a term and of an atomic formula without resorting to a parse tree.
AB - Second of a series of articles laying down the bases for classicalfirst order model theory. A language is defined basically as a tuple made of aninteger-valued function (adicity), a symbol of equality and a symbol for the NORlogical connective. The only requests for this tuple to be a language is that thevalue of the adicity in = is -2 and that its preimage (i.e. the variables set) in 0is infinite. Existential quantification will be rendered (see [11]) by mere prefixinga formula with a letter. Then the hierarchy among symbols according to theiradicity is introduced, taking advantage of attributes and clusters.The strings of symbols of a language are depth-recursively classified as termsusing the standard approach (see for example [16], definition 1.1.2); technically,this is done here by deploying the ‘-multiCat’ functor and the ‘unambiguous’ at-tribute previously introduced in [10], and the set of atomic formulas is introduced.The set of all terms is shown to be unambiguous with respect to concatenation;we say that it is a prefix set. This fact is exploited to uniquely define the subtermsboth of a term and of an atomic formula without resorting to a parse tree.
U2 - 10.2478/v10037-011-0026-1
DO - 10.2478/v10037-011-0026-1
M3 - Journal article
VL - 19
SP - 169
EP - 178
JO - Formalized Mathematics
JF - Formalized Mathematics
IS - 3
ER -