数学/定義
命題A⇒Bを証明するために
・対偶法：同値式を証明する方法。
ちなみに同値なものとして、￢B⇒￢Aや、￢A∨Bなどがある。
 A  ￢A  B  A⇒B  ￢A∨B 
 1  0  1  1  1 
 1  0  0  0  0 
 0  1  1  1  1 
 0  1  0  1  1 
・背理法：(￢A∨B)の否定式であるA∧￢Bを仮定し、矛盾を導びきだす。
ある論理式の否定である論理式を作る時は、
∀,∃,∨,∧,命題Qを∃,∀,∧,∨,命題￢Qに置き換える。
 ∀ ←→このように置き換えると否定論理式になる←→∃
 ∃ ∀
 ∨ ∧
 ∧ ∨
 命題Q 命題￢Q
命題論理は以下の記号を使って表される。
 ∧,∩ ：論理積（かつ）
 ∨,∪ ：論理和（または）
 ￢,＾ ：否定  （でない）
 ⇒,→ ：導出  （ならば）
また、A⇒B then B⇒A よりA⇔B とすることも出来る
----
命題関数
集合 Ｕ 上で定義された命題 A(x) を考える。命題 A(x) が真となるような集合Ｕの要素 x の集合を、
命題関数 A(x) の真理集合といい、Ａで表す。
それぞれの命題関数の真理集合は次のようになる。
 命題関数  真理集合 
 A(x)∨B(x)    Ａ∪Ｂ 
 A(x)∧B(x)    Ａ∩Ｂ 
 ￢A(x)        A^ 
 A(x) ⇒ B(x)  A^∪B 
∀x∈Ｕ：Ａ(x)⇒Ｂ(x)の成立している図
AはBの十分条件、BはAの必要条件である
set.png
Ｕの空間上でＢの方がＡ以上の広い空間を持つ。このとき、全集合Ｕを集合Ａ，Ｂと論理記号(∨,∧,￢)を使っていかにして表すか？！
という問題に帰着できる。
即ち、以下の図で表すことができる。
￢Ａset_1.png∨Ｂset_2.png
この真理集合の考えを用いると、A⇒Bの証明は視覚的に行うことができる。すなわち、
A(x) ⇒ B(x)を証明するには、A⊂Bであることを確かめればよい。(記号は⊂でも⊆でもどちらでも良い)
実際に、A(x) ⇒ B(x)の真理集合は、A^∪Bであり、命題がトートロジーであることから
A^∪B＝Ｕに等しい。このとき、
A＝A∩Ｕ＝A∩（A^∪B）＝（A∩A^）∪（A∩B）＝A∩B⊂Bから、A⊂B
逆に、A⊂Bとすると、
Ｕ＝A^∪A⊂A^∪B⊂Ｕから、A^∪B＝Ｕ
よって、命題A(x) → B(x)は、トートロジーである。
例えば、全集合Ｕ：（生物）の中で、Ａ：（人間）ならばＢ：（動物）である。
A,B⊂Ｕ：A⊂B
以下の4つの命題関数は同値である。
命題関数読み方Mizarの場合
∀x A(x)⇒B(x) for all x being NaturalNumber such that A(x) implies B(x) for x being Nat st A.x implies B.x
∀x A(x)⊂B(x) for all x being NaturalNumber A(x) holds B(x) for x being Nat A.x holds B.x
∀x ￢A(x)∨B(x) for all x being NaturalNumber such that not A(x) ∨ B(x) for x being Nat st not A.x \/ B.x
∀x ￢B(x)⇒￢A(x) for all x being NaturalNumber such that not B(x) implies not A(x) for x being Nat st not B.x implies not A.x
裏
∃x ￢A(x)⇒￢B(x) existence x being NaturalNumber such that not A(x) implies not B(x) ex x being Nat st not A.x implies not B.x
∃x A(x)∨￢B(x) existence x being NaturalNumber such that A(x) ∨ not B(x) ex x being Nat st A.x \/ not B.x 
----
トートロジー（恒真命題） tautology
真理値が全て、１（真）である命題を、トートロジーという。
 A  ￢A   A⇒A  ￢A∨A 
 1  0  1  1 
 0  1  1  1 
このように、全集合Ｕを埋め尽くすことが出来ればトートロジーになる。
math_set0.png
従って、Ａと￢Ａを重ねると
math_set2.png∨math_set3.png＝math_set1.png
となり、被い尽くすことが出来たので、トートロジーである。
矛盾命題 contradiction
真理値が全て、０（偽）である命題を、矛盾命題という。
 A  ￢A   ￢(A⇒A)  ￢A∧A 
 1  0  0  0 
 0  1  0  0 
同様に
math_set2.png∧math_set3.png＝math_set4.png
となり、埋めている部分が無いので、矛盾命題となる。
----
同値関係
 1  反射律  reflexivity a～a 
 2  対象律  symmetry  a～b ⇒ b～a 
 3  推移律  transitive   (a～b ＆ b～c) ⇒ a～c 
読み方(⇒:ならば、 &:かつ)
推移律と等価な関係
   非反射関係 irreflexivity 
   非対称関係 asymmetry 
   強半順序関係 strict partial order 
  律番号   順序関係   説明  
  1,3   前順序（擬順序）   
  1,3   全擬順序    完全的な擬順序 
  1,2,3   同値関係   前順序に対象律が加わったもの  
  1,￢2,3   半順序    前順序に反対称律が加わったもの 
  1,￢2,3  厳密弱順序    強半順序関係で等価関係での比較が不可能な場合 
  ￢2,3   全順序    完全関係 
