Fact-checked by Grok 2 weeks ago

Formal system

A formal system is an abstract framework in mathematics and logic consisting of a formal language defined over a finite alphabet of primitive symbols, a set of axioms serving as initial well-formed formulas, and a finite set of inference rules that enable the syntactic derivation of theorems from the axioms.^[1]^[2] Formal systems facilitate rigorous deductive reasoning by focusing exclusively on the manipulation of symbol strings according to specified rules, independent of any semantic interpretation or external meaning.^[3] This syntactic approach underpins key areas such as proof theory, which studies the structure of proofs, and model theory, which examines interpretations of formal languages.^[2] Historically, the development of formal systems arose in the late 19th century amid efforts to eliminate ambiguities in mathematical foundations, with Gottlob Frege's Begriffsschrift (1879) providing the first complete formal axiomatic treatment of logic and arithmetic.^[4] David Hilbert advanced the idea in the 1920s through his program to formalize all of mathematics as a finite, consistent "game" of symbols, aiming to secure its foundations against paradoxes like Russell's.^[4]^[3] Despite their power, formal systems have inherent limitations, as demonstrated by Kurt Gödel's incompleteness theorems of 1931, which prove that any consistent formal system capable of expressing basic arithmetic is incomplete, meaning some true statements within its language cannot be proved using its axioms and rules.^[5] These theorems undermined Hilbert's full ambitions but highlighted the depth of formal methods in revealing mathematics' boundaries.^[5] Today, formal systems are indispensable in computer science for applications like automated theorem proving, type theory in programming languages, and formal verification of software and hardware, ensuring correctness through machine-checkable proofs.^[4] Notable examples include Peano arithmetic for natural numbers and Zermelo-Fraenkel set theory (ZFC) for set-based mathematics, both of which illustrate how formal systems encode vast swaths of mathematical knowledge.^[2]

Core Components

Formal Language

In a formal system, the formal language constitutes the syntactic foundation, comprising a finite set of symbols known as the alphabet from which finite strings are formed to create meaningful expressions. This language is defined recursively, ensuring that only specific combinations qualify as well-formed formulas (wffs), which are the valid syntactic objects of the system. The alphabet typically includes primitive symbols—basic, indivisible elements such as constants, variables, logical connectives, predicates, function symbols, and quantifiers—while derived symbols are abbreviations or composites built from primitives, such as biconditional (↔) defined via implication (→) and negation (¬).^[6]^[7] The formation rules, or syntax, specify how wffs are constructed inductively. For propositional logic, the alphabet consists of propositional variables (e.g., P, [Q](/page/Q), [R](/page/R)) and primitive connectives such as conjunction (\wedge), disjunction (\vee), and negation (\neg), along with parentheses for grouping. The recursive definition begins with atomic wffs as the propositional variables themselves; compound wffs are then formed by applying connectives, such as \neg P or (P \wedge [Q](/page/Q)). This ensures unambiguous parsing, as every wff has a unique structure. For example, the expression (P \vee \neg [Q](/page/Q)) is a wff, while P \vee is not, due to incomplete grouping.^[6]^[7] In first-order logic, the alphabet expands to include individual variables (e.g., x, y, z), individual constants (e.g., a, b), function symbols (e.g., f for unary functions), predicate symbols (e.g., P^1 for unary predicates, R^2 for binary), and quantifiers (\forall for universal, \exists for existential), in addition to the propositional connectives and parentheses. Terms are built recursively: variables and constants are terms, and if t_1, \dots, t_n are terms, then f(t_1, \dots, t_n) is a term. Atomic wffs are equations like t_1 = t_2 or predicate applications like P(t_1, \dots, t_n); compound wffs extend these with connectives and quantifiers, such as \forall x (P(x) \wedge Q(x)) or \exists y R(x, y). These rules recursively define terms and sentences (closed wffs without free variables), guaranteeing that the language provides a precise, ambiguity-free structure for all expressions in the formal system. The formal language thus interfaces with the deductive apparatus by supplying the wffs from which theorems are derived via inference rules.^[6]^[7]

Deductive Apparatus

