@MISC{FOMODEL0.MIZ,
  AUTHOR = {Caminati, Marco B.},
  NOTE1 = {The author wrote this paper as
    part of his PhD thesis research},
  ACKNOWLEDGEMENT = {I would like to thank Marco Pedicini
    for his encouragement and support.},
  DAY = {29},
  MONTH = {December},
  YEAR = {2010},
  ADDRESS1 = {Mathematics Department "G.Castelnuovo"\\Sapienza University of Rome\\Piazzale Aldo Moro 5, 00185 Roma, Italy},
  TITLE = {Preliminaries to Classical First-order Model Theory},
  SUMMARY = {First of a series of articles laying down the bases
    for classical first order model theory.
    These articles introduce a framework for treating arbitrary
    languages with equality. This framework is kept as generic and
    modular as possible: both the language and the derivation rule
    are introduced as a type, rather than a fixed functor; definitions and
    results regarding syntax, semantics, interpretations and
    sequent derivation rules, respectively, are confined
    to separate articles, to mark out the hierarchy of dependences
    among different definitions and constructions.
As an application limited to countable languages, satisfiability
theorem and a full version of Goedel completeness theorem
are delivered, with respect to a fixed, remarkably thrifty,
set of correct rules.
Besides the self-referential significance for the Mizar
project itself of those theorems being formalized with
respect to a generic, equality-furnished, countable
language, this is the first step to work out other milestones
of model theory, such as Lowenheim-Skolem and compactness theorems.
Being the receptacle of all results of broader scope stemmed
during the various formalizations, this first article stays
at a very generic level, with results and registrations about
objects already in MML. Without introducing the Language structure yet,
three fundamental definitions of wide applicability
are also given: the `unambiguous' attribute
(cfr. \cite{lothaire2002algebraic} definition on page 5),
the functor `-multiCat', which is the iteration of `^'
over a FinSequence of FinSequence,
and the functor SubstWith, which realizes the substitution
of a single symbol inside a generic FinSequence.}}

@BOOK{lothaire2002algebraic,
  AUTHOR={Lothaire, M.},
  TITLE={{Algebraic combinatorics on words}},
  PUBLISHER={Cambridge Univ Pr},
  YEAR={2002}
}
