L’objet de ce travail est l’utilisation de certains formalismes non classiques (analyses non standard, analyses constructives) afin de proposer des bases théoriques nouvelles autour des problèmes de discrétisations d’objets continus. Ceci est fait en utilisant un modèle discret du système des nombres réels appelé droite d’Harthong-Reeb ainsi que la méthode arithmétisation associée qui est un processus de discrétisation des fonctions continues. Cette étude repose sur un cadre arithmétique non standard. Dans un premier temps, nous utilisons une version axiomatique de l’arithmétique non standard. Puis, dans le but d’améliorer le contenu constructif de notre méthode, nous utilisons une autre approche de l’arithmétique non standard découlant de la théorie des Ω-nombres de Laugwitz et Schmieden. Cette seconde approche amène à une représentation discrète et multi-résolution de fonctions continues.Finalement, nous étudions dans quelles mesures, la droite d’Harthong-Reeb satisfait les axiomes de Bridges décrivant le continu constructif. / The aim of this work is to introduce new theoretical basis for the discretization of continuous objects using non classical formalisms. This is done using a discrete model of the continuum called the Harthong-Reeb line together with the related arithmetization method which is a discretisation process of continuous functions. This study stands on a nonstandard arithmetical framework. Firstly, we use an axiomatic version of nonstandard arithmetic. In order to improve the constructive content of our method, the next step is to use another approach of nonstandard arithmetic deriving from the theory of Ω-numbers by Laugwitzand Schmieden. This second approach leads to a discrete multi-resolution representation of continuous functions. Afterwards, we investigate to what extent the Harthong-Reeb line fits Bridges axioms of the constructive continuum.

The work in this thesis contains some contributions to constructive point-free topology and the theory of apartness spaces. The first two papers deal with constructive domain theory using formal topology. In Paper I we focus on the notion of a domain representation of a formal space as a way to introduce generalized points of the represented space, whereas we in Paper II give a constructive and point-free treatment of the domain theoretic approach to differential calculus. The last two papers are of a slightly different nature but still concern constructive topology. In paper III we consider a measure theoretic covering theorem from various constructive angles in both point-set and point-free topology. We prove a point-free version of the theorem. In Paper IV we deal with issues of impredicativity in the theory of apartness spaces. We introduce a notion of set-presented apartness relation which enables a predicative treatment of basic constructions of point-set apartness spaces.

In this thesis we study the concept of well quasi-order, originally developed in order theory but nowadays transversal to many areas, in the over-all context of proof theory - more precisely, in reverse mathematics and constructive mathematics. Reversed mathematics, proposed by Harvey Friedman, aims to classify the strength of mathematical theorems by identifying the required axioms. In this framework, we focus on two classical results relative to well quasi-orders: Kruskal’s theorem and Higman’s lemma. Concerning the former, we compute the proof-theoretic ordinals of two different versions establishing their non equivalence. Regarding the latter, we study, over the base theory RCA0, the relations between Higman’s original achievements and some versions of Kruskal’s theorem. For what concerns constructive mathematics, which goes back to Brouwer’s reflections and rejects the law of excluded middle in favour of more perspicuous reasoning principles, we scrutinize the main definitions of well quasi-order establishing their constructive nature; moreover, a new constructive proof of Higman’s lemma is proposed paving the way for a systematic analysis of well quasi-orders within constructive means. On top of all this we consider a peculiar phenomenon in proof theory, namely phase transitions in provability. Building upon previous results about provability in Peano Arithmetic, we locate the threshold separating provability and unprovability for statements regarding Goodstein sequences, Hydra games and Ackermannian functions. / In questa tesi studiamo il concetto di well quasi-order, originariamente sviluppato nella teoria degli ordini ma oggi trasversale a molti ambiti, nel contesto generale della teoria della dimostrazione - più precisamente, in reverse mathematics e matematica costruttiva. La reverse mathematics, proposta da Harvey Friedman, mira a classificare la forza dei teoremi matematici individuando gli assiomi richiesti. In questo contesto, ci concentriamo su due risultati classici relativi ai well quasiorder: il teorema di Kruskal e il lemma di Higman. Per quanto riguarda il primo, abbiamo calcolato gli ordinali proof-teoretici di due diverse versioni stabilendone la non equivalenza. Per quanto riguarda il secondo, studiamo, sopra la teoria di base RCA0, le relazioni tra i risultati originali di Higman e alcuni versioni del teorema di Kruskal. Per quanto riguarda la matematica costruttiva, che si rifà alle riflessioni di Brouwer e rifiuta la legge del terzo escluso a favore di principidi ragionamento più perspicui, esaminiamo attentamente le principali definizioni di well quasi-order stabilendone la natura costruttiva; inoltre, viene proposta una nuova dimostrazione costruttiva del lemma di Higman aprendo la strada per una sistematica analisi dei well quasi-order all’interno di metodi costruttivi. Oltre a questo consideriamo un fenomeno peculiare nella teoria della dimostrazione, vale a dire le transizioni di fase nella dimostrabilità. Basandoci su risultati precedenti sulla dimostrabilità nell’aritmetica di Peano, abbiamo individuato la soglia che separa dimostrabilità e indimostrabilità per enunciati riguardanti sequenze di Goodstein, Hydra games e funzioni ackermanniane.

