Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics
type: Item
instance of: scholarly article
title: Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics
zbMATH Open document ID: 1114.03007
author: Freek Wiedijk
published in: Journal of Applied Logic
publication date: 2007-02-20T00:00:00Z
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 5128353
zbMATH Keywords: logical frameworks
zbMATH Keywords: foundation of mathematics
zbMATH Keywords: Automath
zbMATH Keywords: set theory
zbMATH Keywords: higher-order logic
zbMATH Keywords: type theory
zbMATH Keywords: category theory
zbMATH Keywords: Zermelo-Fraenkel
zbMATH Keywords: ZF
zbMATH Keywords: ZFC
zbMATH Keywords: New Foundations
zbMATH Keywords: NF
zbMATH Keywords: HOL
zbMATH Keywords: Isabelle
zbMATH Keywords: calculus of constructions
zbMATH Keywords: Martin-Löf type theory
zbMATH Keywords: formalization of mathematics
describes a project that uses: Automath
describes a project that uses: Coq
describes a project that uses: Isabelle
describes a project that uses: Twelf
describes a project that uses: HOL Light
MaRDI profile type: Publication
full work available at URL: j.jal.2005.10.011
OpenAlex ID: W1510554082
cites work: Q4944846
cites work: Q4230782
cites work: Q3889024
cites work: Q3211296
cites work: Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
cites work: Q3999860
cites work: Logical frameworks
cites work: A new implementation of Automath
DOI: 10.1016/J.JAL.2005.10.011
description: scientific article; zbMATH DE number 5128353