Formal System

A Formal System is a formal specification consisting of a formal language and a finite set of formal operations (designed to enable systematic manipulation and derivation of statements within a precisely defined framework).

• AKA: Logical System, Formal Framework, Deductive System.
• Context:
  • It can typically specify Formal Symbols through alphabet definitions.
  • It can typically define Well-Formed Formulas through formation rules.
  • It can typically establish Axiom Sets through primitive truth specifications.
  • It can typically provide Inference Rules through derivation procedures.
  • It can typically generate Formal Theorems through proof constructions.
  • ...
  • It can often enable Mechanical Verification through algorithmic procedures.
  • It can often support Consistency Analysis through formal methods.
  • It can often facilitate Completeness Study through metatheoretical investigations.
  • It can often allow Decidability Assessment through computational analysiss.
  • ...
  • It can range from being a Simple Formal System to being a Complex Formal System, depending on its formal rule complexity.
  • It can range from being a Decidable Formal System to being an Undecidable Formal System, depending on its formal computational properties.
  • It can range from being a Complete Formal System to being an Incomplete Formal System, depending on its formal expressive power.
  • It can range from being a Consistent Formal System to being an Inconsistent Formal System, depending on its formal logical properties.
  • ...
  • It can have Closed Form Properties for computational tractability.
  • It can serve as Input to Simulation Tasks for system behavior analysis.
  • It can exhibit varying Certainty Degrees from high certainty to low certainty.
  • It can be paired with Proof Theory to form Logical System Pairs as (|~, S|~).
  • It can be distinguished from Models that instantiate rather than specify.
  • ...
• Examples:
  • Mathematical Formal Systems, such as:
    • Arithmetic Formal Systems, such as:
      • Peano Arithmetic, with natural number axioms.
      • Robinson Arithmetic, without induction schema.
    • Set Formal Systems, such as:
      • Zermelo-Fraenkel Set Theory, with set construction axioms.
      • Von Neumann-Bernays-Gödel Set Theory, allowing proper classes.
    • Algebraic Formal Systems, such as:
      • Group Theory, with group operation axioms.
      • Ring Theory, with ring structure axioms.
  • Logic Formal Systems, such as:
    • Deductive Logic Systems, such as:
      • Boolean Logic System, with binary truth values.
      • Propositional Logic System, manipulating propositional formulas.
      • First-Order Logic System, including quantifier symbols.
    • Modal Logic Systems, with necessity and possibility operators.
    • Temporal Logic Systems, with temporal operators.
  • Natural Language Formal Systems, such as:
    • HPSG (Head-Driven Phrase Structure Grammar), with feature structures.
    • Generative Grammar, with transformation rules.
    • Categorial Grammar, with type-logical rules.
  • Computational Formal Systems, such as:
    • Lambda Calculus, with function abstraction rules.
    • Turing Machine, with state transition rules.
    • Relational Calculus, with relational operations.
  • Proof-Theoretic Formal Systems, such as:
    • Natural Deduction Systems, with introduction and elimination rules.
    • Sequent Calculus, with sequent manipulation rules.
    • Hilbert Systems, with axiom schemas.
  • ...
• Counter-Examples:
  • Informal Theory, which lacks precise formal specifications.
  • Model, which instantiates rather than specifies formal rules.
  • Natural Language, which lacks formal operations and precise syntax.
  • Empirical Theory, which relies on observation rather than formal derivation.
  • Heuristic System, which uses approximate methods rather than formal rules.
• See: Formal Model, Scientific Theory, Mathematical Theorem, Logical Consequence Relation, Proof Theory, Formal Language, Inference Rule, Axiom System, Formal Mathematical System, Model Theory.

---

---

References

2018

• (Wikipedia, 2018) ⇒ https://en.wikipedia.org/wiki/Formal_system Retrieved:2018-11-3.
  • A formal system is the name of a logic system usually defined in the mathematical way. Logical calculus is carried out in the system. It can represent a well-defined system of abstract thought. Spinoza's Ethics imitates the form of Euclid's Elements. Spinoza employed Euclidean elements such as “axioms" or “primitive truths", rules of inferences, etc., so that a calculus can be built using these.

    Some theoristsuse the term formalism as a rough synonym for formal system, but the term is also used to refer to a particular styleof notation, for example, Paul Dirac's bra–ket notation.

1994

• (Gabbay, 1994) ⇒ Dov M. Gabbay. (1994). “What is a Logical System?." Oxford University Press. ISBN:0198538596
  • The central role which proof theoretical methodologies play in generating logics compels us to put forward the view that a logical system is a pair (|~, S_|~), where S_|~ is a proof theory for |~. In other words, we are saying that it is not enough to know |~ to 'understand' the logic, but we must also know how it is presented (i.e. S_|~).
  • A logical system is a pair (|~, S_|~), where |~ is a structured-consequence, and S_|~ is an algorithmic system for it.

---