Constructivism in mathematics. An introduction. Volume II

zbMath0661.03047MaRDI QIDQ1188522

A. S. Troelstra, Dirk van Dalen

Publication date: 17 September 1992

Published in: Studies in Logic and the Foundations of Mathematics (Search for Journal in Brave)

zbMATH Keywords

higher-order logicalgebraconstructive set theoryBishop's constructive mathematicssitesBrouwer's intuitionismlawless sequencesMarkov's constructive recursive mathematicsmetamathematics of constructivismChoice sequencesFinite type arithmeticMartin-Löf systemsProof theory of intuitionistic logicSemantical completenessSheavestheories of operatorstopology of metric spaces

Mathematics Subject Classification ID

Constructive and recursive analysis (03F60) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Other constructive mathematics (03F65) Metamathematics of constructive systems (03F50) Intuitionistic mathematics (03F55)

Related Items

On co-Filters in Semigroups with Apartness, THE AXIOM OF CHOICE IS FALSE INTUITIONISTICALLY (IN MOST CONTEXTS), AFFINE LOGIC FOR CONSTRUCTIVE MATHEMATICS, Constructive set theoretic models of typed combinatory logic, Principles of bar induction and continuity on Baire space, ON THE UNCOUNTABILITY OF, On Church’s thesis in cubical assemblies, Categorical reconstruction of a reduction free normalization proof, Converse extensionality and apartness, Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice, Unnamed Item, Unnamed Item, A MARRIAGE OF BROUWER’S INTUITIONISM AND HILBERT’S FINITISM I: ARITHMETIC, EPSILON THEOREMS IN INTERMEDIATE LOGICS, Realizability Models Separating Various Fan Theorems, Constructive sheaf models of type theory, THE JACOBSON RADICAL OF A PROPOSITIONAL THEORY, Unnamed Item, Intuitive counterexamples for constructive fallacies, Decidable variables for constructive logics, IMPROVING STRONG NEGATION, A Note on the Internal Logic of Constructive Mathematics: The Gel’fond-Schneider Theorem in Transcendental Number Theory, On feasible numbers, Program extraction from classical proofs, Intuitionistic mereology, A CLASSICAL MODAL THEORY OF LAWLESS SEQUENCES, Conservativity between logics and typed λ calculi, EXTENSIONAL REALIZABILITY AND CHOICE FOR DEPENDENT TYPES IN INTUITIONISTIC SET THEORY, Time and Gödel: fuzzy temporal reasoning in PSPACE, Choice and independence of premise rules in intuitionistic set theory, A note on equality in finite‐type arithmetic, A first-order expansion of Artemov and Protopopescu's intuitionistic epistemic logic, Some forms of excluded middle for linear orders, Bishop's Lemma, Formally continuous functions on Baire space, A novel approach to equality, Embeddings between partial combinatory algebras, Projective sets, intuitionistically, Natural deduction calculi for classical and intuitionistic S5, Revisiting the conservativity of fixpoints over intuitionistic arithmetic, CONSERVATION THEOREMS ON SEMI-CLASSICAL ARITHMETIC, Double negation as minimal negation, Apartness, sharp elements, and the Scott topology of domains, Game semantics of Martin-Löf type theory, Platonism and the Proto-ontology of Mathematics: Learning from the Axiom of Choice, Five stages of accepting constructive mathematics, Quantitative continuity and Computable Analysis in Coq, Empirical Negation, Co-negation and Contraposition Rule I: Semantical Investigations, Extensional constructive real analysis via locators, Implementing Real Numbers With RZ, Converses of Bishop's lemma on located sets, The weak-operator sequential continuity of left multiplication, Rules and arithmetics, The Functional Interpretation of Direct Computations, Co-quasiordered residuated systems: An introduction, THE -PROVABILITY LOGIC OF, The pleasures of anticipation: Enriching intuitionistic logic, Refined program extraction from classical proofs, The axiomatization of randomness, Unnamed Item, CONSTRUCTIVE REFLECTIVITY PRINCIPLES FOR REGULAR THEORIES, COMPUTABILITY THEORY, NONSTANDARD ANALYSIS, AND THEIR CONNECTIONS, SEPARATING THE FAN THEOREM AND ITS WEAKENINGS II, Topos Theory in Montréal in the 1970s: My Personal Involvement, A New Translation for Semi-classical Theories — Backtracking without CPS, A First Look into a Formal and Constructive Approach for Discrete Geometry Using Nonstandard Analysis, Unnamed Item, Prawitz, Proofs, and Meaning, Explaining Deductive Inference, Constructibility and Geometry, Dependency as Question Entailment, Logic, Counterexamples, and Translation, Proof Theory of Constructive Systems: Inductive Types and Univalence, Computable analysis with applications to dynamic systems, Unnamed Item, On the mathematical and foundational significance of the uncountable, Deriving Natural Deduction Rules from Truth Tables, Unnamed Item, COMPUTABILITY IN PARTIAL COMBINATORY ALGEBRAS, Nets and reverse mathematics, Super-Strict Implications, A continuity principle, a version of Baire's theorem and a boundedness principle, Constructive Recursive Functions, Church’s Thesis, and Brouwer’s Theory of the Creating Subject: Afterthoughts on a Parisian Joint Session, Proof-Theoretic Semantics and Feasibility, Gödel and Intuitionism, Unnamed Item, Truth and Proof in Intuitionism, A Computational Interpretation of Forcing in Type Theory, DECIDABILITY OF ADMISSIBILITY: ON A PROBLEM BY FRIEDMAN AND ITS SOLUTION BY RYBAKOV, An Upper Bound for the Proof-Theoretic Strength of Martin-Löf Type Theory with W-type and One Universe, Constructivism and Metamathematics, Theory of Constructive Semigroups with Apartness – Foundations, Development and Practice, PRENEX NORMAL FORM THEOREMS IN SEMI-CLASSICAL ARITHMETIC, ORDINAL ANALYSIS OF PARTIAL COMBINATORY ALGEBRAS, Higher order functions and Brouwer’s thesis, Perception of BCC-algebras under the Bishops principled-philosophical orientation: BCC-algebra with apartness, Bishop-Style Constructive Reverse Mathematics, On the Borel-Cantelli Lemmas, the Erdős-Rényi Theorem, and the Kochen-Stone Theorem, Extending strongly continuous functions between apartness spaces, Representations of empirical set theories, On theorems of Gödel and Kreisel: Completeness and Markov's principle, Brouwer's weak counterexamples and the creative subject: a critical survey, Intuitionistic completeness and classical logic, Refining the taming of the reverse mathematics zoo, The strength of some Martin-Löf type theories, Reverse mathematics and parameter-free transfer, Natural deduction for intuitionistic linear logic, Axioms for classical, intuitionistic, and paraconsistent hybrid logic, Elementary realizability, On A. Ya. Khinchin's paper `Ideas of intuitionism and the struggle for a subject matter in contemporary mathematics' (1926): a translation with introduction and commentary, Generalized functions with pseudobounded support in constructive mathematics, Innovations in computational type theory using Nuprl, Preservation theorems for bounded formulas, Constructing local optima on a compact interval, Constructive sets in computable sets, Provability in principle and controversial constructivistic principles, Another paradox in naive set-theory, A proof-theoretic account of classical principles of truth, Relating first-order set theories, toposes and categories of classes, Intuitionistic completeness of first-order logic, Monad as modality, Experiments in linear natural deduction, Some principles weaker than Markov's principle, Meaning explanations at higher dimension, To be or not to be constructive, that is not the question, Locating the range of an operator with an adjoint, Topological forcing semantics with settling, From the knowability paradox to the existence of proofs, Synonymous logics, Aligning the weak König lemma, the uniform continuity theorem, and Brouwer's fan theorem, The intermediate value theorem in constructive mathematics without choice, Subminimal negation, Kripke models for classical logic, Locatedness and overt sublocales, The eskolemization of universal quantifiers, From the weak to the strong existence property, The binary expansion and the intermediate value theorem in constructive reverse mathematics, Some axioms for constructive analysis, Compactness notions for an apartness space, Crawley completions of residuated lattices and algebraic completeness of substructural predicate logics, Elementary inductive definitions in HA: From strictly positive towards monotone, Metric spaces in synthetic topology, Two subcategories of apartness spaces, The anti-Specker property, a Heine-Borel property, and uniform continuity, Between constructive mathematics and PROLOG, Recursion over realizability structures, Ishihara's proof technique in constructive analysis, Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017, A continuity principle equivalent to the monotone \(\Pi^0_1\) fan theorem, On behavioural abstraction and behavioural satisfaction in higher-order logic, A semantic hierarchy for intuitionistic logic, Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves, Sets, complements and boundaries, The Zariski spectrum as a formal geometry, Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation, Type-theoretic interpretation of iterated, strictly positive inductive definitions, Polynomial-time Martin-Löf type theory, Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice, Provably recursive functions of constructive and relatively constructive theories, Homomorphisms and chains of Kripke models, Omitting types in an intermediate logic, Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi, A very weak Nullstellensatz over Heyting fields, Kronecker's density theorem and irrational numbers in constructive reverse mathematics, Towards constructive DL for abstraction and refinement, Brouwer's \(\epsilon\)-fixed point and Sperner's lemma, A proof-theoretic characterization of the basic feasible functionals, Explicit mathematics: power types and overloading, Continuum, name and paradox, An intuitionistic completeness theorem for classical predicate logic, Uniform Heyting arithmetic, Glueing continuous functions constructively, A functional interpretation for nonstandard arithmetic, On Brouwer's continuity principle, On the constructive Dedekind reals, Reference and perspective in intuitionistic logics, A semantical proof of De Jongh's theorem, Negationless intuitionism, On the strength of dependent products in the type theory of Martin-Löf, On logics with coimplication, Can constructive mathematics be applied in physics?, Representing scope in intuitionistic deductions, Set based logic programming, Generalized real numbers in constructive mathematics, Mass problems associated with effectively closed sets, Interpretations of intuitionist logic in non-normal modal logics, Functional interpretation of Aczel's constructive set theory, Markov's constructive analysis; a participant's view, Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\), Well-ordering proofs for Martin-Löf type theory, Decidable Kripke models of intuitionistic theories, Some results on cut-elimination, provable well-orderings, induction and reflection, Five observations concerning the intended meaning of the intuitionistic logical constants, Some purely topological models for intuitionistic analysis, A Boolean model of ultrafilters, Markov's principle, Church's thesis and Lindelöf's theorem, Spreads and choice in constructive mathematics., Gentzen calculi for the existence predicate, Constructive Ackermann's interpretation, Proofs, grounds and empty functions: epistemic compulsion in Prawitz's semantics, Relative constructivity, The fundamental problem of general proof theory, Connectification for \(n\)-contraction, A constructive approach to nonstandard analysis, Positive Formulas in Intuitionistic and Minimal Logic, The logic of first order intuitionistic type theory with weak sigma-elimination, Totality in applicative theories, A Minimalist Foundation at Work, Logic in Category Theory, CZF does not have the existence property, Parametric Church's thesis: synthetic computability without choice, Mechanizing common knowledge logic using COQ, Quotienting the delay monad by weak bisimilarity, Creative subject, Beth models and neighbourhood functions, Intuitionistic Provability versus Uniform Provability in $$\mathsf{RCA}$$, Spectra of selfadjoint operators in constructive analysis, Equality and equivalence, intuitionistically, Binary modal companions for subintuitionistic logics, Hard provability logics, Systems of explicit mathematics with non-constructive \(\mu\)-operator. II, A classical view of the intuitionistic continuum, Realizing Brouwer's sequences, A universal algorithm for Krull's theorem, Lifting proofs from countable to uncountable mathematics, Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language, Hermann Weyl's Intuitionistic Mathematics, Inverse semigroups with apartness, Equivalence of bar induction and bar recursion for continuous functions with continuous moduli, Finiteness in a Minimalist Foundation, The continuum and first-order intuitionistic logic, A topological approach to full belief, A characterization of ML in many-sorted arithmetic with conditional application, Lifschitz realizability for intuitionistic Zermelo-Fraenkel set theory, Satisfiability is false intuitionistically: a question from Dana Scott, The FAN principle and weak König's lemma in Herbrandized second-order arithmetic, On the independence of premiss axiom and rule, The Logic of Justification, Three faces of natural deduction, Unnamed Item, Reasoning processes in propositional logic, Infinity and verifiability in Carnap's inductive logic, Characterising Brouwer's continuity by bar recursion on moduli of continuity, Constructive Sheaf Semantics, Intuitionistic fixed point logic, A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms, A Calculus of Realizers for EM 1 Arithmetic (Extended Abstract), Mathematics in Philosophy, Philosophy in Mathematics: Three Case Studies, Weyl and Intuitionistic Infinitesimals, On the logical philosophy of assertive graphs, Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting), Unavoidable sequences in constructive analysis, Verificationism and Classical Realizability, The Monotone Completeness Theorem in Constructive Reverse Mathematics, From Mathesis Universalis to Provability, Computability, and Constructivity, Point-Free Spectra of Linear Spreads, A Dialogical Account of the Intersubjectivity of Intuitionism, Reverse mathematics of topology: dimension, paracompactness, and splittings, Brouwer's fixed-point theorem in real-cohesive homotopy type theory, Validating Brouwer's continuity principle for numbers using named exceptions, Extending constructive operational set theory by impredicative principles, Proof-theoretic semantics and inquisitive logic, Univalent polymorphism, Collapsing partial combinatory algebras, Free logics are cut-free, An application of constructive completeness, Classical and constructive hierarchies in extended intuitionistic analysis, Pluralism in Logic: The Square of Opposition, Leibniz’ Principle of Sufficient Reason and Markov’s Principle, Implicit and explicit stances in logic, Toward a clarity of the extreme value theorem, ON ADOPTING KRIPKE SEMANTICS IN SET THEORY, Tableaux for constructive concurrent dynamic logic, On the rules of intermediate logics, Markov's rule revisited, TRUNCATION AND SEMI-DECIDABILITY NOTIONS IN APPLICATIVE THEORIES, INTERRELATION BETWEEN WEAK FRAGMENTS OF DOUBLE NEGATION SHIFT AND RELATED PRINCIPLES, The seeming interdependence between the concepts of valid inference and proof, Two questions from Dana Scott: Intuitionistic topologies and continuous functions, Announcement as effort on topological spaces, Reverse formalism 16, Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus, Ordinal analyses for monotone and cofinal transfinite inductions, Curry-Howard-Lambek correspondence for intuitionistic belief, An intuitionist reasoning upon formal intuitionist logic: logical analysis of Kolmogorov's 1932 paper, A game-semantic model of computation, Game of grounds, A categorical reading of the numerical existence property in constructive foundations, Reflections on reflections in explicit mathematics, First-order logics of evidence and truth with constant and variable domains, A theory of computation based on quantum logic. I, Une Preuve Formelle et Intuitionniste du Théorème de Complétude de la Logique Classique, Truth as an epistemic notion, Constructive algebraic integration theory, An extension of the equivalence between Brouwer's fan theorem and weak König's lemma with a uniqueness hypothesis, Parallelizations in Weihrauch reducibility and constructive reverse mathematics, Idempotent variations on the theme of exclusive disjunction, Formally computing with the non-computable, Constructive mathematics, Church's thesis, and free choice sequences, Denotational semantics for languages of epistemic grounding based on Prawitz's theory of grounds