The study of biodiversity spans many disciplines and includes data pertaining to species distributions and abundances, genetic sequences, trait measurements, and ecological niches, complemented by information on collection and measurement protocols. A review of the current landscape of metadata standards and ontologies in biodiversity science suggests that existing standards such as the Darwin Core terminology are inadequate for describing biodiversity data in a semantically meaningful and computationally useful way. Existing ontologies, such as the Gene Ontology and others in the Open (...) Biological and Biomedical Ontologies (OBO) Foundry library, provide a semantic structure but lack many of the necessary terms to describe biodiversity data in all its dimensions. In this paper, we describe the motivation for and ongoing development of a new Biological Collections Ontology, the Environment Ontology, and the Population and Community Ontology. These ontologies share the aim of improving data aggregation and integration across the biodiversity domain and can be used to describe physical samples and sampling processes (for example, collection, extraction, and preservation techniques), as well as biodiversity observations that involve no physical sampling. Together they encompass studies of: 1) individual organisms, including voucher specimens from ecological studies and museum specimens, 2) bulk or environmental samples (e.g., gut contents, soil, water) that include DNA, other molecules, and potentially many organisms, especially microbes, and 3) survey-based ecological observations. We discuss how these ontologies can be applied to biodiversity use cases that span genetic, organismal, and ecosystem levels of organization. We argue that if adopted as a standard and rigorously applied and enriched by the biodiversity community, these ontologies would significantly reduce barriers to data discovery, integration, and exchange among biodiversity resources and researchers. (shrink)

We present a case study of grammatical constructions and how their function in a single language can be captured through semantic and syntactic classification. Since 2016 an on-going joint project of UiT The Arctic University of Norway and the National Research University Higher School of Economics in Moscow has been collecting and analyzing multiword grammatical constructions of Russian. The main product is the Russian Constructicon, which, with over two thousand two hundred constructions, is arguably the largest openly available constructicon resource (...) for any language. The combination of this large size with depth of analysis, containing both syntactic and semantic tags, makes it possible to view the interrelation of constructions as families and to discover trends in their behavior. Our annotation includes 53 semantic tags of varying frequency, with three tags that are by far more frequent than all the rest, accounting for 30% of the entire inventory of the Russian Constructicon. These three semantic types are Assessment, Attitude, and Intensity, all of which convey a speaker’s evaluation of a topic, in contrast to most of the other tags. Assessment and Attitude constructions are investigated in greater detail in this article. Secondary semantic tags reveal that negative evaluation among these two semantic types is more than twice as frequent as positive evaluation. Examples of negative evaluations are: for Assessment VP tak sebe, as in Na pianino ja igraju tak sebe “I play the piano so-so [lit. thus self]”; for Attitude s PronPers-Gen xvatit/xvatilo, as in S menja xvatit “I’m fed up [lit. from me enough].” In terms of syntax, the most frequent syntactic types of constructions in the Russian Constructicon are clausal constructions [constituting an independent clause like s PronPers-Gen xvatit/xvatilo ] and constructions with the anchor in the role of adverbial modifier. Our semantic and syntactic classification of this large body of Russian constructions makes it possible to postulate patterns of grammatical constructions constituting a radial category with central and peripheral types. Classification of large numbers of constructions reveals systematic relations that structure the grammar of a language. (shrink)

This volume examines the notion of an analytic proof as a natural deduction, suggesting that the proof's value may be understood as its normal form--a concept with significant implications to proof-theoretic semantics.