In a formal system, the deductive apparatus consists of a set of axioms and inference rules that enable the derivation of theorems from initial assumptions within the formal language. This structure, often termed a deductive system, provides a syntactic mechanism for generating new well-formed formulas (wffs) solely based on their form, without reference to meaning.^[8] Axioms serve as the foundational statements of the system, divided into logical axioms and non-logical axioms. Logical axioms are general tautologies inherent to the underlying logic, such as schemata that hold for all interpretations (e.g., \phi \lor \lnot \phi for the law of excluded middle in classical systems). These capture the universal principles of inference and are fixed across applications. Non-logical axioms, in contrast, are domain-specific assumptions tailored to the particular theory, such as Peano's axioms for arithmetic, which introduce concepts like successor functions beyond pure logic.^[9]^[10] Inference rules specify how existing wffs can be transformed to produce new ones, typically in a finite, mechanical manner. A primary example is modus ponens, formally defined as: from premises A and A \to B, infer B. This rule, central to systems like Hilbert's, allows detachment of consequents from conditionals when the antecedent is established. Other rules may include substitution or generalization, but modus ponens exemplifies the step-by-step expansion of derivable content.^[8]^[11] A proof within the deductive apparatus is a finite sequence of wffs where the first formula is the desired theorem, and each subsequent formula is either an axiom or follows from prior formulas via an inference rule. Such sequences formalize the notion of derivability, denoted \Gamma \vdash \phi, indicating that \phi is deducible from a set of premises \Gamma. This process relies on the syntax of the formal language to ensure rigor and unambiguity.^[8]^[11] Syntactic deduction, as facilitated by the deductive apparatus, differs fundamentally from semantic entailment. Syntactic deduction concerns formal proofs constructed via axioms and rules, yielding theorems independent of interpretation. Semantic entailment, however, evaluates whether a formula holds true in all models satisfying the premises, linking syntax to meaning. While related through soundness and completeness theorems, the deductive apparatus operates purely syntactically.^[8]^[11]

Semantics and Interpretation

Semantics in formal systems assigns meaning to syntactic expressions by mapping them to elements within a specified mathematical structure, thereby connecting abstract symbols to concrete interpretations. This process, known as interpretation, bridges the gap between the formal language's rules of formation and well-formed formulas and their referential content in a domain of discourse.^[12] A key component of semantics is the notion of a structure or model, which consists of a non-empty set D serving as the domain of discourse and interpretation functions for the non-logical symbols of the language. Constants are interpreted as elements of D, function symbols as mappings from tuples in D to elements in D, and predicate symbols as relations on D. For instance, a binary predicate P is interpreted as a subset of D \times D, representing the pairs for which P holds. These interpretations fix the "intended" meaning of the language's vocabulary relative to the chosen domain.^[12] Central to semantic evaluation is the definition of truth or satisfaction within a model, pioneered by Alfred Tarski in his recursive theory for first-order logic. Satisfaction is defined inductively over the complexity of formulas: an atomic formula P(t_1, \dots, t_n), where t_i are terms, is satisfied by an assignment of values from D to variables if the tuple of their interpretations lies in the relation denoted by P's interpretation. For compound formulas, satisfaction follows the logical connectives—e.g., a conjunction \phi \land \psi is satisfied if both \phi and \psi are—and quantifiers, where \forall x \phi holds if \phi is satisfied under every variable assignment differing at most in x, and similarly for existential quantification. This Tarskian framework ensures that truth is materially adequate and formally precise, avoiding paradoxes by distinguishing object language from metalanguage.^[13] The distinction between syntax and semantics underscores that syntactic rules manipulate symbols as arbitrary marks without inherent meaning, whereas semantics imposes external interpretations to determine truth values or validity. A sentence may be provable syntactically in a deductive system yet require semantic verification for correspondence to reality; this interplay supports theorems like soundness, where provable sentences are true in all models.^[14] An illustrative application appears in automated theorem proving, where the Herbrand universe provides a canonical domain for skolemized formulas. After skolemization replaces existentially quantified variables with skolem functions, the Herbrand universe is the set of all ground terms generated from the language's constants and function symbols, serving as a minimal domain to test satisfiability without arbitrary elements. Herbrand models over this universe then correspond to interpretations where atomic ground formulas are true exactly when they hold in some model of the original formula, facilitating resolution-based proof search.^[15]

Fundamental Properties

Soundness and Completeness

In formal systems, soundness is a meta-theoretical property that ensures the deductive apparatus does not derive invalid statements. Specifically, the soundness theorem states that if a formula \phi is provable from a set of premises \Gamma (denoted \Gamma \vdash \phi), then \phi is semantically entailed by \Gamma (denoted \Gamma \models \phi), meaning \phi holds true in every model satisfying \Gamma.^[16] This property guarantees that proofs preserve truth, linking the syntactic notion of derivation to semantic validity. The completeness theorem provides the converse relation, asserting that every semantically valid formula is provable. For first-order logic, Kurt Gödel proved in 1930 that if \Gamma \models \phi, then \Gamma \vdash \phi, establishing that the Hilbert-style axiomatization captures all logical truths.^[17] This result demonstrates the adequacy of the formal system in exhaustively representing semantic entailments through syntactic means. In systems that are both sound and complete, syntactic consequence and semantic consequence are equivalent, allowing proofs to fully characterize logical validity without missing or extraneous derivations. This equivalence underpins the reliability of formal systems for reasoning, as it aligns deduction precisely with model-theoretic truth. For restricted fragments, such as propositional logic, completeness holds in a strong sense, where every tautology is provable. Hilbert-style systems for propositional logic, as formalized by Hilbert and Ackermann, achieve both soundness and completeness, with the completeness result originally established by Emil Post in 1921.^[16]

