O druhém Hilbertově problému (Otázka bezespornosti aritmetiky)
O struktuře modelů omezené -indukce
On a connection between algebra, logic and linguistics
On a Foundation for Mathematics- a View of Mathematics I
On a new method in intuitionist linear analysis
On a relationship between countable functionals and projective trees
On a unification problem related to Kreisel's conjecture
On a weakening of Markov's principle.
On an extremely restricted ω-rule
On computable real functions
On constructive versions of the Tychonoff and Schauder fixed point theorems.
On convergence of the Fourier series of a constructive function of weakly bounded variation
On cut elimination in the presence of peirce rule.
On effective speed-up and long proofs of trivial theorems in formal theories
On elementary cuts in models of arithmetic
On global induction mechanisms in a -calculus with explicit approximations
We investigate a Gentzen-style proof system for the first-order -calculus based on cyclic proofs, produced by unfolding fixed point formulas and detecting repeated proof goals. Our system uses explicit ordinal variables and approximations to support a simple semantic induction discharge condition which ensures the well-foundedness of inductive reasoning. As the main result of this paper we propose a new syntactic discharge condition based on traces and establish its equivalence with the semantic...
On global induction mechanisms in a μ-calculus with explicit approximations
We investigate a Gentzen-style proof system for the first-order μ-calculus based on cyclic proofs, produced by unfolding fixed point formulas and detecting repeated proof goals. Our system uses explicit ordinal variables and approximations to support a simple semantic induction discharge condition which ensures the well-foundedness of inductive reasoning. As the main result of this paper we propose a new syntactic discharge condition based on traces and establish its equivalence with the semantic...
On hereditarily separable Hausdorff spaces in the constructible universe
On independent recursive axiomatisation in intuitionistic logic
On interpretability in theories containing arithmetic. II.