First-Order Logic

First-order logic's WFFs are more complex than propositional logic's. They can be composed by following these rules:

• Predicates consisting of terms are valid formulas
  
• Equivalence between terms is a valid formula
  
• Formulas connected by logical operators are valid formulas
  
• If F is a formula containing a term x, quantifiers on x are valid formulas
  

First-order logic's syntax is comprised of symbols divided into logical and non-logical.

Logical symbols correspond to logical operators: and, or, not, implication

Non-logical symbols: predicates, terms, constants, variables, functions, quantifiers

• Predicates indicate relations between objects, e.g. "parent of"
  
• Terms are either variables or functions
  
• Variables are mutable parts of a formula
  
• Functions are terms that refer to other terms
  
• Quantifiers allow the definition of formulas that consider numbers or quantities with respect to some predicates
  

A first-order language is a set of logical symbols and non-logical symbols that can be combined to make formulas.

A theory in a first-order language is a specific set of formulas in the language that are considered to be true. This is by construction - you can make a theory out of any arbitrary (but syntactically valid) set of formulas.

An interpretation I of a first-order theory T is a mapping of atoms in T to truth values.

An intepretation I of a first-order theory T that satisfies T is called a model. I satisfies T iff:

• Every ground atom in T is in I (φ is satisfied)
  
• No negated ground atom in T is in I (~φ is satisfied)
  
• For every rule φ :- φ₁ & … & φₙ in T, once grounded, I satisfies φ only iff I satisfies φ₁ & … & φₙ
  

Basically, a model of T is a set of atoms that are logically consistent with T.

This provides a definition of entailment: T |= α iff α is true in every model of T.

If T admits at least one model, it is called "satisfiable", otherwise "unsatisfiable".