Logic

Definition

A logical system is a formal framework for reasoning about truth and inference. It typically consists of three main components:

1. A formal language specifying the syntax of well-formed formulas
2. A proof system defining rules of inference and derivation
3. A semantics assigning meaning through models, interpretations, or valuations

The study of logic encompasses both the syntax and semantics of propositional and predicate reasoning systems.

Types of Logic

Classical Logic

• Language: Terms, predicates, and connectives $\{\neg ,\wedge ,\vee ,\to ,\leftrightarrow ,\forall ,\exists \}$
• Proof System: Natural Deduction, Sequent Calculus, or Axiomatic Systems
• Semantics: Truth Tables for Propositional Logic, Tarski Semantics for first-order logic
• Satisfies the Law of the Excluded Middle

Intuitionistic Logic

• Language: Same connectives as classical logic
• Proof System: Natural Deduction without excluded middle
• Semantics: Kripke Semantics, Topological Semantics, or Beth Trees
• Constructive: proofs must provide explicit witnesses

Modal Logic

• Language: Classical connectives plus Modal Operators $\square$ (necessity) and $◊$ (possibility)
• Proof System: Extensions of classical systems with modal rules
• Semantics: Kripke models with accessibility relations

Type Theory

• Language: Terms with types, dependent products $\Pi x:A.B(x)$, dependent sums $\Sigma x:A.B(x)$
• Proof System: Type derivation rules following the Curry-Howard Correspondence
• Semantics: Propositions as Types where proofs are programs
• Connection: Provides computational interpretation of intuitionistic proofs through the BHK Interpretation

Non-Classical Systems

• Relevance Logic: Requires relevant connection between premises and conclusion
• Paraconsistent logic: Tolerates certain contradictions without explosion
• Many-valued logic: Allows truth values beyond true and false
• Temporal Logic: Reasoning about time-dependent propositions
• Epistemic Logic: Reasoning about knowledge and belief
• Deontic Logic: Reasoning about obligation and permission

Key Properties

Soundness

A logical system is sound if every provable formula is semantically valid:

\phi$$ ### [[Completeness (Logic)|Completeness]] A logical system is *complete* if every semantically valid formula is provable: $$\text{If } \Gamma \models \phi \text{ then } \Gamma \vdash \phi$$ ### [[Consistency (Logic)|Consistency]] A logical system is *consistent* if no contradiction is derivable from the axioms. ## Applications Logical systems underpin foundational work in mathematics through [[Peano Arithmetic]], [[Set Theory|Zermelo-Fraenkel set theory]], and [[Type Theory|type theory]]. In computer science, they enable [[program verification]], [[Type|type systems]], and [[Proof Assistant]] like [[Agda]]. Philosophy uses formal logic to analyze arguments, paradoxes, and theories of meaning and truth. ## History of Logic - *Syllogistic reasoning (4th century BCE)*: [[Aristotelian Logic]] establishes foundational principles of deduction - *Predicate logic (1879)*: [[Gottlob Frege|Frege]]'s *Begriffsschrift* introduces [[Predicate Calculus|first-order logic]] - *Formalization program (1920s)*: [[David Hilbert|Hilbert]]'s program seeks to formalize all of mathematics - *Intuitionistic logic (1920s-1930s)*: [[L.E.J. Brouwer|Brouwer]] develops constructive approach rejecting excluded middle - *Incompleteness theorems (1931)*: [[Kurt Gödel|Gödel]] proves fundamental [[Gödel's Theorems|limitations of formal systems]] - *Curry-Howard correspondence (1958-1969)*: Discovery that proofs in intuitionistic logic correspond to programs in [[Simply-Typed Lambda Calculus|typed lambda calculus]] - *[[Martin-Löf Type Theory]] (1972)*: Unification of logic and programming through [[Dependent Types|dependent types]] - *Modern developments (1990s-present)*: [[Homotopy Type Theory]], computer-verified mathematics, and proof assistants ## Metatheory The study of logical systems themselves involves [[proof theory]] for structural analysis of derivations, [[model theory]] for semantic structures, [[Computation|computability theory]] for algorithmic aspects, and [[Complexity Theory]] for resource bounds on logical decision problems. ## Related Concepts - [[Formal Language]] - [[Syntax of Logic]] - [[Semantics of Logic]] - [[Proof Theory]] - [[Model Theory]] - [[Curry-Howard Correspondence]] ## References [[enderton2001-mathematical-logic]] [[vanDalen2013-logic-structure]] [[gentzen1935-investigations-logical]] [[troelstra-schwichtenberg2000-basic-proof-theory]] [[dummett2000-intuitionism]] [[hott2013-book]] [[shapiro1991-second-order-foundations]] [[kleene1952-metamathematics]] [[kleene1967-logic]]