Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard

zbMath0275.02025MaRDI QIDQ2265415

No author found.

Publication date: 1973

Published in: Lecture Notes in Mathematics (Search for Journal in Brave)

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Intuitionistic mathematics (03F55) Intermediate logics (03B55) Proof theory and constructive mathematics (03F99)

Related Items

On theorems of Gödel and Kreisel: Completeness and Markov's principle, Axiomatizing higher-order Kleene realizability, Maximality in modal logic, Reverse mathematics and parameter-free transfer, On the syntax of Martin-Löf's type theories, Well-foundedness in realizability, Strong normalization from weak normalization in typed \(\lambda\)-calculi, The basic feasible functionals in computable analysis, Innovations in computational type theory using Nuprl, Bounded functional interpretation and feasible analysis, Equivalence of bar recursors in the theory of functionals of finite type, Provability in principle and controversial constructivistic principles, Negative translations not intuitionistically equivalent to the usual ones, Program extraction for 2-random reals, On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory, Completeness proofs for propositional logic with polynomial-time connectives, Strong normalization theorem for a constructive arithmetic with definition by transfinite recursion and bar induction, On fixed-point theorems in synthetic computability, The equivalence of bar recursion and open recursion, Some principles weaker than Markov's principle, Lewis meets Brouwer: constructive strict implication, Meaning explanations at higher dimension, Arithmetical conservation results, To be or not to be constructive, that is not the question, Brouwer and Euclid, The Peirce translation, Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility, On the disjunctive Markov principle, A quantitative nonlinear strong ergodic theorem for Hilbert spaces, Intuitionist type theory and the free topos, On bounded functional interpretations, A proof-theoretic investigation of a logic of positions, Logical metatheorems for abstract spaces axiomatized in positive bounded logic, Light Dialectica revisited, Inhabitation of polymorphic and existential types, The bounded functional interpretation of bar induction, A propositional logic with explicit fixed points, Intuitionistic nonstandard bounded modified realisability and functional interpretation, On a second order propositional operator in intuitionistic logic, A category-theoretic characterization of functional completeness, Proof mining and effective bounds in differential polynomial rings, The binary expansion and the intermediate value theorem in constructive reverse mathematics, A constructive analysis of learning in Peano arithmetic, A note on non-classical nonstandard arithmetic, Recursion over realizability structures, Inheritance as implicit coercion, Computations in fragments of intuitionistic propositional logic, A constructive version of Tarski's geometry, Primitive recursive selection functions for existential assertions over abstract algebras, A semantic hierarchy for intuitionistic logic, Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves, Hybrids of the \({}^ \times \)-translation for \(\mathsf{CZF}^{\omega}\), The modified realizability topos, An induction principle over real numbers, Bar recursion over finite partial functions, Functional interpretations of feasibly constructive arithmetic, Independence of the induction principle and the axiom of choice in the pure calculus of constructions, Constructing type systems over an operational semantics, Parameter-free polymorphic types, 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, Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice, Functional interpretations of linear and intuitionistic logic, Total sets and objects in domain theory, \(\mathcal {BCDL}\): Basic constructive description logic, Equivalents of the (weak) fan theorem, A complexity analysis of functional interpretations, A functional interpretation for nonstandard arithmetic, Computability in higher types, P\(\omega\) and the completeness of type assignment, The \(\Sigma_1\)-provability logic of \(\mathsf{HA}\), LCF considered as a programming language, A global representation of the recursive functions in the \(\lambda\)- calculus, Injecting uniformities into Peano arithmetic, Realizability interpretation of proofs in constructive analysis, Extensional models for polymorphism, The semantics of second-order lambda calculus, Extended bar induction in applicative theories, Functorial polymorphism, Computable Kripke models and intermediate logics, Modified realizability and predicate logic, From constructivism to computer science, Fragments of arithmetic, Functional interpretation of Aczel's constructive set theory, Axioms and (counter)examples in synthetic domain theory, Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\), Decidable Kripke models of intuitionistic theories, Some results on cut-elimination, provable well-orderings, induction and reflection, On the arithmetical content of restricted forms of comprehension, choice and general uniform boundedness, Extracting Lisp programs from constructive proofs: A formal theory of constructive mathematics based on Lisp, Programs as proofs: A synopsis, Realizability and intuitionistic logic, Some purely topological models for intuitionistic analysis, Set existence property for intuitionistic theories with dependent choice, \({\mathcal M}^\omega\) considered as a programming language, The real-algebraic structure of Scott's model of intuitionistic analysis, Defining concurrent processes constructively, Pointwise hereditary majorization and some applications, The lack of definable witnesses and provably recursive functions in intuitionistic set theories, \(QPC_ 2\): A constructive calculus with parameterized specifications, Program extraction from normalization proofs, Proof mining in \(L_{1}\)-approximation, Reverse mathematics and Weihrauch analysis motivated by finite complexity theory, Intuitionistic completeness and classical logic, A normal form for logical derivations implying one for arithmetic derivations, Representations and the foundations of mathematics, Measure theory and higher order arithmetic, Natural deduction for intuitionistic linear logic, A constructive approach to nonstandard analysis, Combinatory logic with polymorphic types, On Spector's bar recursion, A higher-order calculus and theory abstraction, Uniform proofs as a foundation for logic programming, Term extraction and Ramsey's theorem for pairs, Unnamed Item, A method to single out maximal propositional logics with the disjunction property. I, A method to single out maximal propositional logics with the disjunction property. II, Some logical metatheorems with applications in functional analysis, Intuitionistic Provability versus Uniform Provability in $$\mathsf{RCA}$$, Hard provability logics, A herbrandized functional interpretation of classical first-order logic, The strength of countable saturation, Polymorphic extensions of simple type structures. With an application to a bar recursive minimization, Splittings and disjunctions in reverse mathematics, Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels, A universal algorithm for Krull's theorem, Lifting proofs from countable to uncountable mathematics, Equivalence of bar induction and bar recursion for continuous functions with continuous moduli, Representing definable functions of \(\mathrm{HA}^{\omega}\) by neighbourhood functions, Dialectica principles via Gödel doctrines, Interpreting Localized Computational Effects Using Operators of Higher Type, The FAN principle and weak König's lemma in Herbrandized second-order arithmetic, ON WEIHRAUCH REDUCIBILITY AND INTUITIONISTIC REVERSE MATHEMATICS, A Computable Solution to Partee’s Temperature Puzzle, On the independence of premiss axiom and rule, Ordered combinatory algebras and realizability, Three faces of natural deduction, Generalized tableau systems for intermediate propositional logics, Unnamed Item, Classical consequences of continuous choice principles from intuitionistic analysis, Characterising Brouwer's continuity by bar recursion on moduli of continuity, Intuitionistic fixed point logic, From Nonstandard Analysis to Various Flavours of Computability Theory, Unnamed Item, An application of proof mining to nonlinear iterations, Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting), On the Constructive and Computational Content of Abstract Mathematics, Reverse mathematics of topology: dimension, paracompactness, and splittings, Validating Brouwer's continuity principle for numbers using named exceptions, The abstract type of the real numbers, Two different strong normalization proofs?, On a weakening of Markov's Principle, Classical and constructive hierarchies in extended intuitionistic analysis, A Logical Uniform Boundedness Principle for Abstract Metric and Hyperbolic Spaces, Formalizing Type Operations Using the “Image” Type Constructor, Dialectica Interpretation with Fine Computational Control, A realizability interpretation for classical analysis, Extracting Herbrand disjunctions by functional interpretation, Bounded functional interpretation, Uniform Heyting arithmetic, CZF and second order arithmetic, Strongly uniform bounds from semi-constructive proofs, Double negation semantics for generalisations of Heyting algebras, Using Ramsey's theorem once, An arithmetic for polynomial-time computation, A version of the ∑1-reflection principle for CFA provable in PRA, The admissible rules of \(\mathsf{BD}_2\) and \(\mathsf{GSc}\), Markov's rule revisited, Some derived rules of intuitionistic second order arithmetic, INTERRELATION BETWEEN WEAK FRAGMENTS OF DOUBLE NEGATION SHIFT AND RELATED PRINCIPLES, Unnamed Item, A Context-based Approach to Proving Termination of Evaluation, Constructing illoyal algebra-valued models of set theory, A semantical proof of De Jongh's theorem, Remarks on Herbrand normal forms and Herbrand realizations, Choice sequences and reduction processes, THE HERBRAND FUNCTIONAL INTERPRETATION OF THE DOUBLE NEGATION SHIFT, Dependent choice as a termination principle, Embedding intuitionistic-type theory in negationless-type theory, From Coinductive Proofs to Exact Real Arithmetic, Extraction and verification of programs by analysis of formal proofs, Ptykes in Gödels T und Definierbarkeit von Ordinalzahlen. (Ptykes in Gödel's T and definability of ordinal numbers), Not all Kripke models of \(\mathsf{HA}\) are locally \(\mathsf{PA}\), Solovay's relative consistency proof for FIM and BI, Weihrauch and constructive reducibility between existence statements, Nets and reverse mathematics, The strength of compactness in computability theory and nonstandard analysis, On maximal intermediate predicate constructive logics, A simple proof of second-order strong normalization with permutative conversions, THE CHARACTERIZATION OF WEIHRAUCH REDUCIBILITY IN SYSTEMS CONTAINING, On Goodman realizability, \(\Delta^0_1\) variants of the law of excluded middle and related principles, Aspects of Categorical Recursion Theory, Light Dialectica Program Extraction from a Classical Fibonacci Proof, PRENEX NORMAL FORM THEOREMS IN SEMI-CLASSICAL ARITHMETIC, Nonstandardness and the bounded functional interpretation, An extension of the equivalence between Brouwer's fan theorem and weak König's lemma with a uniqueness hypothesis, Bishop-Style Constructive Reverse Mathematics, Randomising realizability, Minimum classical extensions of constructive theories, Splittings and robustness for the Heine-Borel theorem, THE AXIOM OF CHOICE IS FALSE INTUITIONISTICALLY (IN MOST CONTEXTS), Countable sets versus sets that are countable in reverse mathematics, A NOTE ON FRAGMENTS OF UNIFORM REFLECTION IN SECOND ORDER ARITHMETIC, ON THE UNCOUNTABILITY OF, Converse extensionality and apartness, CONSTRUCTIVE GEOMETRY AND THE PARALLEL POSTULATE, Hardwiring truth in functional interpretations, Decidable fan theorem and uniform continuity theorem with continuous moduli, König's lemma, weak König's lemma, and the decidable fan theorem, Program extraction from classical proofs, Intuitionistic mereology, EXTENDED FRAMES AND SEPARATIONS OF LOGICAL PRINCIPLES, Logic of refinement types, Refining the arithmetical hierarchy of classical principles, EXTENSIONAL REALIZABILITY AND CHOICE FOR DEPENDENT TYPES IN INTUITIONISTIC SET THEORY, A proof‐theoretic metatheorem for tracial von Neumann algebras, Coding of real‐valued continuous functions under WKL$\mathsf {WKL}$, Choice and independence of premise rules in intuitionistic set theory, Interpreting weak Kőnig's lemma in theories of nonstandard arithmetic, A note on equality in finite‐type arithmetic, On computational properties of Cauchy problems generated by accretive operators, Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language, Projective sets, intuitionistically, Types, abstraction, and parametric polymorphism, part 2, CONSERVATION THEOREMS ON SEMI-CLASSICAL ARITHMETIC, The finitary content of sunny nonexpansive retractions, Refined program extraction from classical proofs, Logical problems of functional interpretations, Proof theory in the abstract, On uniform weak König's lemma, Intrinsic reasoning about functional programs. I: First order theories, Analyzing realizability by Troelstra's methods, Substitutions of \(\Sigma_1^0\)-sentences: Explorations between intuitionistic propositional logic and intuitionistic arithmetic, Finite methods in 1-order formalisms, A(nother) characterization of intuitionistic propositional logic, Arithmetic complexity of the predicate logics of certain complete arithmetic theories, COMPUTABILITY THEORY, NONSTANDARD ANALYSIS, AND THEIR CONNECTIONS, Explaining Deductive Inference, Functional Interpretations of Intuitionistic Linear Logic, Unnamed Item