About the completeness of a certain system of integer arithmetic in which addition is the only operation (translated, with additional remarks)
https://cs.fit.edu/~ryan/papers/presburger.pdf
https://cs.fit.edu/~ryan/papers/presburger.pdf
Complexity Hierarchies beyond ELEMENTARY
https://arxiv.org/pdf/1312.5686.pdf
https://arxiv.org/pdf/1312.5686.pdf
The Realm of Ordinal Analysis
https://www1.maths.leeds.ac.uk/~rathjen/realm.pdf
https://www1.maths.leeds.ac.uk/~rathjen/realm.pdf
Valery Isaev - Arend Proof Assistant.pdf
140.2 KB
Arend Proof Assistant
Andrea Vezzosi - Indexed Families in Cubical Agda.pdf
74 KB
Indexed Families' computation in Cubical Agda
An Introduction to Proof Theory
http://www.math.ucsd.edu/~sbuss/ResearchWeb/handbookI/ChapterI.pdf
http://www.math.ucsd.edu/~sbuss/ResearchWeb/handbookI/ChapterI.pdf
First-Order Theorem Proving and Vampire
http://www.vprover.org/cav2013.pdf
http://www.vprover.org/cav2013.pdf
Transfinite Ordinals and their Notations
http://www.cs.fsu.edu/~levitz/ords.ps
http://www.cs.fsu.edu/~levitz/ords.ps
An Introduction to Set Theory
https://www.math.toronto.edu/weiss/set_theory.pdf
https://www.math.toronto.edu/weiss/set_theory.pdf
Introduction to Ordinal Analysis
https://www.uni-goettingen.de/de/document/download/1bb43144c8c4bb68805337a25d8d1db9.pdf/pohlers_handout_3.pdf
https://www.uni-goettingen.de/de/document/download/1bb43144c8c4bb68805337a25d8d1db9.pdf/pohlers_handout_3.pdf
First- and Second-Order Models of Recursive Arithmetics
https://arxiv.org/pdf/1705.05459.pdf
https://arxiv.org/pdf/1705.05459.pdf
Algebraic Topology
https://pi.math.cornell.edu/~hatcher/AT/AT.pdf
https://pi.math.cornell.edu/~hatcher/AT/AT.pdf
Non-commutative Logic I: the Multiplicative Fragment
https://static.aminer.org/pdf/PDF/000/753/432/non_commutative_logic_i_the_multiplicative_fragment.pdf
https://static.aminer.org/pdf/PDF/000/753/432/non_commutative_logic_i_the_multiplicative_fragment.pdf
A Formally Verified Abstract Account of Gödel's Incompleteness Theorems
https://www21.in.tum.de/~traytel/papers/cade19-incompleteness/incompleteness.pdf
https://www21.in.tum.de/~traytel/papers/cade19-incompleteness/incompleteness.pdf
4_5831262430465884843.pdf
218.5 KB
Corecursion and coinduction: how they relate to recursion and induction
Three Equivalent Ordinal Notation Systems in Cubical Agda
https://arxiv.org/pdf/1904.10759.pdf
https://arxiv.org/pdf/1904.10759.pdf
Ordinals and Interactive Programs
https://pdfs.semanticscholar.org/89c9/a2bca07752f9ed631c304bad8c34c2b163a2.pdf
https://pdfs.semanticscholar.org/89c9/a2bca07752f9ed631c304bad8c34c2b163a2.pdf
4_5862880936021983758.pdf
1 MB
Fundamental Theorems in Mathematics (2019)
A tutorial implementation of a dependently typed Lambda Calculus
https://www.andres-loeh.de/LambdaPi/LambdaPi.pdf
[Thanks to Elias]
https://www.andres-loeh.de/LambdaPi/LambdaPi.pdf
[Thanks to Elias]