Formal Logic II Unit 5 study guides

Key Concepts and Definitions

• First-order logic (FOL) extends propositional logic by introducing quantifiers, variables, and predicates
• Equality ($=$) is a binary predicate that asserts two terms are identical
• Normal forms are standardized representations of logical formulas that facilitate analysis and computation
• Prenex normal form (PNF) moves all quantifiers to the beginning of a formula
• Skolem normal form (SNF) eliminates existential quantifiers by introducing Skolem functions
• Predicates are symbols that represent relations between objects (e.g., $P(x)$, $Q(x, y)$)
• Variables are symbols that represent arbitrary objects in the domain of discourse (e.g., $x$, $y$, $z$)
• Quantifiers specify the scope and quantity of variables in a formula
  • Universal quantifier ($\forall$) asserts a property holds for all objects in the domain
  • Existential quantifier ($\exists$) asserts a property holds for at least one object in the domain

First-Order Logic Basics

• FOL formulas consist of predicates, variables, quantifiers, logical connectives, and equality
• The domain of discourse is the set of objects that the variables in a formula can represent
• Free variables are not bound by any quantifier and can be assigned any value from the domain
• Bound variables are within the scope of a quantifier and their values are determined by the quantifier
• Formulas without free variables are called sentences and have a definite truth value
• Logical connectives ($\land$, $\lor$, $\rightarrow$, $\leftrightarrow$, $\neg$) combine predicates to form complex formulas
• The order of precedence for logical connectives is: $\neg$, $\land$, $\lor$, $\rightarrow$, $\leftrightarrow$
• Parentheses can be used to override the default order of precedence

Equality in First-Order Logic

• Equality is a binary predicate that asserts two terms are identical
• The equality predicate is reflexive ($\forall x (x = x)$), symmetric ($\forall x \forall y (x = y \rightarrow y = x)$), and transitive ($\forall x \forall y \forall z ((x = y \land y = z) \rightarrow x = z)$)
• The substitution property allows replacing one term with an equal term in any formula without changing its truth value
• Equality can be used to define new predicates and functions in terms of existing ones
• The inequality predicate ($\neq$) asserts two terms are not identical
• Equality and inequality can be used to express uniqueness and distinctness of objects
• The identity of indiscernibles principle states that objects with identical properties are equal

Normal Forms: Introduction

• Normal forms are standardized representations of logical formulas that facilitate analysis and computation
• Normal forms can simplify the structure of formulas and make them easier to reason about
• Different normal forms have different properties and are suited for different purposes
• Converting a formula to a normal form is a mechanical process that can be automated
• Normal forms can reveal hidden structure and symmetries in formulas
• Some common normal forms in FOL are prenex normal form, Skolem normal form, and conjunctive/disjunctive normal forms
• Normal forms are often used as intermediate steps in theorem proving and model finding algorithms

Prenex Normal Form

• Prenex normal form (PNF) is a normal form where all quantifiers appear at the beginning of the formula
• The quantifier-free part of a PNF formula is called the matrix
• To convert a formula to PNF, quantifiers are moved outward using logical equivalences
  • $(\forall x \phi) \land \psi \equiv \forall x (\phi \land \psi)$ if $x$ is not free in $\psi$
  • $(\exists x \phi) \land \psi \equiv \exists x (\phi \land \psi)$ if $x$ is not free in $\psi$
  • Similar equivalences hold for $\lor$, $\rightarrow$, and $\leftrightarrow$
• The order of quantifiers in a PNF formula can affect its meaning and satisfiability
• PNF is useful for identifying the quantifier structure of a formula and applying quantifier elimination techniques

Skolem Normal Form

• Skolem normal form (SNF) is a normal form where all existential quantifiers are eliminated by introducing Skolem functions
• A Skolem function is a new function symbol that represents a choice of a witness for an existential quantifier
• To convert a PNF formula to SNF, each existential quantifier is replaced by a Skolem function that depends on the universally quantified variables preceding it
  • $\forall x \exists y \phi(x, y)$ becomes $\forall x \phi(x, f(x))$, where $f$ is a new Skolem function
• Skolemization preserves satisfiability but not logical equivalence
• SNF formulas are always universal and can be written as a conjunction of clauses
• SNF is useful for automated theorem proving and model finding, as it simplifies the quantifier structure and enables resolution-based methods

Applications and Examples

• Normal forms are used in various areas of logic, mathematics, and computer science
• In automated theorem proving, normal forms like SNF enable efficient proof search and resolution
• In model theory, normal forms can simplify the construction and analysis of models
• In database theory, normal forms ensure the integrity and consistency of relational schemas (e.g., Boyce-Codd Normal Form)
• Example: The formula $\forall x (P(x) \rightarrow \exists y Q(x, y))$ can be converted to PNF as $\forall x \exists y (P(x) \rightarrow Q(x, y))$ and further to SNF as $\forall x (P(x) \rightarrow Q(x, f(x)))$
• Example: The formula $\exists x \forall y (x = y)$ asserts the existence of a unique object in the domain, which can be Skolemized as $\forall y (c = y)$, where $c$ is a Skolem constant

Common Pitfalls and Tips

• Be careful when moving quantifiers outward, as the order of quantifiers can affect the meaning of the formula
• Ensure that variables are properly renamed to avoid unintended capturing of free variables
• Remember that Skolemization preserves satisfiability but not logical equivalence
• When converting to SNF, introduce Skolem functions only for existential quantifiers that are in the scope of universal quantifiers
• Use parentheses liberally to make the structure of the formula clear and unambiguous
• Break down complex formulas into smaller subformulas and convert them to normal forms separately
• Check your work by applying the conversion rules carefully and verifying that the resulting formula is indeed in the desired normal form
• Practice converting formulas to normal forms by hand to develop intuition and understanding of the process