この 方面 で の 重要 な 成果 として は 、 ゲンツェン による LK の 基本 定理 、 すなわち 「 式 S が LK で provable なら ば 、 S は LK で 三段論法 なし でも provable で ある 」 が あげ られる 。

この 定理 は 「 対偶 や 背理法 の よう な 間接 証明 法 を 用い て 証明 できる 命題 は 、 間接 証明 法 を 用い なく て も 証明 できる 」 という よう な こと を 一般 化 し た 、 論理 について 成り立つ 非常 に 美しい 法則 で ある 。

基本 定理 の 応用 として は 、 命題 論理 ・ 述語 論理 の 無 矛盾 性 、 そして 命題 論理 の 決定 可能 性 が ある 。

この 方面 で の 重要 な 成果 として は ゲーデル の 完全 性 定理 が あげ られる 。

命題 論理 は 、 （ 内部 的 に 無 矛盾 性 が 証明 さ れ た という 意味 で ） 完全 に 解決 さ れ た 数少ない 数学 の 分野 の 一つ で あり 、 命題 論理 において 任意 の 定理 は 真 で あり 、 任意 の 真 なる 言明 が 証明 可能 で ある （ この 事実 と ゲーデル の 不完全性 定理 から 、 命題 論理 が 自然 数 論 を 構成 する に は 不十分 で ある こと を 知る の は 簡単 で ある ） 。

ド ・ モルガン の 法則 （ ド ・ モルガン の ほう そく 、 De Morgan ' s laws ） と は 、 数理 論理 学 や 集合 論 において 、 論理 積 （ 集合 の 積 、 共通 部分 ） と 論理 和 （ 集合 の 和 、 合併 ） 、 否定 （ 補 集合 ） の 間 に 成り立つ 関係 を 記述 する 定理 で あり 、 数学 者 の オーガスタス・ド・モルガン に ちなん で この 名前 が つい て いる 。

微分 積分 学 は 、 局所 的 な 変化 を 捉える 微分 と 局所 的 な 量 の 大域 的 な 集積 を 扱う 積分 の 二 本 の 柱 から なり 、 分野 として の 範囲 を 確定 する の は 難しい が 、 大体 多 変数 実数 値 関数 の 微分 と 積分 に 関わる 事柄 （ 逆 関数 定理 や ベクトル 解析 も ） を 含ん で いる 。

（ 微分 積分 学 の 基本 定理 ） 古代 に も いくつ か の 積分 法 の アイデア は 存在 し た が 、 厳密 あるいは 体系 的 な 方法 で それら の アイデア を 発展 さ せよ う という 動き は 見 られ ない 。

12 世紀 の インド の 数学 者 バー スカラ 2 世 は 極微 の 変化 を 表す 微分 法 の 先駆け と なる 手法 を 考案 し 、 ロル の 定理 の 原始 的 形式 も 記述 し て いる 。

この 統合 を 行っ た の が ジョン・ウォリス 、 アイザック ・ バロー 、 ジェームズ ・ グレゴリー で あり 、 バロー と グレゴリー は 1675 年 ごろ 微分 積分 学 の 基本 定理 の 第 2 定理 を 証明 し た 。

ニュートン の 時代 まで に は 、 微分 積分 学 の 基本 定理 は 既に 知ら れ て い た 。

教員 として の 仕事 （ 数学 に 国語 に 地理 、 そして 体操 まで 教え た ） を し ながら 、 ニールス・アーベル の 定理 と カール ・ グスタフ・ヤコブ・ヤコビ の 二 重 周期 関数 の 研究 の 統合 を 目指し た 。

完全 数 と メルセンヌ 数 の 関係 、 素数 が 無限 に 存在 する こと 、 因数 分解 について の ユークリッド の 補題 （ ここ から 素因数 分解 の 一意 性 について の 算術 の 基本 定理 が 導か れる ） 、 2 つ の 数 の 最大公約数 を 捜す ユークリッド の 互除 法 など が 含ま れる 。

ただし 、 「 中間 値 の 定理 」 の 中間 値 は この 意味 で は ない 。

四 色 定理 （ よん し ょくていり / し し ょくていり ） と は 、 いかなる 地図 も 、 隣接 する 領域 が 異なる 色 に なる よう に 塗る に は 4 色 あれ ば 十分 だ という 定理 で ある 。

四 色 定理 の 示す よう に 領域 の 塗り 分け が 有限 の 色 数 で 必ず 可能 と なる の は 平面 （ 二 次元 ） 以下 の 次元 まで で あり 、 三 次元 以上 で は 領域 の 取り 方 次第 で いくらでも 色 数 が 必要 と なっ て しまう よう に なる 。

1976 年 に ケネス・アッペル ( Kenneth Appel ) と ヴォルフガング・ハーケン ( Wolfgang Haken ) は 、 ヘーシュ ( Heinrich Heesch ) により 考案 さ れ た 「 放電 」 と 呼ば れる 手続き を 改良 し 、 コンピュータ を 利用 し て 約 2000 個 の （ 後 に 1400 個 あまりに 整理 さ れ た ） 可 約 な 配置 から なる 不可避 集合 を 見出し 、 四 色 定理 を 証明 する に 至っ た 。

更に 、 2004 年 に は ジョルジュ・ゴンティエ ( Georges Gonthier ) が 定理 証明 支援 系 言語 で ある Coq を 用い て 、 より シンプル な 証明 を 行っ た 。

四 色 定理 は 実用 的 に は 地図 作製 だけ で なく 、 携帯 電話 の 基地 局 配置 に も 応用 さ れ て いる 。

四 色 定理 の 証明 法 は 次 の 2 段階 に 分け られる 。