Workshop "Logic and its Applications", 12th October 2016
A small workshop "Logic and its Applications" will be held on Wednesday October 12, 2016, in Room B349 of Mathematisches Institut der Universität München Theresienstr. 39, D-80333 München.
Talks
- Sam Sanders, On the interplay between Nonstandard Analysis and
computability theory
- Chuangjie Xu, Extracting computer programs from nonstandard proofs
- Kenji Miyamoto, Progress report on Minlog's soundness proof generator
- Iosif Petrakis, Constructive uniformities of pseudometrics
- Hajime Ishihara, Versions of the weak Koenig lemma and the disjunctive
dependent choice (joint work with Josef Berger and Takako Nemoto)
- Takako Nemoto, Non-deterministic inductive definitions and Fullness
- Tatsuji Kawai, Localic completion of uniform space
- Masahiko Sato, Proof theory of the lambda-calculus
Schedule
09:00-09:45 Sam Sanders
09:50-10:35 Chuangjie Xu
11:00-11:45 Kenji Miyamoto
11:50-12:35 Iosif Petrakis
14:30-15:15 Hajime Ishihara
15:20-16:05 Takako Nemoto
16:30-17:15 Tatsuji Kawai
17:20-18:05 Masahiko Sato
Abstracts
- Sam Sanders, On the interplay between Nonstandard Analysis and
computability theory
Abstract. We survey recent results on the connection between Nonstandard
Analysis (NSA) and computability theory. We present a number of
negative and positive results and how they translate back and forth
between NSA and computability theory. Of particular interest is how a
negative result regarding the axioms of NSA (namely 'Transfer =/=>
Standardization') gives rise to two fundamentally different paths from
second-order to higher-order mathematics (and the associated notions
of computability).
-
Chuangjie Xu, Extracting computer programs from nonstandard proofs
Abstract.
A constructive fragment of Nelson's Internal Set Theory, namely system
H (as it is based on Heyting Arithmetic), has been introduced by van
den Berg et al. [1]. We are interested in H because it allows us to
obtain computational content from Nonstandard Analysis via a
nonstandard variant of the Dialectica interpretation [1]. To extract
computer programs from nonstandard proofs, we reformulate the
nonstandard Dialectica interpretation in a way that is suitable for a
type-theoretic development. Then we embed H within the Agda proof
assistant and formalise (parts of) the soundness proof of the
Dialectica interpretation of H to obtain Agda programs from proofs in
H.
[1] Benno van den Berg, Eyvind Briseid, and Pavol Safarik, A
functional interpretation for nonstandard arithmetic, Annals of Pure
and Applied Logic 163 (2012), no. 12, 1962?1994.
- Kenji Miyamoto, Progress report on Minlog's soundness proof generator
Abstract: I am going to report the progress of the implementation of
Minlog's soundness proof generator. Within the behind theory of
Minlog, the soundness theorem of program extraction claims that for a
given constructive proof M of a formula A, there exists another proof
M', so-called a soundness proof, concluding that the program extracted
from M is a realizer of A. Based on this theorem, Minlog can
automatically generates soundness proofs, but not yet for all proofs
in the theory. I talk about the recent work in order to extend this
feature to support coinductive proofs.
- Hajime Ishihara, Versions of the weak Koenig lemma and the disjunctive
dependent choice
Abstract. The weak Koenig lemma (WKL) is equivalent to the
disjunctive dependent choice for $\Pi^0_1$ formulae and the lesser
limited principle of omniscience (LLOP). We will look into a proof of
the equivalence, and adoptations of it for the equivalences between
WKL for trees having at most two nodes at each level and a version of
the disjunctive dependent choice with LLPO, and between WKL for convex
trees and another version of the disjunctive dependent choice with
LLPO.
- Iosif Petrakis, Constructive uniformities of pseudometrics
Abstract. We show how the theory of uniform spaces the uniformities of
which are defined through pseudometrics can be developed in the same
system and in a similar way to the theory of Bishop spaces. We also
discuss the interplay between these two approaches to constructive
function-theoretic topology.
- Takako Nemoto, Non-deterministic inductive definitions and Fullness.
Abstract. We consider the non-deterministic inductive definition
principle NID with the weak notion of a set-generated class
introduced by van den Berg [2] and with the strong notion of a
set-generated class adopted by Aczel et al. [1]. We introduce
a principle, called nullary NID, and prove that nullary NID is
equivalent to Fullness in a subsystem of the
constructive Zermelo-Fraenkel set theory.
[1] Peter Aczel, Hajime Ishihara, Takako Nemoto and Yasushi Sangu,
Generalized geometric theories and set-generated classes,
Mathematical Structures Computer Science, Volume 25, Issue 7
(Computing with Infinite Data:
Topological and Logical Foundations Part 1) October 2015, pp. 1466-1483
[2] Benno van den Berg, Non-deterministic inductive definitions,
Archive for Mathematical Logic Volume 52, Issue 1, pp. 113-135
- Tatsuji Kawai, Localic completion of uniform space
Abstract. We extend the localic completion of generalised metric
spaces by Steven Vickers to the setting of uniform spaces defined via
family of pseudometrics. In particular, the localic completion gives
rise to an embedding of Bishop's locally compact uniform spaces into
formal topologies. As a by-product, the localic completion gives
predicative completions of uniform spaces.
- Masahiko Sato, Proof theory of the lambda-calculus
Abstract. We develop a proof theory of the lambda-calculus where we
study the set of closed lambda terms by inductively defining the set
as a free algebra. The novelty of the approach is that we construct
and study lambda-calculus without using the notions of variables and
alpha-equivalence. In this approach we can study lambda-terms as
combinators and can have a clean proof of the Church-Rosser Theorem in
the Minlog proof assistant. This is a joint work with Helmut
Schwichtenberg and Takafumi Sakurai.
Helmut Schwichtenberg
Last change: 11. October 2016
09:00-09:45 Sam Sanders 09:50-10:35 Chuangjie Xu 11:00-11:45 Kenji Miyamoto 11:50-12:35 Iosif Petrakis 14:30-15:15 Hajime Ishihara 15:20-16:05 Takako Nemoto 16:30-17:15 Tatsuji Kawai 17:20-18:05 Masahiko Sato
Abstracts
- Sam Sanders, On the interplay between Nonstandard Analysis and
computability theory
Abstract. We survey recent results on the connection between Nonstandard
Analysis (NSA) and computability theory. We present a number of
negative and positive results and how they translate back and forth
between NSA and computability theory. Of particular interest is how a
negative result regarding the axioms of NSA (namely 'Transfer =/=>
Standardization') gives rise to two fundamentally different paths from
second-order to higher-order mathematics (and the associated notions
of computability).
-
Chuangjie Xu, Extracting computer programs from nonstandard proofs
Abstract.
A constructive fragment of Nelson's Internal Set Theory, namely system
H (as it is based on Heyting Arithmetic), has been introduced by van
den Berg et al. [1]. We are interested in H because it allows us to
obtain computational content from Nonstandard Analysis via a
nonstandard variant of the Dialectica interpretation [1]. To extract
computer programs from nonstandard proofs, we reformulate the
nonstandard Dialectica interpretation in a way that is suitable for a
type-theoretic development. Then we embed H within the Agda proof
assistant and formalise (parts of) the soundness proof of the
Dialectica interpretation of H to obtain Agda programs from proofs in
H.
[1] Benno van den Berg, Eyvind Briseid, and Pavol Safarik, A
functional interpretation for nonstandard arithmetic, Annals of Pure
and Applied Logic 163 (2012), no. 12, 1962?1994.
- Kenji Miyamoto, Progress report on Minlog's soundness proof generator
Abstract: I am going to report the progress of the implementation of
Minlog's soundness proof generator. Within the behind theory of
Minlog, the soundness theorem of program extraction claims that for a
given constructive proof M of a formula A, there exists another proof
M', so-called a soundness proof, concluding that the program extracted
from M is a realizer of A. Based on this theorem, Minlog can
automatically generates soundness proofs, but not yet for all proofs
in the theory. I talk about the recent work in order to extend this
feature to support coinductive proofs.
- Hajime Ishihara, Versions of the weak Koenig lemma and the disjunctive
dependent choice
Abstract. The weak Koenig lemma (WKL) is equivalent to the
disjunctive dependent choice for $\Pi^0_1$ formulae and the lesser
limited principle of omniscience (LLOP). We will look into a proof of
the equivalence, and adoptations of it for the equivalences between
WKL for trees having at most two nodes at each level and a version of
the disjunctive dependent choice with LLPO, and between WKL for convex
trees and another version of the disjunctive dependent choice with
LLPO.
- Iosif Petrakis, Constructive uniformities of pseudometrics
Abstract. We show how the theory of uniform spaces the uniformities of
which are defined through pseudometrics can be developed in the same
system and in a similar way to the theory of Bishop spaces. We also
discuss the interplay between these two approaches to constructive
function-theoretic topology.
- Takako Nemoto, Non-deterministic inductive definitions and Fullness.
Abstract. We consider the non-deterministic inductive definition
principle NID with the weak notion of a set-generated class
introduced by van den Berg [2] and with the strong notion of a
set-generated class adopted by Aczel et al. [1]. We introduce
a principle, called nullary NID, and prove that nullary NID is
equivalent to Fullness in a subsystem of the
constructive Zermelo-Fraenkel set theory.
[1] Peter Aczel, Hajime Ishihara, Takako Nemoto and Yasushi Sangu,
Generalized geometric theories and set-generated classes,
Mathematical Structures Computer Science, Volume 25, Issue 7
(Computing with Infinite Data:
Topological and Logical Foundations Part 1) October 2015, pp. 1466-1483
[2] Benno van den Berg, Non-deterministic inductive definitions,
Archive for Mathematical Logic Volume 52, Issue 1, pp. 113-135
- Tatsuji Kawai, Localic completion of uniform space
Abstract. We extend the localic completion of generalised metric
spaces by Steven Vickers to the setting of uniform spaces defined via
family of pseudometrics. In particular, the localic completion gives
rise to an embedding of Bishop's locally compact uniform spaces into
formal topologies. As a by-product, the localic completion gives
predicative completions of uniform spaces.
- Masahiko Sato, Proof theory of the lambda-calculus
Abstract. We develop a proof theory of the lambda-calculus where we
study the set of closed lambda terms by inductively defining the set
as a free algebra. The novelty of the approach is that we construct
and study lambda-calculus without using the notions of variables and
alpha-equivalence. In this approach we can study lambda-terms as
combinators and can have a clean proof of the Church-Rosser Theorem in
the Minlog proof assistant. This is a joint work with Helmut
Schwichtenberg and Takafumi Sakurai.
Helmut Schwichtenberg
Last change: 11. October 2016
Abstract. We survey recent results on the connection between Nonstandard Analysis (NSA) and computability theory. We present a number of negative and positive results and how they translate back and forth between NSA and computability theory. Of particular interest is how a negative result regarding the axioms of NSA (namely 'Transfer =/=> Standardization') gives rise to two fundamentally different paths from second-order to higher-order mathematics (and the associated notions of computability).
Abstract. A constructive fragment of Nelson's Internal Set Theory, namely system H (as it is based on Heyting Arithmetic), has been introduced by van den Berg et al. [1]. We are interested in H because it allows us to obtain computational content from Nonstandard Analysis via a nonstandard variant of the Dialectica interpretation [1]. To extract computer programs from nonstandard proofs, we reformulate the nonstandard Dialectica interpretation in a way that is suitable for a type-theoretic development. Then we embed H within the Agda proof assistant and formalise (parts of) the soundness proof of the Dialectica interpretation of H to obtain Agda programs from proofs in H.
[1] Benno van den Berg, Eyvind Briseid, and Pavol Safarik, A functional interpretation for nonstandard arithmetic, Annals of Pure and Applied Logic 163 (2012), no. 12, 1962?1994.
Abstract: I am going to report the progress of the implementation of Minlog's soundness proof generator. Within the behind theory of Minlog, the soundness theorem of program extraction claims that for a given constructive proof M of a formula A, there exists another proof M', so-called a soundness proof, concluding that the program extracted from M is a realizer of A. Based on this theorem, Minlog can automatically generates soundness proofs, but not yet for all proofs in the theory. I talk about the recent work in order to extend this feature to support coinductive proofs.
Abstract. The weak Koenig lemma (WKL) is equivalent to the disjunctive dependent choice for $\Pi^0_1$ formulae and the lesser limited principle of omniscience (LLOP). We will look into a proof of the equivalence, and adoptations of it for the equivalences between WKL for trees having at most two nodes at each level and a version of the disjunctive dependent choice with LLPO, and between WKL for convex trees and another version of the disjunctive dependent choice with LLPO.
Abstract. We show how the theory of uniform spaces the uniformities of which are defined through pseudometrics can be developed in the same system and in a similar way to the theory of Bishop spaces. We also discuss the interplay between these two approaches to constructive function-theoretic topology.
Abstract. We consider the non-deterministic inductive definition principle NID with the weak notion of a set-generated class introduced by van den Berg [2] and with the strong notion of a set-generated class adopted by Aczel et al. [1]. We introduce a principle, called nullary NID, and prove that nullary NID is equivalent to Fullness in a subsystem of the constructive Zermelo-Fraenkel set theory.
[1] Peter Aczel, Hajime Ishihara, Takako Nemoto and Yasushi Sangu, Generalized geometric theories and set-generated classes, Mathematical Structures Computer Science, Volume 25, Issue 7 (Computing with Infinite Data: Topological and Logical Foundations Part 1) October 2015, pp. 1466-1483
[2] Benno van den Berg, Non-deterministic inductive definitions, Archive for Mathematical Logic Volume 52, Issue 1, pp. 113-135
Abstract. We extend the localic completion of generalised metric spaces by Steven Vickers to the setting of uniform spaces defined via family of pseudometrics. In particular, the localic completion gives rise to an embedding of Bishop's locally compact uniform spaces into formal topologies. As a by-product, the localic completion gives predicative completions of uniform spaces.
Abstract. We develop a proof theory of the lambda-calculus where we study the set of closed lambda terms by inductively defining the set as a free algebra. The novelty of the approach is that we construct and study lambda-calculus without using the notions of variables and alpha-equivalence. In this approach we can study lambda-terms as combinators and can have a clean proof of the Church-Rosser Theorem in the Minlog proof assistant. This is a joint work with Helmut Schwichtenberg and Takafumi Sakurai.