|
|
|
|
|
The
seminar is held in hybrid
format, in person (Múzeum
krt. 4/i Room 224) and
online at the following
link:
|
| 7
March (Friday) 4:15
PM Room 224 + ONLINE
|
|
Ambrus
Kaposi
|
|
Department
of Programming Languages
and Compilers
Faculty of Informatics,
Eötvös University
Budapest
|
| |
Proof as
code
|
Martin-Löf's type
theory combines ideas from
Hilbert's formalism, Brouwer's
intuitionism and Russell's theory
of types. In this talk, I will
explain how terms in Martin-Löf's
type theory can represent proofs
and how they can be executed as
programs. I will also compare the
set-theoretic and type-theoretic
foundations of mathematics, and
present an open problem for
foundations.
|
|
| 14
March (Friday) 4:15
PM Room 224 + ONLINE
|
|
Joanna
Luc
|
|
Institute
of Philosophy,
Jagiellonian University,
Kraków
|
| |
What are
the bearers of hidden states?
On an important ambiguity in
the formulation of Bell’s
theorem
|
Bell’s conclusion
from his famous inequality was
that any hidden variable theory
that satisfies Local Causality is
incompatible with the predictions
of Quantum Mechanics (QM) for
Bell’s Experiment. However, Local
Causality does not appear in the
derivation of Bell’s inequality.
Instead, two other assumptions are
used, namely Factorizability and
Settings Independence. Therefore,
in order to establish Bell’s
conclusion, we need to relate
these two assumptions to Local
Causality. The prospects for doing
so turn out to depend on the
assumed location of the hidden
states that appear in Bell’s
inequality. In this paper, I
consider the following two views
on such states: (1) that they are
states of the twoparticle system
at the moment of preparation, and
(2) that they are states of thick
slices of the past light cones of
measurements. I argue that
straightforward attempts to
establish Bell’s conclusion fail
in both approaches. Then, I
consider three refined attempts,
which I also criticise, and I
propose a new way of establishing
Bell’s conclusion that combines
intuitions underlying several
previous approaches.
|
|
| 21
March (Friday) 4:15
PM Room 224 + ONLINE
|
AND (!)
|
| 28
March (Friday) 4:15
PM Room 224 + ONLINE |
|
Kristóf
Kanalas
|
|
Department
of Mathematics, Masaryk
University, Brno
|
| |
Coherent
and accessible categories
|
|
Categorical logic
is
1. The algebraization of logic,
using categories. Coherent
theories, models and
homomorphisms are in bijection
with coherent categories ("fat
distributive lattices"),
Set-valued coherent functors and
natural transformations.
2. A framework for abstract
model theory. Given a theory in
the coherent fragment of
infinitary first-order logic,
its models (with homomorphisms)
form a category. Those
categories which arise this way
can be characterized: they are
called accessible. (The notion
of an accessible category
happens to be a slight
generalization of Shelah's
notion of an abstract elementary
class.)
In these talks I will give an
introduction to coherent
categories and accessible
categories. At the end I will
try to illustrate how techniques
coming from the syntactic side
of categorical logic (number 1)
can solve problems coming from
the semantic side (number 2), by
proving the following: if T is a
coherent theory then in Mod(T)
pure maps are strict
monomorphisms. This gives a
partial positive answer to one
of the open questions from the
book Locally Presentable and
Accessible Categories.
|
|
|
|
|
