Metalogic

Metalogic is the metatheory of logic. Whereas logic studies how logical systems can be used to construct valid and sound arguments, metalogic studies the properties of logical systems.^[1] Logic concerns the truths that may be derived using a logical system; metalogic concerns the truths that may be derived about the languages and systems that are used to express truths.^[2]

The basic objects of metalogical study are formal languages, formal systems, and their interpretations. The study of interpretation of formal systems is the branch of mathematical logic that is known as model theory, and the study of deductive systems is the branch that is known as proof theory.

History[edit]

Metalogical questions have been asked since the time of Aristotle.^[4] However, it was only with the rise of formal languages in the late 19th and early 20th century that investigations into the foundations of logic began to flourish. In 1904, David Hilbert observed that in investigating the foundations of mathematics that logical notions are presupposed, and therefore a simultaneous account of metalogical and metamathematical principles was required. Today, metalogic and metamathematics are largely synonymous with each other, and both have been substantially subsumed by mathematical logic in academia. A possible alternate, less mathematical model may be found in the writings of Charles Sanders Peirce and other semioticians.

Proof of the of the power set of the natural numbers (Cantor's theorem 1891)

uncountability

(Leopold Löwenheim 1915 and Thoralf Skolem 1919)

Löwenheim–Skolem theorem

Proof of the consistency of truth-functional (Emil Post 1920)

propositional logic

Proof of the semantic completeness of truth-functional propositional logic ( 1918),^[5] (Emil Post 1920)^[2]

Paul Bernays

Proof of the syntactic completeness of truth-functional propositional logic (Emil Post 1920)

[2]

Proof of the decidability of truth-functional propositional logic (Emil Post 1920)

[2]

Proof of the consistency of first-order (Leopold Löwenheim 1915)

monadic predicate logic

Proof of the semantic completeness of first-order monadic predicate logic (Leopold Löwenheim 1915)

Proof of the decidability of first-order monadic predicate logic (Leopold Löwenheim 1915)

Proof of the consistency of first-order predicate logic ( and Wilhelm Ackermann 1928)

David Hilbert

Proof of the semantic completeness of first-order (Gödel's completeness theorem 1930)

predicate logic

Proof of the for the sequent calculus (Gentzen's Hauptsatz 1934)

cut-elimination theorem

Proof of the undecidability of first-order predicate logic ( 1936)

Church's theorem

1931

Gödel's first incompleteness theorem

1931

Gödel's second incompleteness theorem

(Gödel and Tarski in the 1930s)

Tarski's undefinability theorem

Results in metalogic consist of such things as formal proofs demonstrating the consistency, completeness, and decidability of particular formal systems.

Major results in metalogic include: