3.1 Construction of terms and formulas in first-order logic

First-order logic builds the foundation for formal reasoning in mathematics and computer science. It provides a structured way to represent and analyze complex statements about objects and their relationships. Understanding its syntax is crucial for constructing valid arguments and proofs.

The construction of terms and formulas in first-order logic follows specific rules. These rules ensure that expressions are well-formed and meaningful, allowing us to create increasingly complex logical statements from simpler components. Mastering this process is essential for effectively using first-order logic in various applications.

Syntax of First-Order Logic

Symbols and Components

Top images from around the web for Symbols and Components

• 

  Logic - Wikipedia View original

  Is this image relevant?

• 

  Logical symbols | JD2718 View original

  Is this image relevant?

• 

  Logic for Computer Scientists/Predicate Logic/Syntax - Wikibooks, open books for an open world View original

  Is this image relevant?

• 

  Logic - Wikipedia View original

  Is this image relevant?

• 

  Logical symbols | JD2718 View original

  Is this image relevant?

1 of 3

Top images from around the web for Symbols and Components

• 

  Logic - Wikipedia View original

  Is this image relevant?

• 

  Logical symbols | JD2718 View original

  Is this image relevant?

• 

  Logic for Computer Scientists/Predicate Logic/Syntax - Wikibooks, open books for an open world View original

  Is this image relevant?

• 

  Logic - Wikipedia View original

  Is this image relevant?

• 

  Logical symbols | JD2718 View original

  Is this image relevant?

1 of 3

• First-order logic syntax forms a formal language with specific symbols and combination rules for meaningful expressions
• Constants represent individual objects in the domain of discourse (a, b, c)
• Variables act as placeholders for objects in the domain (x, y, z)
• Function symbols map objects to other objects (f(x), g(y,z), h(x,y,z))
• Predicate symbols express properties of objects or relationships between objects (P(x), Q(x,y), R(x,y,z))
• Arity of function or predicate symbols denotes the number of arguments required
  • Must remain consistent throughout a formula
  • Affects how terms and formulas are constructed

Constructing Terms

• Terms built recursively from constants, variables, and function symbols applied to other terms
• Simple terms consist of constants or variables (a, x)
• Complex terms created by applying function symbols to other terms (f(g(x), h(y,z)))
• Well-formed terms follow specific syntactic rules
  • Constants and variables are always well-formed terms
  • Function symbols must be applied to the correct number of arguments
• Examples of well-formed terms:

  • x

  • f(a)

  • g(x, h(y, z))

Atomic Formulas

• Atomic formulas form the basic building blocks of more complex formulas
• Constructed by applying predicate symbols to terms or using equality between terms
• Examples of atomic formulas:

  • P(x)

  • Q(f(a), y)

  • x = g(y, z)

• Atomic formulas express basic statements about objects in the domain
• Serve as the foundation for constructing more complex logical expressions

Constructing Formulas

Complex Formulas

• Complex formulas combine atomic formulas using logical connectives and quantifiers
• Logical connectives join simpler formulas to create more complex expressions
  • Negation (¬):

    ¬P(x)

  • Conjunction (∧):

    P(x) ∧ Q(y)

  • Disjunction (∨):

    P(x) ∨ Q(y)

  • Implication (→):

    P(x) → Q(y)

  • Biconditional (↔):

    P(x) ↔ Q(y)

• Quantifiers bind variables and express properties for all or some objects in the domain
  • Universal quantifier (∀):

    ∀x P(x)

  • Existential quantifier (∃):

    ∃x P(x)

• Examples of complex formulas:

  • ∀x (P(x) → Q(x))

  • ∃x (P(x) ∧ ¬Q(x))

Well-Formed Formulas (WFFs)

• Well-formed formulas follow strict syntactic rules ensuring every subformula maintains proper structure
• Atomic formulas always qualify as well-formed formulas
• Complex formulas constructed from well-formed subformulas using logical connectives and quantifiers
• Rules for constructing WFFs:
  • If φ is a WFF, then ¬φ is a WFF
  • If φ and ψ are WFFs, then (φ ∧ ψ), (φ ∨ ψ), (φ → ψ), and (φ ↔ ψ) are WFFs
  • If φ is a WFF and x is a variable, then ∀x φ and ∃x φ are WFFs
