Constructive Logic
Classical logic에서는 어떤 명제를 증명하는 것이, 해당 명제의 진리값이 참임을 증명하는 것이다. 이와 달리, constructive logic은 명제의 증명에 해당하는 무언가를 직접 제시하거나, 그 무언가를 제시하는 방법을 제시하는 것을 증명이라고 본다.
True and False
Constructive logic에서 참과 거짓은 각각 증명 가능하고 불가능한 고유의 명제이다.
Negation
어떤 명제 P의 부정은 “P -> False”이다. 즉, P가 증명 가능하면 거짓이 증명 가능하다는(즉, 말도 안되는) 명제가 P의 부정이다.
Excluded Middle
Classical logic에서는 모든 명제가 참 또는 거짓이라는 진리값을 가진다. 따라서 모든 명제는 참이거나 거짓이다. 이 axiom을 excluded middle이라고 한다.
Equivalent Lemma
Excluded middle은 다음 네 정리와 동치이다.
- peirce’s law: $((P \rightarrow Q) \rightarrow P) \rightarrow P$
- double negation elimination: $\neg \neg P \rightarrow P$
- de morgan’s law (not and not): $\neg(\neg P \land ~Q) \rightarrow P \lor Q$
- implies to or: $(P \rightarrow Q) \rightarrow (\neg P \lor Q)$