Some intuitionistic equivalents of classical principles for degree 2 formulas (Q2368911): Difference between revisions
From MaRDI portal
Created a new Item |
Added link to MaRDI item. |
||
links / mardi / name | links / mardi / name | ||
Revision as of 19:04, 2 February 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Some intuitionistic equivalents of classical principles for degree 2 formulas |
scientific article |
Statements
Some intuitionistic equivalents of classical principles for degree 2 formulas (English)
0 references
28 April 2006
0 references
This paper is concerned with the study of intuitionistic equivalences between mathematical theorems in frequent use, on the one hand, and classical logical principles like Excluded Middle, Markov's Principle, and König's Lemma restricted to \(\Sigma^0_2\)-formulas, on the other hand, provided universal quantification over maps is restricted to (effectively given families of) recursive maps. Among the mathematical statements and definitions treated are (weak) infinity axioms, various definitions of the notion of quasi-well-ordering, convergence principles, and several versions of Dickson's Lemma. For example, it is shown that the restriction of Excluded Middle to \(\Sigma^0_2\)-formulas is equivalent (in the context of intuitionistic arithmetic with function quantifiers and Dependent Choice) to the principle that any effectively decidable set is either finite or infinite, that the said version of Markov's Principle is equivalent both to the principle ``every recursive sequence over the set of natural numbers which does not change value infinitely many times is stationary'' and to ``any effectively decidable set which is not infinite is finite'', and that König's Lemma for \(\Sigma^0_2\)-formulas is likewise equivalent to one version of Dickson's Lemma (for recursive sequences).
0 references
excluded middle
0 references
Markov's principle
0 references
König's lemma
0 references
reverse mathematics
0 references
intuitionistic logic
0 references