truth-value semantics for intuitionistic propositional logic

A truth-value semantic system for intuitionistic propositional logicPlanetmathPlanetmath consists of the set Vn:={0,1,,n}, where n1, and a function v from the set of wff’s (well-formed formulas) to Vn satisfying the following properties:

  1. 1.


  2. 2.


  3. 3.

    v(AB)=n if v(A)v(B), and v(B) otherwise

  4. 4.

    v(¬A)=n if v(A)=0, and 0 otherwise.

This function v is called an interpretationMathworldPlanetmath for the propositional logic. A wff A is said to be true for (Vn,v) if v(A)=n, and a tautologyMathworldPlanetmath for Vn if A is true for (Vn,v) for all interpretations v. When A is a tautology for Vn, we write nA. It is not hard see that any truth-value semantic system is sound, in the sense that iA (A is a theoremMathworldPlanetmath) implies nA, for any n. A proof of this fact can be found here (

(Vn,v) is a generalizationPlanetmathPlanetmath of the truth-value semantics for classical propositional logic. Indeed, when n=1, we have the truth-value system for classical propositional logic.

However, unlike the truth-value semantic system for classical propositional logic, no truth-value semantic systems for intuitionistic propositional logic are completePlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath: there are tautologies that are not theorems for each n. For example, for each n, the wff


is a tautology for Vn that is not a theorem, where each pi is a propositional letter. The formulaMathworldPlanetmathPlanetmath k=1mAi is the abbreviation for ((A1A2))Am, where each Ai is a formula. The following is a proof of this fact:


Let A be the j=1n+2i=jn+1(pjpi+1). Note that p1,,pn+2 are all the proposition letters in A. However, there are only n+1 elements in Vn, so for every interpretation v, there are some pi and pj such that v(pi)=v(pj) by the pigeonhole principleMathworldPlanetmath. Then v(pipj)=n, and hence v(A)=n, implying that A is a tautology for Vn. However, A is not a tautology for Vn+1: let v be the interpretation that maps pi to i-1. Then v(pipj)=min{i,j}-1, so that v(A)=nn+1. Therefore, A is not a theorem. ∎

Nevertheless, the truth-value semantic systems are useful in showing that certain theorems of the classical propositional logic are not theorems of the intuitionistic propositional logic. For example, the wff p¬p (law of the excluded middle) is not a theorem, because it is not a tautology for V2, for if v(p)=1, then v(p¬p)=12. Similarly, neither ¬¬pp (law of double negation) nor ((pq)p)p (Peirce’s law) are theorems of the intuitionistic propositional logic.

Remark. The linearly ordered set Vn:={0,1,,n} turns into a Heyting algebraMathworldPlanetmath if we define the relative pseudocomplementation operationMathworldPlanetmath by xy:=n if xy and xy:=y otherwise. Then the pseudocomplement x* of x is just x0. This points to the connection of the intuitionistic propositional logic and Heyting algebra.

Title truth-value semantics for intuitionistic propositional logic
Canonical name TruthvalueSemanticsForIntuitionisticPropositionalLogic
Date of creation 2013-03-22 19:31:04
Last modified on 2013-03-22 19:31:04
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 21
Author CWoo (3771)
Entry type Definition
Classification msc 03B20
Related topic AxiomSystemForIntuitionisticLogic