Bioassessment is the process of using living organisms to assess the ecological health of a particular ecosystem. It typically relies on identifying specific organisms that are sensitive to changes in environmental conditions. Benthic macroinvertebrates are widely used for examining the ecological status of freshwaters. However, a time-consuming process of species identification that requires high expertise represents one of the key obstacles to more precise bioassessment of aquatic ecosystems. Partial automation of this process using deep learning-based image classification is the goal (...) of an ongoing project AIAQUAMI we are participating in. One of the project goals is to develop software support for image classification with visualization and reporting. For that purpose, we developed desktop and web applications that we open-sourced as Imagelytics Suite. Both desktop and web applications rely on a convolutional neural network (CNN) to classify images and the Grad-CAM algorithm to produce heatmaps of the image areas that mostly influenced the network decision. Along with the source code of the applications, we also open-sourced scripts that can be used to train CNN on an arbitrary dataset and produce required metadata, so it can be used with Imagelytics applications. In this article, we presented technical details regarding the design of the applications and the training method that will enable their general use for image classification tasks. As a part of the evaluation, we will show a use case related to species identification of non-biting midges (Diptera: Chironomidae). (shrink)

Logicians have often suggested that the use of Euler-type diagrams has influenced the idea of the quantification of the predicate. This is mainly due to the fact that Euler-type diagrams display more information than is required in traditional syllogistics. The paper supports this argument and extends it by a further step: Euler-type diagrams not only illustrate the quantification of the predicate, but also solve problems of traditional proof theory, which prevented an overall quantification of the predicate. Thus, (...) Euler-type diagrams can be called the natural basis of syllogistic reasoning and can even go beyond. In the paper, these arguments are presented in connection with the book Nucleus Logicae Weisaniae by Johann Christian Lange from 1712. (shrink)

An intermediate predicate logicS + n (n>0) is introduced and investigated. First, a sequent calculusGS n is introduced, which is shown to be equivalent toS + n and for which the cut elimination theorem holds. In § 2, it will be shown thatS + n is characterized by the class of all linear Kripke frames of the heightn.

Kripke completeness of some infinitary predicate modal logics is presented. More precisely, we prove that if a normal modal logic above is -persistent and universal, the infinitary and predicate extension of with BF and BF is Kripke complete, where BF and BF denote the formulas pi pi and x x, respectively. The results include the completeness of extensions of standard modal logics such as , and its extensions by the schemata T, B, 4, 5, D, and their combinations. (...) The proof is obtained by extending the correspondence between the representation of modal algebras and the completeness of propositional modal logic to infinite. (shrink)

I begin with an exposition of the two main variants of the Prosentential Theory of Truth (PT), those of Dorothy Grover et al. and Robert Brandom. Three main types of criticisms are then put forward: (1) material criticisms to the effect that (PT) does not adequately explain the linguistic data, (2) an objection to the effect that no variant of (PT) gives a properly unified account of the various occurrences of "true" in English, and, most importantly, (3) a charge that (...) the comparison with proforms is explanatorily idle. The last objection is that, given a complete semantic account of pronouns, proadjectives, antecedents, etc., together with a complete (PT), the essential semantic character of "true" could be deduced, but then, the idleness of the comparison with pronouns would be apparent. It turns out that objections (2) and (3) are related in the following way: the prosentential terminology is held to conceal the lack of unity in (PT), by describing the different data in the same terms ("proform", "antecedent", etc.). But this, I argue, is only a way of truly describing, rather than explaining, the data, these being certain relations of equivalence and consequence between sentences. I consider a language for which (PT) would be not only true, but also explanatory, but note that this language is very different from English. I end by showing that Robert Brandom's case that "is true" is not a predicate fails, and that his motivation for saying so is based on fallacious reasoning (namely, Boghossian's argument against deflationism). (shrink)

Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers systems of illative combinatory logic that are sound for first-order propositional and predicate calculus. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators or, in a more direct way, in which derivations are not translated. Both translations (...) are closely related in a canonical way. The two direct translations turn out to be complete. The paper fulfills the program of Church [1932], [1933] and Curry [1930] to base logic on a consistent system of λ-terms or combinators. Hitherto this program had failed because systems of ICL were either too weak (to provide a sound interpretation) or too strong (sometimes even inconsistent). (shrink)

