8.1 Syntax and semantics of second-order logic

Second-order logic takes first-order logic up a notch. It adds new variables and quantifiers that let us talk about predicates and functions, not just objects. This gives us more power to express complex ideas.

The syntax of second-order logic introduces predicate and function variables. We can quantify over these, making statements about all properties or relations. This expands what we can say and reason about in formal logic.

Syntax of Second-Order Logic

Extending First-Order Logic

• Second-order logic extends the syntax of first-order logic
• Introduces new types of variables and quantifiers
• Allows for quantification over predicates and functions
• Increases the expressive power of the language

Quantifiers and Variables

• Second-order quantifiers $\forall$ and $\exists$ range over predicates and functions
• Predicate variables represent properties or relations (P, Q, R)
• Function variables represent functions (f, g, h)
• Variables can be quantified to make statements about all predicates or functions

Constructing Well-Formed Formulas

• Well-formed formulas (wffs) are constructed using logical connectives and quantifiers
• Predicate variables can be applied to terms to form atomic formulas ($P(x)$, $Q(a, b)$)
• Function variables can be applied to terms to form complex terms ($f(x)$, $g(a, b)$)
• Quantifiers can bind predicate and function variables ($\forall P \exists x P(x)$, $\exists f \forall x f(x) = x$)

Semantics of Second-Order Logic

Interpreting Second-Order Formulas

• Interpretation assigns meaning to the symbols in a second-order formula
• Domain of discourse specifies the objects that variables can refer to
• Predicate variables are assigned subsets of the domain or relations on the domain
• Function variables are assigned functions from the domain to itself

Henkin and Standard Semantics

• Henkin semantics allows the interpretation of predicate and function variables to be restricted
• Not all possible subsets or functions of the domain must be considered
• Standard semantics requires that all possible subsets and functions of the domain are included
• Standard semantics is more expressive but can lead to incompleteness

Satisfaction and Models

• A second-order formula is satisfied by an interpretation if it evaluates to true under that interpretation
• An interpretation that satisfies a formula is called a model of the formula
• A formula is valid if it is satisfied by every interpretation ($\forall P \forall x P(x) \rightarrow P(x)$)
• A formula is satisfiable if there exists an interpretation that satisfies it ($\exists P \forall x P(x)$)