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:

all axioms of intuitionistic logic belong to L;
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);
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
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))).

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Concepts associés (14)

Cours associés (6)

Séances de cours associées (32)

Sémantique de Kripke

En logique mathématique, la sémantique de Kripke est une sémantique formelle utilisée pour les logiques non-classiques comme la logique intuitionniste et certaines logiques modales. Elle a été développée à la fin des années 1950 et début des années 1960 par Saul Kripke et est fondée sur la théorie des mondes possibles. Un cadre de Kripke est un couple (W, R), où W est un ensemble de mondes appelés parfois mondes possibles et où R est une relation binaire sur W. L'ensemble W s'appelle parfois l'univers des mondes possibles.

Intermediate logic

Modal companion

In logic, a modal companion of a superintuitionistic (intermediate) logic L is a normal modal logic that interprets L by a certain canonical translation, described below. Modal companions share various properties of the original intermediate logic, which enables to study intermediate logics using tools developed for modal logic. Let A be a propositional intuitionistic formula. A modal formula T(A) is defined by induction on the complexity of A: for any propositional variable , As negation is in intuitionistic logic defined by , we also have T is called the Gödel translation or Gödel–McKinsey–Tarski translation.

Discrete mathematics is a discipline with applications to almost all areas of study. It provides a set of indispensable tools to computer science in particular. This course reviews (familiar) topics a

Branche des mathématiques en lien avec le fondement des mathématiques et l'informatique théorique. Le cours est centré sur la logique du 1er ordre et l'articulation entre syntaxe et sémantique.

Le cours se concentre sur l'examen interdisciplinaire de phénomènes associatifs et émotionnels et de leurs principes structurants; ordonné autour d'un thème déterminant pour la théorie et la pratique

Portes logiques et élimination des dangers EE-110: Logic systems (for MT)

Explore les portes logiques, l'élimination des risques, les ALU, les compteurs et les registres à décalage dans la technologie des semi-conducteurs.

Logique propositionnelle : bases et applications CS-101: Advanced information, computation, communication I

Couvre les bases de la logique propositionnelle, son histoire, son langage et ses applications informatiques.

Calcul séquentiel: bases et applications CS-550: Formal verification

Couvre les bases et les applications du calcul séquentiel en logique et théorie des preuves, y compris l'élimination des coupes et l'analyse des preuves pratiques.