Formal System

A formal system is a precisely specified framework for constructing symbolic expressions and deriving conclusions according to explicit rules. In logic and mathematics, it typically consists of a language, axioms, and rules of inference. Its defining feature is that the acceptability of a derivation depends on its formal structure rather than unstated intuitions about what its expressions mean. An effectively presented system makes these requirements mechanically checkable. (plato.stanford.edu)

Components and derivations

A formal system distinguishes expressions that can be written from expressions that count as legitimate conclusions. Its usual components are:

• A formal language: symbols and formation rules specifying admissible expressions, or well-formed formulas. In predicate languages, these rules distinguish terms, which represent objects, from formulas, which express conditions or assertions.
• Axioms: formulas accepted as starting points without derivation within the system. An axiom schema specifies a family of axioms by allowing appropriate substitutions.
• Rules of inference: instructions permitting conclusions to be derived from specified premises, subject to any stated restrictions.
• Formal proofs: finite, structured derivations whose steps are justified by axioms, assumptions, or inference rules. A formula proved without undischarged assumptions is a theorem of the system. (builds.openlogicproject.org)

For example, modus ponens permits the inference of $Q$ from $P$ and $P\rightarrow Q$. The letters stand for arbitrary formulas, not particular English sentences. The rule therefore describes a reusable pattern of deductive reasoning. Formation rules instead determine whether expressions such as $P\rightarrow Q$ belong to the language at all; they do not establish those expressions as theorems. (builds.openlogicproject.org)

Different proof architectures organize derivations differently. Axiomatic calculi commonly use sequences of formulas and relatively few inference rules. Natural deduction allows temporary assumptions and rules for discharging them. Sequent calculus works with judgments relating collections of premises to conclusions. Different calculi can characterize the same consequence relation while making different aspects of proof structure explicit. (builds.openlogicproject.org)

Syntax and interpretation

The distinction between syntax and semantics is fundamental. Syntax concerns symbols, formulas, and derivations. Semantics supplies interpretations under which formulas have meanings and truth conditions. In propositional logic, interpretations assign truth values to propositional variables. In first-order logic, an interpretation specifies a domain and assigns meanings to the language’s constants, function symbols, and relation symbols. (builds.openlogicproject.org)

The notation

states that $\varphi$ is formally derivable from assumptions $\Gamma$. By contrast,

states that every interpretation satisfying all members of $\Gamma$ also satisfies $\varphi$. These express syntactic derivability and semantic consequence, respectively. Their correspondence requires proof; it is not built into the notation. (forallx.openlogicproject.org)

A formal system need not have only one intended interpretation. A theory’s models are structures satisfying its axioms, and those structures may differ substantially. Model theory studies such structures and their relationships to theories, whereas proof theory studies derivations and their mathematical properties. Statements about a system—such as a theorem establishing its soundness—belong to its metatheory, rather than automatically being theorems inside that system. (builds.openlogicproject.org)

Soundness, consistency, and completeness

Several properties describe different aspects of a formal system:

Soundness relative to a semantics means that derivability implies semantic consequence: if $\Gamma\vdash\varphi$, then $\Gamma\models\varphi$. A sound calculus does not derive conclusions that fail to follow from its premises under the specified interpretation rules. (forallx.openlogicproject.org)

Consistency, in the usual classical setting, means that no sentence and its negation are both provable. Soundness and consistency are distinct: soundness compares proofs with semantics, while consistency concerns what can be derived. For classical logic, a sound theory with a model is consistent. (plato.stanford.edu)

Semantic completeness means that every semantic consequence is derivable. Gödel’s completeness theorem establishes this correspondence for standard first-order logic. Completeness of a theory, however, means that for every sentence in its language, the theory proves either that sentence or its negation. A complete logical calculus can therefore support an incomplete theory. (forallx.openlogicproject.org)

An axiom is independent of the remaining axioms when it is not derivable from them. Questions of independence concern the strength of particular assumptions, rather than merely the correctness of the underlying inference rules. (builds.openlogicproject.org)

Effective procedures and limitations

An effectively presented system permits its proofs to be checked by an algorithm. Nevertheless, checking a supplied proof is different from deciding whether some proof exists. Effective proof enumeration can eventually discover a theorem’s derivation, but may continue indefinitely when the proposed statement is not a theorem. Classical propositional validity is decidable by finite truth tables; general first-order validity is undecidable. (plato.stanford.edu)

Gödel’s incompleteness theorems establish further limitations. Every consistent, effectively axiomatized theory sufficiently strong to represent elementary arithmetic contains sentences that it neither proves nor refutes. Under the appropriate strength and formalization conditions, it also cannot prove its own standard consistency statement. These results do not apply indiscriminately to every symbolic calculus, nor do they conflict with first-order semantic completeness. (plato.stanford.edu)

Historical development and computerized proofs

Gottlob Frege’s Begriffsschrift of 1879 introduced a formal logical framework for analyzing quantified statements and mathematical proofs. David Hilbert subsequently promoted the study of formalized mathematics through Hilbert’s program, including the search for finitistic consistency proofs. Gödel’s 1931 results imposed major limitations on that program’s original ambitions. (plato.stanford.edu)

Formal systems also underpin proof assistants and formal verification. In Lean, mathematical assertions are represented within type theory, and a kernel checks proof terms against the underlying rules. Acceptance establishes derivability from the definitions and axioms used; it does not independently establish that the formal statement captures its intended informal meaning or that every assumed axiom is justified. (lean-lang.org)