Second order arithmetic and autonomous computability.
Second order arithmetic and pulsating hierarchies.
Sémantique catégorique des types : comprendre le système F
Semisemiological structure of the prime numbers and conditional Goldbach theorems.
Separatedness in constructive topology.
Sequent Calculus, Derivability, Provability. Gödel's Completeness Theorem
Fifth of a series of articles laying down the bases for classical first order model theory. This paper presents multiple themes: first it introduces sequents, rules and sets of rules for a first order language L as L-dependent types. Then defines derivability and provability according to a set of rules, and gives several technical lemmas binding all those concepts. Following that, it introduces a fixed set D of derivation rules, and proceeds to convert them to Mizar functorial cluster registrations...
Shiftings of the horizon
Simultane Rekursionen in der Theorie der Funktionale endlicher Typen.
Solution to a problem of Gandy's
Some combinatorics involving ξ-large sets
We prove a version of the Ramsey theorem for partitions of (increasing) n-tuples. We derive this result from a version of König's infinity lemma for ξ-large trees. Here ξ < ε₀ and the notion of largeness is in the sense of Hardy hierarchy.
Some comments on the paper by Artigue, Isambert, Perrin and Zalc
Some constructive topological properties of function spaces
Some diophantine forms of Gödel's theorem.
Some remarks on bicommutability
Some simple decidability proofs
Speed-up for propositional Frege systems via generalizations of proofs
Spielquantorinterpretationen unstetiger Funktionale der höheren Analysis.
Společný spůsob dokazování různých pouček a vzorců. [I.]
Společný spůsob dokazování různých pouček a vzorců. [II.]
Stable surjection logic