Consistency and Decidability

In a formal system, consistency is the property that ensures no formula \phi and its negation \neg \phi can both be derived as theorems.^[18] This syntactic condition prevents the system from deriving contradictions, meaning not every formula is provable.^[19] Consistency can be absolute, established through finitary methods independent of stronger assumptions, or relative, demonstrated by showing that if a base theory is consistent, then the extended system is also consistent.^[20] Proofs of consistency often rely on semantic models, where Gödel's completeness theorem establishes that every consistent first-order theory has a model, thereby confirming its consistency via satisfiability.^[21] Finitary methods, such as Gentzen's cut-elimination theorem in sequent calculus, provide absolute consistency proofs for systems like Peano arithmetic by reducing proofs to atomic forms without the cut rule, ensuring no contradictions arise through transfinite induction up to the ordinal \epsilon_0.^[19] Decidability in a formal system refers to the existence of an algorithm that, for any sentence, determines whether it is provable within the system. Church's theorem (1936) proves that first-order logic is undecidable, as there is no general algorithm to determine the validity or provability of arbitrary sentences, linking this to the undecidability of the halting problem via lambda calculus reductions.^[22] However, certain fragments are decidable; for instance, Presburger arithmetic, which interprets addition over the integers without multiplication, admits a decision procedure using quantifier elimination, as shown by Presburger in 1930.^[23] Independence arises when a statement is neither provable nor disprovable in a consistent system, highlighting its limitations. A prominent example is the continuum hypothesis in Zermelo-Fraenkel set theory with the axiom of choice (ZFC), which Gödel (1940) showed is consistent relative to ZFC via the constructible universe, and Cohen (1963) proved independent by forcing a model where it fails.^[24]

Historical Development

Early Foundations in Logic

The origins of formal systems can be traced to ancient Greek philosophy, particularly Aristotle's syllogistic logic, which served as a proto-formal system for deductive reasoning. In his Prior Analytics, Aristotle defined a syllogism as a deductive argument in which, given certain premises, a distinct conclusion necessarily follows, structured around categorical propositions involving subject and predicate terms connected by a copula.^[25] He identified four types of categorical sentences—universal affirmative (AaB: "Every A is B"), universal negative (AeB: "No A is B"), particular affirmative (AiB: "Some A is B"), and particular negative (AoB: "Some A is not B")—and organized valid inferences into three figures based on the position of the middle term, yielding 14 valid syllogistic moods such as Barbara (AaB and BaC imply AaC).^[25] These inference rules, including conversion (e.g., AeB implies BeA) and reductio ad impossibile, provided a systematic framework for evaluating arguments, though interpreted as a fragment of modern first-order logic with assumptions of non-empty classes.^[25] Medieval logicians built upon Aristotelian foundations through developments in supposition theory and terminist logic, refining the semantics of terms in propositions. Supposition theory, emerging in the 12th–13th centuries, analyzed how terms "supposit" or stand for things in context, distinguishing personal supposition (terms referring to extra-linguistic entities) from material supposition (terms referring to themselves or concepts), which allowed for more precise handling of ambiguity in sentences.^[26] Terminist logic, associated with works like the Dialectica Monacensis, emphasized terms as the basic units of analysis, incorporating modal distinctions such as de dicto (propositional modality) and de re (real modality) to address quantified modal statements.^[26] A notable advancement came from John Buridan in the 14th century, who streamlined terminist methods in his Summulae de dialectica and developed a modal logic rejecting essentialist assumptions in favor of a temporalist approach using simultaneous supposition for alternatives, treating possibility and necessity symmetrically and influencing late medieval logical treatises.^[27]^[26] In the 19th century, the algebra of logic marked a shift toward symbolic manipulation, pioneered by George Boole in his 1854 work An Investigation of the Laws of Thought. Boole treated logical classes algebraically, using symbols like x and y to represent subsets of the universe (with 1 as the universe and 0 as the empty set), and defined operations such as multiplication for intersection (xy) and addition for disjoint union (x + y), governed by laws including commutativity (xy = yx), idempotence (x² = x), and distributivity (z(x + y) = zx + zy).^[28] This Boolean algebra replaced traditional syllogistic reasoning with algorithmic equation-solving, enabling the expansion theorem to derive conclusions from premises like "All X is Y" as x = vy, thus founding modern algebraic logic.^[28] Gottlob Frege advanced this trajectory in 1879 with Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens, introducing the first formal notation for first-order predicate logic complete with quantifiers. Frege's two-dimensional script represented complex thoughts through functional expressions, negations, conditionals, and generality indicators (e.g., concavities for universal quantification like "every" and Roman letters for variables), allowing precise formulation of quantified statements beyond subject-predicate structures.^[29] This system formalized inferences via axioms and rules, emphasizing the unsaturated nature of predicates as functions awaiting arguments, and laid the groundwork for modern predicate calculus despite initial resistance due to its novel notation.^[29] Subsequent developments bridged the late 19th and early 20th centuries. Giuseppe Peano formalized the axioms of arithmetic in 1889, providing a rigorous symbolic foundation for natural numbers that influenced later axiomatic systems. Bertrand Russell's discovery of the paradox in naive set theory (1901) highlighted foundational issues, leading to his and Alfred North Whitehead's Principia Mathematica (1910–1913), which attempted a comprehensive formalization of mathematics using ramified type theory to avoid paradoxes. These works emphasized axiomatic rigor and symbolic precision, setting the stage for 20th-century efforts.^[30]^[31]^[32] A key limitation of these pre-20th-century systems was their lack of rigorous axiomatization; Aristotelian and medieval logics relied on intuitive rules without comprehensive axiomatic foundations, while Boole's algebra handled extensional relations but inadequately captured generality, and even Frege's early work used minimal axioms without full type distinctions or bivalence principles.^[33] This paved the way for 20th-century axiomatic refinements.^[33]

