輪講

目的

前提A1…Anから結論Bを導くこと。
A,Bの意味を問わずルールで形式的に導く。

論理演算子

¬（否定）、∨（選言）、∧（連言）、⇒（含意）
これらには優先度がある。
否定＞連言＞（＝？）選言＞含意

シーケント

φ,…,φ├ψ
のようなもののこと。

ルール

The rules for conjunction.
The rules for double negation.
The rules for eliminating implication.
The rules for implies introduction.
The rules for disjunction.
The rules 'copy'.

矛盾

矛盾した前提からはなにを言ってもいい。
p ∧ ¬p |― q
（PでPでなければqである。）
⊥は矛盾の意。