----
数学の証明は厳密性を保つため「一階述語論理」を使って行う。
「無限」に関する議論も「有限」と同様にして扱うことが可能となる。
[[全称記号
[[存在記号
 ∃Φ{1,2,3,4, ... ,n}
  このとき、以下の関係式が成り立つ
 
 ∀ｘ  Φ(ｘ) ⇔ Φ(1)∧Φ(2)∧...∧Φ(n)
 ∃ｘ  Φ(ｘ) ⇔ Φ(1)∨Φ(2)∨...∨Φ(n)
 全てのｘにおいて、Ｈ(x)、ならば、Ａ(x)。
 ∀x  (Ｈ(ｘ) → Ａ(ｘ) ）
 ある x が存在し、A(x)、かつ、B(x)
 ∃x (A(x) ∧ B(x))
 
 ※∃の場合は、→ではなく、∧となる!
関係記号 Ψ(ｘ,ｙ)における同値関係
関係記号Ψ(ｘ,ｙ)は、集合における写像に対応している。
ただし、この場合は、ある固体領域内における要素と要素の対応関係とみるべきである。
限量記号（∀、∃）と、関係記号Ψ(ｘ,ｙ)を組み合わせた場合、
固体領域 (ａ,ｂ) を考えてみる。この場合の対応関係は、以下の４通りである。
(ａ,ｂ)、(ａ,ａ)、(ｂ,ａ)、(ｂ,ｂ)
この、Ψ(ｘ,ｙ)の組み合わせは以下のようになる。
∀x∀yΨ(x,y）⇔ ((a,a)∧(a,b))∧((b,a)∧(b,b))⇔(a,a)∧(a,b)∧(b,a)∧(b,b)：全てのxについて、全てのyが、Ψ(x,y)において対応する
∀ｙ∀ｘΨ(ｘ,ｙ) ⇔ ((ａ,ａ)∧(ｂ,ａ)) ∧ ((ａ,ｂ)∧(ｂ,ｂ))⇔ (ａ,ａ)∧(ｂ,ａ) ∧ (ａ,ｂ)∧(ｂ,ｂ)：全てのyについて、全てのxが、Ψ(x,y)において対応する
∃ｘ∃ｙΨ(ｘ,ｙ) ⇔ ((ａ,ａ)∨(ａ,ｂ)) ∨ ((ｂ,ａ)∨(ｂ,ｂ))⇔ (ａ,ａ)∨(ａ,ｂ) ∨ (ｂ,ａ)∨(ｂ,ｂ)：あるｘについて、あるｙが、Ψ(ｘ,ｙ)において対応する
∃ｙ∃ｘΨ(ｘ,ｙ) ⇔ ((ａ,ａ)∨(ｂ,ａ)) ∨ ((ａ,ｂ)∨(ｂ,ｂ))⇔(ａ,ａ)∨(ｂ,ａ) ∨ (ａ,ｂ)∨(ｂ,ｂ)：あるｙについて、あるｘが、Ψ(ｘ,ｙ)において対応する
∀ｘ∃ｙΨ(ｘ,ｙ) ⇔ ((ａ,ａ)∨(ａ,ｂ)) ∧ ((ｂ,ａ)∨(ｂ,ｂ))⇔ ((ａ,ａ)∨(ａ,ｂ)) ∧ ((ｂ,ａ)∨(ｂ,ｂ)):全てのｘについて、あるｙが、Ψ(ｘ,ｙ)において対応する
∃ｘ∀ｙΨ(ｘ,ｙ) ⇔ ((ａ,ａ)∧(ａ,ｂ)) ∨ ((ｂ,ａ)∧(ｂ,ｂ))⇔ ((ａ,ａ)∧(ａ,ｂ)) ∨ ((ｂ,ａ)∧(ｂ,ｂ))：あるｘについて、全てのｙが、Ψ(ｘ,ｙ)において対応する
∀ｙ∃ｘΨ(ｘ,ｙ) ⇔ ((ａ,ａ)∨(ｂ,ａ)) ∧ ((ａ,ｂ)∨(ｂ,ｂ))⇔ ((ａ,ａ)∨(ｂ,ａ)) ∧ ((ａ,ｂ)∨(ｂ,ｂ))：全てのｙについて、あるｘが、Ψ(ｘ,ｙ)において対応する
∃ｙ∀ｘΨ(ｘ,ｙ) ⇔ ((ａ,ａ)∧(ｂ,ａ)) ∨ ((ａ,ｂ)∧(ｂ,ｂ))⇔ ((ａ,ａ)∧(ｂ,ａ)) ∨ ((ａ,ｂ)∧(ｂ,ｂ))：あるｙについて、全てのｘが、Ψ(ｘ,ｙ)において対応する
----
「二階述語論理」とは数学的帰納法、f(f(x))、などのように論理演算がそれ自身を含むものをいう。
従って自己を含む為に、その論理演算が証明可能か否かを判断できない命題が存在する。(ゲーデルの不完全定理)
----
数学の証明(Proof Check)はMizarという数理処理システムで行うことができる。