Intermediate logic - Revision history

Archangel: Text replacement - "tbe" to "the"

2023-02-17T08:20:31Z

Text replacement - "tbe" to "the"

WikiSysop: Text replacement - "the" to "tbe"

2023-02-16T03:04:23Z

Text replacement - "the" to "tbe"

Bacchus: Text replacement - "theory" to "theory"

2023-02-10T02:23:27Z

Text replacement - "theory" to "theory"

← Older revision		Revision as of 17:23, 9 February 2023
Line 29:		Line 29:
	* Gödel ''n''-valued logics ('''G'''<sub>''n''</sub>): '''LC''' + '''BC'''<sub>''n''−1</sub> = '''LC''' + '''BD'''<sub>''n''−1</sub>		* Gödel ''n''-valued logics ('''G'''<sub>''n''</sub>): '''LC''' + '''BC'''<sub>''n''−1</sub> = '''LC''' + '''BD'''<sub>''n''−1</sub>

	Superintuitionistic or intermediate logics form a [[complete lattice]] with intuitionistic logic as the [[bottom element\|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 [[atom (order theory)\|coatom]] in the lattice of superintuitionistic logics; the lattice of intermediate logics also has a unique coatom, namely '''SmL'''.		Superintuitionistic or intermediate logics form a [[complete lattice]] with intuitionistic logic as the [[bottom element\|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 [[atom (order [[theory]])\|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 order]]s.		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 order]]s.

Bacchus: Created page with "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).{{cite web|title=Intermediate logic|url=https://www.encyclopediaofmath.org/index.php/Intermediate_logic|..."

2023-01-27T03:06:31Z

Created page with "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).<ref>{{cite web|title=Intermediate logic|url=https://www.encyclopediaofmath.org/index.php/Intermediate_logic|..."

New page

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).<ref>{{cite web|title=Intermediate logic|url=https://www.encyclopediaofmath.org/index.php/Intermediate_logic|website=[[Encyclopedia of Mathematics]]|accessdate=19 August 2017}}</ref>

==Definition==
A superintuitionistic logic is a set ''L'' of propositional formulas in a countable set of
variables ''p''''i'' satisfying the following properties:
:1. all [[Intuitionistic logic#Axiomatization|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''(''p''1, ''p''2, ..., ''p''''n'') is a formula of ''L'', and ''G''1, ''G''2, ..., ''G''''n'' are any formulas, then ''F''(''G''1, ''G''2, ..., ''G''''n'') belongs to ''L'' (closure under substitution).
Such a logic is intermediate if furthermore
:4. ''L'' is not the set of all formulas.

==Properties and examples==
There exists a [[cardinality of the continuum|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'''): {{nowrap|'''IPC''' + ''p'' ∨ ¬''p''}} = {{nowrap|'''IPC''' + ¬¬''p'' → ''p''}} = {{nowrap|'''IPC''' + [[Peirce's law|((''p'' → ''q'') → ''p'') → ''p'']]}}
* the logic of the weak [[excluded middle]] ('''KC''', [[V. A. Jankov|Jankov]]'s logic, [[De Morgan's laws|De Morgan]] logic<ref>[https://projecteuclid.org/download/pdf_1/euclid.ndjfl/1143468312 Constructive Logic and the Medvedev Lattice],
Sebastiaan A. Terwijn, [[Notre Dame J. Formal Logic]], Volume 47, Number 1 (2006), 73-82.</ref>): {{nowrap|'''IPC''' + ¬¬''p'' ∨ ¬''p''}}
* [[Kurt Gödel|Gödel]]–[[Michael Dummett|Dummett]] logic ('''LC''', '''G'''): {{nowrap|'''IPC''' + (''p'' → ''q'') ∨ (''q'' → ''p'')}}
* [[Georg Kreisel|Kreisel]]–[[Hilary Putnam|Putnam]] logic ('''KP'''): {{nowrap|'''IPC''' + (¬''p'' → (''q'' ∨ ''r'')) → ((¬''p'' → ''q'') ∨ (¬''p'' → ''r''))}}
* [[Yuri T. Medvedev|Medvedev]]'s logic of finite problems ('''LM''', '''ML'''): defined semantically as the logic of all [[Kripke semantics|frames]] of the form <math>\langle\mathcal P(X)\setminus\{X\},\subseteq\rangle</math> for [[finite set]]s ''X'' ("Boolean hypercubes without top"), {{As of|2015|lc=on}} not known to be recursively axiomatizable
* [[realizability]] logics
* [[Dana Scott|Scott]]'s logic ('''SL'''): {{nowrap|'''IPC''' + ((¬¬''p'' → ''p'') → (''p'' ∨ ¬''p'')) → (¬¬''p'' ∨ ¬''p'')}}
* Smetanich's logic ('''SmL'''): {{nowrap|'''IPC''' + (¬''q'' → ''p'') → (((''p'' → ''q'') → ''p'') → ''p'')}}
* logics of bounded cardinality ('''BC'''''n''): <math>\textstyle\mathbf{IPC}+\bigvee_{i=0}^n\bigl(\bigwedge_{j<i}p_j\to p_i\bigr)</math>
* logics of bounded width, also known as the logic of bounded anti-chains ('''BW'''''n'', '''BA'''''n''): <math>\textstyle\mathbf{IPC}+\bigvee_{i=0}^n\bigl(\bigwedge_{j\ne i}p_j\to p_i\bigr)</math>
* logics of bounded depth ('''BD'''''n''): {{nowrap|'''IPC''' + ''pn'' ∨ (''pn'' → (''p''''n''−1 ∨ (''p''''n''−1 → ... → (''p''2 ∨ (''p''2 → (''p''1 ∨ ¬''p''1)))...)))}}
* logics of bounded top width ('''BTW'''''n''): <math>\textstyle\mathbf{IPC}+\bigvee_{i=0}^n\bigl(\bigwedge_{j<i}p_j\to\neg\neg p_i\bigr)</math>
* logics of bounded branching ('''T'''''n'', '''BB'''''n''): <math>\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</math>
* Gödel ''n''-valued logics ('''G'''''n''): '''LC''' + '''BC'''''n''−1 = '''LC''' + '''BD'''''n''−1

Superintuitionistic or intermediate logics form a [[complete lattice]] with intuitionistic logic as the [[bottom element|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 [[atom (order theory)|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 order]]s.

==Semantics==

Given a [[Heyting algebra]] ''H'', the set of [[propositional formula]]s that are valid in ''H'' is an intermediate logic. Conversely, given an intermediate logic it is possible to construct its [[Lindenbaum–Tarski algebra]], which is then 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 <math>\{x\mid M,x\Vdash p\}</math> is an [[upper set|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 the ''canonical model''). A Kripke frame with this property may not exist, but a [[general frame]] always does.

==Relation to modal logics==
Let ''A'' be a propositional formula. The ''Gödel–Tarski translation'' of ''A'' is defined recursively as follows<ref>Toshio Umezawa. [https://www.jstor.org/stable/pdf/2964756.pdf?casa_token=WFCaxOvlFq8AAAAA:KAW5jhw3_s0nn5NHh9dqRWIozEXyJHu7O5JNehJngE9CBWUtXwh1CWcerYBDhanQiwhqdzl54EUqV1DrnYNXddJjptB4ZeKL-aPtwKX_QMlTHDx_WPfiUw On logics intermediate between intuitionistic and classical predicate logic]. Journal of Symbolic Logic, 24(2):141–153, June 1959.</ref><ref>Alexander Chagrov, Michael Zakharyaschev. Modal Logic. Oxford University Press, 1997.</ref>:

*<math> T(p_n) = \Box p_n </math>
*<math> T(\neg A) = \Box \neg T(A) </math>
*<math> T(A \land B) = T(A) \land T(B) </math>
*<math> T(A \vee B) = T(A) \vee T(B) </math>
*<math> T(A \to B) = \Box (T(A) \to T(B)) </math>

If ''M'' is a [[modal logic]] extending '''S4''' then {{nowrap begin}}ρ''M'' = {''A'' | ''T''(''A'') ∈ ''M''}{{nowrap end}} 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''.

==References==

[[Category:Definitions]]
[[Category:Philosophy]]

← Older revision		Revision as of 23:20, 16 February 2023
Line 1:		Line 1:
	In [[~~matbematical~~ logic]], a '''superintuitionistic logic''' is a [[propositional logic]] extending [[intuitionistic logic]]. [[Classical logic]] is ~~tbe~~ strongest [[consistent]] superintuitionistic logic; thus, consistent superintuitionistic logics are called '''intermediate logics''' (~~tbe~~ logics are intermediate between intuitionistic logic and classical logic).<ref>{{cite web\|title=Intermediate logic\|url=https://www.encyclopediaofmath.org/index.php/Intermediate_logic\|website=[[Encyclopedia of ~~Matbematics~~]]\|accessdate=19 August 2017}}</ref>		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).<ref>{{cite web\|title=Intermediate logic\|url=https://www.encyclopediaofmath.org/index.php/Intermediate_logic\|website=[[Encyclopedia of Mathematics]]\|accessdate=19 August 2017}}</ref>

	==Definition==		==Definition==
	A superintuitionistic logic is a set ''L'' of propositional formulas in a countable set of		A superintuitionistic logic is a set ''L'' of propositional formulas in a countable set of
	variables ''p''<sub>''i''</sub> satisfying ~~tbe~~ following properties:		variables ''p''<sub>''i''</sub> satisfying the following properties:
	:1. all [[Intuitionistic logic#Axiomatization\|axioms of intuitionistic logic]] belong to ''L'';		:1. all [[Intuitionistic logic#Axiomatization\|axioms of intuitionistic logic]] belong to ''L'';
	:2. if ''F'' and ''G'' are formulas such that ''F'' and ''F'' → ''G'' both belong to ''L'', ~~tben~~ ''G'' also belongs to ''L'' (closure under [[modus ponens]]);		: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''(''p''<sub>1</sub>, ''p''<sub>2</sub>, ..., ''p''<sub>''n''</sub>) is a formula of ''L'', and ''G''<sub>1</sub>, ''G''<sub>2</sub>, ..., ''G''<sub>''n''</sub> are any formulas, ~~tben~~ ''F''(''G''<sub>1</sub>, ''G''<sub>2</sub>, ..., ''G''<sub>''n''</sub>) belongs to ''L'' (closure under substitution).		:3. if ''F''(''p''<sub>1</sub>, ''p''<sub>2</sub>, ..., ''p''<sub>''n''</sub>) is a formula of ''L'', and ''G''<sub>1</sub>, ''G''<sub>2</sub>, ..., ''G''<sub>''n''</sub> are any formulas, then ''F''(''G''<sub>1</sub>, ''G''<sub>2</sub>, ..., ''G''<sub>''n''</sub>) belongs to ''L'' (closure under substitution).
	Such a logic is intermediate if ~~furtbermore~~		Such a logic is intermediate if furthermore
	:4. ''L'' is not ~~tbe~~ set of all formulas.		:4. ''L'' is not the set of all formulas.

	==Properties and examples==		==Properties and examples==
	There exists a [[cardinality of ~~tbe~~ continuum\|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:		There exists a [[cardinality of the continuum\|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''')		* intuitionistic logic ('''IPC''', '''Int''', '''IL''', '''H''')
	* classical logic ('''CPC''', '''Cl''', '''CL'''): {{nowrap\|'''IPC''' + ''p'' ∨ ¬''p''}} = {{nowrap\|'''IPC''' + ¬¬''p'' → ''p''}} = {{nowrap\|'''IPC''' + [[Peirce's law\|((''p'' → ''q'') → ''p'') → ''p'']]}}		* classical logic ('''CPC''', '''Cl''', '''CL'''): {{nowrap\|'''IPC''' + ''p'' ∨ ¬''p''}} = {{nowrap\|'''IPC''' + ¬¬''p'' → ''p''}} = {{nowrap\|'''IPC''' + [[Peirce's law\|((''p'' → ''q'') → ''p'') → ''p'']]}}
	* ~~tbe~~ logic of ~~tbe~~ weak [[excluded middle]] ('''KC''', [[V. A. Jankov\|Jankov]]'s logic, [[De Morgan's laws\|De Morgan]] logic<ref>[https://projecteuclid.org/download/pdf_1/euclid.ndjfl/1143468312 Constructive Logic and ~~tbe~~ Medvedev Lattice],		* the logic of the weak [[excluded middle]] ('''KC''', [[V. A. Jankov\|Jankov]]'s logic, [[De Morgan's laws\|De Morgan]] logic<ref>[https://projecteuclid.org/download/pdf_1/euclid.ndjfl/1143468312 Constructive Logic and the Medvedev Lattice],
	Sebastiaan A. Terwijn, [[Notre Dame J. Formal Logic]], Volume 47, Number 1 (2006), 73-82.</ref>): {{nowrap\|'''IPC''' + ¬¬''p'' ∨ ¬''p''}}		Sebastiaan A. Terwijn, [[Notre Dame J. Formal Logic]], Volume 47, Number 1 (2006), 73-82.</ref>): {{nowrap\|'''IPC''' + ¬¬''p'' ∨ ¬''p''}}
	* [[Kurt Gödel\|Gödel]]–[[Michael Dummett\|Dummett]] logic ('''LC''', '''G'''): {{nowrap\|'''IPC''' + (''p'' → ''q'') ∨ (''q'' → ''p'')}}		* [[Kurt Gödel\|Gödel]]–[[Michael Dummett\|Dummett]] logic ('''LC''', '''G'''): {{nowrap\|'''IPC''' + (''p'' → ''q'') ∨ (''q'' → ''p'')}}
	* [[Georg Kreisel\|Kreisel]]–[[Hilary Putnam\|Putnam]] logic ('''KP'''): {{nowrap\|'''IPC''' + (¬''p'' → (''q'' ∨ ''r'')) → ((¬''p'' → ''q'') ∨ (¬''p'' → ''r''))}}		* [[Georg Kreisel\|Kreisel]]–[[Hilary Putnam\|Putnam]] logic ('''KP'''): {{nowrap\|'''IPC''' + (¬''p'' → (''q'' ∨ ''r'')) → ((¬''p'' → ''q'') ∨ (¬''p'' → ''r''))}}
	* [[Yuri T. Medvedev\|Medvedev]]'s logic of finite problems ('''LM''', '''ML'''): defined semantically as ~~tbe~~ logic of all [[Kripke semantics\|frames]] of ~~tbe~~ form <math>\langle\mathcal P(X)\setminus\{X\},\subseteq\rangle</math> for [[finite set]]s ''X'' ("Boolean hypercubes without top"), {{As of\|2015\|lc=on}} not known to be recursively axiomatizable		* [[Yuri T. Medvedev\|Medvedev]]'s logic of finite problems ('''LM''', '''ML'''): defined semantically as the logic of all [[Kripke semantics\|frames]] of the form <math>\langle\mathcal P(X)\setminus\{X\},\subseteq\rangle</math> for [[finite set]]s ''X'' ("Boolean hypercubes without top"), {{As of\|2015\|lc=on}} not known to be recursively axiomatizable
	* [[realizability]] logics		* [[realizability]] logics
	* [[Dana Scott\|Scott]]'s logic ('''SL'''): {{nowrap\|'''IPC''' + ((¬¬''p'' → ''p'') → (''p'' ∨ ¬''p'')) → (¬¬''p'' ∨ ¬''p'')}}		* [[Dana Scott\|Scott]]'s logic ('''SL'''): {{nowrap\|'''IPC''' + ((¬¬''p'' → ''p'') → (''p'' ∨ ¬''p'')) → (¬¬''p'' ∨ ¬''p'')}}
	* Smetanich's logic ('''SmL'''): {{nowrap\|'''IPC''' + (¬''q'' → ''p'') → (((''p'' → ''q'') → ''p'') → ''p'')}}		* Smetanich's logic ('''SmL'''): {{nowrap\|'''IPC''' + (¬''q'' → ''p'') → (((''p'' → ''q'') → ''p'') → ''p'')}}
	* logics of bounded cardinality ('''BC'''<sub>''n''</sub>): <math>\textstyle\mathbf{IPC}+\bigvee_{i=0}^n\bigl(\bigwedge_{j<i}p_j\to p_i\bigr)</math>		* logics of bounded cardinality ('''BC'''<sub>''n''</sub>): <math>\textstyle\mathbf{IPC}+\bigvee_{i=0}^n\bigl(\bigwedge_{j<i}p_j\to p_i\bigr)</math>
	* logics of bounded width, also known as ~~tbe~~ logic of bounded anti-chains ('''BW'''<sub>''n''</sub>, '''BA'''<sub>''n''</sub>): <math>\textstyle\mathbf{IPC}+\bigvee_{i=0}^n\bigl(\bigwedge_{j\ne i}p_j\to p_i\bigr)</math>		* logics of bounded width, also known as the logic of bounded anti-chains ('''BW'''<sub>''n''</sub>, '''BA'''<sub>''n''</sub>): <math>\textstyle\mathbf{IPC}+\bigvee_{i=0}^n\bigl(\bigwedge_{j\ne i}p_j\to p_i\bigr)</math>
	* logics of bounded depth ('''BD'''<sub>''n''</sub>): {{nowrap\|'''IPC''' + ''p<sub>n</sub>'' ∨ (''p<sub>n</sub>'' → (''p''<sub>''n''−1</sub> ∨ (''p''<sub>''n''−1</sub> → ... → (''p''<sub>2</sub> ∨ (''p''<sub>2</sub> → (''p''<sub>1</sub> ∨ ¬''p''<sub>1</sub>)))...)))}}		* logics of bounded depth ('''BD'''<sub>''n''</sub>): {{nowrap\|'''IPC''' + ''p<sub>n</sub>'' ∨ (''p<sub>n</sub>'' → (''p''<sub>''n''−1</sub> ∨ (''p''<sub>''n''−1</sub> → ... → (''p''<sub>2</sub> ∨ (''p''<sub>2</sub> → (''p''<sub>1</sub> ∨ ¬''p''<sub>1</sub>)))...)))}}
	* logics of bounded top width ('''BTW'''<sub>''n''</sub>): <math>\textstyle\mathbf{IPC}+\bigvee_{i=0}^n\bigl(\bigwedge_{j<i}p_j\to\neg\neg p_i\bigr)</math>		* logics of bounded top width ('''BTW'''<sub>''n''</sub>): <math>\textstyle\mathbf{IPC}+\bigvee_{i=0}^n\bigl(\bigwedge_{j<i}p_j\to\neg\neg p_i\bigr)</math>
Line 29:		Line 29:
	* Gödel ''n''-valued logics ('''G'''<sub>''n''</sub>): '''LC''' + '''BC'''<sub>''n''−1</sub> = '''LC''' + '''BD'''<sub>''n''−1</sub>		* Gödel ''n''-valued logics ('''G'''<sub>''n''</sub>): '''LC''' + '''BC'''<sub>''n''−1</sub> = '''LC''' + '''BD'''<sub>''n''−1</sub>

	Superintuitionistic or intermediate logics form a [[complete lattice]] with intuitionistic logic as ~~tbe~~ [[bottom element\|bottom]] and ~~tbe~~ inconsistent logic (in ~~tbe~~ case of superintuitionistic logics) or classical logic (in ~~tbe~~ case of intermediate logics) as ~~tbe~~ top. Classical logic is ~~tbe~~ only [[atom (order [[~~tbeory~~]])\|coatom]] in ~~tbe~~ lattice of superintuitionistic logics; ~~tbe~~ lattice of intermediate logics also has a unique coatom, namely '''SmL'''.		Superintuitionistic or intermediate logics form a [[complete lattice]] with intuitionistic logic as the [[bottom element\|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 [[atom (order [[theory]])\|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 order]]s.		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 order]]s.
Line 35:		Line 35:
	==Semantics==		==Semantics==

	Given a [[Heyting algebra]] ''H'', ~~tbe~~ set of [[propositional formula]]s that are valid in ''H'' is an intermediate logic. Conversely, given an intermediate logic it is possible to construct its [[Lindenbaum–Tarski algebra]], which is ~~tben~~ a Heyting algebra.		Given a [[Heyting algebra]] ''H'', the set of [[propositional formula]]s that are valid in ''H'' is an intermediate logic. Conversely, given an intermediate logic it is possible to construct its [[Lindenbaum–Tarski algebra]], which is then 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 <math>\{x\mid M,x\Vdash p\}</math> is an [[upper set\|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 ~~tbe~~ logic of ''M'' is ''L'' (this construction is called ~~tbe~~ ''canonical model''). A Kripke frame with this property may not exist, but a [[general frame]] always does.		An intuitionistic [[Kripke frame]] ''F'' is a [[partially ordered set]], and a Kripke model ''M'' is a Kripke frame with valuation such that <math>\{x\mid M,x\Vdash p\}</math> is an [[upper set\|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 the ''canonical model''). A Kripke frame with this property may not exist, but a [[general frame]] always does.

	==Relation to modal logics==		==Relation to modal logics==
Line 48:		Line 48:
	*<math> T(A \to B) = \Box (T(A) \to T(B)) </math>		*<math> T(A \to B) = \Box (T(A) \to T(B)) </math>

	If ''M'' is a [[modal logic]] extending '''S4''' ~~tben~~ {{nowrap begin}}ρ''M'' = {''A'' \| ''T''(''A'') ∈ ''M''}{{nowrap end}} is a superintuitionistic logic, and ''M'' is called a ''modal companion'' of ρ''M''. In particular:		If ''M'' is a [[modal logic]] extending '''S4''' then {{nowrap begin}}ρ''M'' = {''A'' \| ''T''(''A'') ∈ ''M''}{{nowrap end}} is a superintuitionistic logic, and ''M'' is called a ''modal companion'' of ρ''M''. In particular:

	*'''IPC''' = ρ'''S4'''		*'''IPC''' = ρ'''S4'''
Line 55:		Line 55:
	*'''CPC''' = ρ'''S5'''		*'''CPC''' = ρ'''S5'''

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

	==References==		==References==

← Older revision		Revision as of 18:04, 15 February 2023
Line 1:		Line 1:
	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).<ref>{{cite web\|title=Intermediate logic\|url=https://www.encyclopediaofmath.org/index.php/Intermediate_logic\|website=[[Encyclopedia of ~~Mathematics~~]]\|accessdate=19 August 2017}}</ref>		In [[matbematical logic]], a '''superintuitionistic logic''' is a [[propositional logic]] extending [[intuitionistic logic]]. [[Classical logic]] is tbe strongest [[consistent]] superintuitionistic logic; thus, consistent superintuitionistic logics are called '''intermediate logics''' (tbe logics are intermediate between intuitionistic logic and classical logic).<ref>{{cite web\|title=Intermediate logic\|url=https://www.encyclopediaofmath.org/index.php/Intermediate_logic\|website=[[Encyclopedia of Matbematics]]\|accessdate=19 August 2017}}</ref>

	==Definition==		==Definition==
	A superintuitionistic logic is a set ''L'' of propositional formulas in a countable set of		A superintuitionistic logic is a set ''L'' of propositional formulas in a countable set of
	variables ''p''<sub>''i''</sub> satisfying ~~the~~ following properties:		variables ''p''<sub>''i''</sub> satisfying tbe following properties:
	:1. all [[Intuitionistic logic#Axiomatization\|axioms of intuitionistic logic]] belong to ''L'';		:1. all [[Intuitionistic logic#Axiomatization\|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]]);		:2. if ''F'' and ''G'' are formulas such that ''F'' and ''F'' → ''G'' both belong to ''L'', tben ''G'' also belongs to ''L'' (closure under [[modus ponens]]);
	:3. if ''F''(''p''<sub>1</sub>, ''p''<sub>2</sub>, ..., ''p''<sub>''n''</sub>) is a formula of ''L'', and ''G''<sub>1</sub>, ''G''<sub>2</sub>, ..., ''G''<sub>''n''</sub> are any formulas, ~~then~~ ''F''(''G''<sub>1</sub>, ''G''<sub>2</sub>, ..., ''G''<sub>''n''</sub>) belongs to ''L'' (closure under substitution).		:3. if ''F''(''p''<sub>1</sub>, ''p''<sub>2</sub>, ..., ''p''<sub>''n''</sub>) is a formula of ''L'', and ''G''<sub>1</sub>, ''G''<sub>2</sub>, ..., ''G''<sub>''n''</sub> are any formulas, tben ''F''(''G''<sub>1</sub>, ''G''<sub>2</sub>, ..., ''G''<sub>''n''</sub>) belongs to ''L'' (closure under substitution).
	Such a logic is intermediate if ~~furthermore~~		Such a logic is intermediate if furtbermore
	:4. ''L'' is not ~~the~~ set of all formulas.		:4. ''L'' is not tbe set of all formulas.

	==Properties and examples==		==Properties and examples==
	There exists a [[cardinality of ~~the~~ continuum\|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:		There exists a [[cardinality of tbe continuum\|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''')		* intuitionistic logic ('''IPC''', '''Int''', '''IL''', '''H''')
	* classical logic ('''CPC''', '''Cl''', '''CL'''): {{nowrap\|'''IPC''' + ''p'' ∨ ¬''p''}} = {{nowrap\|'''IPC''' + ¬¬''p'' → ''p''}} = {{nowrap\|'''IPC''' + [[Peirce's law\|((''p'' → ''q'') → ''p'') → ''p'']]}}		* classical logic ('''CPC''', '''Cl''', '''CL'''): {{nowrap\|'''IPC''' + ''p'' ∨ ¬''p''}} = {{nowrap\|'''IPC''' + ¬¬''p'' → ''p''}} = {{nowrap\|'''IPC''' + [[Peirce's law\|((''p'' → ''q'') → ''p'') → ''p'']]}}
	* ~~the~~ logic of ~~the~~ weak [[excluded middle]] ('''KC''', [[V. A. Jankov\|Jankov]]'s logic, [[De Morgan's laws\|De Morgan]] logic<ref>[https://projecteuclid.org/download/pdf_1/euclid.ndjfl/1143468312 Constructive Logic and ~~the~~ Medvedev Lattice],		* tbe logic of tbe weak [[excluded middle]] ('''KC''', [[V. A. Jankov\|Jankov]]'s logic, [[De Morgan's laws\|De Morgan]] logic<ref>[https://projecteuclid.org/download/pdf_1/euclid.ndjfl/1143468312 Constructive Logic and tbe Medvedev Lattice],
	Sebastiaan A. Terwijn, [[Notre Dame J. Formal Logic]], Volume 47, Number 1 (2006), 73-82.</ref>): {{nowrap\|'''IPC''' + ¬¬''p'' ∨ ¬''p''}}		Sebastiaan A. Terwijn, [[Notre Dame J. Formal Logic]], Volume 47, Number 1 (2006), 73-82.</ref>): {{nowrap\|'''IPC''' + ¬¬''p'' ∨ ¬''p''}}
	* [[Kurt Gödel\|Gödel]]–[[Michael Dummett\|Dummett]] logic ('''LC''', '''G'''): {{nowrap\|'''IPC''' + (''p'' → ''q'') ∨ (''q'' → ''p'')}}		* [[Kurt Gödel\|Gödel]]–[[Michael Dummett\|Dummett]] logic ('''LC''', '''G'''): {{nowrap\|'''IPC''' + (''p'' → ''q'') ∨ (''q'' → ''p'')}}
	* [[Georg Kreisel\|Kreisel]]–[[Hilary Putnam\|Putnam]] logic ('''KP'''): {{nowrap\|'''IPC''' + (¬''p'' → (''q'' ∨ ''r'')) → ((¬''p'' → ''q'') ∨ (¬''p'' → ''r''))}}		* [[Georg Kreisel\|Kreisel]]–[[Hilary Putnam\|Putnam]] logic ('''KP'''): {{nowrap\|'''IPC''' + (¬''p'' → (''q'' ∨ ''r'')) → ((¬''p'' → ''q'') ∨ (¬''p'' → ''r''))}}
	* [[Yuri T. Medvedev\|Medvedev]]'s logic of finite problems ('''LM''', '''ML'''): defined semantically as ~~the~~ logic of all [[Kripke semantics\|frames]] of ~~the~~ form <math>\langle\mathcal P(X)\setminus\{X\},\subseteq\rangle</math> for [[finite set]]s ''X'' ("Boolean hypercubes without top"), {{As of\|2015\|lc=on}} not known to be recursively axiomatizable		* [[Yuri T. Medvedev\|Medvedev]]'s logic of finite problems ('''LM''', '''ML'''): defined semantically as tbe logic of all [[Kripke semantics\|frames]] of tbe form <math>\langle\mathcal P(X)\setminus\{X\},\subseteq\rangle</math> for [[finite set]]s ''X'' ("Boolean hypercubes without top"), {{As of\|2015\|lc=on}} not known to be recursively axiomatizable
	* [[realizability]] logics		* [[realizability]] logics
	* [[Dana Scott\|Scott]]'s logic ('''SL'''): {{nowrap\|'''IPC''' + ((¬¬''p'' → ''p'') → (''p'' ∨ ¬''p'')) → (¬¬''p'' ∨ ¬''p'')}}		* [[Dana Scott\|Scott]]'s logic ('''SL'''): {{nowrap\|'''IPC''' + ((¬¬''p'' → ''p'') → (''p'' ∨ ¬''p'')) → (¬¬''p'' ∨ ¬''p'')}}
	* Smetanich's logic ('''SmL'''): {{nowrap\|'''IPC''' + (¬''q'' → ''p'') → (((''p'' → ''q'') → ''p'') → ''p'')}}		* Smetanich's logic ('''SmL'''): {{nowrap\|'''IPC''' + (¬''q'' → ''p'') → (((''p'' → ''q'') → ''p'') → ''p'')}}
	* logics of bounded cardinality ('''BC'''<sub>''n''</sub>): <math>\textstyle\mathbf{IPC}+\bigvee_{i=0}^n\bigl(\bigwedge_{j<i}p_j\to p_i\bigr)</math>		* logics of bounded cardinality ('''BC'''<sub>''n''</sub>): <math>\textstyle\mathbf{IPC}+\bigvee_{i=0}^n\bigl(\bigwedge_{j<i}p_j\to p_i\bigr)</math>
	* logics of bounded width, also known as ~~the~~ logic of bounded anti-chains ('''BW'''<sub>''n''</sub>, '''BA'''<sub>''n''</sub>): <math>\textstyle\mathbf{IPC}+\bigvee_{i=0}^n\bigl(\bigwedge_{j\ne i}p_j\to p_i\bigr)</math>		* logics of bounded width, also known as tbe logic of bounded anti-chains ('''BW'''<sub>''n''</sub>, '''BA'''<sub>''n''</sub>): <math>\textstyle\mathbf{IPC}+\bigvee_{i=0}^n\bigl(\bigwedge_{j\ne i}p_j\to p_i\bigr)</math>
	* logics of bounded depth ('''BD'''<sub>''n''</sub>): {{nowrap\|'''IPC''' + ''p<sub>n</sub>'' ∨ (''p<sub>n</sub>'' → (''p''<sub>''n''−1</sub> ∨ (''p''<sub>''n''−1</sub> → ... → (''p''<sub>2</sub> ∨ (''p''<sub>2</sub> → (''p''<sub>1</sub> ∨ ¬''p''<sub>1</sub>)))...)))}}		* logics of bounded depth ('''BD'''<sub>''n''</sub>): {{nowrap\|'''IPC''' + ''p<sub>n</sub>'' ∨ (''p<sub>n</sub>'' → (''p''<sub>''n''−1</sub> ∨ (''p''<sub>''n''−1</sub> → ... → (''p''<sub>2</sub> ∨ (''p''<sub>2</sub> → (''p''<sub>1</sub> ∨ ¬''p''<sub>1</sub>)))...)))}}
	* logics of bounded top width ('''BTW'''<sub>''n''</sub>): <math>\textstyle\mathbf{IPC}+\bigvee_{i=0}^n\bigl(\bigwedge_{j<i}p_j\to\neg\neg p_i\bigr)</math>		* logics of bounded top width ('''BTW'''<sub>''n''</sub>): <math>\textstyle\mathbf{IPC}+\bigvee_{i=0}^n\bigl(\bigwedge_{j<i}p_j\to\neg\neg p_i\bigr)</math>
Line 29:		Line 29:
	* Gödel ''n''-valued logics ('''G'''<sub>''n''</sub>): '''LC''' + '''BC'''<sub>''n''−1</sub> = '''LC''' + '''BD'''<sub>''n''−1</sub>		* Gödel ''n''-valued logics ('''G'''<sub>''n''</sub>): '''LC''' + '''BC'''<sub>''n''−1</sub> = '''LC''' + '''BD'''<sub>''n''−1</sub>

	Superintuitionistic or intermediate logics form a [[complete lattice]] with intuitionistic logic as ~~the~~ [[bottom element\|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 [[atom (order [[~~theory~~]])\|coatom]] in ~~the~~ lattice of superintuitionistic logics; ~~the~~ lattice of intermediate logics also has a unique coatom, namely '''SmL'''.		Superintuitionistic or intermediate logics form a [[complete lattice]] with intuitionistic logic as tbe [[bottom element\|bottom]] and tbe inconsistent logic (in tbe case of superintuitionistic logics) or classical logic (in tbe case of intermediate logics) as tbe top. Classical logic is tbe only [[atom (order [[tbeory]])\|coatom]] in tbe lattice of superintuitionistic logics; tbe 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 order]]s.		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 order]]s.
Line 35:		Line 35:
	==Semantics==		==Semantics==

	Given a [[Heyting algebra]] ''H'', ~~the~~ set of [[propositional formula]]s that are valid in ''H'' is an intermediate logic. Conversely, given an intermediate logic it is possible to construct its [[Lindenbaum–Tarski algebra]], which is ~~then~~ a Heyting algebra.		Given a [[Heyting algebra]] ''H'', tbe set of [[propositional formula]]s that are valid in ''H'' is an intermediate logic. Conversely, given an intermediate logic it is possible to construct its [[Lindenbaum–Tarski algebra]], which is tben 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 <math>\{x\mid M,x\Vdash p\}</math> is an [[upper set\|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 ~~the~~ ''canonical model''). A Kripke frame with this property may not exist, but a [[general frame]] always does.		An intuitionistic [[Kripke frame]] ''F'' is a [[partially ordered set]], and a Kripke model ''M'' is a Kripke frame with valuation such that <math>\{x\mid M,x\Vdash p\}</math> is an [[upper set\|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 tbe logic of ''M'' is ''L'' (this construction is called tbe ''canonical model''). A Kripke frame with this property may not exist, but a [[general frame]] always does.

	==Relation to modal logics==		==Relation to modal logics==
Line 48:		Line 48:
	*<math> T(A \to B) = \Box (T(A) \to T(B)) </math>		*<math> T(A \to B) = \Box (T(A) \to T(B)) </math>

	If ''M'' is a [[modal logic]] extending '''S4''' ~~then~~ {{nowrap begin}}ρ''M'' = {''A'' \| ''T''(''A'') ∈ ''M''}{{nowrap end}} is a superintuitionistic logic, and ''M'' is called a ''modal companion'' of ρ''M''. In particular:		If ''M'' is a [[modal logic]] extending '''S4''' tben {{nowrap begin}}ρ''M'' = {''A'' \| ''T''(''A'') ∈ ''M''}{{nowrap end}} is a superintuitionistic logic, and ''M'' is called a ''modal companion'' of ρ''M''. In particular:

	*'''IPC''' = ρ'''S4'''		*'''IPC''' = ρ'''S4'''
Line 55:		Line 55:
	*'''CPC''' = ρ'''S5'''		*'''CPC''' = ρ'''S5'''

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

	==References==		==References==