Modern Formalizations

In the 1920s, David Hilbert proposed a program to establish the foundations of mathematics through the complete formal axiomatization of all mathematical theories, aiming to prove their consistency using only finitary methods that avoid infinite processes.^[34] This approach sought to secure classical mathematics against the paradoxes uncovered in set theory by reducing all proofs to concrete, combinatorial operations verifiable by humans, thereby providing an absolute foundation immune to revision.^[35] Hilbert's vision emphasized the axiomatic method as a tool for rigor, where formal systems would encapsulate mathematics in a finite set of symbols and rules, allowing consistency to be demonstrated without appealing to non-constructive ideal elements.^[34] Kurt Gödel's incompleteness theorems of 1931 profoundly impacted Hilbert's program by demonstrating that any consistent formal system capable of expressing basic arithmetic is incomplete, meaning there exist true statements within the system that cannot be proved or disproved using its axioms and rules. The first theorem shows that such a system cannot prove its own consistency, while the second implies that if consistent, it cannot establish the consistency of any stronger system containing it. These results, derived through arithmetization of syntax and self-referential statements, revealed inherent limitations in formal axiomatization, shifting focus from absolute consistency proofs to relative ones and influencing subsequent developments in proof theory.^[5] Alfred Tarski's 1933 work provided a rigorous semantic foundation by defining truth for formal languages in a materially adequate and non-paradoxical manner, using a hierarchical structure of languages to distinguish object language from metalanguage. His Convention T requires that a truth definition satisfy instances like "'Snow is white' is true if and only if snow is white," ensuring semantic concepts align with intuitive notions while avoiding liar paradoxes through syntactic levels. This framework enabled precise model-theoretic interpretations of formal systems, separating syntax from semantics and facilitating the study of satisfaction and validity in interpreted structures.^[36] Gerhard Gentzen's 1934 introduction of natural deduction and sequent calculus advanced proof theory by offering systems that mimic human reasoning more closely than axiomatic methods, emphasizing structural rules for inference.^[37] Natural deduction uses introduction and elimination rules for logical connectives, allowing proofs to build intuitively from assumptions, while sequent calculus represents derivations as sequences of formulas separated by turnstiles, enabling cut-elimination theorems that normalize proofs and prove consistency for classical and intuitionistic logics.^[37] These innovations provided tools for analyzing proof complexity and substructural logics, bridging Hilbert's formalist ideals with more flexible deductive frameworks.^[37] The mid-20th century saw formal systems evolve toward type theory and category theory as alternatives to set-theoretic foundations, addressing paradoxes and incompleteness through structured hierarchies and abstract relations. Type theory, building on Bertrand Russell's ramified types and Alonzo Church's simple typed lambda calculus from the 1940s, imposes levels on expressions to prevent self-reference issues, enabling constructive mathematics where types classify terms and ensure well-formed computations. Church's system formalized higher-order logic with functional types, providing a basis for lambda calculi that underpin modern proof assistants. Meanwhile, category theory, formalized by Samuel Eilenberg and Saunders Mac Lane in 1945 and extended by William Lawvere's 1964 elementary theory of categories, treats mathematical structures via objects, morphisms, and compositions, offering a relational foundation that unifies diverse fields without privileging sets. Lawvere's approach axiomatizes categories to recover set theory internally, supporting variable-set foundations and emphasizing functorial semantics over extensional equality.^[38] These developments shifted formal systems toward modular, abstract frameworks suitable for both rigorous proof and computational implementation.

