🤔Proof Theory Unit 8 – Second–Order Logic and Higher–Order Logics

What's the Deal with Second-Order Logic?

• Extends first-order logic by introducing quantification over predicates and functions
• Allows for expressing properties of properties and relations between relations
• Increases expressive power compared to first-order logic
• Enables defining concepts like finiteness, connectedness, and continuity
• Provides a foundation for mathematics and set theory
• Introduces new logical concepts such as comprehension axioms and standard models
• Enables reasoning about infinite structures and uncountable sets

Key Concepts and Notation

• Predicates: Relations or properties of objects, denoted by uppercase letters (e.g., $P(x)$)
  • Monadic predicates: Predicates with one argument (e.g., $P(x)$)
  • Dyadic predicates: Predicates with two arguments (e.g., $R(x, y)$)
• Functions: Mappings from objects to objects, denoted by lowercase letters (e.g., $f(x)$)
• Quantification over predicates and functions: $\forall P$ (for all predicates $P$) and $\exists f$ (there exists a function $f$)
• Comprehension axioms: Axioms that assert the existence of predicates or functions with certain properties
  • Example: $\exists P \forall x (P(x) \leftrightarrow \varphi(x))$ (there exists a predicate $P$ such that for all $x$, $P(x)$ holds if and only if $\varphi(x)$ holds)
• Standard models: Models that satisfy comprehension axioms and have a full power set
• Non-standard models: Models that satisfy the axioms but have a different structure than the intended interpretation

How Second-Order Logic Differs from First-Order

• First-order logic quantifies only over individual objects, while second-order logic quantifies over predicates and functions
• Second-order logic can express properties of properties and relations between relations, which first-order logic cannot
• Second-order logic is more expressive than first-order logic, allowing for the definition of concepts like finiteness and continuity
• Second-order logic is not complete, meaning there is no effective proof system that can derive all valid formulas
• Second-order logic does not have a compactness theorem, unlike first-order logic
• The Löwenheim-Skolem theorem does not hold for second-order logic, as it can characterize infinite structures up to isomorphism

Expressing Complex Ideas in Second-Order Logic

• Finiteness: A set is finite if and only if every injective function from the set to itself is surjective
  • $\forall P ((\forall x \forall y (P(x) \wedge P(y) \rightarrow x = y)) \rightarrow (\forall x P(x)))$
• Connectedness: A graph is connected if there is a path between any two vertices
  • $\forall x \forall y \exists P (P(x) \wedge P(y) \wedge \forall z \forall w ((P(z) \wedge E(z, w)) \rightarrow P(w)))$
• Continuity: A function is continuous if the preimage of every open set is open
  • $\forall P ((\forall x (P(x) \rightarrow \exists \varepsilon \forall y (d(x, y) < \varepsilon \rightarrow P(y)))) \rightarrow (\forall x (f^{-1}(P)(x) \rightarrow \exists \delta \forall y (d(x, y) < \delta \rightarrow f^{-1}(P)(y)))))$
• Inductive definitions: Defining a predicate or function using a base case and an inductive step
  • Example: Natural numbers: $\forall P ((P(0) \wedge \forall x (P(x) \rightarrow P(s(x)))) \rightarrow \forall x P(x))$

Pros and Cons of Second-Order Logic

Pros:

• Increased expressive power allows for defining complex mathematical concepts
• Provides a foundation for mathematics and set theory
• Enables reasoning about infinite structures and uncountable sets
• Allows for categorical axiomatizations of structures (e.g., natural numbers, real numbers)

Cons:

• Lacks completeness, meaning there is no effective proof system that can derive all valid formulas
• Does not have a compactness theorem, which limits its applicability in some areas
• Higher computational complexity compared to first-order logic
• Non-standard models can lead to unexpected results and inconsistencies
• Some proofs in second-order logic may not be constructive or may rely on non-effective methods

Diving into Higher-Order Logics

• Extend second-order logic by allowing quantification over predicates and functions of higher arities
• Third-order logic: Quantification over predicates and functions that take predicates and functions as arguments
• Fourth-order logic and beyond: Quantification over even higher-order predicates and functions
• Increase expressive power with each higher order, allowing for more complex concepts to be defined
• Face similar limitations as second-order logic, such as lack of completeness and compactness
• Higher-order logics are used in some areas of mathematics, such as topology and category theory
• Require careful handling of semantics and proof theory to avoid paradoxes and inconsistencies

Real-World Applications

• Formal verification: Using second-order logic to specify and verify properties of software and hardware systems
  • Example: Specifying security properties, such as non-interference and information flow
• Knowledge representation: Representing and reasoning about complex domains using second-order logic
  • Example: Ontologies in artificial intelligence and semantic web
• Automated theorem proving: Developing proof systems and algorithms for second-order logic to automate mathematical reasoning
  • Example: Proof assistants like Coq and Isabelle/HOL
• Philosophical logic: Analyzing and formalizing philosophical arguments and concepts using higher-order logics
  • Example: Formalizing modal logics and epistemic logics

Tricky Bits and Common Pitfalls

• Non-standard models: Second-order logic admits non-standard models that may not align with the intended interpretation
  • Example: Non-standard models of arithmetic that contain infinite numbers
• Impredicativity: Defining a predicate or function using a quantification that includes the predicate or function being defined
  • Can lead to paradoxes and inconsistencies if not handled carefully
• Higher-order quantification: Quantifying over predicates and functions of higher orders can be difficult to reason about and may lead to confusion
• Lack of completeness: There is no effective proof system that can derive all valid formulas in second-order logic
  • Some true statements may not be provable within the system
• Computational complexity: Reasoning in second-order logic and higher-order logics can be computationally expensive
  • Many problems are undecidable or have high complexity classes