Proof calculus

In mathematical logic, a proof calculus or a proof system is built to prove statements.

Overview

A proof system includes the components:[1]

  • Language: The set of formulas admitted by the system, for example, propositional logic or first-order logic.
  • Rules of inference: List of rules that can be employed to prove theorems from axioms and theorems.
  • Axioms: Formulas in L assumed to be valid. All theorems are derived from axioms.

Usually a given proof calculus encompasses more than a single particular formal system, since many proof calculi are under-determined and can be used for radically different logics. For example, a paradigmatic case is the sequent calculus, which can be used to express the consequence relations of both intuitionistic logic and relevance logic. Thus, loosely speaking, a proof calculus is a template or design pattern, characterized by a certain style of formal inference, that may be specialized to produce specific formal systems, namely by specifying the actual inference rules for such a system. There is no consensus among logicians on how best to define the term.

Examples of proof calculi

The most widely known proof calculi are those classical calculi that are still in widespread use:

Many other proof calculi were, or might have been, seminal, but are not widely used today.

Modern research in logic teems with rival proof calculi:

gollark: GPT-3 apparently already reaches "plausibly human-written if you're not concentrating much", and apparently the architecture scales quite nicely.
gollark: Rust is a neat language.
gollark: Sounds fun.
gollark: It would be interesting if they scaled it up another order of magnitude or two.
gollark: Neural network stuff, and the fancy GPT models, tend to be better, but also far more complex and computationally intensive.

See also

References

  1. Anita Wasilewska. "General proof systems" (PDF).
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.