Applications and Extensions

In Mathematical Logic

Formal systems play a central role in the foundations of mathematics by providing axiomatic frameworks that encode the entirety of mathematical reasoning. Zermelo-Fraenkel set theory with the axiom of choice (ZFC) serves as the predominant formal system for this purpose, consisting of a first-order language with a single binary predicate for set membership and a set of axioms that govern the formation and properties of sets.^[39] Introduced by Ernst Zermelo in 1908 and refined by Abraham Fraenkel in 1922 through the addition of the axiom schema of replacement and adjustments to separation, ZFC enables the formal derivation of theorems across arithmetic, analysis, and geometry from its axioms.^[40] Within ZFC, all mathematical objects—such as numbers, functions, and spaces—are constructed as sets, ensuring a unified and rigorous basis for proofs that avoids paradoxes like Russell's through the axiom of foundation.^[41] In model theory, formal systems facilitate the study of mathematical structures by interpreting their languages in diverse models, revealing relationships like isomorphism between seemingly distinct objects. A structure for a formal system is a set equipped with interpretations of the system's non-logical symbols, allowing theorems to be evaluated as true or false within that model.^[42] The back-and-forth method, originating in Georg Cantor's work on dense linear orders and developed in model theory by Roland Fraïssé, constructs isomorphisms between countable models of a theory by alternately extending partial isomorphisms to match elements from each side, ensuring equivalence under the theory's axioms.^[43]^[44] For instance, this technique proves that all countable dense linear orders without endpoints, such as the rationals, are isomorphic, highlighting how formal systems classify structures up to elementary equivalence.^[42] Proof theory employs formal systems to analyze the strength and consistency of mathematical theories through ordinal assignments that measure proof complexity. Ordinal analysis assigns to a theory, like Peano arithmetic (PA), a proof-theoretic ordinal representing the supremum of ordinals embeddable into its cut-free proofs, providing a relative consistency proof via transfinite induction.^[45] Gerhard Gentzen's 1936 consistency proof for PA establishes that if transfinite induction up to the ordinal \epsilon_0—the least fixed point of \alpha \mapsto \omega^\alpha—holds, then PA is consistent, as cut-elimination reduces proofs to quantifier-free forms without contradiction.^[45] This ordinal \epsilon_0 quantifies PA's consistency strength, showing that stronger systems like second-order arithmetic require larger ordinals for analogous analyses.^[45] Recursion theory, or computability theory, uses formal systems to classify computable functions and their hierarchies within arithmetic. Formal systems like primitive recursive arithmetic formalize the computable functions via schemes for zero, successor, and composition, extended by minimization in full recursion theory.^[46] Kleene's recursion theorem (1938) asserts that for any computable functional \Phi_e indexing partial recursive functions, there exists an index i such that \Phi_i = \Phi_i(\langle i \rangle), enabling self-referential programs where a function can compute its own index and modify its behavior accordingly.^[46]^[47] This theorem underpins fixed-point constructions in computability, illustrating how formal systems capture the self-applicability of recursive definitions.^[46] Despite their power, formal systems face inherent limitations in mathematical logic, particularly regarding decidability. Hilbert's tenth problem, posed in 1900, sought an algorithm to determine solvability of Diophantine equations—polynomial equations with integer coefficients and unknowns. Yuri Matiyasevich's 1970 theorem proves this problem undecidable by showing that every recursively enumerable set is Diophantine, reducing Turing machine halting to integer solutions via exponential growth encoded in polynomials like Fibonacci relations.^[48] Thus, no formal system encompassing arithmetic can decide all such equations, underscoring Gödel's incompleteness as a barrier to fully mechanizing number theory.^[48]

In Computer Science and Computation