Constructive reverse mathematics is a programme in which non- and semi-constructive principles are classified in accordance with which other principles they imply or are implied by, relative to the framework of Bishop-style constructive mathematics. One such principle that has come under focus in recent years is an antithesis of Specker's theorem (that theorem being a characteristic result of Russian recursive mathematics): this so-called anti-Specker property is intuitionistically valid, and of considerable utility in proving results of real and complex analysis. We introduce several new weakenings of the anti-Specker property and explore their role in constructive reverse mathematics, identifying implication relationships that they stand in to other notable principles. These include, but are not limited to: variations upon Brouwer's fan theorem, certain compactness properties, and so-called zero-stability properties. We also give similar classification results for principles arising directly from Specker's theorem itself, and present new, direct proofs of related fan-theoretic results. We investigate how anti-Specker properties, alongside power-series-based arguments, enable us to recover information about the structure of holomorphic functions: in particular, they allow us to streamline a sequence of maximum-modulus theorems.

In this thesis we present the Stone representation theorem, generally known as Stone duality in the point-free context. The proof is choice-free and, since we do not have to be concerned with points, it is by far simpler than the original. For each infinite cardinal κ we show that the counter- part of the κ-complete Boolean algebras is constituted by the κ-basically disconnected Stone frames. We also present a precise characterization of the morphisms which correspond to the κ-complete Boolean homomorphisms. Although Booleanization is not functorial in general, in the part of the dual- ity for extremally disconnected Stone frames it is, and constitutes an equiv- alence of categories. We finish the thesis by focusing on the De Morgan (or extremally disconnected) frames and present a new characterization of these by their superdense sublocales. We also show that in contrast with this phenomenon, a metrizable frame has no non-trivial superdense sublocale; in other words, a non-trivial Čech-Stone compactification of a metrizable frame is never metrizable. 1

