Formal systems are the backbone of mathematical logic, providing a structured framework for reasoning. They consist of a language, axioms, and inference rules that allow for precise and unambiguous derivation of theorems from initial assumptions.

Proofs and derivations are the heart of formal systems, demonstrating the logical validity of statements. Through step-by-step reasoning, they show how conclusions follow from premises, forming the basis for establishing mathematical truths within the system.

Formal Systems

Components of Formal Systems

• Formal language consists of an alphabet of symbols and a set of formation rules that define well-formed formulas (wffs)
• Axioms are the starting assumptions or premises of the formal system
  • Serve as the foundation for deriving other statements
  • Cannot be proven within the system itself
• Inference rules specify how new well-formed formulas can be derived from existing ones
  • Allow for the generation of theorems from the axioms and previously derived statements
  • Examples include modus ponens ($P \rightarrow Q, P \vdash Q$) and hypothetical syllogism ($P \rightarrow Q, Q \rightarrow R \vdash P \rightarrow R$)

Properties of Formal Systems

• Formal systems aim to be precise, unambiguous, and mechanically checkable
  • Removes potential for misinterpretation or ambiguity in reasoning
• The choice of axioms and inference rules determines the specific formal system
  • Different systems can be constructed for various areas of mathematics and logic (propositional logic, first-order logic, Peano arithmetic)
• Formal systems provide a rigorous framework for mathematical and logical reasoning
  • Enable the systematic derivation of theorems from a set of initial assumptions

Proofs and Derivations

Formal Proofs

• A formal proof is a sequence of well-formed formulas, each of which is either an axiom or derived from previous formulas using inference rules
  • Demonstrates the logical validity of a statement within the formal system
• The final formula in the proof sequence is the theorem being proven
  • Represents a logically necessary consequence of the axioms and inference rules
• Formal proofs are constructed using a step-by-step process, justifying each step with the appropriate axiom or inference rule

Derivations

• A derivation is a sequence of well-formed formulas that leads from the premises to the conclusion
  • Shows how the conclusion can be obtained from the premises using the inference rules of the formal system
• Derivations are often represented using a proof tree or a sequence of lines, with each line justified by the premises or previous lines
  • Helps to visualize the logical structure of the argument
• The existence of a derivation for a statement demonstrates its provability within the formal system

Theorems

• A theorem is a well-formed formula that can be derived from the axioms using the inference rules of the formal system
  • Represents a logically necessary truth within the system
• Theorems are proven through formal proofs or derivations
  • The proof provides a convincing argument for the truth of the theorem based on the axioms and rules of the system
• Examples of theorems include the law of excluded middle ($P \lor \neg P$) in propositional logic and the fundamental theorem of arithmetic in number theory

Metatheory

Metatheorems

• Metatheorems are statements about the properties of a formal system itself
  • Proven using meta-reasoning, which is reasoning about the formal system from an external perspective
• Metatheorems make assertions about the consistency, completeness, or other characteristics of the formal system
  • Help to establish the reliability and limitations of the system
• Examples of metatheorems include Gödel's completeness theorem for first-order logic and the undecidability of the halting problem in computability theory

Soundness and Completeness

• Soundness is a metatheoretical property that ensures every theorem provable in the formal system is actually true
  • If a statement can be derived using the inference rules, it is guaranteed to be a valid consequence of the axioms
  • Soundness prevents the derivation of false statements within the system
• Completeness is a metatheoretical property that ensures every true statement expressible in the formal language is provable using the axioms and inference rules
  • If a statement is a logical consequence of the axioms, there exists a formal proof for it within the system
  • Completeness guarantees that all valid statements can be derived

Significance of Metatheory

• Metatheory allows for the study of the properties and limitations of formal systems
  • Helps to establish the reliability, consistency, and expressive power of the system
• Metatheoretical results provide insights into the foundations of mathematics and logic
  • Shed light on the nature of mathematical truth and the capabilities of formal reasoning
• Metatheory plays a crucial role in areas such as proof theory, model theory, and computability theory
  • Enables the analysis of the strengths and weaknesses of different formal systems and their applications