ロゴ
ユニオンペディア
コミュニケーション
Google Play で手に入れよう
新しい! あなたのAndroid™デバイスでユニオンペディアをダウンロードしてください!
無料
ブラウザよりも高速アクセス!
 

一階述語論理

索引 一階述語論理

一階述語論理(いっかいじゅつごろんり、first-order predicate logic)とは、個体の量化のみを許す述語論理 (predicate logic) である。述語論理とは、数理論理学における論理の数学的モデルの一つであり、命題論理を拡張したものである。個体の量化に加えて述語や関数の量化を許す述語論理を二階述語論理(にかいじゅつごろんり、second-order predicate logic)と呼ぶ。それにさらなる一般化を加えた述語論理を高階述語論理(こうかいじゅつごろんり、higher-order predicate logic)という。本項では主に一階述語論理について解説する。二階述語論理や高階述語論理についての詳細は「二階述語論理」「高階述語論理」を参照。.

49 関係: 停止性問題名前妥当性存在記号中置記法帰納的可算集合二階述語論理二項関係ペアノの公理ポーランド記法モーダスポネンストートロジーダフィット・ヒルベルト命題論理アラン・チューリングアリティアルフレト・タルスキアルゴリズムアロンゾ・チャーチゲルハルト・ゲンツェンゲーデルの完全性定理ゲーデルの不完全性定理ゲーデル数コンパクト性定理シークエント計算写像全称記号公理的集合論無限論理高階述語論理論理的帰結議論領域述語論理部分集合関係代数 (数学)量化自然演繹自然数集合Prolog推論規則様相論理決定可能性濃度 (数学)有限集合数学的直観主義数理論理学整数普遍例化

停止性問題

計算可能性理論において停止(性)問題(ていしせいもんだい・ていしもんだい、halting problem)は、あるチューリング機械(≒コンピュータプログラム・アルゴリズム)が、そのテープのある初期状態(≒入力)に対し、有限時間で停止するか、という問題。アラン・チューリングが1936年、停止性問題を解くチューリング機械が存在しない事をある種の対角線論法のようにして証明した。すなわち、そのようなチューリング機械の存在を仮定すると「自身が停止すると判定したならば無限ループを行い、停止しないと判定したならば停止する」ような別のチューリング機械が構成でき、矛盾となる。.

新しい!!: 一階述語論理と停止性問題 · 続きを見る »

名前

名前(なまえ、όνομα、nomen、name)とは、物や人物に与えられた言葉のことで、対象を呼んだりする際に使われる。名称、あるいは単に名とも言う。名前をつけることを「名付ける」「命名(めいめい)する」という。名前として使われる言葉を名詞という。 多くの場合、名前とは人名である。また、人名のうち、家族を表す姓(名字)でない方、個人を識別する名を指すことも多い。ただし、名ではなく姓を指して「名前」と呼ぶこともある。.

新しい!!: 一階述語論理と名前 · 続きを見る »

妥当性

妥当性(Validity)は、演繹的論証が持つ論理的特性であるが、一般に任意の文に対して使われる(ここでいう文とは、真か偽かという真理値を持つものをいう)。ここでは、論証を文の集まりとし、そのうちの1つの文が結論で残りは前提であるとする。前提とは、結論が(おそらく)真であると示す根拠である。 論証の結論が「確かに」真であるとされている場合、その論証は演繹的である。結論が「おそらく」真であるとされている論証は帰納的であると言われる。ある論証が妥当であるとは、結論が正しく前提から導き出されることを意味する。すなわち、妥当な演繹的論証であれば、真の前提から偽の結論が導き出されることはあり得ない。(一方、前提に偽がある場合には、真・偽どちらの結論も導き出されうる。) 次のような定義が一般的である。.

新しい!!: 一階述語論理と妥当性 · 続きを見る »

存在記号

存在記号(そんざいきごう、existential quantifier)とは、数理論理学(特に述語論理)において、少なくとも1つのメンバーが述語の特性や関係を満たすことを表す記号である。通常「∃」と表記され、存在量化子(そんざいりょうかし)、存在限量子(そんざいげんりょうし)、存在限定子(そんざいげんていし)などとも呼ばれる。 これとは対照的に全称記号は、何かが常に真であることを示す。.

新しい!!: 一階述語論理と存在記号 · 続きを見る »

中置記法