A Matemática Intervalar se assenta em dois conceitos fundamentais, a propriedade da inclusão-monotonicidade de sua aritmética e uma topologia de Hausdorff definida no conjunto dos intervalos. A propriedade da inclusão-monotonicidade tem se revelado uma ferramenta útil na elaboração de algoritmos intervalares, enquanto a topologia de Hausdorff não consegue refletir as características lógicas daquela propriedade, comprometendo, desse modo, a construção de uma lógica cujo modelo seria a estrutura intervalar munida dessa topologia. Essa lógica seria necessária para fundamentação da matemática intervalar como uma teoria de algorítmos da análise real. Neste trabalho se mostra que o insucesso na construção dessa fundamentação se deve a incompatibilidade entre a propriedade da inclusão-monotonicidade e a topologia de Hausdorff. A partir dessa constatação se descarta essa topologia e define-se uma outra topologia - a topologia de Scott - que é compatível com essa propriedade, no sentido de que todo resultado obtido usando-se a lógica, isto é, a propriedade da inclusão-monotonicidade, obtém-se também usando-se a ferramenta topológica e reciprocamente. A teoria resultante da substituição da topologia de Hausdorff pela topologia de Scott tem duas características fundamentais. A Análise Funcional Intervalar resultante possui a maioria das propriedades interessantes da Análise Real, suprimindo, assim, as deficiências da Análise Intervalar anterior. A elaboração da propriedade da inclusão-monotoniciadade permite construir uma lógica geométrica e uma teoria lambda cujo modelo é essa nova matemática intervalar. Além disso, a partir dessa lógica e da teoria lambda se elabora uma teoria construtiva, como a teoria dos tipos de Martin-Löf, que permite se raciocinar com programas dessa matemática. Isso significa a possibilidade de se fazer correção automática de programas da matemática intervalar. Essa nova abordagem da matemática intervalar é desenvolvida pressupondo, apenas, o conceito de número racional, além, é claro, da linguagem da teoria dos conjuntos. Desse modo é construído o sistema intervalar de um modo análogo ao sistema real. Para isso é generalizado o conceito de corte de Dedekind, resultando dessa construção um sistema ordenado denominado de quasi-corpo, em contraste com o números reais cujo sistema é algébrico, o corpo dos números reais. Assim, no sistema intervalar a ordem é um conceito intrínseco ao sistema, diferentemente do sistema de números reais cuja a ordem não faz parte da álgebra do sistema. A lógica dessa nova matemática intervalar é uma lógica categórica. Isto significa que todo resultado obtido para domínios básicos se aplica para o produto cartesiano, união disjunta, o espaço de funções, etc., desses domínios. Isto simplifica consideravelmente a teoria. Um exemplo dessa simplificação é a definição de derivada nessa nova matemática intervalar, conceito ainda não bem definido na teoria intervalar clássica. / The Interval Mathematics is based on two fundamental concepts, the inclusion-monotonicity of its arithmetics and a Hausdorff topology defined on the interval set. The property of inclusion-monotonicity has risen as an useful tool for elaboration of interval algorithms. In contrast, because the Hausdorff topology does not reflect the logical features of that property, the interval mathematics did not, permit the elaboration of a logic whose model is this interval mathematics with that topology. This logic should be necessary to the foundation of the interval mathematics as a Real Analysis Theory of Algorithms. This thesis shows that the theory of algorithms refered above was not possible because of the incompatibility between the property of inclusion-monotonicity and the Hausdorff topology. By knowing the shortcoming of this topology, the next step is to set it aside and to define a new topology - the Scott topology - compatible with the refered property in the sense that every result, obtained via the logic is also obtainable via the topology and vice-versa. After changing the topology the resulting theory has two basic features. The Interval Functional Analysis has got the most, interesting properties belonging to Real Analysis, supressing the shortcomings of previous interval analysis. The elaboration of the inclusion-monotonicity property allows one to construct a geometric logic and a lambda theory whose model is this new interval mathematics. From this logic and from the lambda theory a constructive theory is then elaborated, similar to Martin-Löf type theory, being possible then to reason about programs of this new interval mathematics. This means the possibility of automatically checking the correctness of programs of interval mathematics. This new approach assumes only the concept, of rational numbers beyond, of course, the set theory language. It is constructed an interval system similar to the real system. A general notion of the concept of Dedekind cut was necessary to reach that. The resulting construction is an ordered system which will be called quasi-field, in opposition to the real numbers system which is algebraic. Thus, in the interval system the order is an intrinsic concept, unlike the real numbers sistems whose order does not belong to the algebraic system. The logic of this new interval mathematics is a categorical logic. This means that, every result got for basic domains applies also to cartesian product, disjoint union, function spaces, etc., of these domains. This simplifies considerably the new theory. An example of this simplication is given by the definition of derivative, a concept not, derived by the classical interval theory.