In computer science, formal systems underpin the theoretical foundations of computation, particularly through models like Turing machines and the lambda calculus, which define what is computable. A Turing machine, introduced by Alan Turing in 1936, is an abstract formal system consisting of a tape, a read-write head, and a finite set of states with transition rules that manipulate symbols on the tape.^[49] This system formalizes sequential computation and proves key results in computability theory, such as the undecidability of the halting problem. Similarly, the lambda calculus, developed by Alonzo Church around 1936, serves as a formal system for expressing functions via abstraction and application, where terms like \lambda x. M denote functions that take input x and yield output M.^[50] Church's framework demonstrates the equivalence of lambda terms to Turing machine computations under the Church-Turing thesis, establishing it as a foundational model for functional programming and higher-order functions.^[51] In automata theory, these formal systems extend to hierarchies like finite automata and pushdown automata, which recognize regular and context-free languages, respectively, providing computability bounds for algorithmic processes. Type systems in programming languages leverage formal systems to ensure program safety and correctness, with the simply-typed lambda calculus exemplifying this approach. Introduced by Church in 1940, the simply-typed lambda calculus augments the untyped version with base types (e.g., individuals and truth values) and function types \sigma \to \tau, enforced by typing rules that prevent ill-formed expressions like applying a function to an incompatible type.^[52] This formal system guarantees strong normalization—every well-typed term reduces to a unique normal form—eliminating paradoxes such as the untyped calculus's self-application, and it directly influences type checkers in languages like ML and Haskell.^[53] By modeling types as a simply-typed lambda calculus itself, modern type systems support features like polymorphism and dependent types, enabling compile-time detection of errors and facilitating modular software design. Formal verification employs formal systems to prove properties of computational systems, notably through model checking with linear temporal logic (LTL). LTL, pioneered by Amir Pnueli in 1977, is a modal logic extending propositional logic with temporal operators like \mathbf{G} (always) and \mathbf{F} (eventually), allowing specifications of system behaviors over infinite execution paths, such as "a request is eventually granted" via \mathbf{G}(request \to \mathbf{F} grant).^[54] In model checking, a formal system like a Kripke structure (states, transitions, and labeling) is exhaustively explored against LTL formulas using algorithms that translate specifications to automata, verifying properties like safety (no bad states) or liveness (progress).^[55] Tools implementing LTL model checking, such as SPIN, have scaled to industrial applications, detecting bugs in protocols by counterexample generation when properties fail. Hoare logic provides an axiomatic formal system for deductive verification of imperative programs, focusing on partial correctness. Proposed by C. A. R. Hoare in 1969, it uses triples \{P\} S \{Q\}, where precondition P, statement S, and postcondition Q ensure that if P holds before executing S and S terminates, then Q holds afterward; axioms like assignment x := e yield \{Q[e/x]\} x := e \{Q\}, and rules compose proofs for compound statements.^[56] This system formalizes reasoning about loops via invariants and has been extended to concurrent programs, underpinning tools like VCC for verifying device drivers through weakest precondition calculus. The Curry-Howard isomorphism bridges formal systems in logic and computation, interpreting proofs in intuitionistic logic as programs in typed lambda calculus. Originating in Haskell Curry and Robert Feys' 1958 work on combinatory logic and formalized by William Howard in 1980, it equates propositions with types (e.g., A \to B as type of functions from A to B) and proofs with terms (introduction rules as lambda abstractions, elimination as applications).^[57] In intuitionistic settings, this yields the propositions-as-types principle, where normalization of proofs corresponds to program termination, influencing proof assistants like Coq that extract verified programs from logical proofs.

References

