User:Hans Adler/Glossary of mathematical logic

Predicate logic

Semantics

• A structure consists of a domain together with named finitary functions (operations) on the domain and named finitary relations on the domain.
  • Constants are nullary functions. Many authors treat constants separately and do not count them as functions.
  • An algebra (universal algebra) is a structure whose signature is algebraic.
  • The signature of a structure consists of the names of operations and relations together with information on their type (operation or relation) and arity.
    • A signature is relational if it has only relations, but no functions.
    • A signature is algebraic if it has only functions, but no relations.
• A reduct of a structure is the result of forgetting some of its functions and relations.
• An expansion of a structure is the result of adding more functions and relations.
• A substructure (induced substructure) of a structure M consists of a closed subset of the domain of M together with the restrictions of the functions and relations of M. The relations of a weak substructure of M may be subsets of the corresponding relations of M.
  • A subset of the domain of a structure M is closed if it is closed under all functions. In particular, a closed set contains all constants. The closure of a subset of the domain of M is the smallest closed set containing it.
• A homomorphism h: A → B of structures is a map from the domain of A to the domain of B which commutes with the functions and preserves the relations.
  • A strong homomorphism additionally has the property that every instance of a relation in the image has a preimage that is also an instance of the relation.
  • An isomorphism h: A → B of structures is a homomorphism which has an inverse homomorphism. Equivalently, it is a bijective strong homomorphism.
  • An embedding of a structure A into a structure B is an injective strong homomorphism, i.e. an injective homomorphism which preserves the negations of relations. Equivalently, it is an isomorphism of A with an induced substructure of B.

Syntax of first-order logic

• A signature consists of function symbols and relation symbols, each of which has a finite arity.
  • Constant symbols are nullary function symbols. Many authors treat constant symbols separately and do not count them as function symbols.
• A formula over a signature σ is a string of symbols that is true or false in a σ-structure, once the free variables in it have been assigned values: An atomic formula, a quantified formula, or a boolean combination of formulas.
  • A quantified formula is either an existentially quantified formula $\exists$x φ or a universally quantified formula $\forall$x φ, where φ is a formula.
  • An atom (atomic formula) over a signature σ is an equation or a string of the form R(t₁, …, t_n), where t₁, …, t_n are terms and R is an n-ary relation symbol.
    • In logic with equality (logic with identity; the standard case), an eqation is a string of the form t₁=t₂.
    • In logic without equality there are no equations.
    • A term over a signature σ is a string of symbols that is intended to represent an element of the domain: a constant, a variable, or a string of the form f(t₁, …, t_n), where t₁, …, t_n are terms and f is an n-ary function symbol.
      • A variable (first-order variable) is a symbol that is intended to represent varying elements of the domain.
• Properties of terms:
  • A closed term has no free variables. Every closed term in first-order logic is a ground term, i.e. it does not contain any variables at all.
• Properties of formulas:
  • A literal is either an atomic formula or a negated atomic formula.
  • A clause is a disjunction of literals.
  • A ground formula does not contain any variables.
  • A sentence (closed formula) has no free variables.
  • A Horn clause is either a definite clause or a goal clause.
    • A goal clause is a disjunction of negated atoms. Equivalently, it is of the form (p₁$\land$…$\land$p_n) → $\bot$.
    • A definite clause is a disjunction of negated atoms and one atom. Equivalently, it is of the form (p₁$\land$…$\land$p_n) → q.
      • A quasiidentity is a definite clause in which all atoms are equations. Equivalently, it is of the form (s₁=t₁ $\land$ … $\land$ s_n=t_n) → s=t.
• A (first-order) theory over a signature σ is a set of first-order σ-sentences.