Logic

Formal Logic Reference

Overview

Formal logic provides mathematical frameworks for representing and analyzing reasoning. The hierarchy progresses from propositional logic (truth-functional connectives over atomic propositions) through first-order logic (quantifiers over individuals with predicates) to second- and higher-order logics (quantification over sets, functions, and properties). Modal logic extends these systems with operators for necessity, possibility, knowledge, obligation, and time. Soundness ensures that provable statements are true, while inductive reasoning covers non-deductive inference from specific observations to general conclusions.

When to Use

• Building theorem provers, SAT solvers, or SMT solvers
• Designing type systems or programming language semantics
• Formalizing mathematical theories (arithmetic, set theory, geometry)
• Analyzing argument validity, soundness, and completeness
• Implementing knowledge representation and reasoning systems
• Working with modal operators in verification, epistemic reasoning, or temporal logic
• Distinguishing deductive certainty from inductive probability
• Choosing the appropriate logic level for a formalization task

Core Concepts

Logic hierarchy by expressive power:

Key metalogical properties:

• Validity: A formula true in every interpretation (tautology).
• Soundness: Every provable formula is valid. If Gamma |- phi, then Gamma |= phi.
• Completeness: Every valid formula is provable. If Gamma |= phi, then Gamma |- phi.
• Decidability: An algorithm exists to determine validity of any formula.
• Compactness: A set has a model iff every finite subset has a model (holds for FOL, not SOL with standard semantics).
• Lowenheim-Skolem: Any FOL theory with an infinite model has models of every infinite cardinality.

Notation:

• |- (turnstile): Syntactic consequence / provability
• |= (double turnstile): Semantic consequence / logical entailment
• True, False: Propositional constants (also written top, bot)
• forall x. P(x): Universal quantification ("for all x, P holds")
• exists x. P(x): Existential quantification ("there exists an x such that P holds")
• Box phi: Necessity ("necessarily phi")
• Diamond phi: Possibility ("possibly phi")

Advanced Topics

Propositional Logic: Syntax, semantics, truth tables, natural deduction, axiomatic systems, and valid argument forms → Propositional Logic

First-Order Logic: Quantifiers, predicates, terms, free/bound variables, structures, Gödel's completeness, undecidability, decidable fragments, Lowenheim-Skolem, compactness, Lindström's theorem → First-Order Logic

Second and Higher-Order Logic: Quantification over sets and functions, standard vs Henkin semantics, expressive power, categoricity, deductive incompleteness, monadic fragments, computational complexity connections → Second and Higher-Order Logic

Modal Logic: Kripke semantics, frames, accessibility relations, axiomatic systems (K, T, S4, S5), alethic/epistemic/temporal/deontic/doxastic modalities → Modal Logic

Soundness and Inductive Reasoning: Weak vs strong soundness for formal systems, soundness of arguments, completeness duality, inductive generalization, prediction, causal inference, problem of induction → Soundness and Inductive Reasoning