数学/証明
命題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の必要条件である
Ｕの空間上でＢの方がＡ以上の広い空間を持つ。このとき、全集合Ｕを集合Ａ，Ｂと論理記号(∨,∧,￢)を使っていかにして表すか？！ という問題に帰着できる。
即ち、以下の図で表すことができる。
￢Ａ
∨Ｂ
この真理集合の考えを用いると、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 |
このように、全集合Ｕを埋め尽くすことが出来ればトートロジーになる。
従って、Ａと￢Ａを重ねると
∨
＝
となり、被い尽くすことが出来たので、トートロジーである。
矛盾命題 contradiction
真理値が全て、０（偽）である命題を、矛盾命題という。
| A | ￢A | ￢(A⇒A) | ￢A∧A |
| 1 | 0 | 0 | 0 |
| 0 | 1 | 0 | 0 |
同様に
∧＝
となり、埋めている部分が無いので、矛盾命題となる。
同値関係
| 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という数理処理システムで行うことができる。