Ibn al-'Arabī (d. 1240) was one of the towering figures of Islamic intellectual history, and among Sufis still bears the title of al-shaykh al-akbar, or "the greatest master." Ibn al-'Arabī and Islamic Intellectual Culturetraces the history of the concept of "oneness of being" (wahdat al-wujūd) in the school of Ibn al- 'Arabī, in order to explore the relationship between mysticism and philosophy in Islamic intellectual life. It examines how the conceptual language used by early mystical writers became increasingly engaged over (...) time with the broader Islamic intellectual culture, eventually becoming integrated with the latter's common philosophical and theological vocabulary. It focuses on four successive generations of thinkers (Sadr al-Dīn al-Qūnawī, Mu'ayyad al-Dīn al-Jandī, 'Abd al-Razzāq al-Kāshānī, and Dāwūd al-Qaysarī), and examines how these "philosopher-mystics" refined and developed the ideas of Ibn al-'Arabī. Through a close analysis of texts, the book clearly traces the crystallization of an influential school of thought in Islamic history and its place in the broader intellectual culture. Offering an exploration of the development of Sufi expression and thought, this book will be a valuable resource for students and scholars of Islamic thought, philosophy, and mysticism. (shrink)

In the analysis of the ethicalproblems of online research, there is much tobe learned from the work that has already beendone on research ethics in the socialsciences and the humanities. I discuss thestructure of norms in the Norwegian ethicalguidelines for research in the social scienceswith respect to their relevance for the ethicalissues of Internet research. A four-stepprocedure for the ethical evaluation ofresearch is suggested. I argue that eventhough, at one level, the problems of onlineresearch are very similar to those we (...) find intraditional areas of social scientificresearch, there still are some issues that areunique to research online. A general model forthe analysis of privacy and data protection issuggested. This model is then used tocharacterize the special problems pertaining tothe protection of privacy in online contexts,and to argue that one cannot assume a simpledistinction between the private and the publicwhen researching in such contexts. (shrink)

According to a main idea of Gentzen the meanings of the logical constants are reflected by the introduction rules in his system of natural deduction. This idea is here understood as saying roughly that a closed argument ending with an introduction is valid provided that its immediate subarguments are valid and that other closed arguments are justified to the extent that they can be brought to introduction form. One main part of the paper is devoted to the exact development of (...) this notion. Another main part of the paper is concerned with a modification of this notion as it occurs in Michael Dummett’s book The Logical Basis of Metaphysics. The two notions are compared and there is a discussion of how they fare as a foundation for a theory of meaning. It is noted that Dummett’s notion has a simpler structure, but it is argued that it is less appropriate for the foundation of a theory of meaning, because the possession of a valid argument for a sentence in Dummett’s sense is not enough to be warranted to assert the sentence. (shrink)

Reviewed Works:Gaisi Takeuti, Proof Theory.Georg Kreisel, Proof Theory: Some Personal Recollections.Wolfram Pohlers, Contributions of the Schutte School in Munich to Proof Theory.Stephen G. Simpson, Subsystems of $\mathbf{Z}_2$ and Reverse Mathematics.Solomon Feferman, Proof Theory: A Personal Report.

We investigate the connections between computability theory and Nonstandard Analysis. In particular, we investigate the two following topics and show that they are intimately related. A basic property of Cantor space$2^ $ is Heine–Borel compactness: for any open covering of $2^ $, there is a finite subcovering. A natural question is: How hard is it to compute such a finite subcovering? We make this precise by analysing the complexity of so-called fan functionals that given any $G:2^ \to $, output a (...) finite sequence $\langle f_0, \ldots,f_n \rangle $ in $2^ $ such that the neighbourhoods defined from $\overline {f_i } G\left$ for $i \le n$ form a covering of $2^ $. A basic property of Cantor space in Nonstandard Analysis is Abraham Robinson’s nonstandard compactness, i.e., that every binary sequence is “infinitely close” to a standard binary sequence. We analyse the strength of this nonstandard compactness property of Cantor space, compared to the other axioms of Nonstandard Analysis and usual mathematics.Our study of yields exotic objects in computability theory, while leads to surprising results in Reverse Mathematics. We stress that and are highly intertwined, i.e., our study is holistic in nature in that results in computability theory yield results in Nonstandard Analysis and vice versa. (shrink)

