Concept

Intermediate logic

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 F → G 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
  4. L is not the set of all formulas. 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 + ¬¬p → p = IPC + ((p → q) → p) → p the logic of the weak excluded middle (KC, Jankov's logic, De Morgan logic): IPC + ¬¬p ∨ ¬p Gödel–Dummett logic (LC, G): IPC + (p → q) ∨ (q → p) = IPC + (p → (q ∨ r)) → ((p → q) ∨ (p → r)) Kreisel–Putnam logic (KP): IPC + (¬p → (q ∨ r)) → ((¬p → q) ∨ (¬p → r)) Medvedev's logic of finite problems (LM, ML): defined semantically as the logic of all frames of the form for finite sets X ("Boolean hypercubes without top"), not known to be recursively axiomatizable realizability logics Scott's logic (SL): IPC + ((¬¬p → p) → (p ∨ ¬p)) → (¬¬p ∨ ¬p) Smetanich's logic (SmL): IPC + (¬q → p) → (((p → q) → p) → p) logics of bounded cardinality (BCn): logics of bounded width, also known as the logic of bounded anti-chains (BWn, BAn): logics of bounded depth (BDn): IPC + pn ∨ (pn → (pn−1 ∨ (pn−1 → ... → (p2 ∨ (p2 → (p1 ∨ ¬p1))).
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Graph Chatbot

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.