Oberseminar Mathematische Logik
Veranstalter:
J. Berger, W. Buchholz, H.-D. Donder, H. Osswald,
I. Petrakis, P. Schuster, H. Schwichtenberg
Zeit und Ort
Mi 16:30-18, B252
WS 2018/19
- Chuangjie Xu
(joint work with Fredrik Nordvall Forsberg and Nicolai Kraus),
Two type-theoretic approaches to ordinals in Cantor normal form,
20. Februar 2019
Abstract: We construct two data structures to directly represent
ordinals in Cantor normal form: (1) decreasing sequences, using
induction-recursion, and (2) finite multisets, using higher inductive
types. Both have been easily and neatly implemented in the Agda proof
assistant.
- Quirin Schroll, TBA. Termin noch offen.
Frühere Vorträge im WS 2018/19
- Yong Cheng, The current state of research on incompleteness.
23. Janar 2019
Abstract. Gödel's incompleteness theorem is the most
profound and important theorem in foundations of
mathematics. There are still some open problems related to
incompleteness. In this talk, firstly I will classify some
misinterpretations of Gödel's incompleteness theorem and give
an overview of the current state of research on incompleteness
from the following aspects: (1) The property of provability and
truth; (2) The generalization of Incompleteness theorem to
arithmetical definable theory; (3) The classification of proofs of
the incompleteness theorem; (4) Proving incompleteness via logical
paradox; (5) The intensionality problem of G2; (6) Incompleteness
and provability logic. Finally, I will talk about some recent
progress on the open problem of finding the limit of
incompleteness for subsystems of PA.
- Philipp Scheufele,
The Fundamental Theorem of Asset Pricing in constructive mathematics.
21. November 2018
Abstract. We consider different versions of the FTAP in the
context of constructive reverse mathematics. In particular we will
show that the two standard FTAPs (existence of an arbitrage
strategy <-> absence of an equivalent martingale measure, and vice
versa) are equivalent to LPO. Moreover, we will develop different
modifications of these standard FTAPs and examine their relation
to Markov?s Principle and LPO. Finally, we will provide a guide
for obtaining constructive formulations of the FTAP from the
non-constructive ones and provide some explicit examples.
- Kenji Miyamoto, The epsilon calculus with equality and Herbrand
complexity. 14. November 2018
Abstract. Hilbert's epsilon-calculus is an extension of
elementary or predicate calculus by a term-forming operator
\(\varepsilon\) and initial formulas involving such terms. The
fundamental results about the epsilon-calculus are so-called
epsilon theorems, which have been proven by means of the epsilon
substitution method. It is a procedure of transforming a proof in
epsilon-calculus into a proof in elementary or predicate calculus
through getting rid of those initial formulas. One remarkable
consequence is a proof of Herbrand's theorem by Bernays and
Hilbert which comes as a corollary of extended first epsilon
theorem. Our contribution is the upper and lower bounds analysis
of the length of Herbrand disjunctions in extended first epsilon
theorem for epsilon-calculus with equality. It is an extension of
the results by Moser and Zach including the complexity analysis in
epsilon-calculus without equality, where extended first epsilon
theorem was the main target for analysis, since the epsilon
substitution method shows its general figure in the proof of this
theorem.
- Martin Escardo, Ordinals in constructive univalent mathematics.
31. Oktober 2018
Abstract. We consider ordinal codes (certain countably branching
trees) and ordinals (types equipped with transitive, extensional, well
founded relations) and two interpretations of codes into ordinals. One
of them gives discrete ordinals. The other one gives "compact"
ordinals (also called "searchable"). These two interpretations are
classically equivalent, but constructively very different, and have
some interesting relationships. The ordinals in the image of the
compact interpretation satisfy the property that every detachable
inhabited subset has a least element. For the ordinals in the image of
the discrete interpretation this fails (or, more, precisely, is
equivalent to LPO).
Frühere Vorträge im SS 2018
- Peter Schuster (Univ. Verona), Das Zornsche Lemma als bloss
heuristisches Prinzip. Dienstag (!), 19. Juni 2018, 12.30 Uhr, B252.
- Ingo Blechschmidt, Without loss of generality, any reduced ring
is a field, 11. April 2018, 15:15-16:45 (!), B349 (Sitzungszimmer) (!)
Abstract. We present a semantics which allows to pretend that
any reduced ring is a field, as long as we restrict to
constructive reasoning. We illustrate the usefulness of this
general technique by giving a constructive proof of Grothendieck's
generic freeness lemma. Because the lemma is trivial for fields,
the new proof is short and simple; in contrast, all previously
known proofs were somewhat convoluted and employed classical
logic, such that it came as a surprise that the lemma admits a
constructive proof. Some aspects are related to Dickson's lemma,
which was analyzed by Berger and Schwichtenberg.
Frühere Vorträge im WS 2017/18
- Toshiyasu Arai, Proof-theoretic strengths of weak theories
for positive inductive definitions. 21. Februar 2018, 16:30, B349
(Sitzungszimmer)
Abstract. In this paper the lightface \Pi^{1}_{1}-Comprehension
axiom is shown to be proof-theoretically strong even over
RCA_{0}^{*}, and we calibrate the proof-theoretic ordinals of weak
fragments of the theory ID_{1} of positive inductive definitions
over natural numbers. Conjunctions of negative and positive
formulas in the transfinite induction axiom of ID_{1} are shown to
be weak, and disjunctions are strong. Thus we draw a boundary
line between predicatively reducible and impredicative fragments
of ID_{1}.
- Ryota Akiyoshi, "Proofs as Programs" Revisited, and Chuangjie
Xu, An Agda implementation of Oliva & Steila's proof of the Bar
Recursion Closure Theorem. 14. Februar 2018, 16:00, B349
(Sitzungszimmer) (!)
Abstract Xu: Oliva and Steila [2] present a direct proof of
Schwichtenberg's theorem that the System T definable functionals
are closed under a rule-like version Spector's bar recursion of
lowest type levels 0 and 1. We implement it in the Agda proof
assistant to convert bar recursive definitions to Agda programs
under the conditions of Schwichtenberg's theorem. In particular,
we make use of Escardo's construction of dialogue monad [1] to
simplify our implementation.
[1] M. Escardo, Continuity of Godel's system T functionals via
effectful forcing. MFPS'2013. Electronic Notes in Theoretical Computer
Science 01/2013, volume 298, pages 119-141. 2013.
[2] P. Oliva and S. Steila, A direct proof of Schwichtenberg's bar
recursion closure theorem. To appear in The Journal of Symbolic Logic,
2017.
Abstract Akiyoshi: Schwichtenberg has developed the program called
"Proofs as Programs" by measuring the "complexity as programs" of
proofs in an arithmetical system (with recursion). Technically, he
used a slow growing hierarchy to "clime down" tree ordinals, which
are introduced by Buchholz. This observation is due to Arai and is
going back to Girard's "Hierarchy comparison theorem".
In this talk, we sketch another approach to this program by
focusing on parameter-free subsystems of Girard's F. There are at
least two advantages in this approach. (i) Our approach is simpler
and smoother than the original one. (ii) It is relatively easy and
uniform to extend our results to stronger fragments (corresponding
to iterated inductive definitions) though the theory analysed by
Schwichtenberg has the strength of Peano Arithmetic. This work is
based on discussions with Schwichtenberg.
- Nils Köpp, Program extraction from coinductive proofs in Minlog
applied to some constructive analysis, 24. Januar 2018
Abstract: We review the theory underlying the proof assistant
Minlog, which allows for automatically verified program extraction
from (co)inductive proofs. We will apply these methods to some
constructive analysis, especially the representation of
constructive cauchy-reals by sd-code.
- Philipp Schlicht, Class forcing and reverse mathematics of
second-order set theory. 20. Dezember 2017
Abstract: The forcing theorem, the most fundamental result about
set forcing, states that every set forcing admits forcing
relations for all formulas and the truth lemma holds: statements
true in the corresponding forcing extensions are forced and forced
statements are true. Unlike for set forcing, the forcing theorem
for class forcing can fail in models of Gödel-Bernays class theory
GBC with global choice. We show that the class forcing theorem is
equivalent over the base theory GBC to the principle ETR_Ord of
class recursion of length Ord; the existence of Ord-length
iterated truth predicates relative to any class; the statement
that every separative class partial order has a set-complete class
Boolean completion; and the principle of determinacy for clopen
class games of rank at most Ord+1. This situates the class forcing
theorem in an emerging hierarchy of reverse mathematics of
second-order set theory. This is joint work with Victoria Gitman,
Joel Hamkins, Peter Holy and Kameryn Williams.
- Chuangjie Xu, Using function extensionality in Agda,
(non-)computationally. 6. Dezember 2017
Abstract: I implemented my thesis [2] in the Agda proof assistant
to compute moduli of uniform continuity. The main difficulty is
the lack of function extensionality (i.e., two functions are equal
if they are pointwise equal) in Agda. If it is directly
postulated, then the implementation fails to compute. We developed
a few approaches to use function extensionality in a
non-computational way to address this problem. Cubical Type Theory
[1] proves function extensionality. Recently it was implemented as
a part of the beta version of Agda. We ported our original
development to this cubical Agda and the computation correctly
produced zero, while it was a 367-lines long normal-form term in
the development where functional extensionality was postulated.
[1] C. Cohen, T. Coquand, S. Huber, and A. Mörtberg, Cubical type
theory: a constructive interpretation of the univalence axiom
(2016). To appear in the proceedings of TYPES 2015.
[2] C. Xu, A continuous computational interpretation of type theories,
doctoral dissertation, the University of Birmingham, 2015.
- Hajime Ishihara, The Hahn-Banach theorem, constructively revisited.
15. November 2017
Abstract: We review known constructive versions, such as the
separation theorem and continuous extension theorem, of the
Hahn-Banach theorem and their proofs, and consider new versions
including the dominated extension theorem and their proofs.
- Matthias Eberl, It's a Matter of Dependency, Not of Size.
25. Oktober 2017
Abstract: We develop a finitistic point of view based on an
interpretation with reflection principle. The basic idea is that
of a potential infinite set, which leads to the replacement of
infinite collections by unbounded, indefinitely extensible
collections. A universal quantifier referring to such indefinitely
large domains ranges over a sufficiently large finite part of it.
- Michael Beeson (Joint work with Julien Narboux and Freek Wiedijk),
Proof-checking Euclid. 11. Oktober 2017
Abstract: We used computer proof-checking methods to verify the
correctness of our proofs of the propositions in Euclid Book I.
We used axioms as close as possible to those of Euclid, in a language
closely related to that used in Tarski's formal geometry. We used
proofs as close as possible to those given by Euclid, but filling
Euclid's gaps and correcting errors. Then we checked those proofs
in the well-known and trusted proof checkers
HOL Light and Coq. The talk will contain many geometrical diagrams
and discuss both the geometry and the proof-checking.
Frühere Vorträge im SS 2017
- Auke Booij, Analysis in univalent type theory. 20. Sep. 2017
Abstract: It is not possible to exhibit information about real numbers
such as Dedekind reals or (quotiented) Cauchy reals (as opposed to
Bishop-style Cauchy reals), because, for example, there are no
non-constant functions into observable types such as the booleans or
the integers. We overcome this by considering real numbers that have
additional structure, which we call strong locatedness. With this
structure, it is possible, for instance, to construct a signed-digit
representation or a Cauchy approximation. Such constructions are
reminiscent of computable analysis. However, the main point is that
instead of working with a notion of computability, we simply work
constructively to extract observational information.
- Franziskus Wiesnet, Signed Digit Code of Reals. 23. August 2017
Abstract: This speech is about an insight in the master theses
"Constructive Analysis with Exact Reals". This paper deals with three
subjects: - An introduction to the theory of computable functionals
(TCF) - A tutorial about the handling of the prove assistent Minlog -
Real numbers and their signed digit code (SD code) There will be an
overview of all three parts but especially we will take a look at the
third part. Here the object is, that we get form the SD code of the
reals x,y the SD code of (x+y)/2 and under certain conditions the SD
code of x/y. Therefore we use the method of program extraction from
proves, which is object of the first chapter. In so doing we gain the
correctness of our algorithm for free. For an efficient
implementation we use the prove assistent Minlog. The prove itself is
done by coinduction and thus the extracted term will use
corecursion. We will see how efficient it is.
- Paulo Oliva, Bar recursion over finite partial functions. 16. August 2017
Abstract: We introduce a new, demand-driven variant of Spector's bar
recursion in the spirit of the Berardi-Bezem-Coquand functional of
[4]. The recursion takes place over finite partial functions u, where
the control parameter omega, used in Spector's bar recursion to terminate
the computation at sequences s satisfying omega(hat{s})<|s|, now acts
as a guide for deciding exactly where to make bar recursive updates,
terminating the computation whenever omega(hat{u}) in dom(u). We
begin by exploring theoretical aspects of this new form of recursion,
then in the main part of the paper we show that demand-driven bar
recursion can be directly used to give an alternative functional
interpretation of classical countable choice. We provide a short case
study as an illustration, in which we extract a new bar recursive
program from the proof that there is no injection from N -> N to N,
and compare this with the program that would be obtained using
Spector's original variant. We conclude by formally establishing that
our new bar recursor is primitive recursively equivalent to the
original Spector bar recursion, and thus defines the same class of
functionals when added to Gödel's system T.
- Makoto Fujiwara, Weak fragments of double negation shift and related
principles in arithmetic. 9. August 2017
Abstract: We investigate two weak fragments of the double negation
shift schema, which are motivated respectively from Spector's
consistency proof of ACA_0 and from the negative translation of RCA_0
(both of which are well-known axiom systems in reverse mathematics),
as well as double negated variants of logical principles. Their
interrelations over both intuitionistic arithmetic and analysis are
completely solved. This is a joint work with Ulrich Kohlenbach.
- Andreas Franz, Wedge sum and smash product in homotopy type theory.
2. August 2017
Abstract: Martin-Löf's intensional type theory can be extended with higher
inductive types (HITs), which generalize ordinary inductive types,
since, in addition to point constructors, constructors that output
(higher) paths are allowed. We focus on a specific class of HITs, the
so-called pushout types, which define important types from the geometric
point of view. In order to show that pushouts are invariant under
homotopy, and thus feasible in the framework of homotopy type theory, we
develop a tool-set to induce the right morphisms between them. We
elaborate two fundamental examples of puhsouts types, the wedge sum and
the smash product of pointed types. Using our tool-set we show that
these two pushouts correspond to the coproduct and tensor product,
respectively, in the subcategory of pointed types and base-point
preserving functions.
- Christoph Mussenbrock, tba. 19. Juli 2017. Fällt aus;
verschoben aus das Wintersemester.
- Thomas Powell, Some applications of monads in proof theory. 12. Juli 2017
Abstract. During the last year I ended up thinking a little about monads,
as they appear in functional programming. In this talk I would like
present two applications of monads in proof theory: The first concerning
the complexity analysis of higher-order functionals, and the second a
variant of Goedel's functional interpretation with a global state.
- Alexander Leitsch, CERES: automated deduction in proof theory.
5. Juli 2017
Abstract. CERES (cut-elimination by resolution) is a method of cut-elimination
which strongly differs from cut-elimination a la Gentzen. Instead of
reducing a proof p stepwise (and thereby simplifying the cuts) CERES
computes a formula CL(p) represented as so-called characteristic
clause set. CL(p) encodes the structure of the derivations of cuts in
p and is always unsatisfiable. In classical logic any resolution
refutation r of CL(p) can be taken as a skeleton of a CERES normal
form p* of p (in p* all cuts are atomic); p* can be constructed from r
by inserting proof projections in the leaves of r (a proof projections
p' of a proof p of F |- G is a cut-free proof of A,F |- G,B where A |-
B is an element of CL(p) and p' is constructed from p by skipping
inferences going to a cut). CERES was mainly designed as a
computational tool for proof analysis and for performing
cut-elimination in long and complex proofs (an implementation of the
method was successfully applied to Fürstenberg's proof of the
infinitude of primes).
There is, however, also an interesting theoretical aspect of the CERES
method: reductive cut-elimination based on the rules of Gentzen can be
shown to be ``redundant'' with respect to CERES in the following
sense: if p reduces to p' then CL(p) subsumes CL(p') (subsumption is a
principle of redundancy-elimination in automated deduction). This
redundancy property can be used to prove that reductive methods (of a
specific type) can never outperform CERES. But subsumption also plays
a major role in proving the completeness of intuitionistic CERES
(CERES-i). If CERES is applied to an intuitionistic proof p of S its
CERES normal form p* is typically a classical proof of S which (in
general) cannot be transformed into a cut-free intuitionistic proof of
S; in particular it turns out that some resolution refutations of
CL(p) do not admit constructions of intuitionistic proofs at
all. CERES-i
solves this problem by introducing the concept of proof resolution, a
generalization of clausal resolution to resolution of cut-free
proofs. The completeness of CERES-i can then be proven via a
subsumption property for cut-free proofs and a subsumption property
for proof projections under reductive cut-elimination. The results
demonstrate that principles invented in the area of automated
deduction can be fruitfully applied to proof theory.
- Benedikt Hoeltgen, Explizite Berechnung von gemeinsamen Kontrakta
durch einen neuen Beweis des Satzes von Church Rosser. 7. Juni 2017
Zusammenfassung:
Mithilfe des Beweises von Ken-etsu Fujita lässt sich ein "gemeinsames
Kontrakum" von zwei beta-gleichen Lambda-Termen berechnen. Dieser Beweis
soll auf die alternative Darstellung des Lambda-Kalküls angewendet werden,
welche Masahiko Sato in seinem Vortrag vorgestellt hat.
- Kenji Miyamoto,
Computational interpretation and complexity analysis in epsilon-calculi.
31. Mai 2017
Abstract: I am going to give a progress report of the research project
for computational interpretation and complexity analysis in
epsilon-calculi. This is joint work with Georg Moser.
One benefit of using epsilon-calculus is that some proofs can be
remarkably shorter than the case in first-order predicate logic. An
objective of our research is to make use of this advantage in
computational interpretation of proofs and applications. Proof
complexity is also the main issue as it is a computational metric of
analyzing proofs.
I firstly talk about existing results in intuitionistic epsilon
calculus, and present my observation about what would be possible and
what would not be. I secondary talk about a result in complexity
analysis in classical epsilon calculus with the equality.
- Masahiko Sato,
A common notation system for both lambda calculus and combinatory logic.
24. Mai 2017
Abstract:
We present a notation system which can be used to faithfully represent
both the terms of lambda calculus and combinatory logic. We show
the faithfullness of the representations by observing that the
representations respect the beta and eta reduction rules. We also
argue that Curry's Last Problem (J.R.Hindley, Curry's Last Problem:
Imitating lambda-beta-reduction in Combinatory Logic) in its original
form is an ill-posed problem, and can be solved naturally by expressing
the problem in our notation system.
- Dirk Schlimm, Frege's Begriffsschrift notation:
Design principles and trade-offs. 17. Mai 2017
- Anton Freund, A Well-Ordering Principle of Higher Type. 3. Mai 2017
Abstract: A construction which transforms well-orderings into
(stronger) well-orderings is called a well-ordering principle. Many
set existence axioms of complexity Pi^1_2 have been characterized in
terms of well-ordering principles (e.g. arithmetical comprehension,
arithmetical transfinite recursion, existence of omega-models of bar
induction). I will present a well-ordering principle of higher type,
which takes well-ordering principles as input and transforms them into
well-orderings. This "higher Bachmann-Howard principle" is equivalent
(over Simpson's set theoretic version of ATR_0) to the existence of
admissible sets, and thus to Pi^1_1-comprehension (preprint available
as arXiv:1704.01662).
- Besprechung mit Examenskandidaten, 10. Mai 2017
- Konstantin Schlagbauer, A syntactic approach to extension
theorems. 26. April 2017
Frühere Vorträge im WS 2016/17
- Ryota Akiyoshi, Strong normalization for the parameter-free subsystem
of system F based on the Omega-rule and
Makoto Fujiwara, Constructive reverse mathematics of weak fragments of
bar induction,
22. Februar 2017
Abstract Akiyoshi: In this talk, we present a proof of the strong
normalization of the parameter-free subsystem of Girard's system F
using the Omega-rule due to Buchholz. This is joint work with
Kazushige Terui.
Abstract Fujiwara: Bar induction is a principle which is accepted in
Brouwer's intuitionistic mathematics. In the context of constructive
reverse mathematics, we investigate the interrelation between weak
fragments of bar induction and the negative translation of weak
countable choice which comes from Goedel-Spector reduction of
classical subsystem ACA of second-order arithmetic.
- SunYoung Kim, An overview of the state of the art of the formalisation of
linear algebra using Coq, 8. Februar 2017
Abstract: In this talk, we discuss the state of the art of the
formalisation of linear algebra related with our recent project. The
main goal of the project is to develop a library for Coq which
suffices for a semester course in the undergraduate level.
- Gyesik Lee, Towards an efficient implementation of real algebraic numbers,
Freitag, 2. Februar 2017, 10:15-11:45, B349 (Sitzungszimmer)
Abstract: This talk gives an introduction to a new project on exact real
number arithmetic. We explain first our motivation and intention, then
introduce a work we currently study, which is done by Cyril Cohen as a part
of the Mathematical Components library for the proof assistant Coq.
- AG Normalisierung und Dekoration, 25. Januar 2017
- Hans Leiss, $\mu$-Continuous Chomsky Algebras:
Equational Theory and Closure under Matrix Ring Formation, 11. Januar 2017
Zusammenfassung: In the course of providing an (infinitary)
axiomatization of the equational theory of the class of context-free
languages, N.Grathwohl, D.Kozen and F.Henglein (2013) have introduced
the class of $\mu$-continuous Chomsky algebras. These are idempotent
semirings where systems of polynomial inequations (i.e.~context-free
grammars) have least solutions -although they are not CPOs- and where
multiplication is continuous with respect to the least fixed point
operator $\mu$. We review their equational theory and prove that the
matrix ring of a $\mu$-continuous Chomsky algebra also is a
$\mu$-continuous Chomsky algebra.
- Arbeitsgemeinschaft Bern München (ABM),
Donnerstag und Freitag, 8. und 9. Dezember 2016.
Program
- Wieslaw Kubis, Generic objects and infinite games, 26. October 2016.
Abstract. Let $F$ be a fixed class of `small' mathematical structures
(e.g. finite graphs, finite-dimensional normed spaces, etc.) and
assume that a notion of `embedding' has been defined so that we can
say that one structure is an extension of another. We say that a
structure is `big' if it can be build as the union (or, more formally,
colimit) of a chain of embeddings in $F$. Fix a big structure $U$. We
consider the following infinite game for two players: Player I chooses
a structure $S_0$ from $F$. Player II responds by its extension $S_1$,
again in $F$. Player I responds by an extension $S_2$ of $S_1$. And so
on. We say that Player II wins if the union of the infinite chain of
$S_n$'s is isomorphic to $U$, otherwise Player I wins. We say that $U$
is generic, if Player II has a winning strategy.
In the talk I will present examples of generic objects in several
areas of mathematics. Further, I will show some of their basic
properties and relations to the theory of universal homogeneous
models.
- Imme van den Berg, Nonstandard Analysis, external numbers and the Sorites paradox, Friday 21. October 2016, 10-12 (!), B132 (!)
Abstract. The Sorites paradox says that a heap of sand remains a heap by removing one
grain, while adding a grain to a set of individual grains remains a set of
individual grains. The paradox can be consistently modeled within
nonstandard analysis: the successor of a standard integer is a standard
integer, while the predecessor of a nonstandard integer is a nonstandard
integer.
More in general, intuitive orders of magnitude of numbers have the Sorites
property. Within classical analysis they can be modeled only functionally,
by O^{\prime }s and o^{\prime }s, but in nonstandard analysis they can
be modeled by external sets, and give rise to the notions of \emph{neutrices}
and \emph{external numbers}. A neutrix is a convex additive subgroup of the
nonstandard real numbers. Obvious neutrices are \pounds, the external set
of limited numbers and \oslash, the external set of infinitesimals, as
external sets they are not of the same logical nature. An external number
\alpha is the sum \alpha =a+A of a nonstandard real number a and a
neutrix A.
The external set E of external numbers has strong algebraic
properties; distributivity has to be handled with some care, but it can be
completely characterized [1]. Also, E is
totally ordered and Dedekind completeness holds if the underlying
nonstandard structure is sufficiently saturated for Nelson's reduction
algorithm [3], [2] to hold.
Some applications are given in mathematical modeling of vague concepts and
error analysis.
Finally we present a first-order axiomatics for the calculus of external
numbers. It is formulated in the language \{+,\cdot ,\leq \}, using
schemes for the Dedekind property and induction. In a sense the axiomatics
gives an approach to the nonstandard reals, which, like in the case of the
classical reals, is based on algebraic, analytic and arithmetical axioms.
[1] B. Dinis, I. P. van den Berg, Algebraic
properties of external numbers, J. Logic and Analysis 3:9 (2011) 1--30.
[2] F. Koudjeti, I.P. van den Berg,
Neutrices, external numbers and external calculus, in: Nonstandard Analysis
in Practice, F. and M. Diener (eds.), Springer Universitext (1995) 145-170.
[3] E. Nelson, Internal Set Theory, an axiomatic
approach to nonstandard analysis, Bull. Am. Math. Soc., 83:6 (1977)
1165-1198.
Frühere Vorträge
Ab
SS 2006.
Letzte Änderung
11. Februar 2019