Die Axiomatisierung der Mengenlehre
Die Cantorsche Abbildung ist ein Borel-Isomorphismus.
Die m-Grade logischer Entscheidungsprobleme.
Die mit Nestedstackautomaten berechenbaren Funktionen sind elementar.
Die Nichtaxiomatisierbarkeit der unendlichwertigen Mengenlehre.
Die Nichtkonstruktivität des Brouwerschen Fixpunktsatzes.
Die Problematik apriorischer Wahrscheinlichkeiten im System der induktiven Logik von Rudolf Carnap.
Die Struktur kartesischer Produkte ganzer Zahlen modulo kartesische Produkte ganzer Zahlen.
Die Unentscheidbarkeit der einstelligen unendlichwertigen Prädikatenlogik.
Die Varietät der auflösbaren Ternare der Ordnung 2
Die Vollständigkeit einer unverzweigten Variante des "analytischen" Entscheidungsverfahrens der klassischen Logik.
Difference functions of periodic measurable functions
We investigate some problems of the following type: For which sets H is it true that if f is in a given class ℱ of periodic functions and the difference functions are in a given smaller class G for every h ∈ H then f itself must be in G? Denoting the class of counter-example sets by ℌ(ℱ,G), that is, , we try to characterize ℌ(ℱ,G) for some interesting classes of functions ℱ ⊃ G. We study classes of measurable functions on the circle group that are invariant for changes on null-sets (e.g. measurable...
Difference of Function on Vector Space over F
In [11], the definitions of forward difference, backward difference, and central difference as difference operations for functions on R were formalized. However, the definitions of forward difference, backward difference, and central difference for functions on vector spaces over F have not been formalized. In cryptology, these definitions are very important in evaluating the security of cryptographic systems [3], [10]. Differential cryptanalysis [4] that undertakes a general purpose attack against...
Different levels of word problems for some varieties.
Differentiability of Polynomials over Reals
In this article, we formalize in the Mizar system [3] the notion of the derivative of polynomials over the field of real numbers [4]. To define it, we use the derivative of functions between reals and reals [9].
Differential Equations on Functions from R into Real Banach Space
In this article, we describe the differential equations on functions from R into real Banach space. The descriptions are based on the article [20]. As preliminary to the proof of these theorems, we proved some properties of differentiable functions on real normed space. For the proof we referred to descriptions and theorems in the article [21] and the article [32]. And applying the theorems of Riemann integral introduced in the article [22], we proved the ordinary differential equations on real...
Differentiation in Normed Spaces
In this article we formalized the Fréchet differentiation. It is defined as a generalization of the differentiation of a real-valued function of a single real variable to more general functions whose domain and range are subsets of normed spaces [14].
Dijkstra's Interpretation of the Approach to Solving a Problem of Program Correctness
Dimension in algebraic frames, II: Applications to frames of ideals in
This paper continues the investigation into Krull-style dimensions in algebraic frames. Let be an algebraic frame. is the supremum of the lengths of sequences of (proper) prime elements of . Recently, Th. Coquand, H. Lombardi and M.-F. Roy have formulated a characterization which describes the dimension of in terms of the dimensions of certain boundary quotients of . This paper gives a purely frame-theoretic proof of this result, at once generalizing it to frames which are not necessarily...
Dimension of indiscernibility equivalences