Objective Bayesian probability is often defined over rather simple domains, e.g., finite event spaces or propositional languages. This paper investigates the extension of objective Bayesianism to first-order logical languages. It is argued that the objective Bayesian should choose a probability function, from all those that satisfy constraints imposed by background knowledge, that is closest to a particular frequency-induced probability function which generalises the λ = 0 function of Carnap’s continuum of inductive methods.

In this essay, I argue for the conclusion that the Chinese sentences that are regularly translated into subject-predicate sentences in English may be understood as all non-subject-predicate sentences. My argument is based on the premise that some grammatical features are crucial to yield the sense of contrast between the completeness of subject and the incompleteness of predicate. The absence of such grammatical features in Chinese makes it impossible to establish any criterion for the distinction between subject and (...) predicate in Chinese. (shrink)

In the last few decades many formal systems of fuzzy logics have been developed. Since the main differences between fuzzy and classical logics lie at the propositional level, the fuzzy predicate logics have developed more slowly (compared to the propositional ones). In this text we aim to promote interest in fuzzy predicate logics by contributing to the model theory of fuzzy predicate logics. First, we generalize the completeness theorem, then we use it to get results on conservative (...) extensions of theories and on witnessed models. (shrink)

Tarski's indefinability theorem shows us that truth is not definable in arithmetic. The requirement to define truth for a language in a stronger language (if contradiction is to be avoided) lapses for particularly weak languages. A weaker language, however, is not necessary for that lapse. It also lapses for an adequately weak theory. It turns out that the set of G{\"o}del numbers of sentences true in arithmetic modulo $n$ is definable in arithmetic modulo $n$.

What precisely are fragments of classical first-order logic showing “modal” behaviour? Perhaps the most influential answer is that of Gabbay 1981, which identifies them with so-called “finite-variable fragments”, using only some fixed finite number of variables (free or bound). This view-point has been endorsed by many authors (cf. van Benthem 1991). We will investigate these fragments, and find that, illuminating and interesting though they are, they lack the required nice behaviour in our sense. (Several new negative results support this claim.) (...) As a counterproposal, then, we define a large fragment of predicate logic characterized by its use of only bounded quantification. This so-called guarded fragment enjoys the above nice properties, including decidability, through an effectively bounded finite model property. (These are new results, obtained by generalizing notions and techniques from modal logic.) Moreover, its own internal finite variable hierarchy turns out to work well. Finally, we shall make another move. The above analogy works both ways. Modal operators are like quantifiers, but quantifiers are also like modal operators. This observation inspires a generalized semantics for first-order predicate logic with accessibility constraints on available assignments (cf. N´emeti 1986, 1992) which moves the earlier quantifier restrictions into the semantics. This provides a fresh look at the landscape of possible predicate logics, including candidates sharing various desirable features with basic modal logic – in particular, its decidability. (shrink)

Recent studies in semantics of modal and superintuitionistic predicate logics provided many examples of incompleteness, especially for Kripke semantics. So there is a problem: to find an appropriate possible- world semantics which is equivalent to Kripke semantics at the propositional level and which is strong enough to prove general completeness results. The present paper introduces a new semantics of Kripke metaframes' generalizing some earlier notions. The main innovation is in considering "n"-tuples of individuals as abstract "n"-dimensional vectors', together with (...) some transformations of these vectors. Soundness of the semantics is proved to be equivalent to some non- logical properties of metaframes; and thus we describe the maximal semantics of Kripke- type. (shrink)

