World Library  
Flag as Inappropriate
Email this Article

Intermediate logics

Article Id: WHEBN0003410949
Reproduction Date:

Title: Intermediate logics  
Author: World Heritage Encyclopedia
Language: English
Subject: Intuitionistic logic
Publisher: World Heritage Encyclopedia

Intermediate logics

In mathematical logic, a superintuitionistic logic is a propositional logic extending intuitionistic logic. Classical logic is the strongest consistent superintuitionistic logic, thus consistent superintuitionistic logics are called intermediate logics (the logics are intermediate between intuitionistic logic and classical logic).


A superintuitionistic logic is a set L of propositional formulas in a countable set of variables pi satisfying the following properties:

  1. all axioms of intuitionistic logic belong to L;
  2. if F and G are formulas such that F and FG both belong to L, then G also belongs to L (closure under modus ponens);
  3. if F(p1, p2, ..., pn) is a formula of L, and G1, G2, ..., Gn are any formulas, then F(G1, G2, ..., Gn) belongs to L (closure under substitution).

Such a logic is intermediate if furthermore

  1. L is not the set of all formulas.

Properties and examples

There exists a continuum of different intermediate logics. Specific intermediate logics are often constructed by adding one or more axioms to intuitionistic logic, or by a semantical description. Examples of intermediate logics include:

  • intuitionistic logic (IPC, Int, IL, H)
  • classical logic (CPC, Cl, CL): IPC + p ∨ ¬p = IPC + ¬¬pp = IPC + ((pq) → p) → p
  • the logic of the weak excluded middle (KC, Jankov's logic, De Morgan logic[1]): IPC + ¬¬p ∨ ¬p
  • GödelDummett logic (LC, G): IPC + (pq) ∨ (qp)
  • KreiselPutnam logic (KP): IPC + (¬p → (qr)) → ((¬pq) ∨ (¬pr))
  • Medvedev's logic of finite problems (LM, ML): defined semantically as the logic of all frames of the form \langle\mathcal P(X)\setminus\{X\},\subseteq\rangle for finite sets X ("Boolean hypercubes without top"), as of 2010 not known to be recursively axiomatizable
  • realizability logics
  • Scott's logic (SL): IPC + ((¬¬pp) → (p ∨ ¬p)) → (¬¬p ∨ ¬p)
  • Smetanich's logic (SmL): IPC + (¬qp) → (((pq) → p) → p)
  • logics of bounded cardinality (BCn): \textstyle\mathbf{IPC}+\bigvee_{i=0}^n\bigl(\bigwedge_{j
  • logics of bounded width, also known as the logic of bounded anti-chains (BWn, BAn): \textstyle\mathbf{IPC}+\bigvee_{i=0}^n\bigl(\bigwedge_{j\ne i}p_j\to p_i\bigr)
  • logics of bounded depth (BDn): IPC + pn ∨ (pn → (pn−1 ∨ (pn−1 → ... → (p2 ∨ (p2 → (p1 ∨ ¬p1)))...)))
  • logics of bounded top width (BTWn): \textstyle\mathbf{IPC}+\bigvee_{i=0}^n\bigl(\bigwedge_{j
  • logics of bounded branching (Tn, BBn): \textstyle\mathbf{IPC}+\bigwedge_{i=0}^n\bigl(\bigl(p_i\to\bigvee_{j\ne i}p_j\bigr)\to\bigvee_{j\ne i}p_j\bigr)\to\bigvee_{i=0}^np_i
  • Gödel n-valued logics (Gn): LC + BCn−1 = LC + BDn−1

Superintuitionistic or intermediate logics form a complete lattice with intuitionistic logic as the bottom and the inconsistent logic (in the case of superintuitionistic logics) or classical logic (in the case of intermediate logics) as the top. Classical logic is the only coatom in the lattice of superintuitionistic logics; the lattice of intermediate logics also has a unique coatom, namely SmL.

The tools for studying intermediate logics are similar to those used for intuitionistic logic, such as Kripke semantics. For example, Gödel–Dummett logic has a simple semantic characterization in terms of total orders.


Given a Heyting algebra H, the set of propositional formulas that are valid in H is an intermediate logic. Conversely, given an intermediate logic it is possible to construct its Lindenbaum algebra which is a Heyting algebra.

An intuitionistic Kripke frame F is a partially ordered set, and a Kripke model M is a Kripke frame with valuation such that \{x\mid M,x\Vdash p\} is an upper subset of F. The set of propositional formulas that are valid in F is an intermediate logic. Given an intermediate logic L it is possible to construct a Kripke model M such that the logic of M is L (this construction is called canonical model). A Kripke frame with this property may not exist, but a general frame always does.

Relation to modal logics

Main article: Modal companion

Let A be a propositional formula. The Gödel–Tarski translation of A is defined recursively as follows:

  • T(p_n) = \Box p_n
  • T(\neg A) = \Box \neg T(A)
  • T(A \and B) = T(A) \and T(B)
  • T(A \vee B) = T(A) \vee T(B)
  • T(A \to B) = \Box (T(A) \to T(B))

If M is a modal logic extending S4 then ρM = {A | T(A) ∈ M} is a superintuitionistic logic, and M is called a modal companion of ρM. In particular:

  • IPC = ρS4
  • KC = ρS4.2
  • LC = ρS4.3
  • CPC = ρS5

For every intermediate logic L there are many modal logics M such that L = ρM.


  • Toshio Umezawa. On logics intermediate between intuitionistic and classical predicate logic. Journal of Symbolic Logic, 24(2):141–153, June 1959.
  • Alexander Chagrov, Michael Zakharyaschev. Modal Logic. Oxford University Press, 1997.
This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a non-profit organization.

Copyright © World Library Foundation. All rights reserved. eBooks from National Public Library are sponsored by the World Library Foundation,
a 501c(4) Member's Support Non-Profit Organization, and is NOT affiliated with any governmental agency or department.