A Matemática Intervalar se assenta em dois conceitos fundamentais, a propriedade da inclusão-monotonicidade de sua aritmética e uma topologia de Hausdorff definida no conjunto dos intervalos. A propriedade da inclusão-monotonicidade tem se revelado uma ferramenta útil na elaboração de algoritmos intervalares, enquanto a topologia de Hausdorff não consegue refletir as características lógicas daquela propriedade, comprometendo, desse modo, a construção de uma lógica cujo modelo seria a estrutura intervalar munida dessa topologia. Essa lógica seria necessária para fundamentação da matemática intervalar como uma teoria de algorítmos da análise real. Neste trabalho se mostra que o insucesso na construção dessa fundamentação se deve a incompatibilidade entre a propriedade da inclusão-monotonicidade e a topologia de Hausdorff. A partir dessa constatação se descarta essa topologia e define-se uma outra topologia - a topologia de Scott - que é compatível com essa propriedade, no sentido de que todo resultado obtido usando-se a lógica, isto é, a propriedade da inclusão-monotonicidade, obtém-se também usando-se a ferramenta topológica e reciprocamente. A teoria resultante da substituição da topologia de Hausdorff pela topologia de Scott tem duas características fundamentais. A Análise Funcional Intervalar resultante possui a maioria das propriedades interessantes da Análise Real, suprimindo, assim, as deficiências da Análise Intervalar anterior. A elaboração da propriedade da inclusão-monotoniciadade permite construir uma lógica geométrica e uma teoria lambda cujo modelo é essa nova matemática intervalar. Além disso, a partir dessa lógica e da teoria lambda se elabora uma teoria construtiva, como a teoria dos tipos de Martin-Löf, que permite se raciocinar com programas dessa matemática. Isso significa a possibilidade de se fazer correção automática de programas da matemática intervalar. Essa nova abordagem da matemática intervalar é desenvolvida pressupondo, apenas, o conceito de número racional, além, é claro, da linguagem da teoria dos conjuntos. Desse modo é construído o sistema intervalar de um modo análogo ao sistema real. Para isso é generalizado o conceito de corte de Dedekind, resultando dessa construção um sistema ordenado denominado de quasi-corpo, em contraste com o números reais cujo sistema é algébrico, o corpo dos números reais. Assim, no sistema intervalar a ordem é um conceito intrínseco ao sistema, diferentemente do sistema de números reais cuja a ordem não faz parte da álgebra do sistema. A lógica dessa nova matemática intervalar é uma lógica categórica. Isto significa que todo resultado obtido para domínios básicos se aplica para o produto cartesiano, união disjunta, o espaço de funções, etc., desses domínios. Isto simplifica consideravelmente a teoria. Um exemplo dessa simplificação é a definição de derivada nessa nova matemática intervalar, conceito ainda não bem definido na teoria intervalar clássica. / The Interval Mathematics is based on two fundamental concepts, the inclusion-monotonicity of its arithmetics and a Hausdorff topology defined on the interval set. The property of inclusion-monotonicity has risen as an useful tool for elaboration of interval algorithms. In contrast, because the Hausdorff topology does not reflect the logical features of that property, the interval mathematics did not, permit the elaboration of a logic whose model is this interval mathematics with that topology. This logic should be necessary to the foundation of the interval mathematics as a Real Analysis Theory of Algorithms. This thesis shows that the theory of algorithms refered above was not possible because of the incompatibility between the property of inclusion-monotonicity and the Hausdorff topology. By knowing the shortcoming of this topology, the next step is to set it aside and to define a new topology - the Scott topology - compatible with the refered property in the sense that every result, obtained via the logic is also obtainable via the topology and vice-versa. After changing the topology the resulting theory has two basic features. The Interval Functional Analysis has got the most, interesting properties belonging to Real Analysis, supressing the shortcomings of previous interval analysis. The elaboration of the inclusion-monotonicity property allows one to construct a geometric logic and a lambda theory whose model is this new interval mathematics. From this logic and from the lambda theory a constructive theory is then elaborated, similar to Martin-Löf type theory, being possible then to reason about programs of this new interval mathematics. This means the possibility of automatically checking the correctness of programs of interval mathematics. This new approach assumes only the concept, of rational numbers beyond, of course, the set theory language. It is constructed an interval system similar to the real system. A general notion of the concept of Dedekind cut was necessary to reach that. The resulting construction is an ordered system which will be called quasi-field, in opposition to the real numbers system which is algebraic. Thus, in the interval system the order is an intrinsic concept, unlike the real numbers sistems whose order does not belong to the algebraic system. The logic of this new interval mathematics is a categorical logic. This means that, every result got for basic domains applies also to cartesian product, disjoint union, function spaces, etc., of these domains. This simplifies considerably the new theory. An example of this simplication is given by the definition of derivative, a concept not, derived by the classical interval theory.

