🤹🏼Formal Logic II Unit 4 – First–Order Theories and Models

Key Concepts and Definitions

• First-order logic extends propositional logic by introducing quantifiers, variables, and predicates
• Predicates are symbols that represent relations or properties of objects
• Variables are symbols that stand for arbitrary objects in the domain of discourse
• Quantifiers (universal $\forall$ and existential $\exists$) express the scope and quantity of variables
• Terms are expressions that refer to objects and can be variables, constants, or function applications
• Formulas are well-formed expressions that can be atomic (predicates applied to terms) or compound (built using logical connectives and quantifiers)
• Theories are sets of formulas, often used to axiomatize a particular domain or structure
  • A theory can be seen as a set of assumptions or axioms that define a specific context or system
• Models are interpretations that assign meaning to the symbols in a first-order language and satisfy a given theory
  • A model consists of a non-empty domain (or universe) and an interpretation function that maps symbols to elements, relations, or functions in the domain

Syntax and Formation Rules

• The syntax of first-order logic specifies the rules for constructing well-formed formulas
• Alphabet consists of variables, constants, function symbols, predicate symbols, and logical symbols (connectives and quantifiers)
• Terms are built recursively from variables, constants, and function symbols
  • If $t_1, \ldots, t_n$ are terms and $f$ is an $n$-ary function symbol, then $f(t_1, \ldots, t_n)$ is a term
• Formulas are built recursively from atomic formulas using logical connectives and quantifiers
  • If $P$ is an $n$-ary predicate symbol and $t_1, \ldots, t_n$ are terms, then $P(t_1, \ldots, t_n)$ is an atomic formula
  • If $\phi$ and $\psi$ are formulas, then so are $\neg \phi$, $(\phi \land \psi)$, $(\phi \lor \psi)$, $(\phi \to \psi)$, and $(\phi \leftrightarrow \psi)$
  • If $\phi$ is a formula and $x$ is a variable, then $\forall x \phi$ and $\exists x \phi$ are formulas
• Free variables are those not bound by a quantifier, while bound variables are those within the scope of a quantifier
• Sentences are formulas with no free variables

Semantics and Interpretations

• Semantics assigns meaning to the symbols and formulas in a first-order language
• An interpretation $\mathcal{I}$ consists of a non-empty domain $D$ and a function that maps:
  • Constants to elements in $D$
  • $n$-ary function symbols to functions from $D^n$ to $D$
  • $n$-ary predicate symbols to relations (subsets of $D^n$)
• A variable assignment $s$ is a function that maps variables to elements in $D$
• The value of a term under an interpretation $\mathcal{I}$ and assignment $s$ is denoted by $\mathcal{I}[t]_s$
• The satisfaction relation $\mathcal{I} \models \phi[s]$ defines when an interpretation $\mathcal{I}$ satisfies a formula $\phi$ under an assignment $s$
  • For atomic formulas, $\mathcal{I} \models P(t_1, \ldots, t_n)[s]$ iff $(\mathcal{I}[t_1]_s, \ldots, \mathcal{I}[t_n]_s) \in \mathcal{I}(P)$
  • For compound formulas, satisfaction is defined recursively using the truth tables for connectives and the semantics of quantifiers
• A formula $\phi$ is satisfiable if there exists an interpretation $\mathcal{I}$ and assignment $s$ such that $\mathcal{I} \models \phi[s]$
• A formula $\phi$ is valid (tautology) if for all interpretations $\mathcal{I}$ and assignments $s$, $\mathcal{I} \models \phi[s]$

Proof Systems and Inference Rules

• Proof systems provide a syntactic method for deriving formulas from a set of axioms and inference rules
• Natural deduction is a common proof system that uses introduction and elimination rules for each logical connective and quantifier
  • Introduction rules allow inferring a formula with a specific connective or quantifier (e.g., $\land$-intro, $\to$-intro, $\forall$-intro)
  • Elimination rules allow using a formula with a specific connective or quantifier to infer simpler formulas (e.g., $\land$-elim, $\to$-elim, $\forall$-elim)
• Sequent calculus is another proof system that uses sequents (expressions of the form $\Gamma \vdash \Delta$) and left/right introduction rules
• Inference rules are schema that allow deriving new formulas from existing ones
  • Modus ponens: from $\phi$ and $\phi \to \psi$, infer $\psi$
  • Universal instantiation: from $\forall x \phi$, infer $\phi[t/x]$ for any term $t$
  • Existential generalization: from $\phi[t/x]$, infer $\exists x \phi$
• A proof is a sequence of formulas, each of which is either an axiom or derived from previous formulas using inference rules
• A formula $\phi$ is provable from a theory $T$ (denoted $T \vdash \phi$) if there exists a proof of $\phi$ using axioms from $T$ and inference rules

