Publication:3679172
From MaRDI portal
zbMath0565.03028MaRDI QIDQ3679172
Publication date: 1985
constructive mathematics; proof theory; set theory; constructive proof; intuitionistic logic; formal systems; constructive metamathematics
03F60: Constructive and recursive analysis
03-02: Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
03F65: Other constructive mathematics
03F50: Metamathematics of constructive systems
03F55: Intuitionistic mathematics
Related Items
Polynomial time operations in explicit mathematics, Reflection principles for synthetic theories of smooth manifolds, Wellordering proofs for metapredicative Mahlo, The axiom of choice and combinatory logic, Ranked partial structures, Some logical metatheorems with applications in functional analysis, Strong and Uniform Continuity – the Uniform Space Case, A First Look into a Formal and Constructive Approach for Discrete Geometry Using Nonstandard Analysis, Explicit mathematics: power types and overloading, Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves, Sets, complements and boundaries, Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation, On specifications, subset types and interpretation of proposition in type theory, Type-theoretic interpretation of iterated, strictly positive inductive definitions, Equivalents of the (weak) fan theorem, A proof-theoretic characterization of the basic feasible functionals, Preference, indifference, and Markov's principle, Extended bar induction in applicative theories, Extraction of redundancy-free programs from constructive natural deduction proofs, Gentzen calculi for the existence predicate, Mathematics based on incremental learning -- excluded middle and inductive inference, Partial Horn logic and Cartesian categories, Computability of analog networks, Proof-theoretical analysis: Weak systems of functions and classes, Rationality, computability, and complexity, Fixed point theory in weak second-order arithmetic, Primitive recursive selection functions for existential assertions over abstract algebras, On the syntax of Martin-Löf's type theories, Between constructive mathematics and PROLOG, On the status of proofs by contradiction in the seventeenth century, Finite type structures within combinatory algebras, Extensions and fixed points of contractive maps in \(\mathbb{R}^ n\), Extension of combinatory logic to a theory of combinatory representation, A transfer theorem in constructive \(p\)-adic algebra, Some aspects of effectively constructive mathematics that are relevant to the foundations of neoclassical mathematical economics and the theory of games, A theory for program and data type specification, Self-witnessing polynomial-time complexity and prime factorization, Hilbert's \(\varepsilon{}\)-operator and classical logic, Constructive mathematics: a foundation for computable analysis, Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\), Well-ordering proofs for Martin-Löf type theory, Point-free topological spaces, functions and recursive points; filter foundation for recursive analysis. I, Realizability interpretation of coinductive definitions and program synthesis with streams, Systems of explicit mathematics with non-constructive \(\mu\)-operator. I, Realizability interpretation of generalized inductive definitions, The strength of some Martin-Löf type theories, Formalizing non-termination of recursive programs, On the proof-theoretic strength of monotone induction in explicit mathematics, Extensional realizability, The constructive theory of preference relations on a locally compact space. II, Provability in principle and controversial constructivistic principles, Unique existence, approximate solutions, and countable choice., A constructive theory of point-set nearness., Theories with self-application and computational complexity., Ishihara's proof technique in constructive analysis, Polynat in PER models, Functional interpretation of Aczel's constructive set theory, The unfolding of non-finitist arithmetic, The non-constructive \(\mu\) operator, fixed point theories with ordinals, and the bar rule, Category theory and the foundations of mathematics: philosophical excavations., Wittgenstein and finitism, Computationalism, Rational presented metric spaces and complexity, the case of the space of real functions uniformly continuous on a compact interval, A new graph characteristic and its application to numerical computability, Kernels of seminorms in constructive analysis., Specification of real-time and hybrid systems in rewriting logic, Inaccessible set axioms may have little consistency strength, Axioms for strict and lazy functional programs, A theory of rules for enumerated classes of functions, A semantical proof of De Jongh's theorem, Can constructive mathematics be applied in physics?, Towards a computation system based on set theory, Constructing extensions of ultraweakly continuous linear functionals, Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe, Apartness spaces as a framework for constructive topology, Universes over Frege structures, Computational complexity of optimization and crude range testing: A new approach motivated by fuzzy optimization, Nominal logic, a first order theory of names and binding, A constructive approach to nonstandard analysis, Totality in applicative theories, Spectra of selfadjoint operators in constructive analysis, Systems of explicit mathematics with non-constructive \(\mu\)-operator. II, On Feferman's operational set theory \textsf{OST}, Abstraction in algorithmic logic, CZF and second order arithmetic, Characterizing the interpretation of set theory in Martin-Löf type theory, On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting, The Skolemization of existential quantifiers in intuitionistic logic, Formalizing forcing arguments in subsystems of second-order arithmetic, Systems of explicit mathematics with non-constructive \(\mu\)-operator and join, Remarks on applicative theories, Reflections on reflections in explicit mathematics, Strong continuity implies uniform sequential continuity, Dynamical algebraic structures, pointfree topological spaces and Hilbert's program. (Structures algébriques dynamiques, espaces topologiques sans points et programme de Hilbert), Strongly Noetherian rings and constructive ideal theory, Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory, A proof–technique in uniform space theory, Singular coverings and non‐uniform notions of closed set computability, The knaster-tarski fixed-point theorem is not uniformly constructive, On the Lebesgue measurability of continuous functions in constructive analysis, On the proof theory of type two functionals based on primitive recursive operations, Elementary patterns of resemblance, Universes in explicit mathematics, A partial functions version of Church's simple theory of types, Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms, On the proof theory of Coquand's calculus of constructions
