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))).
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.
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.
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.
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
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.