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)

We introduce Gentzen calculi for intuitionistic logic extended with an existence predicate. Such a logic was first introduced by Dana Scott, who provided a proof system for it in Hilbert style. We prove that the Gentzen calculus has cut elimination in so far that all cuts can be restricted to very simple ones. Applications of this logic to Skolemization, truth value logics and linear frames are also discussed.

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)

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)

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)

Along the same line as that in Ono (Ann Pure Appl Logic 161:246–250, 2009), a proof-theoretic approach to Glivenko theorems is developed here for substructural predicate logics relative not only to classical predicate logic but also to arbitrary involutive substructural predicate logics over intuitionistic linear predicate logic without exponentials QFLe. It is shown that there exists the weakest logic over QFLe among substructural predicate logics for which the Glivenko theorem holds. Negative translations of substructural (...) class='Hi'>predicate logics are studied by using the same approach. First, a negative translation, called extended Kuroda translation is introduced. Then a translation result of an arbitrary involutive substructural predicate logics over QFLe is shown, and the existence of the weakest logic is proved among such logics for which the extended Kuroda translation works. They are obtained by a slight modification of the proof of the Glivenko theorem. Relations of our extended Kuroda translation with other standard negative translations will be discussed. Lastly, algebraic aspects of these results will be mentioned briefly. In this way, a clear and comprehensive understanding of Glivenko theorems and negative translations will be obtained from a substructural viewpoint. (shrink)

For each intermediate propositional logicJ, J * denotes the least predicate extension ofJ. By the method of canonical models, the strongly Kripke completeness ofJ *+D(=x(p(x)q)xp(x)q) is shown in some cases including:1. J is tabular, 2. J is a subframe logic. A variant of Zakharyashchev's canonical formulas for intermediate logics is introduced to prove the second case.

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 prove that the theory of the extensional compositional truth predicate for the language of arithmetic with \Delta 0 -induction scheme for the truth predicate and the full arithmetical induction scheme is not conservative over Peano Arithmetic. In addition, we show that a slightly modified theory of truth actually proves the global reflection principle over the base theory.

