Universe of Discourse

The Universe of Discourse (UoD) is the set of all objects being considered in a specific logical context.

In First-Order Logic, the UoD defines what objects the variables can represent when using quantifiers like ∀ (for all) and ∃ (there exists).
Example:

If our UoD is "all people", then the statement ∀x Mortal(x) means "For all people x, x is mortal".

Another Example:

If our UoD is "natural numbers", then ∃x (x > 5) means "There exists a natural number x such that x is greater than 5".

The UoD provides context and meaning to logical statements by defining the domain of objects being discussed.

Atom (Atomic Formula)

An Atom or Atomic Formula is the most basic building block of First-Order Logic.

An atomic formula is a predicate applied to a tuple of terms. It cannot be broken down into smaller logical components.
Examples of Atomic Formulas:
  • P(c) - A predicate P applied to a constant c
  • Q(x, y) - A predicate Q applied to variables x and y
  • R(f(a), b) - A predicate R applied to a function term and a constant
  • Equals(x, y) - Often written as x = y

Atoms are the simplest formulas that can be evaluated as true or false when interpreted in a structure with a defined Universe of Discourse.

Global

In First-Order Logic, Global typically refers to statements that apply to the entire Universe of Discourse.

A global statement or property is one that holds for all elements in the domain, often expressed using the universal quantifier (∀).
Example:

∀x (Student(x) → HasID(x))

This global statement means "All students have IDs" - it applies to every object in the Universe of Discourse.

Global statements define constraints or properties that must hold for the entire domain.

In model theory, a global type is a set of formulas that is consistent and complete with respect to a given theory.

Leaf

In the context of First-Order Logic, a Leaf typically refers to the atomic components of a formula tree.

When logical formulas are represented as trees (parse trees), the leaves are the atomic formulas that have no sub-formulas.
Formula Tree Example:

Consider the formula: ∀x (P(x) ∧ Q(x))

The tree representation would have:

  • Root: ∀x
  • Branch: ∧ (conjunction)
  • Leaves: P(x) and Q(x)

Leaves are the endpoints of the formula tree - they cannot be decomposed further into smaller logical components.

In semantic tableaux proof methods, leaves represent completed branches that are either closed (contradictory) or open (consistent).