A Matemática Intervalar se assenta em dois conceitos fundamentais, a propriedade da inclusão-monotonicidade de sua aritmética e uma topologia de Hausdorff definida no conjunto dos intervalos. A propriedade da inclusão-monotonicidade tem se revelado uma ferramenta útil na elaboração de algoritmos intervalares, enquanto a topologia de Hausdorff não consegue refletir as características lógicas daquela propriedade, comprometendo, desse modo, a construção de uma lógica cujo modelo seria a estrutura intervalar munida dessa topologia. Essa lógica seria necessária para fundamentação da matemática intervalar como uma teoria de algorítmos da análise real. Neste trabalho se mostra que o insucesso na construção dessa fundamentação se deve a incompatibilidade entre a propriedade da inclusão-monotonicidade e a topologia de Hausdorff. A partir dessa constatação se descarta essa topologia e define-se uma outra topologia - a topologia de Scott - que é compatível com essa propriedade, no sentido de que todo resultado obtido usando-se a lógica, isto é, a propriedade da inclusão-monotonicidade, obtém-se também usando-se a ferramenta topológica e reciprocamente. A teoria resultante da substituição da topologia de Hausdorff pela topologia de Scott tem duas características fundamentais. A Análise Funcional Intervalar resultante possui a maioria das propriedades interessantes da Análise Real, suprimindo, assim, as deficiências da Análise Intervalar anterior. A elaboração da propriedade da inclusão-monotoniciadade permite construir uma lógica geométrica e uma teoria lambda cujo modelo é essa nova matemática intervalar. Além disso, a partir dessa lógica e da teoria lambda se elabora uma teoria construtiva, como a teoria dos tipos de Martin-Löf, que permite se raciocinar com programas dessa matemática. Isso significa a possibilidade de se fazer correção automática de programas da matemática intervalar. Essa nova abordagem da matemática intervalar é desenvolvida pressupondo, apenas, o conceito de número racional, além, é claro, da linguagem da teoria dos conjuntos. Desse modo é construído o sistema intervalar de um modo análogo ao sistema real. Para isso é generalizado o conceito de corte de Dedekind, resultando dessa construção um sistema ordenado denominado de quasi-corpo, em contraste com o números reais cujo sistema é algébrico, o corpo dos números reais. Assim, no sistema intervalar a ordem é um conceito intrínseco ao sistema, diferentemente do sistema de números reais cuja a ordem não faz parte da álgebra do sistema. A lógica dessa nova matemática intervalar é uma lógica categórica. Isto significa que todo resultado obtido para domínios básicos se aplica para o produto cartesiano, união disjunta, o espaço de funções, etc., desses domínios. Isto simplifica consideravelmente a teoria. Um exemplo dessa simplificação é a definição de derivada nessa nova matemática intervalar, conceito ainda não bem definido na teoria intervalar clássica. / The Interval Mathematics is based on two fundamental concepts, the inclusion-monotonicity of its arithmetics and a Hausdorff topology defined on the interval set. The property of inclusion-monotonicity has risen as an useful tool for elaboration of interval algorithms. In contrast, because the Hausdorff topology does not reflect the logical features of that property, the interval mathematics did not, permit the elaboration of a logic whose model is this interval mathematics with that topology. This logic should be necessary to the foundation of the interval mathematics as a Real Analysis Theory of Algorithms. This thesis shows that the theory of algorithms refered above was not possible because of the incompatibility between the property of inclusion-monotonicity and the Hausdorff topology. By knowing the shortcoming of this topology, the next step is to set it aside and to define a new topology - the Scott topology - compatible with the refered property in the sense that every result, obtained via the logic is also obtainable via the topology and vice-versa. After changing the topology the resulting theory has two basic features. The Interval Functional Analysis has got the most, interesting properties belonging to Real Analysis, supressing the shortcomings of previous interval analysis. The elaboration of the inclusion-monotonicity property allows one to construct a geometric logic and a lambda theory whose model is this new interval mathematics. From this logic and from the lambda theory a constructive theory is then elaborated, similar to Martin-Löf type theory, being possible then to reason about programs of this new interval mathematics. This means the possibility of automatically checking the correctness of programs of interval mathematics. This new approach assumes only the concept, of rational numbers beyond, of course, the set theory language. It is constructed an interval system similar to the real system. A general notion of the concept of Dedekind cut was necessary to reach that. The resulting construction is an ordered system which will be called quasi-field, in opposition to the real numbers system which is algebraic. Thus, in the interval system the order is an intrinsic concept, unlike the real numbers sistems whose order does not belong to the algebraic system. The logic of this new interval mathematics is a categorical logic. This means that, every result got for basic domains applies also to cartesian product, disjoint union, function spaces, etc., of these domains. This simplifies considerably the new theory. An example of this simplication is given by the definition of derivative, a concept not, derived by the classical interval theory.