In §93 of The Principles of Mathematics, Bertrand Russell observes that “the variable is a very complicated logical entity, by no means easy to analyze correctly”. This assessment is borne out by the fact that even now we have no fully satisfactory understanding of the role of variables in a compositional semantics for first-order logic. In standard Tarskian semantics, variables are treated as meaning-bearing entities; moreover, they serve as the basic building blocks of all meanings, which are constructed out of (...) variable assignments. But this has disquieting consequences, including Fine’s antinomy of the variable and an undue dependence of meanings on language. Here I develop an alternative, Fregean version of predicate logic that uses the traditional quantifier–variable apparatus for the expression of generality, possesses a fully compositional, non-representational semantics, and is not subject to the antinomy of the variable. The advantages of Fregean over Tarskian predicate logic are due to the former’s treating variables not as meaningful lexical items, but as mere marks of punctuation, similar to parentheses. I submit that this is indeed how the variables of predicate logic should be construed. (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 recent years combinations of tense and modality have moved intothe focus of logical research. From a philosophical point of view, logical systems combining tense and modality are of interest because these logics have a wide field of application in original philosophical issues, for example in the theory of causation, of action, etc. But until now only methods yielding completeness results for propositional languages have been developed. In view of philosophical applications, analogous results with respect to languages of predicate (...) logic are desirable, and in this paper I present two such results. The main developments in this area can be split into two directions, differing in the question whether the ordering of time is world-independent or not. Semantically, this difference appears in the discussion whether T x W-frames or Kamp-frames (resp. Ockham-frames) provide a suitable semantics for combinations of tense and modality. Here, two calculi are presented, the first adequate with respect to Kamp-semantics, the second to T x Wsemantics. (Both calculi contain an appropriate version of Gabbay's irreflexivity rule.) Furthermore, the proposed constructions of canonical frames simplify some of those which have hitherto been discussed. (shrink)

According to what I call the ‘Vagueness Thesis’ about belief, ‘believes’ is a vague predicate. On this view, our concept of belief admits of borderline cases: one can ‘half-believe’ something or be ‘in-between believing’ it. In this article, I argue that VT is false and present an alternative picture of belief. I begin by considering a case—held up as a central example of vague belief—in which someone sincerely claims something to be true and yet behaves in a variety of (...) other ways as if she believes that it is not. I argue that, even from the third-person perspective prioritised by proponents of VT, the case does not motivate VT. I present an alternative understanding of the case according to which the person in question believes as they say they do yet also has a belief-discordant implicit attitude otherwise. Moreover, I argue that, independently of the interpretation of any particular case, VT fails to accommodate the first-person perspective on belief. Belief is not only an item of one’s psychology that helps explain one’s behaviour; it is what one takes to be true. This fact about belief manifests itself in the nature of deliberation concerning whether to believe something and that of introspection regarding whether one believes something. Attending to these phenomena reveals that VT is not merely unmotivated, but untenable. (shrink)

This essay is devoted to an analysis of the semantic significance of a fashionable view of proper names, the Predicate Theory of names, typically developed in the direction of the Metalinguistic Theory of names. According to MT, ‘syntactic evidence supports the conclusion that a name such as ‘Kennedy’ is analyzable in terms of the predicate ‘individual named ‘Kennedy’’. This analysis is in turn alleged to support a descriptivist treatment of proper names in designative position, presumably in contrast with (...) theories of names as ‘directly referring rigid designators’. The main aim of this essay is that of questioning the significance of PT and MT as theories of designation: even granting for the argument’s sake that names are analyzable as predicates, their designative occurrences may be interpreted in consonance with the dictates of Direct Reference—indeed, in consonance with the radically anti-descriptivist version of Direct Reference I call Millianism. (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.

Joan Weiner has recently claimed that Frege neither uses, nor has any need to use, a truth-predicate in his justification of the logical laws. She argues that because of the assimilation of sentences to proper names in his system, Frege does not need to make use of the Quinean device of semantic ascent in order to formulate the logical laws, and that the predicate ‘is the True’, which is used in Frege's justification, is not to be considered as (...) a truth-predicate, because it does not apply to true sentences or true thoughts. The present paper aims to show that Frege needs to use, and does use, a truth-predicate in this context. It is argued, first, that Frege needs to use a truthpredicate in order to show that the truth of the logical laws is evident from the senses of the sentences by means of which they are formulated, and second, that the predicate that he actually uses, ‘is the True’, must be considered as a truth-predicate in the relevant sense, because it can be used and is actually used by Frege to explain the truth-conditions of thoughts. To defend this interpretation, it is discussed whether the explanatory use of ‘is the True’ in Frege's system is compatible with his deflationary analysis of ‘true’. The paper's conclusion is that there is indeed a conflict here; but, from Frege's point of view, this conflict is due merely to the logical imperfection of natural language and does not affect the proper system but only its propaedeutic. (shrink)

Kolmogorov established the principle of the double negation translation by which to embed Classical Predicate Logic |${\operatorname {CQC}}$| into Intuitionistic Predicate Logic |${\operatorname {IQC}}$|⁠. We show that the obvious generalizations to the Basic Predicate Logic of [3] and to |${\operatorname {BQC}}$| of [12], a proper subsystem of |${\operatorname {IQC}}$|⁠, go through as well. The obvious generalizations of Kuroda’s embedding are shown to be equivalent to the Kolmogorov variant. In our proofs novel nontrivial techniques are needed to overcome (...) the absence of full modus ponens in Basic Predicate Logic. In [3] we argued that |${\operatorname {IQC}}$| is not the logic of constructive mathematics. Our doubts were far from new. New was that we put forward an alternative, |${\operatorname {BQC}}$|⁠. One concern is that |${\operatorname {BQC}}$| is too weak for serious mathematics, or even trivial. This paper is one step to alleviate such concerns. (shrink)

We introduce the simpler and shorter proof of Hajek’s theorem that the mathematical induction on ω implies a contradiction in the set theory with the comprehension principle within Łukasiewicz predicate logic Ł ${\forall}$ (Hajek Arch Math Logic 44(6):763–782, 2005) by extending the proof in (Yatabe Arch Math Logic, accepted) so as to be effective in any linearly ordered MV-algebra.

This paper investigates a first-order extension of GL called \. We outline briefly the history that led to \, its key properties and some of its toolbox: the \emph{conservation theorem}, its cut-free Gentzenisation, the ``formulators'' tool. Its semantic completeness is fully stated in the current paper and the proof is retold here. Applying the Solovay technique to those models the present paper establishes its main result, namely, that \ is arithmetically complete. As expanded below, \ is a first-order modal logic (...) that along with its built-in ability to simulate general classical first-order provability―"\" simulating the the informal classical "\"―is also arithmetically complete in the Solovay sense. (shrink)

Plural predication is a pervasive part of ordinary language. We can say that some people are fifty in number, are surrounding a building, come from many countries, and are classmates. These predicates can be true of some people without being true of any one of them; they are non-distributive predications. However, the apparatus of modern logic does not allow a place for them. Thomas McKay here explores the enrichment of logic with non-distributive plural predication and quantification. His book will be (...) of great interest to philosophers of language, linguists, metaphysicians, and logicians. (shrink)

Solovay proved the arithmetical completeness theorem for the system GL of propositional modal logic of provability. Montagna proved that this completeness does not hold for a natural extension QGL of GL to the predicate modal logic. Let Th(QGL) be the set of all theorems of QGL, Fr(QGL) be the set of all formulas valid in all transitive and conversely well-founded Kripke frames, and let PL(T) be the set of all predicate modal formulas provable in Tfor any arithmetical interpretation. (...) Montagna’s results are described as Th(QGL) ⊊ (Fr(QGL), PL(PA) ⊈ Fr(QGL), and Th(QGL) ⊊ PL(PA). In this paper, we prove the following three theorems: (1) Fr(QGL) ⊈ PL(T) for any Σ1-sound recursively enumerable extension T of I Σ1, (2) PL(T) ⊈ Fr(QGL) for any recursively enumerable S1755020312000275_inline1 A -theory T extending I Σ1, and (3) Th(QGL) ⊊ Fr(QGL) ∩ PL(T) for any recursively enumerable S1755020312000275_inline2 A -theory T extending I Σ2. To prove these theorems, we use iterated consistency assertions and nonstandard models of arithmetic, and we improve Artemov’s lemma which is used to prove Vardanyan’s theorem on the Π0 2-completeness of PL(T). (shrink)

I agree that Wollheim is wrong in his reconstruction of Bradley's arguments on Subject-Predicate judgements, but not completely. Wollheim is right about the conclusion of Bradley's arguments. I argue that Bradley does not reject subject-predicate form of judgements rather he attack's the idea that there is some judgement in which the subject is the nude reality.

In this paper, a paradox is shown to arise in the context of classical logic from prima facie highly plausible assumptions for the existence predicate as applied to definite descriptions. There are several possibilities to evade the paradox; all involve modifications in the principles of first-order logic with identity, existence, and definite descriptions; some stay within classical logic, others leave it. The merits of the various "ways out" are compared. The most attractive "way out," it is argued, stays within (...) classical logic, except for the fact that it involves a new logical truth: "There is at least one non-existent object." But this "exit" will certainly not be to everyone's taste and liking. Thus, the paradox defies complete resolution. (shrink)

Summary We have considered complete consistent systems in the first‐oder predicate calculus with identity, and have studied the set of the models of such a system by means of the maximal consistent condition‐sets associated with the system. The results may be summarized thus: (a) A complete consistent system is no‐categorical (= categorical in the denumerable domain) if and only if for every n, the number of different conditions in n variables is finite (T10). (b) If a complete consistent system (...) has a model M with finite character (i.e. a model M such that every maximal consistent condition‐set satisfied in M has a finite basis), then this model M is uniquely characterized by the property that every other model is an arithmetic extension of M (T 5). (c) Every complete consistent system, which has only a denumerable number of different associated maximal consistent condition‐sets, has a model with finite character (T8). (shrink)

Using the framework of categorical logic, this paper analyzes and streamlines Gabbay's semantical proof of the Craig interpolation theorem for intuitionistic predicate logic. In the process, an apparently new and interesting fact about the relation of coherent and intuitionistic logic is found.

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)

We give a simple proof-theoretic argument showing that Glivenko’s theorem for propositional logic and its version for predicate logic follow as an easy consequence of the deduction theorem, which also proves some Glivenko type theorems relating intermediate predicate logics between intuitionistic and classical logic. We consider two schemata, the double negation shift (DNS) and the one consisting of instances of the principle of excluded middle for sentences (REM). We prove that both schemata combined derive classical logic, while each (...) one of them provides a strictly weaker intermediate logic, and neither of them is derivable from the other. We show that over every intermediate logic there exists a maximal intermediate logic for which Glivenko’s theorem holds. We deduce as well a characterization of DNS, as the weakest (with respect to derivability) scheme that added to REM derives classical logic. (shrink)

In the article we study the existence predicate \(\varepsilon\) in the context of semantics for first-order modal logic. For a formula \(\varphi\) we define \(\varphi^{\varepsilon}\) - the so called existence relativization. We point to a gap in the work of Fitting and Mendelsohn concerning the relationship between the truth of \(\varphi\) and \(\varphi^{\varepsilon}\) in classes of varying- and constant-domain models. We introduce operations on models which allow us to fill the gap and provide a more general perspective on the (...) issue. As a result we obtain a series of theorems describing the logical connection between the notion of truth of a formula with the existence predicate in constant-domain models and the notion of truth of a formula without the existence predicate in varying-domain models. (shrink)

In this paper I argue that descriptive content associated with a proper name can serve as a truth-conditionally relevant adjunct and be an additional contribution of the name to the truth-conditions. Definite descriptions the so-and-so associated by speakers with a proper name can be used as qualifying prepositional phrases as so-and-so, so sentences containing a proper name NN is doing something could be understood as NN is doing something as NN (which means as so-and-so). Used as an adjunct, the descriptive (...) content of a proper name expresses the additional circumstances of an action (a manner, reason, goal, time or purpose) and constitute a part of a predicate. I argue that qualifying prepositional phrases should be analyzed as predicate modifiers and propose a formal representation of modified predicates. The additional truth-conditional relevance of the descriptive content of a proper name helps to explain the phenomenon of the substitution failure of coreferential names in simple sentences. (shrink)