グッドスタイン の 定理 は （ ペアノ 算術 を 逸脱 する 技法 を 用い て ） 以下 の よう に し て 証明 できる 。

グッドスタイン の 定理 に関する この 証明 は かなり 易しい が 、 一方 この 定理 が ペアノ 算術 に は 含ま れ ない と 述べる 「 Kirby - Paris の 定理 」 は テクニカル で はるか に 難しい 。

そこで Kirby は グッドスタイン の 定理 から ゲンツェン の 定理 ( en ) が 導か れる こと を 示し た 。

つまり 、 グッドスタイン の 定理 は ε 0 まで の 帰納 法 の 代わり と なる の で ある 。

グッドスタイン の 定理 を 応用 する と 、 全体 関数 で あっ て 、 かつ 全体 関数 で ある こと が ペアノ 算術 で は 証明 でき ない よう な 計算 可能 関数 を 構成 できる 。

ディリクレ の ディオファントス 近似 定理 (- きんじ て いり ) は ディリクレ が 証明 し た 実数 の 有理数 による 近似 について の 定理 で 、 単に ディリクレ の 定理 と 呼ば れる こと も ある 。

ディリクレ の ディオファントス 近似 定理 は 次 の よう な 定理 で ある 。

この 定理 の 証明 は 鳩 の 巣 原理 に よる 。

場合 によって は 、 この 定理 から 直ちに 導か れる 次 の 結果 を 指す こと も ある 。

この 系 は 、 ツゥエ・ジーゲル・ロス の 定理 が 、 代数 的 数 の 有理数 で の 近似 の 下界 は 2 を 超え て 2 + ε へ の 改善 は でき ない という 意味 で 、 最良 で ある こと を 示し て いる 。

一般 に HOL 、 ACL 2 、 Isabelle 、 Coq といった 定理 証明 ソフトウェア を 使い 、 システム に関して 形式 的 な 推論 を 行う 。

解析 学 の 分野 で は 「 ボルツァーノ ＝ ワイエルシュトラス の 定理 」 など 、 彼 の 名 が 冠さ れる 定理 を いくつ か 残し て いる 。

1981 年 に 、 グッドスタイン の 定理 にまつわる 研究 によって 有名 に なっ た 。

ネーター の 定理 （ ネーター の て いり 、 Noether ' s theorem ） は 、 系 に 連続 的 な 対称 性 が ある 場合 は それ に 対応 する 保存 則 が 存在 する 、 と 述べる 定理 で ある 。

解析 力学 や 場 の 理論 における 重要 な 定理 で ある 。

ネーター の 定理 は 、 ラグランジアン の 変数 に対する 連続 的 な 変換 が 系 の 対称 性 に なっ て いる 場合 に 、 対称 性 の 下 で の 作用 の 変 分 ( ゼロ に 等しい ) が 或 る 保存 量 の 時間 について の 全 微分 に なっ て いる 事 を 言っ て いる 。

IPL の 最初 の 利用 例 は 、 『 プリンキピア・マテマティカ 』 （ バートランド・ラッセル と アルフレッド ・ ノース ・ ホワイト ヘッド の 労作 ） の 中 の 定理 を 計算 によって 証明 する デモンストレーション で あっ た 。

例えば 、 定理 証明 、 幾何 学 問題 、 チェス の プレイ など で ある 。

アルハゼン の 定理 と は 、 円 と 交わる 2 つ の 直線 が ある 1 点 で 交わっ て でき た 角 の 大き さ に関する 定理 で あり 、 13 世紀 の アラビア の 科学 者 イブン・アル・ハイサム （ ラテン 名 アルハゼン ） によって 発見 さ れ た 。

自動 化 技術 は 2 つ に 分類 さ れる : 一部 の 自動 定理 証明 は 人間 の 補助 なし に は 機能 せ ず 、 追跡 す べき 特性 を 人間 が 指定 し て やる 必要 が ある 。