中置記法(ちゅうちきほう、infix notation)とは、数式やプログラムを記述する方法(記法)の一種。演算子を操作対象の中間に記述することから、このように呼ばれる。 その他の記法として、演算子を操作対象の前(左)に記述する前置記法(ポーランド記法)、演算子を操作対象の後(右)に記述する後置記法(逆ポーランド記法)がある。 四則演算など初歩的な算術においては、もっぱら中置記法が多用されている。.

新しい!!: 一階述語論理と中置記法 · 続きを見る »

帰納的可算集合

帰納的可算集合(きのうてきかさんしゅうごう、Recursively enumerable set)は、計算理論または再帰理論におけるある種の集合に付与された名前。自然数の集合 S について以下が成り立つ場合、その集合を指して帰納的可算、計算可枚挙、半決定可能、証明可能、チューリング-認識可能などと称する。.

新しい!!: 一階述語論理と帰納的可算集合 · 続きを見る »

二階述語論理

二階述語論理(にかいじゅつごろんり、second-order predicate logic)あるいは単に二階論理(にかいろんり、second-order logic)は、一階述語論理を拡張した論理体系であり、一階述語論理自体も命題論理を拡張したものである。二階述語論理もさらに高階述語論理や型理論に拡張される。 一階述語論理と同様に議論領域(ドメイン)の考え方を使う。ドメインとは、量化可能な個々の元の集合である。一階述語論理では、そのドメインの個々の元が変項の値となり、量化される。例えば、一階の論理式 ∀x (x ≠ x + 1) では、変項 x は任意の個体を表す。二階述語論理は個体の集合を変項の値とし、量化することができる。例えば、二階の論理式 ∀S ∀x (x ∈ S ∨ x ∉ S) は、個体の全ての集合 S と全ての個体 x について、x が S に属するか、あるいは属さないかのどちらかであるということを主張している。最も一般化された二階述語論理は関数の量化をする変項も含んでいる(詳しくは後述)。.

新しい!!: 一階述語論理と二階述語論理 · 続きを見る »

二項関係

数学において、二項関係(にこうかんけい、binary relation)あるいは二変数関係 (dyadic relation, 2-place relation) は、集合 の元からなる順序対のあつまりである。別な言い方をすれば、直積集合 の部分集合を、集合 上の二項関係と呼ぶ。あるいはもっと一般に、二つの集合 に対して、 と との間の二項関係とは、直積 の部分集合のことをいう。 二項関係の一つの例は素数全体の成す集合 と整数全体の成す集合 の間の整除関係である。この整除関係では任意の素数 は、 の倍数である任意の整数 に関係を持ち、倍数でない整数には関係しないものとして扱われる。例えば、素数 が関係を持つ整数には などが含まれるが や は含まれない。同様に素数 が関係する整数として などが挙げられるが、 や はそうではない。 二項関係は数学のさまざまな分野で用いられ、不等関係、恒等関係、算術の整除関係、初等幾何学の合同関係、グラフ理論の隣接関係、線型代数学の直交関係などのさまざまな概念が二項関係として定式化することができる。また、写像の概念を特別な種類の二項関係として定義することもできる。二項関係は計算機科学においても重用される。 二項関係はn-項関係 (各 -番目の成分が関係の -番目の始集合 からとられているようなn-組からなる集合)で とした特別の場合である。 ある種の公理的集合論では(集合の一般化としての)類の上の関係を考えることができる。このような拡張は、集合論における元の帰属関係や包含関係の概念(に限った話ではないが)のモデル化を、ラッセルの逆理のような論理矛盾に陥らずに行うために必要である。.

新しい!!: 一階述語論理と二項関係 · 続きを見る »

ペアノの公理

ペアノの公理(ペアノのこうり、Peano axioms) とは、自然数全体を公理化したものである。1891年に、ジュゼッペ・ペアノによって定義された。.

新しい!!: 一階述語論理とペアノの公理 · 続きを見る »

ポーランド記法

ポーランド記法(ポーランドきほう、Polish Notation)とは、数式やプログラムを記述する方法(記法)の一種。演算子(オペレータ)を被演算子(オペランド)の前(左)に記述することから、前置記法(ぜんちきほう、prefix notation)とも言う。 その他の記法として、演算子を被演算子の中間に記述する中置記法、後(右)に記述する後置記法(逆ポーランド記法)がある。 名称の由来は、ポーランド人の論理学者ヤン・ウカシェヴィチ (Jan Łukasiewicz) が考案したことによる。.