• Examples of well-formed formulas:

  • P(x) ∧ Q(y)

  • ∀x (P(x) → ∃y Q(x, y))

Free and Bound Variables

• Free variables occur in a formula without being bound by a quantifier
• Bound variables fall within the scope of a quantifier
• Same variable can be free in one part of a formula and bound in another
• Distinguishing free and bound variables crucial for understanding formula meaning
• Examples:
  • In

    P(x) ∧ Q(y)

    , both x and y are free
  • In

    ∀x (P(x) → Q(y))

    , x becomes bound while y remains free

Connectives and Quantifiers

Logical Connectives

• Negation (¬) reverses the truth value of a formula

  • ¬P(x)

    true when P(x) false
• Conjunction (∧) true when both operands true

  • P(x) ∧ Q(y)

    true when both P(x) and Q(y) true
• Disjunction (∨) true when at least one operand true

  • P(x) ∨ Q(y)

    true when either P(x) or Q(y) (or both) true
• Implication (→) false only when antecedent true and consequent false

  • P(x) → Q(y)

    false only when P(x) true and Q(y) false
• Biconditional (↔) true when both operands have same truth value

  • P(x) ↔ Q(y)

    true when P(x) and Q(y) both true or both false

Quantifiers and Their Scope

• Universal quantifier (∀) expresses property holds for all objects in domain

  • ∀x P(x)

    true when P(x) true for every object x in domain
• Existential quantifier (∃) indicates at least one object in domain satisfies property

  • ∃x P(x)

    true when P(x) true for at least one object x in domain
• Quantifiers have specific scope within formula typically indicated by parentheses or brackets
  • In

    ∀x (P(x) → Q(x))

    , scope of ∀x includes entire subformula P(x) → Q(x)
• Order and interaction of multiple quantifiers significantly affect formula meaning

  • ∀x ∃y P(x,y)

    different from

    ∃y ∀x P(x,y)

Negating Quantified Formulas

• Negation of quantified formulas follows specific rules
• Negating universal quantifier results in existential quantifier with negated formula

  • ¬∀x P(x)

    equivalent to

    ∃x ¬P(x)

• Negating existential quantifier results in universal quantifier with negated formula

  • ¬∃x P(x)

    equivalent to

    ∀x ¬P(x)

• Examples of negating quantified formulas:

  • ¬∀x (P(x) → Q(x))

    equivalent to

    ∃x ¬(P(x) → Q(x))

  • ¬∃x (P(x) ∧ Q(x))

    equivalent to

    ∀x ¬(P(x) ∧ Q(x))

Parentheses and Precedence

Using Parentheses

• Parentheses explicitly indicate scope and grouping of subformulas within larger formula
• Proper use clarifies intended logical structure and interpretation
• Parentheses override default precedence rules and change formula meaning
• Examples of parentheses usage:

  • (P(x) ∧ Q(x)) → R(x)

    different from

    P(x) ∧ (Q(x) → R(x))

  • ∀x (P(x) → ∃y Q(x,y))

    specifies scope of universal quantifier

Precedence Rules

• Precedence rules determine order of logical connective application when parentheses omitted
• Standard precedence order for logical connectives (highest to lowest):
  1. Negation (¬)
  2. Conjunction (∧)
  3. Disjunction (∨)
  4. Implication (→)
  5. Biconditional (↔)
• Quantifiers have higher precedence than logical connectives
• Quantifiers bind as much of formula to their right as possible
• Examples of precedence in action:

  • ¬P(x) ∧ Q(x)

    interpreted as

    (¬P(x)) ∧ Q(x)

  • P(x) ∨ Q(x) → R(x)

    interpreted as

    (P(x) ∨ Q(x)) → R(x)

Resolving Ambiguity

• Ambiguity in formulas resolved by adding parentheses to clarify intended logical structure
• Proper parentheses usage ensures correct interpretation of complex formulas
• Understanding precedence rules and parentheses crucial for translating natural language into first-order logic
• Examples of resolving ambiguity:
  • Ambiguous:

    P(x) ∧ Q(x) ∨ R(x)

  • Clarified:

    (P(x) ∧ Q(x)) ∨ R(x)

    or

    P(x) ∧ (Q(x) ∨ R(x))

• Practice translating natural language statements into unambiguous first-order logic formulas