The second isomorphism theorem on ordered set under antiorders
The strength of Turing determinacy within second order arithmetic
We investigate the reverse mathematical strength of Turing determinacy up to Σ₅⁰, which is itself not provable in second order arithmetic.
The "World's Simplest Axiom of Choice" Fails.
Theorem Provers for Substructural Logics
Three-valued logic and cut-elimination: The actual meaning of Takeuti's conjecture [Book]
Topological properties of the real numbers object in a topos
Transition of Consistency and Satisfiability under Language Extensions
This article is the first in a series of two Mizar articles constituting a formal proof of the Gödel Completeness theorem [17] for uncountably large languages. We follow the proof given in [18]. The present article contains the techniques required to expand formal languages. We prove that consistent or satisfiable theories retain these properties under changes to the language they are formulated in.
Über das Markov-Prinzip.
Über das Markov-Prinzip II.
Über das Verhältnis zwischen intuitionistischer und klassischer Arithmetik.
Über die mit dem Bar-Rekursor vom Typ 0 definierbaren Ordinalzahlen.
Über ein konstruktives Analogon eines Satzes von K. M. Garg über Ableitungszahlen
Über Hilbert's reale und ideale Elemente.
Über katalogisierte Räume
Über konstruktive Methoden der Galoistheorie.
Über Teilsysteme von ...({g}).
Über zwei Bezeichnungssysteme für Ordinalzahlen.
Un anneau de Prüfer
Let be the ring of integer valued polynomials over . This ring is known to be a Prüfer domain. But it seems there does not exist an algorithm for inverting a nonzero finitely generated ideal of . In this note we show how to obtain such an algorithm by deciphering a classical abstract proof that uses localisations of at all prime ideals of . This confirms a general program of deciphering abstract classical proofs in order to obtain algorithmic proofs.
Una teoria-quadro per i fondamenti della matematica
We propose a "natural" axiomatic theory of the Foundations of Mathematics (Theory Q) where, in addition to the membership relation (between elements and classes), pairs, sets, natural numbers, n-tuples and operations are also introduced as primitives by means of suitable ground classes. Moreover, the theory Q allows an easy introduction of other mathematical and logical entities. The theory Q is finitely axiomatized in § 2, using a first-order language with a binary relation (membership) and five...
Undecidability vs transfinite induction for the consistency of hyperarithmetical sets.