新しい!!: 一階述語論理とポーランド記法 · 続きを見る »

モーダスポネンス

モーダスポネンス(ラテン語: 、MP)とは、論理学における妥当で単純な「論証」である。ラテン語で「肯定によって肯定する様式」の意。前件肯定 または分離規則 とも呼ぶ。.

新しい!!: 一階述語論理とモーダスポネンス · 続きを見る »

トートロジー

トートロジー(英語:tautology, ギリシャ語:ταυτολογία, 語源はギリシャ語で「同じ」を意味するταυτοから)とは、ある事柄を述べるのに、同義語または類語または同語を反復させる修辞技法のこと。同義語反復、類語反復、同語反復等と訳される。関連した概念に冗語があり、しばしば同じ意味で使われることもある。また、撞着語法はトートロジーの反対の技法である。 A Dictionary of Modern English Usage の定義では「同じ事を二度言う」とされ、スタイルの誤りと見なされることが多い。.

新しい!!: 一階述語論理とトートロジー · 続きを見る »

ダフィット・ヒルベルト

ーニヒスベルクにて私講師を務めていた頃(1886年) ヒルベルトの墓碑。「我々は知らねばならない、我々は知るだろう」と記されている。 ダフィット・ヒルベルト(David Hilbert,, 1862年1月23日 - 1943年2月14日)は、ドイツの数学者。「現代数学の父」と呼ばれる。名はダヴィット,ダヴィド、ダーフィットなどとも表記される。.

新しい!!: 一階述語論理とダフィット・ヒルベルト · 続きを見る »

命題論理

命題論理(propositional logic)とは、数理論理学(記号論理学)の基礎的な一部門であり、命題全体を1つの記号に置き換えて単純化し、論理演算を表す記号(論理記号・論理演算子)を用いて、その命題(記号)間の結合パターンを表現・研究・把握することを目的とした分野のこと。ブール論理はブール代数で形式化され2値の意味論を与えられた命題論理とみることができる。 命題を1つの記号で大まかに置き換える命題論理に対して、命題の述語(P)と主語(S)を、関数のF(x)のように別記号で表現し、更に量化子で主語(S)の数・量・範囲もいくらか表現し分けることを可能にした、すなわちより詳細に命題の内部構造を表現できるようにしたものを、述語論理と呼ぶ。.

新しい!!: 一階述語論理と命題論理 · 続きを見る »

アラン・チューリング

アラン・マシスン・チューリング(Alan Mathieson Turing、〔テュァリング〕, 1912年6月23日 - 1954年6月7日)はイギリスの数学者、論理学者、暗号解読者、コンピュータ科学者。.

新しい!!: 一階述語論理とアラン・チューリング · 続きを見る »

アリティ

アリティ (arity) とは、代数学、論理学、計算機科学などにおいて、関数や算法(演算) が取る引数(オペランド)の個数を意味する用語である。 項数のような訳語が当てられる場合もあるが、arityと英単語のまま用いられることも多い。 複合語としてならば、「変数」(例えば二変数函数、多変数函数)や単に「項」(二項演算、多項関係など)あるいはまた(不定元の数という意味で)「(-)元」(例えば二元連立一次方程式)などはアリティに言及する訳語として存外よく用いられるものである。(しかし同じ語でも、例えば数列や多項式などに用いられる「項」や「項数」はアリティではなく "term" に関する言及である。).

新しい!!: 一階述語論理とアリティ · 続きを見る »

アルフレト・タルスキ

アルフレト・タルスキ(Alfred Tarski, 1901年1月14日 - 1983年10月26日)はポーランドおよびアメリカの数学者・論理学者。彼の生年を1902年とする記述も散見されるが、これは誤りである。 アリストテレス、クルト・ゲーデル、ゴットロープ・フレーゲとともに、「四人の偉大な論理学者」の一人として数えられる。また、彼の名前は「バナッハ=タルスキーの定理」などで知られる。.

新しい!!: 一階述語論理とアルフレト・タルスキ · 続きを見る »

アルゴリズム

フローチャートはアルゴリズムの視覚的表現としてよく使われる。これはランプがつかない時のフローチャート。 アルゴリズム(algorithm )とは、数学、コンピューティング、言語学、あるいは関連する分野において、問題を解くための手順を定式化した形で表現したものを言う。算法と訳されることもある。 「問題」はその「解」を持っているが、アルゴリズムは正しくその解を得るための具体的手順および根拠を与える。さらに多くの場合において効率性が重要となる。 コンピュータにアルゴリズムをソフトウェア的に実装するものがコンピュータプログラムである。人間より速く大量に計算ができるのがコンピュータの強みであるが、その計算が正しく効率的であるためには、正しく効率的なアルゴリズムに基づいたものでなければならない。.

