Definition of First Order Language with Arbitrary Alphabet. Syntax of Terms, Atomic Formulas and their Subterms

Marco Caminati

Formalized Mathematics (2011)

  • Volume: 19, Issue: 3, page 169-178
  • ISSN: 1426-2630

Abstract

top
Second of a series of articles laying down the bases for classical first order model theory. A language is defined basically as a tuple made of an integer-valued function (adicity), a symbol of equality and a symbol for the NOR logical connective. The only requests for this tuple to be a language is that the value of the adicity in = is -2 and that its preimage (i.e. the variables set) in 0 is infinite. Existential quantification will be rendered (see [11]) by mere prefixing a formula with a letter. Then the hierarchy among symbols according to their adicity is introduced, taking advantage of attributes and clusters.The strings of symbols of a language are depth-recursively classified as terms using the standard approach (see for example [16], definition 1.1.2); technically, this is done here by deploying the ‘-multiCat' functor and the ‘unambiguous’ attribute 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 subterms both of a term and of an atomic formula without resorting to a parse tree.

How to cite

top

Marco Caminati. "Definition of First Order Language with Arbitrary Alphabet. Syntax of Terms, Atomic Formulas and their Subterms." Formalized Mathematics 19.3 (2011): 169-178. <http://eudml.org/doc/268167>.

@article{MarcoCaminati2011,
abstract = {Second of a series of articles laying down the bases for classical first order model theory. A language is defined basically as a tuple made of an integer-valued function (adicity), a symbol of equality and a symbol for the NOR logical connective. The only requests for this tuple to be a language is that the value of the adicity in = is -2 and that its preimage (i.e. the variables set) in 0 is infinite. Existential quantification will be rendered (see [11]) by mere prefixing a formula with a letter. Then the hierarchy among symbols according to their adicity is introduced, taking advantage of attributes and clusters.The strings of symbols of a language are depth-recursively classified as terms using the standard approach (see for example [16], definition 1.1.2); technically, this is done here by deploying the ‘-multiCat' functor and the ‘unambiguous’ attribute 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 subterms both of a term and of an atomic formula without resorting to a parse tree.},
author = {Marco Caminati},
journal = {Formalized Mathematics},
language = {eng},
number = {3},
pages = {169-178},
title = {Definition of First Order Language with Arbitrary Alphabet. Syntax of Terms, Atomic Formulas and their Subterms},
url = {http://eudml.org/doc/268167},
volume = {19},
year = {2011},
}

TY - JOUR
AU - Marco Caminati
TI - Definition of First Order Language with Arbitrary Alphabet. Syntax of Terms, Atomic Formulas and their Subterms
JO - Formalized Mathematics
PY - 2011
VL - 19
IS - 3
SP - 169
EP - 178
AB - Second of a series of articles laying down the bases for classical first order model theory. A language is defined basically as a tuple made of an integer-valued function (adicity), a symbol of equality and a symbol for the NOR logical connective. The only requests for this tuple to be a language is that the value of the adicity in = is -2 and that its preimage (i.e. the variables set) in 0 is infinite. Existential quantification will be rendered (see [11]) by mere prefixing a formula with a letter. Then the hierarchy among symbols according to their adicity is introduced, taking advantage of attributes and clusters.The strings of symbols of a language are depth-recursively classified as terms using the standard approach (see for example [16], definition 1.1.2); technically, this is done here by deploying the ‘-multiCat' functor and the ‘unambiguous’ attribute 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 subterms both of a term and of an atomic formula without resorting to a parse tree.
LA - eng
UR - http://eudml.org/doc/268167
ER -

References

top
  1. Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990. 
  2. Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. Zbl06213858
  3. Grzegorz Bancerek. König's theorem. Formalized Mathematics, 1(3):589-593, 1990. 
  4. Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990. 
  5. Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990. 
  6. Czesław Byliński. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529-536, 1990. 
  7. Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990. 
  8. Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990. 
  9. Czesław Byliński. The modification of a function by a function and the iteration of the composition of a function. Formalized Mathematics, 1(3):521-527, 1990. 
  10. Marco B. Caminati. Preliminaries to classical first order model theory. Formalized Mathematics, 19(3):155-167, 2011, doi: 10.2478/v10037-011-0025-2.[Crossref] Zbl1276.03030
  11. Marco B. Caminati. First order languages: Further syntax and semantics. Formalized Mathematics, 19(3):179-192, 2011, doi: 10.2478/v10037-011-0027-0.[Crossref] Zbl1276.03032
  12. Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990. 
  13. Katarzyna Jankowska. Transpose matrices and groups of permutations. Formalized Mathematics, 2(5):711-717, 1991. 
  14. Rafał Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relative primes. Formalized Mathematics, 1(5):829-832, 1990. 
  15. Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147-152, 1990. 
  16. W. Pohlers and T. Glaß. An introduction to mathematical logic. Vorlesungsskriptum, WS, 93, 1992. 
  17. Marta Pruszyńska and Marek Dudzicz. On the isomorphism between finite chains. Formalized Mathematics, 9(2):429-430, 2001. 
  18. Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115-122, 1990. 
  19. Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505, 1990. 
  20. Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 
  21. Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73-83, 1990. 
  22. Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181-186, 1990. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.