Ulrik Buchholtz

499

Reputation

255 views

Registered User

Name	Ulrik Buchholtz
Member for	3 years
Seen	2 days ago
Website	math.stanford.edu/~utb
Location
Age

stats recent reputation favorites

0

Questions

10

Answers

votes newest views recent

Reference request for type theory

Arithmetic strength of Peano + the Howard ordinal

Ackermann-related function

Is any true sentence in the second-order Peano Axioms provable

Reduction rules for inductive types

Theorems for nothing (and the proofs for free)

categorifying induction in homotopy type theory

Is there any proof assistant based on first-order logic?

Mechanically instantiating abstract constructions

Why no morphisms from the contradictory proposition to the inconsistent context?

41

Votes

41

15

Tags

lo.logic× 7
type-theory× 4
proof-assistant× 2
ct.category-theory× 2
soft-question
reference-request
proof-theory
ordinal-numbers
nt.number-theory
homotopy-theory

computer-science
computability-theory
categorification
big-list
abstract-algebra

5

Badges

● Commentator
● Editor

● Enthusiast
● Supporter