Statistical approach to proof theory
Statistical testing procedure for lengths of formalized proofs
Statistical theory of logical derivability
Strong functors and interleaving fixpoints in game semantics
We describe a sequent calculus μLJ with primitives for inductive and coinductive datatypes and equip it with reduction rules allowing a sound translation of Gödel’s system T. We introduce the notion of a μ-closed category, relying on a uniform interpretation of open μLJ formulas as strong functors. We show that any μ-closed category is a sound model for μLJ. We then turn to the construction of a concrete μ-closed category based on Hyland-Ong game semantics. The model relies on three main ingredients:...
Strong initial segments of models of IΔ₀
McAloon showed that if 𝓐 is a nonstandard model of IΔ₀, then some initial segment of 𝓐 is a nonstandard model of PA. Sommer and D'Aquino characterized, in terms of the Wainer functions, the elements that can belong to such an initial segment. The characterization used work of Ketonen and Solovay, and Paris. Here we give conditions on a model 𝓐 of IΔ₀ guaranteeing that there is an n-elementary initial segment that is a nonstandard model of PA. We also characterize the elements that can be included....
Strong normalization of barrecursive terms without using infinite terms.
Strong normalization proofs for cut elimination in Gentzen's sequent calculi
We define an equivalent variant of the Gentzen sequent calculus . In weakenings or contractions can be performed in parallel. This modification allows us to interpret a symmetrical system of mix elimination rules by a finite rewriting system; the termination of this rewriting system can be machine checked. We give also a self-contained strong normalization proof by structural induction. We give another strong normalization proof by a strictly monotone subrecursive interpretation; this interpretation...
Subalgebras of diagonalizable algebras of theories containing arithmetic [Book]
Sul problema dell'autoriferimento
We formulate, within the frame-theory for the foundations of Mathematics outlined in [2], a list of axioms which state that almost all "interesting" collections and almost all "interesting" operations are elements of the universe. The resulting theory would thus have the important foundational feature of being completely self-contained. Unfortunately, the whole list is inconsistent, and we are led to formulate the following problem, which we call the problem of self-reference: "Find out...
Sur la limite du degré des groupes primitifs qui contiennent une substitution donnée.
The Consistency Of A Variant Of Church's Thesis With An Axiomatic Theory Of An Epistemic Notion.
The creative subject and Heyting's arithmetic
The Dialectica interpretation of first-order classical affine logic.
The double powerlocale and exponentiation: A case study in geometric logic.
The Frobenius relations meet linear distributivity.
The Gödel Completeness Theorem for Uncountable Languages
This article is the second in a series of two Mizar articles constituting a formal proof of the Gödel Completeness theorem [15] for uncountably large languages. We follow the proof given in [16]. The present article contains the techniques required to expand a theory such that the expanded theory contains witnesses and is negation faithful. Then the completeness theorem follows immediately.
The lattices of numerations of theories containing Peano's arithmetic
The limit lemma in fragments of arithmetic
The recursion theoretic limit lemma, saying that each function with a graph is a limit of certain function with a graph, is provable in .
The polynomial bounds of proof complexity in Frege systems.
The projective spectrum as a distributive lattice