In [Ono 1987] H. Ono put the question about axiomatizing the intermediate predicate logicLFin characterized by the class of all finite Kripke frames. It was established in [ Skvortsov 1988] thatLFin is not recursively axiomatizable. One can easily show that for any finite posetM, the predicate logic characterized byM is recursively axiomatizable, and its axiomatization can be constructed effectively fromM. Namely, the set of formulas belonging to this logic is recursively enumerable, since it is embeddable in the two-sorted (...) classical predicate calculusCPC 2. Thus the logicLFin is II 2 0 -arithmetical.Here we give a more explicit II 2 0 -description ofLFin: it is presented as the intersection of a denumerable sequence of finitely axiomatizable Kripke-complete logics. Namely, we give an axiomatization of the logicLB n P m + characterized by the class of all posets of the finite height m and the finite branching n. A finite axiomatization of the predicate logicLP m + characterized by the class of all posets of the height m is known from [Yokota 1989]. We prove thatLB n P m + =,B n being the propositional axiom of the branching n. (shrink)

We prove that the positive fragment of first-order intuitionistic logic in the language with two individual variables and a single monadic predicate letter, without functional symbols, constants, and equality, is undecidable. This holds true regardless of whether we consider semantics with expanding or constant domains. We then generalise this result to intervals \ and \, where QKC is the logic of the weak law of the excluded middle and QBL and QFL are first-order counterparts of Visser’s basic and formal (...) logics, respectively. We also show that, for most “natural” first-order modal logics, the two-variable fragment with a single monadic predicate letter, without functional symbols, constants, and equality, is undecidable, regardless of whether we consider semantics with expanding or constant domains. These include all sublogics of QKTB, QGL, and QGrz—among them, QK, QT, QKB, QD, QK4, and QS4. (shrink)

We define notions of homomorphism, submodel, and sandwich of Kripke models, and we define two syntactic operators analogous to universal and existential closure. Then we prove an intuitionistic analogue of the generalized (dual of the) Lyndon-Łoś-Tarski Theorem, which characterizes the sentences preserved under inverse images of homomorphisms of Kripke models, an intuitionistic analogue of the generalized Łoś-Tarski Theorem, which characterizes the sentences preserved under submodels of Kripke models, and an intuitionistic analogue of the generalized Keisler Sandwich Theorem, which characterizes the (...) sentences preserved under sandwiches of Kripke models. We also define several intuitionistic formula hierarchies analogous to the classical formula hierarchies $\forall_n (= \Pi^0_n)$ and $\exists_n (=\Sigma^0_n)$ , and we show how our generalized syntactic preservation theorems specialize to these hierarchies. Each of these theorems implies the corresponding classical theorem in the case where the Kripke models force classical logic. (shrink)

This paper is devoted to the algebraization of an arithmetical predicate introduced by S. Feferman. To this purpose we investigate the equational class of Boolean algebras enriched with an operation (g=rtail), which translates such predicate, and an operation τ, which translates the usual predicate Theor. We deduce from the identities of this equational class some properties of (g=rtail) and some ties between (g=rtail) and τ; among these properties, let us point out a fixed-point theorem for a sufficiently (...) large class of (g=rtail)-τ polynomials. The last part of this paper concerns the duality theory for (g=rtail)-τ algebras. (shrink)

Although a great deal has been written concerning the verifiability of empirical, declarative sentences, yet some further clarification in this area seems possible and desirable. I think it is important to determine what sort of property ‘verified by’ is. Obviously it is a semiotical property. Only sentences, never matters of fact, are verified. But where, in the area of semiotics, is it to be placed? To use Charles Morris's useful and now somewhat traditional classification, is it a syntactic, semantic, or (...) pragmatic predicate? My answer is that it falls within semantics. Before developing this, however, I should like to point out why I do not place it in either of the other two subdivisions. (shrink)

Noun phrases with overt determiners, such as <i>some apples</i> or <i>a quantity of milk</i>, differ from bare noun phrases like <i>apples</i> or <i>milk</i> in their contribution to aspectual composition. While this has been attributed to syntactic or algebraic properties of these noun phrases, such accounts have explanatory shortcomings. We suggest instead that the relevant property that distinguishes between the two classes of noun phrases derives from two modes of existential quantification, one of which holds the values of a variable fixed (...) throughout a quantificational context while the other allows them to vary. Inspired by Dynamic Plural Logic and Dependence Logic, we propose Plural Predicate Logic as an extension of Predicate Logic to formalize this difference. We suggest that temporal <i>for</i>-adverbials are sensitive to aspect because of the way they manipulate quantificational contexts, and that analogous manipulations occur with spatial <i>for</i>-adverbials, habituals, and the quantifier <i>all</i>. (shrink)