L’objectif de cette thèse est de démontrer que π4(S3) ≃ Z/2Z en théorie des types homotopiques. En particulier, c’est une démonstration constructive et purement homotopique. On commence par rappeler les concepts de base de la théorie des types homotopiques et on démontre quelques résultats bien connus sur les groupes d’homotopie des sphères : le calcul des groupes d’homotopie du cercle, le fait que ceux de la forme πk(Sn) avec k < n sont triviaux et la construction de la fibration de Hopf. On passe ensuite à des outils plus avancés. En particulier, on définit la construction de James, ce qui nous permetde démontrer le théorème de suspension de Freudenthal et le fait qu’il existe un entier naturel n tel que π4(S3) ≃ Z/2Z. On étudie ensuite le produit smash des sphères, on construit l’anneau de cohomologie des espaces et on introduit l’invariant de Hopf, ce qui nous permet de montrer que n est égal soit à 1, soit à 2. L’invariant de Hopf nous permet également de montrer que tous les groupes de la forme π4n−1(S2n) sont infinis. Finalement, on construit la suite exacte de Gysin, ce qui nous permet de calculer la cohomologie de CP2 et de démontrer que π4(S3) ≃ Z/2Z, et que plus généralement on a πn+1(Sn) ≃ Z/2Z pour tout n ≥ 3 / The goal of this thesis is to prove that π4(S3) ≃ Z/2Z in homotopy type theory. In particular it is a constructive and purely homotopy-theoretic proof. We first recall the basic concepts of homotopy type theory, and we prove some well-known results about the homotopy groups of spheres: the computation of the homotopy groups of the circle, the triviality of those of the form πk(Sn) with k < n, and the construction of the Hopf fibration. We then move to more advanced tools. In particular, we define the James construction which allows us to prove the Freudenthal suspension theorem and the fact that there exists a natural number n such that π4(S3) ≃ Z/nZ. Then we study the smash product of spheres, we construct the cohomology ring of a space, and we introduce the Hopf invariant, allowing us to narrow down the n to either 1 or 2. The Hopf invariant also allows us to prove that all the groups of the form π4n−1(S2n) are infinite. Finally we construct the Gysin exact sequence, allowing us to compute the cohomology of CP2 and to prove that π4(S3) ≃ Z/2Z and that more generally πn+1(Sn) ≃ Z/2Z for every n ≥ 3

Meaningful learning requires active teaching and learning approaches. Thus, with a specific focus on Mathematics teaching at university in Oramia, the study aimed to: • examine the extent to which active learning/student-centered approaches were implemented; • assess the attitudes of university lecturers towards active-learning; • investigate whether appropriate training and support have been provided for the implementation of an active learning approaches • assess the major challenges that hinder the implementation of active learning approaches and • recommend ways that could advance the use of active learning approaches in Mathematics teaching at university. A mixed-methods design was used. Among the six universities in the Oromia Regional State of Ethiopia, two of the newly established universities (younger than 5 years) and two of the old universities (15 years and older) were involved in the study. A total of 84 lecturers participated in the study and completed questionnaires. This was complemented by a qualitative approach that used observation checklists and interviews for data gathering: 16 lessons were observed while the lecturers taught their mathematics classes (two lecturers from each of the four sample universities were twice observed). In addition, semi-structured interviews were conducted with four mathematics department heads and eight of the observed lecturers. The study adhered to ethical principles and to applied several techniques to enhance the validity/trustworthiness of the findings. / Psychology of Education / D. Ed. (Psychology of Education)