From Mathesis Universalis to Provability, Computability, and Constructivity

DOI10.1007/978-3-030-20447-1_12zbMath1469.03113OpenAlexW2982230606MaRDI QIDQ3305633

Klaus Mainzer

Publication date: 10 August 2020

Published in: Mathesis Universalis, Computability and Proof (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-20447-1_12

zbMATH Keywords

reverse mathematicsprogram extractionmachine learningintuitionistic type theoryproof miningconstructivitymathesis universalisprogram assistanttheoria cum praxisunivalent foundations program

Mathematics Subject Classification ID

Constructive and recursive analysis (03F60) Undecidability and degrees of sets of sentences (03D35) Foundations of classical theories (including reverse mathematics) (03B30) Second- and higher-order arithmetic and fragments (03F35) Turing machines and related notions (03D10) Relative consistency and interpretations (03F25) Topological categories, foundations of homotopy theory (55U40) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Type theory (03B38)

Uses Software

• Coq

Cites Work

• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Recursive unsolvability of Post's problem of Tag und other topics in theory of Turing machines
• The calculus of constructions
• The decision problem for exponential diophantine equations
• Constructivism in mathematics. An introduction. Volume II
• The method of analysis. Its geometrical origin and its general significance
• Inaccessibility in constructive set theory and type theory
• Zur Deutung der intuitionistischen Logik
• Extending Martin-Löf type theory by one Mahlo-universe
• Quasi-categories and Kan complexes
• The universal Turing machine. A half-century survey.
• Feferman on foundations. Logic, mathematics, philosophy
• Turing Computability
• The Universe as Automaton
• Proofs and Computations
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Homotopy theoretic models of identity types
• 100 Years of Zermelo’s Axiom of Choice: What was the Problem with It?
• New Proofs of Euclid's and Euler's Theorems
• Proof and Computation
• The Digital and the Real World
• Local Activity Principle
• Systems of predicative analysis
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Thinking in Complexity
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• Brouwer's fan theorem and unique existence in constructive analysis
• Systems of predicative analysis, II: Representations of ordinals
• MATHEMATISCHER KONSTRUKTIVISMUS IM LICHTE-KANTISCHER PHILOSOPHIE
• Computability of Recursive Functions
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item