Model Theory Basics

• Model theory studies the relationship between theories and their models
• A model of a theory $T$ is an interpretation that satisfies all the formulas (axioms) in $T$
• A theory $T$ is consistent if it has at least one model
• A theory $T$ is complete if for every sentence $\phi$ in the language, either $T \vdash \phi$ or $T \vdash \neg \phi$
• The compactness theorem states that a theory $T$ has a model iff every finite subset of $T$ has a model
  • This implies that a theory is consistent iff every finite subset is consistent
• The Löwenheim-Skolem theorem states that if a theory $T$ has an infinite model, then it has models of all infinite cardinalities
  • The downward version states that if $T$ has an infinite model, it has a countable model
  • The upward version states that if $T$ has an infinite model, it has models of arbitrarily large cardinalities
• Elementary equivalence: two structures $\mathcal{A}$ and $\mathcal{B}$ are elementarily equivalent if they satisfy the same first-order sentences
• Isomorphism: two structures $\mathcal{A}$ and $\mathcal{B}$ are isomorphic if there exists a bijective function $f: A \to B$ that preserves the interpretations of all symbols
  • Isomorphic structures are elementarily equivalent, but the converse is not always true

Soundness and Completeness

• Soundness and completeness are fundamental properties connecting syntax (provability) and semantics (validity)
• Soundness: if a formula $\phi$ is provable from a theory $T$ ($T \vdash \phi$), then $\phi$ is valid in all models of $T$ ($T \models \phi$)
  • In other words, if a formula can be derived using a proof system, it must be true in all models satisfying the axioms
• Completeness: if a formula $\phi$ is valid in all models of a theory $T$ ($T \models \phi$), then $\phi$ is provable from $T$ ($T \vdash \phi$)
  • In other words, if a formula is true in all models satisfying the axioms, it can be derived using a proof system
• Gödel's completeness theorem establishes the completeness of first-order logic with respect to the standard proof systems (natural deduction, sequent calculus, Hilbert-style)
• The compactness theorem and Löwenheim-Skolem theorems are important consequences of the completeness theorem
• Soundness and completeness together imply that syntax and semantics are equivalent ways of characterizing logical consequence in first-order logic

Applications and Examples

• First-order logic is widely used in mathematics, computer science, and philosophy to formalize and reason about various domains
• In mathematics, first-order theories are used to axiomatize structures like groups, rings, fields, and ordered sets
  • Example: the theory of groups consists of axioms for associativity, identity, and inverses
• In computer science, first-order logic is used in formal specification, verification, and automated theorem proving
  • Example: Hoare logic is a first-order theory for reasoning about the correctness of imperative programs
• In philosophy, first-order logic is used to analyze and formalize arguments, theories, and concepts
  • Example: the theory of mereology (parthood relations) can be axiomatized using first-order logic
• Many interesting mathematical structures can be characterized up to isomorphism by first-order theories
  • Example: the theory of dense linear orders without endpoints characterizes the structure of the rational numbers $(\mathbb{Q}, <)$
• First-order logic is also used in the foundations of mathematics, such as in Zermelo-Fraenkel set theory (ZFC) and Peano arithmetic (PA)
  • These theories aim to provide a rigorous basis for all of mathematics using first-order axioms

Common Challenges and Tips

• Translating natural language statements into first-order formulas can be challenging due to ambiguity and implicit assumptions
  • Tip: break down complex statements into simpler components and identify the key predicates, quantifiers, and logical connectives
• Choosing the right signature (symbols) and axioms to model a particular domain requires careful consideration
  • Tip: start with a minimal set of symbols and axioms, and incrementally add more as needed to capture the essential properties of the domain
• Understanding the scope and order of quantifiers is crucial for correctly formalizing statements
  • Tip: use parentheses to clearly indicate the scope of quantifiers and remember that the order of quantifiers matters (e.g., $\forall x \exists y$ is different from $\exists y \forall x$)
• Constructing proofs can be difficult, especially for complex formulas or theories
  • Tip: break down the goal into smaller subgoals, use proof strategies like induction or contradiction, and look for applicable axioms and previously proven lemmas
• Interpreting models and counterexamples requires a good understanding of the semantics and the specific domain being modeled
  • Tip: carefully examine the interpretations of symbols and the satisfaction of formulas in the model, and try to identify the key properties that make it a counterexample
• Dealing with equality in first-order logic requires special attention, as it has its own axioms and proof rules
  • Tip: use the reflexivity, symmetry, transitivity, and substitution axioms for equality, and be aware of the difference between syntactic and semantic equality