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

zbMATH Open0275.02025MaRDI QIDQ2265415FDOQ2265415

Author name not available (Why is that?)

Publication date: 1973

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

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

Cited In (only showing first 100 items - show all)

Parameter-free polymorphic types
Nonstandardness and the bounded functional interpretation
Computations in fragments of intuitionistic propositional logic
On a weakening of Markov's Principle
Remarks on Herbrand normal forms and Herbrand realizations
\(\mathcal {BCDL}\): Basic constructive description logic
Representations and the foundations of mathematics
A semantic hierarchy for intuitionistic logic
Independence of the induction principle and the axiom of choice in the pure calculus of constructions
Realizability interpretation of proofs in constructive analysis
On a second order propositional operator in intuitionistic logic
Well-foundedness in realizability
A functional interpretation for nonstandard arithmetic
Completeness proofs for propositional logic with polynomial-time connectives
Constructing type systems over an operational semantics
On uniform weak König's lemma
Proof theory in the abstract
A global representation of the recursive functions in the \(\lambda\)- calculus
König's lemma, weak König's lemma, and the decidable fan theorem
The basic feasible functionals in computable analysis
Injecting uniformities into Peano arithmetic
The \(\Sigma_1\)-provability logic of \(\mathsf{HA}\)
Strong normalization theorem for a constructive arithmetic with definition by transfinite recursion and bar induction
An extension of the equivalence between Brouwer's fan theorem and weak König's lemma with a uniqueness hypothesis
On the Constructive and Computational Content of Abstract Mathematics
The abstract type of the real numbers
A Logical Uniform Boundedness Principle for Abstract Metric and Hyperbolic Spaces
Strong normalization from weak normalization in typed \(\lambda\)-calculi
Some principles weaker than Markov's principle
On the disjunctive Markov principle
Extended bar induction in applicative theories
Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
The real-algebraic structure of Scott's model of intuitionistic analysis
PRENEX NORMAL FORM THEOREMS IN SEMI-CLASSICAL ARITHMETIC
Computable Kripke models and intermediate logics
ON THE UNCOUNTABILITY OF
Solovay's relative consistency proof for FIM and BI
Extracting Lisp programs from constructive proofs: A formal theory of constructive mathematics based on Lisp
On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory
Projective sets, intuitionistically
From Coinductive Proofs to Exact Real Arithmetic
Ptykes in Gödels T und Definierbarkeit von Ordinalzahlen. (Ptykes in Gödel's T and definability of ordinal numbers)
A proof-theoretic investigation of a logic of positions
Some derived rules of intuitionistic second order arithmetic
Intuitionist type theory and the free topos
Realizability and intuitionistic logic
Markov's rule revisited
Intuitionistic fixed point logic
Primitive recursive selection functions for existential assertions over abstract algebras
Choice and independence of premise rules in intuitionistic set theory
Proof mining and effective bounds in differential polynomial rings
Arithmetic complexity of the predicate logics of certain complete arithmetic theories
A higher-order calculus and theory abstraction
A quantitative nonlinear strong ergodic theorem for Hilbert spaces
A constructive analysis of learning in Peano arithmetic
The equivalence of bar recursion and open recursion
The Peirce translation
A(nother) characterization of intuitionistic propositional logic
A note on equality in finite‐type arithmetic
Types, abstraction, and parametric polymorphism, part 2
An application of proof mining to nonlinear iterations
Strongly uniform bounds from semi-constructive proofs
Pointwise hereditary majorization and some applications
Functional Interpretations of Intuitionistic Linear Logic
Fragments of arithmetic
The modified realizability topos
Functional interpretations of feasibly constructive arithmetic
Total sets and objects in domain theory
The lack of definable witnesses and provably recursive functions in intuitionistic set theories
Equivalents of the (weak) fan theorem
Defining concurrent processes constructively
A simple proof of second-order strong normalization with permutative conversions
An arithmetic for polynomial-time computation
Decidable Kripke models of intuitionistic theories
Substitutions of \(\Sigma_1^0\)-sentences: Explorations between intuitionistic propositional logic and intuitionistic arithmetic
Equivalence of bar recursors in the theory of functionals of finite type
Reverse mathematics and Weihrauch analysis motivated by finite complexity theory
Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels
Axiomatizing higher-order Kleene realizability
On bounded functional interpretations
Extensional models for polymorphism
A complexity analysis of functional interpretations
LCF considered as a programming language
The bounded functional interpretation of bar induction
From constructivism to computer science
Dialectica Interpretation with Fine Computational Control
A propositional logic with explicit fixed points
Computability in higher types, P\(\omega\) and the completeness of type assignment
Bounded functional interpretation and feasible analysis
Functional interpretations of linear and intuitionistic logic
Term extraction and Ramsey's theorem for pairs
Intuitionistic mereology
Intrinsic reasoning about functional programs. I: First order theories
Uniform proofs as a foundation for logic programming
Axioms and (counter)examples in synthetic domain theory
Classical and constructive hierarchies in extended intuitionistic analysis
Set existence property for intuitionistic theories with dependent choice
A category-theoretic characterization of functional completeness
On theorems of Gödel and Kreisel: Completeness and Markov's principle
Aspects of Categorical Recursion Theory

This page was built for publication: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2265415)