We may try to explain proofs as chains of valid inference, but the concept of validity needed in such an explanation cannot be the traditional one. For an inference to be legitimate in a proof it must have sufficient epistemic power, so that the proof really justifies its final conclusion. However, the epistemic concepts used to account for this power are in their turn usually explained in terms of the concept of proof. To get out of this circle we may (...) consider an idea within intuitionism about what it is to justify the assertion of a proposition. It depends on Heyting’s view of the meaning of a proposition, but does not presuppose the concept of inference or of proof as chains of inferences. I discuss this idea and what is required in order to use it for an adequate notion of valid inference. (shrink)

By a valid inference is here understood an inference that succeeds in its aim to justify its conclusion given that its premisses are already justified. For an inference to be valid it is thus not enough that the sentence asserted in the conclusion is a logical consequence of the sentences asserted in the premisses. A proof is understood as a succession of valid inferences that is closed (i.e. all its assumptions are discharged and all its free variables are bound by (...) some of the inferences). On the other hand, in mathematics the justification of an assertion has traditionally been taken to consist in a proof of it, which gives rise to an explanatory circle.In an attempt to avoid this circle, I have in previous works tried to explain the notion of ground for an assertion without referring to valid inferences. However, it turns out that the resulting notion of ground has unwanted consequences like the notion of proof in the so-called BHK-interpretation of intuitionistic logic. For instance, one is guaranteed a ground or a proof of an implication A → B as soon as there is in fact no ground or proof of A, regardless of whether one really knows this fact, and hence without having a real justification of the assertion of the implication.In the absence of a non-circular explanation of the notions of valid inference and proof, I suggest that we should try to formulate a number of principles of how these two epistemic notions depend on each other. A more careful explanation of the validity of an inference results in what I call a heuristic idea about the validity of inference, which is used as a guide to formulate precise principles. One such principle generalizes Gentzen’s idea that his introduction rules define the meaning of the logical constants. Another principle generalizes a previously noted property of Gentzen’s elimination rules that I have called that of satisfying the inversion principle. It results in a notion that I call non-creativity, which implies validity. (shrink)

I see the question what it is that makes an inference valid and thereby gives a proof its epistemic power as the most fundamental problem of general proof theory. It has been surprisingly neglected in logic and philosophy of mathematics with two exceptions: Gentzen’s remarks about what justifies the rules of his system of natural deduction and proposals in the intuitionistic tradition about what a proof is. They are reviewed in the paper and I discuss to what extent they succeed (...) in answering what a proof is. Gentzen’s ideas are shown to give rise to a new notion of valid argument. At the end of the paper I summarize and briefly discuss an approach to the problem that I have proposed earlier. (shrink)

There are two main routes to a concept of (generalized) quantifier. The first starts from first‐order logic, FO, and generalizes from the familiar ∀ and ∃ occurring there. The second route begins with real languages, and notes that many so‐called noun phrases, a kind of phrase which occurs abundantly in most languages, can be interpreted in a natural and uniform way using quantifiers.

We show that to every recursive total continuous functional $\Phi$ there is a PCF-definable representative $\Psi$ of $\Phi$ in the hierarchy of partial continuous functionals, where PCF is Plotkin's programming language for computable functionals. PCF-definable is equivalent to Kleene's S1-S9-computable over the partial continuous functionals.

It is not unreasonable to think that the dispute between classical and intuitionistic mathematics might be unresolvable or 'faultless', in the sense of there being no objective way to settle it. If so, we would have a pretty case of relativism. In this note I argue, however, that there is in fact not even disagreement in any interesting sense, let alone a faultless one, in spite of appearances and claims to the contrary. A position I call classical pluralism is sketched, (...) intended to provide a coherent methodological stance towards the issue. Some reasons to recommend this stance are given, as well as some speculations as to why not everyone might want to follow the recommendation. (shrink)

