We improve the answer to the question: what set of excluded middles for
propositional variables in a formula suffices to prove the formula in
intuitionistic propositional logic whenever it is provable in classical
propositional logic.
In this paper we study the behaviour at infinity of the Fourier transform of
Radon measures supported by the images of fractal sets under an algorithmically
random Brownian motion. We show that, under some computability conditions on
these sets, the Fourier transform of the associated measures have, relative to
the Hausdorff dimensions of these sets, optimal asymptotic decay at infinity.
The argument relies heavily on a direct characterisation, due to Asarin and
Pokrovskii, of algorithmically random Brownian motion in terms of the prefix
free Kolmogorov complexity of finite binary sequences. The study also
necessitates a closer look at the potential theory over fractals from a
computable point of view.
We investigate wether three statements in analysis, that can be proved
classically, are realizable in the realizability model of extensional
continuous functionals induced by Kleene's second model $K_2$. We prove that a
formulation of the Riemann Permutation Theorem as well as the statement that
all partially Cauchy sequences are Cauchy cannot be realized in this model,
while the statement that the product of two anti-Specker spaces is anti-Specker
can be realized.
We study domain representations induced by dyadic subbases and show that a
proper dyadic subbase S of a second-countable regular space X induces an
embedding of X in the set of minimal limit elements of a subdomain D of
$\{0,1,\perp\}\omega$. In particular, if X is compact, then X is a retract of
the set of limit elements of D.
In functional analysis it is well known that every linear functional defined
on the dual of a locally convex vector space which is continuous for the weak
topology is the evaluation at a uniquely determined point of the given vector
space. M. Schroeder and A. Simpson have obtained a similar result for lower
semicontinuous linear functionals on the cone of all Scott-continuous
valuations on a topological space endowed with the weak upper topology, an
asymmetric version of the weak topology. This result has given rise to several
proofs, originally by the Schroeder and Simpson themselves and, more recently,
by the author of these Notes and by J. Goubault-Larrecq. The proofs developed
from very technical arguments to more and more conceptual ones. The present
Note continues on this line, presenting a conceptual approach inspired by
classical functional analysis which may prove useful in other situations.
We introduce Z-stability, a notion capturing the intuition that if a function
f maps a metric space into a normed space and if the norm of f(x) is small,
then x is close to a zero of f. Working in Bishop's constructive setting, we
first study pointwise versions of Z-stability and the related notion of good
behaviour for functions. We then present a recursive counterexample to the
classical argument for passing from pointwise Z-stability to a uniform version
on compact metric spaces. In order to effect this passage constructively, we
bring into play the positivity principle, equivalent to Brouwer's fan theorem
for detachable bars, and the limited anti-Specker property, an intuitionistic
counterpart to sequential compactness. The final section deals with connections
between the limited anti-Specker property, positivity properties, and
(potentially) Brouwer's fan theorem for detachable bars.
We consider a special case of Dickson's lemma: for any two functions $f,g$ on
the natural numbers there are two numbers $i<j$ such that both $f$ and $g$
weakly increase on them, i.e., $f_i\le f_j$ and $g_i \le g_j$. By a
combinatorial argument (due to the first author) a simple bound for such $i,j$
is constructed. The combinatorics is based on the finite pigeon hole principle
and results in a descent lemma. From the descent lemma one can prove Dickson's
lemma, then guess what the bound might be, and verify it by an appropriate
proof. We also extract (via realizability) a bound from (a formalization of)
our proof of the descent lemma.
Keywords: Dickson's lemma, finite pigeon hole principle, program extraction
from proofs, non-computational quantifiers.
We discuss possibilities of application of Numerical Analysis methods to
proving computability, in the sense of the TTE approach, of solution operators
of boundary-value problems for systems of PDEs. We prove computability of the
solution operator for a symmetric hyperbolic system with computable real
coefficients and dissipative boundary conditions, and of the Cauchy problem for
the same system (we also prove computable dependence on the coefficients) in a
cube $Q\subseteq\mathbb R^m$. Such systems describe a wide variety of physical
processes (e.g. elasticity, acoustics, Maxwell equations). Moreover, many
boundary-value problems for the wave equation also can be reduced to this case,
thus we partially answer a question raised in Weihrauch and Zhong (2002).
Compared with most of other existing methods of proving computability for PDEs,
this method does not require existence of explicit solution formulas and is
thus applicable to a broader class of (systems of) equations.
We identify four countable topological spaces $S_2$, $S_1$, $S_D$, and $S_0$
which serve as canonical examples of topological spaces which fail to be
quasi-Polish. These four spaces respectively correspond to the $T_2$, $T_1$,
$T_D$, and $T_0$-separation axioms. $S_2$ is the space of rationals, $S_1$ is
the natural numbers with the cofinite topology, $S_D$ is an infinite chain
without a top element, and $S_0$ is the set of finite sequences of natural
numbers with the lower topology induced by the prefix ordering. Our main result
is a generalization of Hurewicz's theorem showing that a co-analytic subset of
a quasi-Polish space is either quasi-Polish or else contains a countable
$\Pi^0_2$-subset homeomorphic to one of these four spaces.
