形式的論理体系
数理論理学は、形式的な論理体系を用いて表現される数学的概念を扱うことを核としている。これらの論理体系は、細部が異なるものの、固定された形式言語による表現のみを考慮するという共通の性質を持っています。現在最も広く研究されているのは、命題論理と一階論理である。これは、数学の基礎に適用できることと、証明論的な特性を持つことが理由である。また、二階論理や無限論理のような強力な古典論理や、直観主義論理のような非古典論理も研究されています。

一階建ての論理
主な記事 一階の論理
一階論理とは、論理学の形式的な体系の一つである。一階論理の構文は、有限の式を整形したものだけを含み、意味論は、すべての量詞を固定の談話領域に限定することで特徴づけられる。
形式論理学の初期の成果として、一階論理の限界が指摘された。Löwenheim-Skolemの定理（1919年）は、可算一階言語の文の集合が無限のモデルを持つ場合、無限のカーディナリティを持つモデルを少なくとも1つ持つことを示した。これにより、自然数や実数などの無限構造を、一次公理の集合が同型まで特徴づけることは不可能であることが示されました。初期の基礎研究では、数学のすべての部分について公理的な理論を作ることを目標としていたので、この限界は特に厳しかった。
ゲーデルの完全性定理は、一階論理における論理的帰結の意味的定義と構文的定義の同等性を確立したものです。これは、ある文が、ある公理を満たすすべてのモデルにおいて真であるならば、その公理からその文を有限に演繹することができるはずだ、というものです。このコンパクトネス定理は、ゲーデルの完全性定理の証明の中に登場したものですが、論理学者がその重要性を理解し、日常的に適用するようになるまでには、長い年月を要しました。これは、「文の集合がモデルを持つのは、すべての有限部分集合がモデルを持つ場合に限られる」というもので、言い換えれば、「無矛盾な式の集合は、有限の無矛盾部分集合を持たなければならない」ということになります。この完全性定理とコンパクト性定理は、一階論理の論理的帰結の高度な分析やモデル理論の発展を可能にし、数学において一階論理が重要な位置を占めるようになった大きな理由となっています。
ゲーデルの不完全性定理は、第一階の公理化にさらなる限界をもたらします。第1の不完全性定理は、算術を解釈することができる一貫した有効に与えられた（以下に定義する）論理体系において、（自然数について成立するという意味で）真ではあるが、その論理体系の中では証明できない（その論理体系と矛盾しない非標準的な算術のモデルでは実際に失敗する可能性がある）文が存在するというものです。たとえば、ピアノ公理を表現できるすべての論理システムにおいて、ゲーデル文は自然数について成立しますが、証明することはできません。
ここでは、論理体系の言語で書かれた任意の式が与えられたときに、その式が公理であるかどうかを判断できる場合に、論理体系が有効に与えられているといい、ピーノ公理を表現できるものを "sufficiently strong "といいます。第一次論理に適用すると、第一不完全性定理は、十分に強く、一貫性のある、有効な第一次理論は、要素的に等価ではないモデルを持つことを意味し、レーウェンハイム・スコレム定理で確立された制限よりも強い制限となります。第2の不完全性定理は、十分に強く、一貫性のある、有効な算術の公理系は、それ自身の一貫性を証明できないというもので、これはヒルベルトのプログラムに到達できないことを示していると解釈されています。

その他の古典的論理
一階論理以外にも様々な論理が研究されています。その中には、無限の情報を持つことができる無限論理や、集合論の一部を意味論に直接取り込んだ高階論理などがあります。
最もよく研究されているのは、無限論理です。この論理では、量詞は一階論理のように有限の深さまでしか入れ子にできませんが、数式はその中に有限または可算無限の接続詞や分離詞を持つことができます。したがって、例えば、ある物体が整数であることを、次のような式を使って言うことができます。

高階論理では、談話領域の要素だけでなく、談話領域の部分集合、そのような部分集合の集合、その他の高階の対象物を数量化することができる。意味論は、各高次タイプの量化詞のために個別のドメインを持つのではなく、量化詞が適切なタイプのすべてのオブジェクトに及ぶように定義されている。フレーゲの論理など、一階論理が開発される以前に研究されていた論理は、同様に集合論的な側面を持っていました。高階論理は表現力が高く、自然数などの構造を完全に公理化することができますが、一階論理の完全性定理やコンパクト性定理の類似性を満たさないため、証明論的な分析には向いていません。
もう一つのタイプの論理は、固定小数点論理で、原始再帰関数に書くような帰納的な定義が可能です。
一階論理の拡張を正式に定義することができます。この概念は、ある基本的な方法で一階論理のように振る舞うため、このセクションのすべての論理を包含しますが、一般的にすべての論理を包含するわけではありません（例えば、直観主義論理、モーダル論理、ファジー論理は包含しません）。
リンドストロームの定理は、コンパクトネス定理と下向ローウェンハイム-スコレム定理の両方を満たす一階論理の唯一の拡張が一階論理であることを意味しています。

非古典的・様相的論理
主な記事 非古典論理
モーダル論理には、特定の式が真であるだけでなく必然的に真であることを示す演算子など、モーダル演算子が追加されている。モード論理は数学の公理化にはあまり用いられないが、一階の証明可能性や集合論的な強制力の性質を研究するのに用いられている。
直観主義論理は、HeytingがBrouwerの直観主義プログラムを研究するために開発したもので、Brouwer自身は形式化を避けていました。直観主義論理は特に、各文が真であるか、その否定が真であるかのどちらかであるとする排除中間の法則を含まない。クレーネの直観主義論理の証明理論の研究は、直観主義的な証明から建設的な情報が復元できることを示した。例えば、直観主義的な算術における証明可能な全関数は計算可能であるが、これはPeano算術のような古典的な算術理論では当てはまらない。

代数的な論理
代数論理学は、抽象代数の手法を用いて形式論理学の意味論を研究する学問です。古典的命題論理ではブール代数を用いて真理値を表現し、直観的命題論理ではヘイティング代数を用いて真理値を表現するのが基本的な例である。また、一階論理や高階論理のような強い論理は、円筒代数などのより複雑な代数構造を用いて研究されます。