[1]
Formal Systems - Computer Science
A formal system consists of a language over some alphabet of symbols together with (axioms and) inference rules that distinguish some of the strings in the ...
[2]
Syntax & Semantics of Formal Systems
Mar 25, 2010 · A formal system (also known as: "symbol system", "formal symbol system", "formal language", "formal theory", etc.) consists of: primitive (" ...
[3]
Formalism in the Philosophy of Mathematics
Jan 12, 2011 · Any formal system of the usual sort could be 'reduced' into one in which there is only one provability predicate and truth (= provability) in ...
[4]
Formalized Mathematics (AutoMath) - Nuprl - Cornell University
David Hilbert was led to the idea of a formal system for similar but distinct reasons. He developed this notion with increasing precision and clearer purpose in ...
[5]
Kurt Gödel (Stanford Encyclopedia of Philosophy)
Summary of each segment:
[6]
Classical Logic - Stanford Encyclopedia of Philosophy
Sep 16, 2000 · The formal language is a recursively defined collection of strings on a fixed alphabet. As such, it has no meaning, or perhaps better, the ...
[7]
None
Below is a merged summary of formal language concepts from Mendelson's "Introduction to Mathematical Logic" (6th Ed., 2015), consolidating all information from the provided segments into a comprehensive response. To maximize detail and clarity, I will use a structured format with tables where appropriate, followed by a narrative summary. The response retains all key points, examples, page references, and URLs mentioned across the segments.
[8]
Propositional Logic - Stanford Encyclopedia of Philosophy
May 18, 2023 · Propositional logic is the study of the meanings of, and the inferential relationships that hold among, sentences based on the role that a specific class of ...
[9]
[PDF] Rules vs. Axioms - Two Axiomatic Styles from a Modern Perspective
May 12, 2017 · ▻ In a formal theory logical and non-logical terms are distinct. ... What about a larger class of formal systems including non-logical theories.
[10]
[PDF] Lecture 5
In formal systems we divide the axioms into logical and non-logical axioms. • In some systems with very strong deduction rules we have no logical axioms at all.
[11]
Chapter 4 - Stanford Introduction to Logic
We begin this lesson by defining some basic concepts - axiom schemas, rules of inference, and direct proofs. We then look at a couple of proof systems.Missing: formal | Show results with:formal
[12]
Model Theory - Stanford Encyclopedia of Philosophy
Nov 10, 2001 · Model theory is the study of the interpretation of any language, formal or natural, by means of set-theoretic structures, with Alfred Tarski's truth definition ...
[13]
Tarski's truth definitions - Stanford Encyclopedia of Philosophy
Nov 10, 2001 · First-order Zermelo-Fraenkel set theory is widely regarded as the standard of mathematical correctness, in the sense that a proof is correct if ...The 1933 programme and the... · Some kinds of truth definition...
[14]
Theories of Meaning - Stanford Encyclopedia of Philosophy
Jan 26, 2010 · One sort of theory of meaning—a semantic theory—is a specification of the meanings of the words and sentences of some symbol system. Semantic ...Word Meaning · Normativity of Meaning · Meaning Holism · 10
[15]
Herbrand Universe -- from Wolfram MathWorld
Given the completeness of first-order logic, this program is basically a tool for automated theorem proving.
[16]
Grundzüge der theoretischen Logik : Hilbert, David, 1862-1943
Sep 5, 2019 · Grundzüge der theoretischen Logik. by: Hilbert, David, 1862-1943. Publication date: 1967. Topics: Logic, Symbolic and mathematical. Publisher ...
[17]
[PDF] Die Vollst~ndigkeit der Axiome des logischen Funktionenkalkiils ~).
Von Kurt GSdel in Wien. Whitehead und Russell haben bekanntlich die Logik und. Mathematik so aufgebaut, datl sie gewisse evidente S~ttze als Axiome.Missing: Gödel | Show results with:Gödel
[18]
Consistency - Encyclopedia of Mathematics
Dec 30, 2018 · The property of a formal system requiring that not every formula of the system is provable in it. Formal systems having this property are called consistent.
[19]
Proof Theory - Stanford Encyclopedia of Philosophy
Aug 13, 2018 · The two aspects together opened a new era for proof theory and mathematical logic with the goal of proving the consistency of analysis. We will ...Development of · Appendix D · Provably computable functions<|control11|><|separator|>
[20]
[PDF] Relative Consistency - Carnegie Mellon University
Feb 1, 2005 · They are concerned with mathematical analysis and theories in which its practice can be formally represented. So I start out by describing ...
[21]
Gödel's Incompleteness Theorems
Nov 11, 2013 · Any consistent formal system \(F\) within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are ...
[22]
Church's Undecidability Theorem (1936) - PhilPapers
Church's Undecidability Theorem is one of the meta-theoretical results of the mid-third decade of the last century, which along with other limiting theorems ...
[23]
[PDF] A Survival Guide to Presburger Arithmetic
Hilbert became aware of Presburger's work and viewed it as a first ... Another decidable extension of Presburger arithmetic allows for counting the number.
[24]
The Continuum Hypothesis - Stanford Encyclopedia of Philosophy
May 22, 2013 · The combined results of Gödel and Cohen thus demonstrate that assuming the consistency of ZFC, it is in principle impossible to settle either CH ...Independence in Cardinal... · Definable Versions of the... · The Case for ¬CH
[25]
Ancient Logic - Stanford Encyclopedia of Philosophy
Dec 13, 2006 · Aristotle defines a syllogism as 'an argument (logos) in which, certain things having been laid down, something different from what has been ...
[26]
Medieval Theories of Modality - Stanford Encyclopedia of Philosophy
Jun 30, 1999 · The new modal logic was among the most remarkable achievements of medieval logic. Buridan's modal logic was dominant in late medieval times ...Missing: scholarly | Show results with:scholarly
[27]
John Buridan - Stanford Encyclopedia of Philosophy
May 13, 2002 · First, Buridan did much to streamline and better articulate the methods of terminist logic. The most important analytical tool in the Summulae ...
[28]
George Boole - Stanford Encyclopedia of Philosophy
Apr 21, 2010 · George Boole (1815–1864) was an English mathematician and a founder of the algebraic tradition in logic. He worked as a schoolmaster in ...The Context and Background... · The Laws of Thought (1854) · Boole's Methods
[29]
Gottlob Frege - Stanford Encyclopedia of Philosophy
Sep 14, 1995 · A predicate calculus is a formal system (a formal language and a method of proof) in which one can represent valid inferences among predications ...Frege's Theorem · Frege's Logic · 1. Kreiser 1984 reproduces the...<|control11|><|separator|>
[30]
Frege's Logic - Stanford Encyclopedia of Philosophy
Feb 7, 2023 · Frege's formal system only needs to include those logical principles that are required for his reconstructions of arithmetic and analysis—his ...
[31]
[PDF] Hilbert's Program: 1917-1922 - Carnegie Mellon University
in Hilbert and Ackermann's book, Grundzüge der theoretischen Logik, published in 1928. Indeed, the basic structure of the book is the same as that of the ...
[32]
[PDF] Hilbert's Program Then and Now - arXiv
Aug 29, 2005 · Briefly, Hilbert's proposal called for a new foundation of mathematics based on two pillars: the axiomatic method, and finitary proof theory ...
[33]
[PDF] Untersuchungen über das logische Schließen I - Digizeitschriften
Titel: Untersuchungen über das logische Schließen I. Autor: Gentzen, G. Ort: Berlin. Jahr: 1935. PURL: https://resolver.sub.uni-goettingen.de/purl ...
[34]
[PDF] AN ELEMENTARY THEORY OF THE CATEGORY OF SETS (LONG ...
May 23, 2005 · Yet the second categorical foundation ever worked out, and the first in print, was a set theory—Lawvere's axioms for the category of sets, ...
[35]
[PDF] Axioms of Set Theory
In this section we give Zermelo's axiomatic system of Set Theory, called Zermelo–. Fraenkel Set Theory, denoted ZF. This axiomatic system contains all axioms of.
[36]
[PDF] A. A. Fraenkel: The Independence of the Axiom of Choice (1922)
Nov 21, 2017 · If,by the use of Axioms II, IV, and V alone, a set is formed from given objects in such a way that for each of these objects there is a ...
[37]
[PDF] Zermelo-Fraenkel Set Theory
Mar 25, 2022 · Set theory owes its popularity to the fact that it is a unifying system for mathematics: ... those of ZFC (including Foundation),. 2. all ...
[38]
[PDF] Lecture notes - Model Theory (Math 411) Autumn 2002.
Dec 9, 2002 · A well-known back- and forth argument shows that any two countable models of T are isomorphic so T is ω-categorical, so complete. T has 2κ ...
[39]
[PDF] Model Theory - UC Berkeley math
For τ a signature we define the free term τ-structure 디. T(τ) to be the τ-structure with domain T(τ) and with interpretations as follows: • for c ∈ Cτ we ...
[40]
[PDF] On the Consistency of Peano Arithmetic in a Proof-theoretic ... - arXiv
Jun 27, 2025 · Recall that Gentzen's original consistency proof for PA relied on transfinite induc- tion up to the ordinal ε0. Following this tradition, we ...
[41]
[PDF] Kleene's amazing second recursion theorem. - UCLA Mathematics
A notation system for ordinals or r-system (in Kleene [1938]) is a set S ⊆ N, together with a function x | 7→x|S which assigns to each x in S a countable.
[42]
[PDF] HILBERT'S TENTH PROBLEM: What can we do with Diophantine ...
This form of the undecidability of Hilbert's 10th problem indicates that there is a close relationship between algorithms and Diophantine equations. The ...
[43]
[PDF] ON COMPUTABLE NUMBERS, WITH AN APPLICATION TO THE ...
By A. M. TURING. [Received 28 May, 1936.—Read 12 November, 1936.] The "computable" numbers may be described briefly ...
[44]
[PDF] An Unsolvable Problem of Elementary Number Theory Alonzo ...
Mar 3, 2008 · Alonzo Church. American Journal of Mathematics, Vol. 58, No. 2. (Apr., 1936), pp. 345-363. Stable URL:.
[45]
[PDF] THE CALCULI OF LAMBDA-CONVERSION
Alonzo Church, A formulation of the simple theory of types,. The journal of symbolic logic, vol. 5 (1940), pp. 56 - 68. 61. H.B. Curry, A formalization of ...
[46]
[PDF] A Formulation of the Simple Theory of Types Alonzo Church The ...
Apr 2, 2007 · The purpose of the present paper is to give a formulation of the simple ... N. J., 1936, and The calculi of lambda-conversion, forthcoming ...Missing: original | Show results with:original
[47]
Stlc: The Simply Typed Lambda-Calculus - Software Foundations
The simply typed lambda-calculus (STLC) is a tiny core calculus embodying the key concept of functional abstraction.
[48]
The temporal logic of programs - ACM Digital Library
The main proof method suggested is that of temporal reasoning in which the time dependence of events is the basic concept.Missing: original paper
[49]
[PDF] Model Checking for Linear Temporal Logic
We provide the syntax and semantics of LTL, a detailed example of a finite state concurrent program, and express safety and liveness-under-fairness properties ...
[50]
[PDF] An Axiomatic Basis for Computer Programming
In this paper an attempt is made to explore the logical founda- tions ... Volume 12 / Number 10 / October, 1969. Page 6. C. A. R. HOARE-cont'd from page 580.
[51]
[PDF] Curry-Howard Isomorphism
The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in proof theory and computational.