We study the logical and computational properties of basic theorems of uncountable mathematics, in particular Pincherle's theorem, published in 1882. This theorem states that a locally bounded function is bounded on certain domains, i.e. one of the first ‘local-to-global’ principles. It is well-known that such principles in analysis are intimately connected to (open-cover) compactness, but we nonetheless exhibit fundamental differences between compactness and Pincherle's theorem. For instance, the main question of Reverse Mathematics, namely which set existence axioms are necessary to (...) prove Pincherle's theorem, does not have an unique or unambiguous answer, in contrast to compactness. We establish similar differences for the computational properties of compactness and Pincherle's theorem. We establish the same differences for other local-to-global principles, even going back to Weierstrass. We also greatly sharpen the known computational power of compactness, for the most shared with Pincherle's theorem however. Finally, countable choice plays an important role in the previous, we therefore study this axiom together with the intimately related Lindelöf lemma. (shrink)

The aim of this paper is to make a critical assessment of Krister Segerberg''s theory of action. The first part gives a critical presentation of the key concepts in Segerberg''s informal theory of action. These are the ideas that motivate the formal models he develops. In the second part it is argued that if one takes all of Segerberg''s motivating ideas seriously, problems are forthcoming. The main problem is that on this theory the agents seem to be bound to realize (...) all of their intentions, a problem that stems from Segerberg''s attempt to individuate actions in terms of the agent''s intentions. On the ground that this unfortunate result is forthcoming in both of Segerberg''s approaches to the logic of action it is concluded that the conceptual basis of the theory is problematic. (shrink)

Cantor’s first set theory paper (1874) establishes the uncountability of ${\mathbb R}$. We study this most basic mathematical fact formulated in the language of higher-order arithmetic. In particular, we investigate the logical and computational properties of ${\mathsf {NIN}}$ (resp. ${\mathsf {NBI}}$ ), i.e., the third-order statement there is no injection resp. bijection from $[0,1]$ to ${\mathbb N}$. Working in Kohlenbach’s higher-order Reverse Mathematics, we show that ${\mathsf {NIN}}$ and ${\mathsf {NBI}}$ are hard to prove in terms of (conventional) comprehension axioms, (...) while many basic theorems, like Arzelà’s convergence theorem for the Riemann integral (1885), are shown to imply ${\mathsf {NIN}}$ and/or ${\mathsf {NBI}}$. Working in Kleene’s higher-order computability theory based on S1–S9, we show that the following fourth-order process based on ${\mathsf {NIN}}$ is similarly hard to compute: for a given $[0,1]\rightarrow {\mathbb N}$ -function, find reals in the unit interval that map to the same natural number. (shrink)

How should the policies of search engines and other information intermediaries be ethically evaluated? It is argued that Kant’s principles for the public use of reason are useful starting points for the formulation of criteria for such an evaluation. The suggestion is, furthermore, that a search engine can be seen to provide a testimony to the user concerning what information that is most relevant to her query. This suggestion is used as the basis for the development of a broadly Kantian (...) account of a rational searcher. It is argued that the search engine companies are morally required to publish their information policies and act in accordance with them but given the threat of search engine spam they can have no obligation to publish the details of their algorithms. (shrink)

The traditional picture of logic takes it for granted that "valid arguments have a fundamental epistemic significance", but neither model theory nor traditional proof theory dealing with formal system has been able to give an account of this significance. Since valid arguments as usually understood do not in general have any epistemic significance, the problem is to explain how and why we can nevertheless use them sometimes to acquire knowledge. It is suggested that we should distinguish between arguments and acts (...) of inferences and that we have to reconsider the latter notion to arrive at the desired explanation. More precisely, the notions should be developed so that the following relationship holds: one gets in possession of a ground for a conclusion by inferring it from premisses for which one already has grounds, provided that the inference in question is valid. The paper proposes explications of the concepts of ground and deductively valid inference so that this relationship holds as a conceptual truth. Logical validity of inference is seen as a special case of deductive validity, but does not add anything as far as epistemic significance is concerned—it resides already in the deductively valid inferences. (shrink)