新しい!!: 一階述語論理とアルゴリズム · 続きを見る »

アロンゾ・チャーチ

アロンゾ・チャーチ(Alonzo Church, 1903年6月14日 - 1995年8月11日)はアメリカの論理学者、数学者。ラムダ計算の創案者、「チャーチ=チューリングのテーゼ」の提唱者として知られる。.

新しい!!: 一階述語論理とアロンゾ・チャーチ · 続きを見る »

ゲルハルト・ゲンツェン

ルハルト・ゲンツェン ゲルハルト・カール・エーリヒ・ゲンツェン(Gerhard Karl Erich Gentzen、1909年11月24日 - 1945年8月4日)はドイツの論理学者・数学者。 ヘルマン・ワイルとパウル・ベルナイスの弟子。ゲッティンゲン大学でワイルに学び、1934年に学位を取得。プラハ大学で講師となる。1945年、第二次世界大戦でソ連軍に捕らえられ、プラハの捕虜収容所で栄養失調のため死去した。 主要な業績は、自然演繹 NK, NJ とシークエント計算 LK, LJ と呼ばれる証明論の体系の確立である。 自然演繹の体系は、「自然」の名の通り実際の人間の推論過程に近い直観的で分かりやすい体系である。 一方、シーケント計算は、最小限の公理 A → A と、構造および論理結合子に関する推論規則からなる。 NK, LK は古典論理を扱い、NJ, LJ は直観主義論理を扱う。ゲンツェンはこの LK においてカット除去定理 (基本定理) を証明した。 この定理は、ある定理を導く論理の道筋には、その定理自身と公理より複雑なものは現れないようにできることを示し、 LK の完全性の証明に使われた。 他に純粋算術の無矛盾性証明などの業績がある。 「すべての」を意味する記号∀を使い始めたのもゲンツェンである。.

新しい!!: 一階述語論理とゲルハルト・ゲンツェン · 続きを見る »

ゲーデルの完全性定理