In previous work by Baaz and Iemhoff, a Gentzen calculus for intuitionistic logic with existence predicate is presented that satisfies partial cut elimination and Craig's interpolation property; it is also conjectured that interpolation fails for the implication-free fragment. In this paper an equivalent calculus is introduced that satisfies full cut elimination and allows a direct proof of interpolation via Maehara's lemma. In this way, it is possible to obtain much simpler interpolants and to better understand and overcome the failure (...) of interpolation for the implication-free fragment. (shrink)

In this paper we explore how some of the largest US-newspapers linguistically frame immigrants to the USA in articles about Mexican and Central American immigrants. Specifically, it is a corpus-assisted discourse study which examines the frequency of different semantic predicate-types with migrant subjects and migrant by-agents in the quest for underlying positive or negative biases. We wish to ascertain what activities migrants are presented as taking part in, principally as agents. The analysis shows that more than half of the (...) migrant/predicate-pairings reflect the dictionary definitions of migrant. However, immigrants are described as illegal 66% of the times that their location is mentioned with an immigrant/predicate-pairing. The non-definition-confirming pairings also show evidence of a negative framing of immigrants, but not of migrants. Furthermore, immigrants are more often than migrants cast as agents of activities that do not simply reiterate their status as migrants. Finally, we found evidence of the Negation Bias in the immigrant/predicate-pairings. (shrink)

The predicate view on proper names opts for a uniform semantic representation of proper nouns like ‘Alfred’ as predicates on the level of logical form. Early defences of this view can be found in Sloat (Language, vol. 45, pp. 26–30, 1969) and Burge (J. Philos. 70: 425–439, 1973), but there is an increasing more recent interest in this view on proper names. My paper aims to provide a reconstruction and critique of Burge’s main argument for the predicate view (...) on proper names, which is still used by several current philosophers in defence of this view. I have called this argument the unification argument. I will present a stepwise interpretation and reconstruction of this argument, consider several possible responses to it and defend a specific response to it in detail. (shrink)

In this paper, a semantics for predicate logics without the contraction rule will be investigated and the completeness theorem will be proved. Moreover, it will be found out that our semantics has a close connection with Beth-type semantics.

The traditional square of opposition is generalized and extended to a cube of opposition covering and conveniently visualizing inter-sentential oppositions in relational syllogistic logic with the usual syllogistic logic sentences obtained as special cases. The cube comes about by considering Frege–Russell’s quantifier predicate logic with one relation comprising categorical syllogistic sentence forms. The relationships to Buridan’s octagon, to Aristotelian modal logic, and to Klein’s 4-group are discussed.GraphicThe photo shows a prototype sculpture for the cube.

Mirdamad, a prominent philosopher of the Late Medieval Period active in the Islamic world, regards existence as nothing in reality. In this paper, I employ methods devised by contemporary analytic...

We consider the desirability, or otherwise, of various forms of induction in the light of certain principles and inductive methods within predicate uncertain reasoning. Our general conclusion is that there remain conflicts within the area whose resolution will require a deeper understanding of the fundamental relationship between individuals and properties.

We prove that an intermediate predicate logic characterized by a class of finite partially ordered sets is recursively axiomatizable iff it is "finite", i.e., iff it is characterized by a single finite partially ordered set. Therefore, the predicate logic LFin of the class of all predicate Kripke frames with finitely many possible worlds is not recursively axiomatizable.

Rational Pavelka logic extends Lukasiewicz infinitely valued logic by adding truth constants r̄ for rationals in [0, 1]. We show that this is a conservative extension. We note that this shows that provability degree can be defined in Lukasiewicz logic. We also give a counterexample to a soundness theorem of Belluce and Chang published in 1963.