# Chapter 16. Intuitionistic Logic

Intuitionistic logic studies reasoning in which a statement is accepted only when there is a construction, proof, or method that establishes it.

The chapter begins with constructive semantics, where truth is understood through evidence rather than only through truth values, and this changes the interpretation of several familiar logical principles.

Proof interpretation is then introduced to explain how formulas correspond to kinds of constructions, so that a proof of a conjunction gives proofs of both parts, while a proof of an implication gives a method for transforming proofs of the premise into proofs of the conclusion.

The chapter next compares intuitionistic logic with classical logic, especially through principles such as excluded middle and double negation elimination, which are valid classically but not accepted intuitionistically without additional evidence.

Kripke models are then studied as a semantic framework for intuitionistic logic, where truth can grow as information increases, and this gives a precise model of constructive reasoning.

The final part of the chapter discusses applications in computation, where intuitionistic proofs correspond naturally to programs, and logical rules describe how computational objects are constructed and used.