数理論理学においてゲーデルの完全性定理(ゲーデルのかんぜんせいていり、Gödel's completeness theorem、Gödelscher Vollständigkeitssatz)とは、第一階述語論理の恒真な論理式はその公理系からすべて導出可能であることを示した定理を言う。1929年にクルト・ゲーデルが証明した。.

新しい!!: 一階述語論理とゲーデルの完全性定理 · 続きを見る »

ゲーデルの不完全性定理

ーデルの不完全性定理(ゲーデルのふかんぜんせいていり、)又は単に不完全性定理とは、数学基礎論における重要な定理で、クルト・ゲーデルが1930年に証明したものである。;第1不完全性定理: 自然数論を含む帰納的公理化可能な理論が、ω無矛盾であれば、証明も反証もできない命題が存在する。;第2不完全性定理: 自然数論を含む帰納的公理化可能な理論が、無矛盾であれば、自身の無矛盾性を証明できない。.

新しい!!: 一階述語論理とゲーデルの不完全性定理 · 続きを見る »

ゲーデル数

ーデル数(ゲーデルすう、Gödel number)は、数理論理学において何らかの形式言語のそれぞれの記号や整論理式に一意に割り振られる自然数である。クルト・ゲーデルが不完全性定理の証明に用いたことから、このように呼ばれている。また、ゲーデル数を割り振ることをゲーデル数化(Gödel numbering)と呼ぶ。 ゲーデル数のアイデアを暗に使っている例としては、コンピュータにおけるエンコードが挙げられる。 コンピュータでは何でも0と1で表し、「apple」のような文字列も0と1による数字で表す。 ゲーデル数化とは、このように文字列に数字を対応させる事を指す。 ゲーデル数化は、数式におけるシンボルに数を割り当てる符号化の一種でもあり、それによって生成された自然数の列が文字列を表現する。この自然数の列をさらに1つの自然数で表現することもでき、自然数についての形式的算術理論を適用可能となる。 ゲーデルの論文が発表された1931年以来、ゲーデル数はより広範囲な様々な数学的オブジェクトに自然数を割り振るのに使われるようになっていった。.

新しい!!: 一階述語論理とゲーデル数 · 続きを見る »

コンパクト性定理

ンパクト性定理()とは、一階述語論理の文の集合がモデルを持つこと(充足可能であること)と、その集合の任意の有限部分集合がモデルを持つことが同値であるという定理である。つまりある理論の充足可能性を示すにはその有限部分についてのみ調べれば良いという非常に有用性の高い定理であり、モデル理論における最も基本的かつ重要な成果のひとつである。.

新しい!!: 一階述語論理とコンパクト性定理 · 続きを見る »

シークエント計算

ークエント計算(シークエントけいさん、Sequent calculus)は、一階述語論理や特殊な命題論理で広く用いられる演繹手法である。類似の手法もシークエント計算と呼ぶことがあるので、LK と呼んで区別することがある。また類似の手法も含め、総称してゲンツェン・システムとも呼ばれる。 シークエント計算とその概念全般は証明論や数理論理学において重要な意味を持つ。以下では LK について解説する。.

新しい!!: 一階述語論理とシークエント計算 · 続きを見る »

写像

写像(しゃぞう、mapping, map)とは、二つの集合が与えられたときに、一方の集合の各元に対し、他方の集合のただひとつの元を指定して結びつける対応のことである。函数(関数)、変換、作用素、射などが写像の同義語として用いられることもある。 ブルバキに見られるように、写像は集合とともに現代数学の基礎となる道具の一つである。現代的な立場では、「写像」と(一価の)「函数」は論理的におなじ概念を表すものと理解されているが、歴史的には「函数」の語は解析学に出自を持つものであり、一部には必ずしも写像でないものも函数の名の下におなじ範疇に扱われる(多価函数参照)。文献によっては「数の集合(大抵の場合実数体 または複素数体 の部分集合)を終域に持つ写像」をして特に「函数」と呼び、「写像」はより一般の場合に用いる。函数、二項関係、対応の各項も参照のこと。.

新しい!!: 一階述語論理と写像 · 続きを見る »

全称記号

全称記号(ぜんしょうきごう、universal quantifier)とは、数理論理学において「全ての」(全称量化)を表す記号である。通常「∀」と表記され、全称量化子(ぜんしょうりょうかし)、全称限量子(ぜんしょうげんりょうし)、全称限定子(ぜんしょうげんていし)、普遍量化子(ふへんりょうかし)、普通限定子(ふつうげんていし)などとも呼ばれる。.

新しい!!: 一階述語論理と全称記号 · 続きを見る »

公理的集合論

公理的集合論(こうりてきしゅうごうろん、axiomatic set theory)とは、公理化された集合論のことである。.

新しい!!: 一階述語論理と公理的集合論 · 続きを見る »

無限論理

無限論理 (むげんろんり、infinitary logic) は、無限に長い言明および/または無限に長い証明を許す論理である。.

新しい!!: 一階述語論理と無限論理 · 続きを見る »

高階述語論理

階述語論理(こうかいじゅつごろんり、Higher-order logic)は、一階述語論理と様々な意味で対比される用語である。 例えば、その違いは量化される変項の種類にも現われている。一階述語論理では、大まかに言えば述語に対する量化ができない。述語を量化できる論理体系については二階述語論理に詳しい。 その他の違いとして、基盤となる型理論で許されている型構築の違いがある。高階述語(higher-order predicate)とは、引数として1つ以上の別の述語をとることができる述語である。一般に n 階の高階述語の引数は1つ以上の (n − 1) 階の述語である(ここで n > 1)。同じことは高階関数(higher-order function)にも言える。 高階述語論理は表現能力が高いが、その特性、特にモデル理論に関わる部分では、多くの応用について性格が良いとは言えない。クルト・ゲーデルの業績により、古典的高階述語論理は(帰納的に公理化された)健全で完全な証明計算が認められないとされた。しかし、Henkin model によれば、健全で完全な証明計算は存在する。 高階述語論理の例として、アロンゾ・チャーチの Simple Theory of Types や Calculus of Constructions (CoC) がある。.

新しい!!: 一階述語論理と高階述語論理 · 続きを見る »

論理的帰結

論理的帰結(ろんりてききけつ、伴意、logical consequence, entailment)は、論理学における最も基本的な概念であり、複数の文(または命題)の集合と1つの文(命題)の間が「~だから、当然~」という繋がり方をする関係を指す。例えば、「カーミットは緑色だ」という文は、「全てのカエルは緑色だ」と「カーミットはカエルだ」の論理的帰結である。 このような論理的帰結の確かさは、前提が真かどうか、および完全かどうかに依存する。この前提は全てのカエルが緑色でない場合は真ではないことになる。演繹による推論や論理的帰結は認識論の重要な面であり、因果に関する一般的仮説を伝達する意味を持つ。 形式的な論理的帰結関係はモデル理論的なものと証明論的なもの(あるいは両方)がある。 論理的帰結は、文の集合から文の集合への関数としても表現できる(タルスキ風の定式化)し、2つの文の集合の間の関係としても表現できる(multiple-conclusion logic)。.

新しい!!: 一階述語論理と論理的帰結 · 続きを見る »

議論領域

議論領域(ぎろんりょういき、Domain of discourse)は、演繹、特に一階述語論理で使われる用語である。量化子で扱われる実体の適切な集合を指す。 議論領域という用語は一般に、特定の議論で使われる項全体の集合を指す。特定の議論とはすなわち、任意の1つの関心領域での言語学的または意味論的項の集まりである。モデル理論的な意味論では、議論領域という用語は、モデルが基づく実体集合を指す。 データベースは組織の現実のある面をモデル化したものである。このような現実を便宜的に「議論領域」と呼ぶこともある。.

新しい!!: 一階述語論理と議論領域 · 続きを見る »

述語論理

述語論理(じゅつごろんり、)とは、数理論理学における記号的形式体系群を指す用語で、一階述語論理、二階述語論理、、無限論理などが含まれる。これらの形式体系の特徴は、論理式に含まれる変数を量化できる点である。一般的な量化子として、存在量化子 ∃ と全称量化子 ∀ がある。変数は議論領域の要素、関係、関数などである。例えば、関数記号に対する存在量化は「ある関数が存在する」という修飾として解釈される。述語論理の基礎は、ゴットロープ・フレーゲとチャールズ・サンダース・パースがそれぞれ独自に生み出し発展させた。 述語論理と言った場合、一階述語論理を指すこともある。述語論理の公理化された形態を述語計算 (predicate calculus) と呼び、述語論理は非形式的でより直観的なものとする見方もある。 様相作用素と量化子を併用する論理も述語論理の一種とされる。これについては様相論理を参照。.

新しい!!: 一階述語論理と述語論理 · 続きを見る »

部分集合

集合 A が集合 B の部分集合(ぶぶんしゅうごう、subset; 下位集合)であるとは、A が B の一部(あるいは全部)の要素だけからなることである。A が B の一部分であるという意味で部分集合という。二つの集合の一方が他方の部分集合であるとき、この二つの集合の間に包含関係があるという。.

新しい!!: 一階述語論理と部分集合 · 続きを見る »

関係代数 (数学)

数学の抽象代数学の分野において 関係代数 (relation algebra) とは "逆" と呼ばれる対合を持つのことである。動機付けとなるような関係代数の例は、集合 X 上の全ての二項関係からなる集合 Pow(X2) であって、演算 R • S を通常の関係の合成とし、R の逆を逆関係で定義する。関係代数は 19世紀の オーガスタス・ド・モルガン と チャールズ・サンダース・パースの結果から現れ、の代数的論理学において全盛となった。現在の、関係代数の等式による定式化は、1940年代に始まるアルフレト・タルスキと彼の弟子たちの研究によってなされた。.

新しい!!: 一階述語論理と関係代数 (数学) · 続きを見る »

量化

量化(りょうか、Quantification)とは、言語や論理学において、論理式が適用される(または満足される)議論領域の個体の「量」を指定すること。.

新しい!!: 一階述語論理と量化 · 続きを見る »

自然演繹

自然演繹(しぜんえんえき、Natural deduction)は、「自然な」ものとしての論理的推論の形式的モデルを提供する証明理論の手法であり、哲学的論理学の用語である。.

新しい!!: 一階述語論理と自然演繹 · 続きを見る »

自然数

自然数(しぜんすう、natural number)とは、個数、もしくは順番を表す一群の数のことである。集合論においては、自然数は物の個数を数える基数のうちで有限のものであると考えることもできるし、物の並べ方を示す順序数のうちで有限のものであると考えることもできる。 自然数を 1, 2, 3, … とする流儀と、0, 1, 2, 3, … とする流儀があり、前者は数論などでよく使われ、後者は集合論、論理学などでよく使われる(詳しくは自然数の歴史と零の地位の節を参照)。いずれにしても、0 を自然数に含めるかどうかが問題になるときは、その旨を明記する必要がある。自然数の代わりに非負整数または正整数と言い換えることによりこの問題を避けることもある。 数学の基礎付けにおいては、自然数の間の加法についての形式的な逆元を考えることによって整数を定義する。正の整数ないしは負でない整数を自然数と同一視し、自然数を整数の一部として取扱うことができる。自然数と同様に整数の全体も可算無限集合である。 なお、文脈によっては、その一群に属する個々の数(例えば 3 や 18)を指して自然数ということもある。.

新しい!!: 一階述語論理と自然数 · 続きを見る »

集合

数学における集合 (しゅうごう、set, ensemble, Menge) とは、大雑把に言えばいくつかの「もの」からなる「集まり」である。集合を構成する個々の「もの」のことを元 (げん、; 要素) という。 集合は、集合論のみならず現代数学全体における最も基本的な概念の一つであり、現代数学のほとんどが集合と写像の言葉で書かれていると言ってよい。 慣例的に、ある種の集合が系 (けい、) や族 (ぞく、) などと呼ばれることもある。実際には、これらの呼び名に本質的な違いはないが細かなニュアンスの違いを含むと考えられている。たとえば、方程式系(「相互に連立する」方程式の集合)、集合族(「一定の規則に基づく」集合の集合)、加法族(「加法的な性質を持つ」集合族)など。.

新しい!!: 一階述語論理と集合 · 続きを見る »

Prolog

Prolog(プロログ)は、非手続き型プログラミング言語の一つ。論理型言語に分類される。名称は、「論理を使ったプログラミング」を意味するフランス語「programmation en logique」に由来しているRobert Kowalski.

新しい!!: 一階述語論理とProlog · 続きを見る »

推論規則

推論規則(すいろんきそく、rule of inference, inference rule, transformation rule)とは、論理式から他の論理式を導く推論の規則である。 記号、公理、代入規則、推論規則によって理論を形式化したものを公理系という。 公理は記号だけで記述されるが、推論規則や代入規則はこれらの記号について述べているメタ言語で記述される。 恒真式 (トートロジー)から推論規則を導くと妥当性のある推論になる。.

新しい!!: 一階述語論理と推論規則 · 続きを見る »

様相論理

様相論理(ようそうろんり、modal logic)は、いわゆる古典論理の対象でない、様相(modal)と呼ばれる「〜は必然的に真」や「〜は可能である」といった必然性や可能性などを扱う論理である(様相論理は、部分の真理値からは全体の真理値が決定されない内包論理の一種と見ることができる)。 その歴史は古くアリストテレスまで遡ることができるが、形式的な扱いは数理論理学以降、非古典論理としてである。 様相論理では一般に、標準的な論理体系に「~は必然的である」ことを意味する必然性演算子 \Box と、「~は可能である」ことを意味する可能性演算子 \Diamond のふたつの演算子が追加される。.

新しい!!: 一階述語論理と様相論理 · 続きを見る »

決定可能性

決定可能(けっていかのう、decidable)は、論理学において、論理式の集合のメンバーシップの決定をする実効的(effectiveな)方法が存在することを指す。決定可能性(けっていかのうせい、decidability)は、そのような属性を指す。命題論理のような形式体系は、論理的に妥当な論理式(または定理)の集合のメンバーシップを実効的に決定できるなら、決定可能である。ある決まった論理体系における理論(論理的帰結で閉じている論理式の集合)は、任意の論理式がその理論に含まれるか否かを決定する実効的方法があれば、決定可能である。.

新しい!!: 一階述語論理と決定可能性 · 続きを見る »

濃度 (数学)

数学、とくに集合論において、濃度(のうど)あるいは基数(きすう)(cardinal number, cardinality, power)とは、集合の「元の個数」という概念を拡張したものである。有限集合については、濃度は「元の個数」の同意語に過ぎない。。。.

新しい!!: 一階述語論理と濃度 (数学) · 続きを見る »

有限集合

数学において、集合が有限(ゆうげん、finite)であるとは、自然数 n を用いて という形にあらわされる集合との間に全単射が存在することをいう(ただしここでは、n.

新しい!!: 一階述語論理と有限集合 · 続きを見る »

数学的直観主義

数学的直観主義(すうがくてきちょっかんしゅぎ)とは、数学の基礎を数学者の直観におく立場のことを指す。.

新しい!!: 一階述語論理と数学的直観主義 · 続きを見る »

数理論理学

数理論理学(mathematische Logik、mathematical logic)は、論理学(形式論理学)の数学への応用の探求ないしは論理学の数学的な解析を主たる目的とする、数学の関連分野である。局所的には数理論理学は超数学、数学基礎論、理論計算機科学などと密接に関係している。数理論理学の共通な課題としては形式体系の表現力や形式証明系の演繹の能力の研究が含まれる。 数理論理学はしばしば集合論、モデル理論、再帰理論、証明論の4つの領域に分類される。これらの領域はロジックのとくに一階述語論理や定義可能性に関する結果を共有している。計算機科学(とくに)における数理論理学の役割の詳細はこの記事には含まれていない。詳細はを参照。 この分野が始まって以来、数理論理学は数学基礎論の研究に貢献し、また逆に動機付けられてきた。数学基礎論は幾何学、算術、解析学に対する公理的な枠組みの開発とともに19世紀末に始まった。20世紀初頭、数学基礎論は、ヒルベルトのプログラムによって、数学の基礎理論の無矛盾性を証明するものとして形成された。クルト・ゲーデルとゲルハルト・ゲンツェンによる結果やその他は、プログラムの部分的な解決を提供しつつ、無矛盾性の証明に伴う問題点を明らかにした。集合論における仕事は殆ど全ての通常の数学を集合の言葉で形式化できることを示した。しかしながら、集合論に共通の公理からは証明することができない幾つかの命題が存在することも知られた。むしろ現代の数学基礎論では、全ての数学を展開できる公理系を見つけるよりも、数学の一部がどのような特定の形式的体系で形式化することが可能であるか(逆数学のように)ということに焦点を当てている。.

新しい!!: 一階述語論理と数理論理学 · 続きを見る »

整数

数学における整数(せいすう、integer, whole number, Ganze Zahl, nombre entier, número entero)は、0 とそれに 1 ずつ加えていって得られる自然数 (1, 2, 3, 4, …) および 1 ずつ引いていって得られる数 (−1, −2, −3, −4, …) の総称である。 整数は数直線上の格子点として視覚化される 整数の全体からなる集合は普通、太字の Z または黒板太字の \mathbb Z で表す。これはドイツ語 Zahlen(「数」の意・複数形)に由来する。 抽象代数学、特に代数的整数論では、しばしば「代数体の整数環」の元という意味で代数的整数あるいは「整数」という言葉を用いる。有理数全体の成す体はそれ自身が代数体の最も簡単な例であり、有理数体の代数体としての整数環すなわち、「有理数の中で整なもの」の全体の成す環は、本項でいう意味での整数全体の成す環である。一般の「整数」との区別のためにここでいう意味の整数を有理整数 (rational integer) と呼ぶことがある接頭辞「有理(的)」(rational) はそもそも「整数比」であるという意味なので、この呼称は自己循環的にもみえる。しかし、有理整数と呼ぶ場合の「有理」は「有理数の中で」という程度の意味の単なる符牒であって、「整数比」という本来の意味合いに拘るのは徒労である。。.

新しい!!: 一階述語論理と整数 · 続きを見る »

普遍例化

普遍例化(ふへんれいか、Universal instantiation)は、論理学において、あるクラスの全ての個体について真であることからそのクラスの特定の個体について真であると推論すること。全称量化子による量化規則で一般に表されるが、公理としても記述できる。これは、一階述語論理で使われる基本原則の1つである。 例:「全ての犬は動物である。ポチは犬である。従って、ポチは動物である」 ある項 a について公理スキーマとして記号的に表すと以下のようになる。 ここで A(a/x) は A における x の自由な出現を a で置換した結果を表す。 推論規則としては次のように記述される。 from ⊢ ∀x A infer ⊢ A(a/x) ここでの A(a/x) も上と同じ意味である。 Irving Copi は普遍例化について「… ゲルハルト・ゲンツェンと Stanislaw Jaskowski が1934年にそれぞれ独自に生み出した自然演繹の規則のバリエーションに従う」と記している。(-pg.

新しい!!: 一階述語論理と普遍例化 · 続きを見る »

ここにリダイレクトされます:

第一階述語論理

出ていきます入ってきます
ヘイ!私たちは今、Facebook上です! »