Computability, while usually performed within the context of ω, may be extended to larger ordinals by means of α-recursion. In this article, we concentrate on the particular case of ω1-recursion, and study the differences in the behavior of ${\rm{\Pi }}_1^0$-classes between this case and the standard one.Of particular interest are the ${\rm{\Pi }}_1^0$-classes corresponding to computable trees of countable width. Classically, it is well-known that the analog to König’s Lemma—“every tree of countable width and uncountable height has an uncountable (...) branch”—fails; we demonstrate that not only does it fail effectively, but also that the failure is as drastic as possible. This is proven by showing that the ω1-Turing degrees of even isolated paths in computable trees of countable width are cofinal in the ${\rm{\Delta }}_1^1\,{\omega _1}$-Turing degrees.Finally, we consider questions of nonisolated paths, and demonstrate that the degrees realizable as isolated paths and the degrees realizable as nonisolated ones are very distinct; in particular, we show that there exists a computable tree of countable width so that every branch can only be ω1-Turing equivalent to branches of trees with ${\aleph _2}$-many branches. (shrink)

We compute the domination monoid in the theory of dense meet‐trees. In order to show that this monoid is well‐defined, we prove weak binarity of and, more generally, of certain expansions of it by binary relations on sets of open cones, a special case being the theory from [7]. We then describe the domination monoids of such expansions in terms of those of the expanding relations.

We examine the reverse mathematics and computability theory of a form of Ramsey's theorem in which the linear n-tuples of a binary tree are colored.

Several results about the game of cops and robbers on infinite graphs are analyzed from the perspective of computability theory. Computable robber-win graphs are constructed with the property that no computable robber strategy is a winning strategy, and such that for an arbitrary computable ordinal \, any winning strategy has complexity at least \}\). Symmetrically, computable cop-win graphs are constructed with the property that no computable cop strategy is a winning strategy. Locally finite infinite trees and graphs are explored. (...) The Turing computability of a binary relation used to classify cop-win graphs is studied, and the computational difficulty of determining the winner for locally finite computable graphs is discussed. (shrink)

Proof-theoretic models of grammar are based on the view that an explicit characterization of a language comes in the form of the recursive enumeration of strings in that language. That recursive enumeration is carried out by a procedure which strongly generates a set of structural descriptions Σ and weakly generates a set of strings S; a grammar is thus a function that pairs an element of Σ with elements of S. Structural descriptions are obtained by means of Context-Free phrase structure (...) rules or via recursive combinatorics and structure is assumed to beuniform: binary branching trees all the way down. In this work we will analyse natural language constructions for which such a rigid conception of phrase structure is descriptively inadequate and propose a solution for the problem of phrase structure grammars assigning too much or too little structure to natural language strings: we propose that the grammar can oscillate between levels of computational complexity in local domains, which correspond to elementary trees in a lexicalised Tree Adjoining Grammar. (shrink)

This paper continues our study of computable point-free topological spaces and the metamathematical points in them. For us, a point is the intersection of a sequence of basic open sets with compact and nested closures. We call such a sequence a sharp filter. A function fF from points to points is generated by a function F from basic open sets to basic open sets such that sharp filters map to sharp filters. We restrict our study to functions that have at (...) least all computable points in their domains.We follow Turing's approach in stating that a point is computable if it is the limit of a computable sharp filter; we then define the Turing degree Deg of a general point x in an analogous way. Because of the vagaries of the definition, a result of J. Miller applies and we note that not all points in all our spaces have Turing degrees; but we also show a certain class of points do. We further show that in ℝn all points have Turing degrees and that these degrees are the same as the classical Turing degrees of points defined by other researchers.We also prove the following: For a point x that has a Turing degree and lies either on a computable tree T or in the domain of a computable function fF, there is a sharp filter on T or in dom converging to x and with the same Turing degree as x. Furthermore, all possible Turing degrees occur among the degrees of such points for a given computable function fF or a complete, computable, binary tree T. For each x ∈ dom for which x and fF have Turing degrees, Deg) ≤ Deg. Finally, the Turing degrees of the sharp filters convergent to a given x are closed upward in the partial order of all Turing degrees. (shrink)

In this paper we show the adequacy of tense logic with unary operators for dealing with finite trees. We prove that models on finite trees can be characterized by tense formulas, and describe an effective method to find an axiomatization of the theory of a given finite tree in tense logic. The strength of the characterization is shown by proving that adding the binary operators "Until" and "Since" to the language does not result in a better description (...) than that given by unary tense logic; although the greater expressive power of "Until" and "Since" can be exploited by using the semantics of e-frames instead of traditional Kripke semantics. (shrink)

We present a new manifestation of Gödel’s second incompleteness theorem and discuss its foundational significance, in particular with respect to Hilbert’s program. Specifically, we consider a proper extension of Peano arithmetic ( $\mathbf {PA}$ ) by a mathematically meaningful axiom scheme that consists of $\Sigma ^0_2$ -sentences. These sentences assert that each computably enumerable ( $\Sigma ^0_1$ -definable without parameters) property of finite binary trees has a finite basis. Since this fact entails the existence of polynomial time algorithms, (...) it is relevant for computer science. On a technical level, our axiom scheme is a variant of an independence result due to Harvey Friedman. At the same time, the meta-mathematical properties of our axiom scheme distinguish it from most known independence results: Due to its logical complexity, our axiom scheme does not add computational strength. The only known method to establish its independence relies on Gödel’s second incompleteness theorem. In contrast, Gödel’s theorem is not needed for typical examples of $\Pi ^0_2$ -independence (such as the Paris–Harrington principle), since computational strength provides an extensional invariant on the level of $\Pi ^0_2$ -sentences. (shrink)

The satisfiability problem for the two-variable fragment of first-order logic is investigated over finite and infinite linearly ordered, respectively wellordered domains, as well as over finite and infinite domains in which one or several designated binary predicates are interpreted as arbitrary wellfounded relations. It is shown that FO 2 over ordered, respectively wellordered, domains or in the presence of one well-founded relation, is decidable for satisfiability as well as for finite satisfiability. Actually the complexity of these decision problems is (...) essentially the same as for plain unconstrained FO 2 , namely non-deterministic exponential time. In contrast FO 2 becomes undecidable for satisfiability and for finite satisfiability, if a sufficiently large number of predicates are required to be interpreted as orderings, wellorderings, or as arbitrary wellfounded relations. This undecidability result also entails the undecidability of the natural common extension of FO 2 and computation tree logic CTL. (shrink)

In this work we propose the partial Wiener index as one possible measure of branching in phylogenetic evolutionary trees. We establish the connection between the generalized Robinson–Foulds (RF) metric for measuring the similarity of phylogenetic trees and partial Wiener indices by expressing the number of conflicting pairs of edges in the generalized RF metric in terms of partial Wiener indices. To do so we compute the minimum and maximum value of the partial Wiener index WT,r,n\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} (...) \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$W\left(T,r, n\right)$$\end{document}, where T\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$T$$\end{document} is a binary rooted tree with root r\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$r$$\end{document} and n\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$n$$\end{document} leaves. Moreover, under the Yule probabilistic model, we show how to compute the expected value of WT,r,n\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$W\left(T,r, n\right)$$\end{document}. As a direct consequence, we give exact formulas for the upper bound and the expected number of conflicting pairs. By doing so we provide a better theoretical understanding of the computational complexity of the generalized RF metric. (shrink)

We give resource bounded versions of the Completeness Theorem for propositional and predicate logic. For example, it is well known that every computable consistent propositional theory has a computable complete consistent extension. We show that, when length is measured relative to the binary representation of natural numbers and formulas, every polynomial time decidable propositional theory has an exponential time (EXPTIME) complete consistent extension whereas there is a nondeterministic polynomial time (NP) decidable theory which has no polynomial time complete consistent (...) extension when length is measured relative to the binary representation of natural numbers and formulas. It is well known that a propositional theory is axiomatizable (respectively decidable) if and only if it may be represented as the set of infinite paths through a computable tree (respectively a computable tree with no dead ends). We show that any polynomial time decidable theory may be represented as the set of paths through a polynomial time decidable tree. On the other hand, the statement that every polynomial time decidable, relative to the tally representation of natural numbers and formulas, is equivalent to P = NP. For predicate logic, we develop a complexity theoretic version of the Henkin construction to prove a complexity theoretic version of the Completeness Theorem. Our results imply that that any polynomial space decidable theory △ possesses a polynomial space computable model which is exponential space decidable and thus △ has an exponential space complete consistent extension. Similar results are obtained for other notions of complexity. (shrink)

It is known that the full computation-tree logic CTL * is an important base logic for model checking. The bisimulation theorem for CTL* is known to be useful for abstraction in model checking. In this paper, the bisimulation theorems for two paraconsistent four-valued extensions 4CTL* and 4LCTL* of CTL* are shown, and a translation from 4CTL* into CTL* is presented. By using 4CTL* and 4LCTL*, inconsistency-tolerant and spatiotemporal reasoning can be expressed as a model checking framework.

We give a sound and complete axiomatization for the full computation tree logic, CTL*, of R-generable models. This solves a long standing open problem in branching time temporal logic.

Makkai [10] produced an arithmetical structure of Scott rank $\omega _{1}^{\mathit{CK}}$. In [9]. Makkai's example is made computable. Here we show that there are computable trees of Scott rank $\omega _{1}^{\mathit{CK}}$. We introduce a notion of "rank homogeneity". In rank homogeneous trees, orbits of tuples can be understood relatively easily. By using these trees, we avoid the need to pass to the more complicated "group trees" of [10] and [9]. Using the same kind of trees, (...) we obtain one of rank $\omega _{1}^{\mathit{CK}}$ that is "strongly computably approximable". We also develop some technology that may yield further results of this kind. (shrink)

We introduce the appropriate iterated version of the system of ordinal notations from [G1] whose order type is the familiar Howard ordinal. As in [G1], our ordinal notations are partly inspired by the ideas from [P] where certain crucial properties of the traditional Munich' ordinal notations are isolated and used in the cut-elimination proofs. As compared to the corresponding “impredicative” Munich' ordinal notations (see e.g. [B1, B2, J, Sch1, Sch2, BSch]), our ordinal notations arearbitrary terms in the appropriate simple term (...) algebra based on the notion of collapsing functions (which we would rather identify as projective functions). In Sect. 1 below we define the systems of ordinal notationsPRJ( ), for any primitive recursive limit wellordering . In Sect. 2 we prove the crucial well-foundness property by using the appropriate well-quasi-ordering property of the corresponding binary labeled trees [G3]. In Sect. 3 we interprete inPRJ( ) the familiar Veblen-Bachmann hierarchy of ordinal functions, and in Sect. 4 we show that the corresponding Buchholz's system of ordinal notationsOT( ) is a proper subsystem ofPRJ( ), although it has the same order type according to [G3] together with the interpretation from Sect. 2 in the terms of labeled trees. In Sect. 5 we use Friedman's approach in order to obtain an appropriate purely combinatorial statement which is not provable in the theory of iterated inductive definitions ID< λ, for arbitrarily large limit ordinalλ. Formal theories, axioms, etc. used below are familiar in the proof theory of subsystems of analysis (see [BFPS, T, BSch]). (shrink)

We divide the class of infinite computable trees into three types. For the first and second types, 0' computes a nontrivial self-embedding while for the third type 0'' computes a nontrivial self-embedding. These results are optimal and we obtain partial results concerning the complexity of nontrivial self-embeddings of infinite computable trees considered up to isomorphism. We show that every infinite computable tree must have either an infinite computable chain or an infinite Π01 antichain. This result is optimal and (...) has connections to the program of reverse mathematics. (shrink)

A complete axiomatic system CTL$_{rp}$ is introduced for a temporal logic for finitely branching $\omega^+$-trees in a temporal language extended with so called reference pointers. Syntactic and semantic interpretations are constructed for the branching time computation tree logic CTL$^{*}$ into CTL$_{rp}$. In particular, that yields a complete axiomatization for the translations of all valid CTL$^{*}$-formulae. Thus, the temporal logic with reference pointers is brought forward as a simpler (with no path quantifiers), but in a way more expressive medium (...) for reasoning about branching time. (shrink)

Jones argues that extending Seneca kin terms to second cousins requires a revised version of Optimality Theoretic grammar. I extend Seneca terms using three constraints on expression of markers in nested binary classification trees. Multiple constraint rankings on a nested set coupled with local parity checking determines how a given kin classification grammar marks structural endogamy.

This article discusses ways to operationalise the concept of culturally appropriate computer-mediated communication, utilising information systems (IS) development methodologies and adopting a postmodern and postcolonial perspective. By way of illustration, it describes progress on the participative development of the Ieramugadu Cultural Information System. This project is designed to develop and evaluate innovative procedures for elicitation, analysis, storage and communication of indigenous cultural heritage information. It is investigating culturally appropriate IS design techniques, multimedia approaches and ways to ensure protection of secret/sacred (...) information. Ethical issues are foregrounded. (shrink)

A sentence of first-order logic is satisfiable if it is true in some structure, and finitely satisfiable if it is true in some finite structure. The question arises as to whether there exists an algorithm for determining whether a given formula of first-order logic is satisfiable, or indeed finitely satisfiable. This question was answered negatively in 1936 by Church and Turing (for satisfiability) and in 1950 by Trakhtenbrot (for finite satisfiability).In contrast, the satisfiability and finite satisfiability problems are algorithmically solvable (...) for restricted subsets---or, as we say, fragments---of first-order logic, a fact which is today of considerable interest in Computer Science. This book provides an up-to-date survey of the principal axes of research, charting the limits of decision in first-order logic and exploring the trade-off between expressive power and complexity of reasoning. Divided into three parts, the book considers for which fragments of first-order logic there is an effective method for determining satisfiability or finite satisfiability. Furthermore, if these problems are decidable for some fragment, what is their computational complexity? Part I focusses on fragments defined by restricting the set of available formulas. Topics covered include the Aristotelian syllogistic and its relatives, the two-variable fragment, the guarded fragment, the quantifier-prefix fragments and the fluted fragment. Part II investigates logics with counting quantifiers. Starting with De Morgan's numerical generalization of the Aristotelian syllogistic, we proceed to the two-variable fragment with counting quantifiers and its guarded subfragment, explaining the applications of the latter to the problem of query answering in structured data. Part III concerns logics characterized by semantic constraints, limiting the available interpretations of certain predicates. Taking propositional modal logic and graded modal logic as our cue, we return to the satisfiability problem for two-variable first-order logic and its relatives, but this time with certain distinguished binary predicates constrained to be interpreted as equivalence relations or transitive relations. The work finishes, slightly breaching the bounds of first-order logic proper, with a chapter on logics interpreted over trees. (shrink)

We prove that no computable tree of infinite height is computably categorical, and indeed that all such trees have computable dimension ω. Moreover, this dimension is effectively ω, in the sense that given any effective listing of computable presentations of the same tree, we can effectively find another computable presentation of it which is not computably isomorphic to any of the presentations on the list.

The notion of “bounded rationality” was introduced by Simon as an appropriate framework for explaining how agents reason and make decisions in accordance with their computational limitations and the characteristics of the environments in which they exist (seen metaphorically as two complementary scissor blades).We elaborate on how bounded rationality is usually conceived in psychology and on its relationship with logic. We focus on the relationship between heuristics and some non-monotonic logical systems. These two categories of cognitive tools share fundamental features. (...) As a step further, we show that in some cases heuristics themselves can be formalized from this logic perspective. We have therefore two main aims: on the one hand, to demonstrate the relationship between the bounded rationality programme and logic, understood in a broad sense; on the other hand, to provide logical tools of analysis of already known heuristics. This may lead to results such as the characterization of fast and frugal binary trees in terms of their associated logic program here provided. (shrink)

The so-called weak König's lemma WKL asserts the existence of an infinite path b in any infinite binary tree . Based on this principle one can formulate subsystems of higher-order arithmetic which allow to carry out very substantial parts of classical mathematics but are Π 2 0 -conservative over primitive recursive arithmetic PRA . In Kohlenbach 1239–1273) we established such conservation results relative to finite type extensions PRA ω of PRA . In this setting one can consider also a (...) uniform version UWKL of WKL which asserts the existence of a functional Φ which selects uniformly in a given infinite binary tree f an infinite path Φf of that tree. This uniform version of WKL is of interest in the context of explicit mathematics as developed by S. Feferman. The elimination process in Kohlenbach [10] actually can be used to eliminate even this uniform weak König's lemma provided that PRA ω only has a quantifier-free rule of extensionality QF-ER instead of the full axioms of extensionality for all finite types. In this paper we show that in the presence of , UWKL is much stronger than WKL: whereas WKL remains to be Π 2 0 -conservative over PRA, PRA ω ++ UWKL contains full Peano arithmetic PA. We also investigate the proof–theoretic as well as the computational strength of UWKL relative to the intuitionistic variant of PRA ω both with and without the Markov principle. (shrink)

We characterize the structure of computably categorical trees of finite height, and prove that our criterion is both necessary and sufficient. Intuitively, the characterization is easiest to express in terms of isomorphisms of (possibly infinite) trees, but in fact it is equivalent to a Σ03-condition. We show that all trees which are not computably categorical have computable dimension ω. Finally, we prove that for every n≥ 1 in ω, there exists a computable tree of finite height which (...) is δ0n+1-categorical but not δ0n-categorical. (shrink)

We show that for no chain C there is a monadic-second order interpretation of the full binary tree in C.

We study the position of the computable setting in the “common theory of locality” developed in [4, 5] for local problems on $\Delta $ -regular trees, $\Delta \in \omega $. We show that such a problem admits a computable solution on every highly computable $\Delta $ -regular forest if and only if it admits a Baire measurable solution on every Borel $\Delta $ -regular forest. We also show that if such a problem admits a computable solution on every computable (...) maximum degree $\Delta $ forest then it admits a continuous solution on every maximum degree $\Delta $ Borel graph with appropriate topological hypotheses, though the converse does not hold. (shrink)

This paper presents a method to compute a posteriori probability intervals when the initial conditional information is also given with probability intervals. The right way to make an exact computation is with the associated convex set of probabilities. Probability trees are used to represent these initial conditional convex sets because they greatly save the space required. This paper proposes a simulated annealing algorithm, which uses probability trees to represent the convex sets in order to compute the a (...) posteriori intervals. (shrink)

The first collection of Leibniz's key writings on the binary system, newly translated, with many previously unpublished in any language. -/- The polymath Gottfried Wilhelm Leibniz (1646–1716) is known for his independent invention of the calculus in 1675. Another major—although less studied—mathematical contribution by Leibniz is his invention of binary arithmetic, the representational basis for today's digital computing. This book offers the first collection of Leibniz's most important writings on the binary system, all newly translated by the (...) authors with many previously unpublished in any language. Taken together, these thirty-two texts tell the story of binary as Leibniz conceived it, from his first youthful writings on the subject to the mature development and publication of the binary system. -/- As befits a scholarly edition, Strickland and Lewis have not only returned to Leibniz's original manuscripts in preparing their translations, but also provided full critical apparatus. In addition to extensive annotations, each text is accompanied by a detailed introductory “headnote” that explains the context and content. Additional mathematical commentaries offer readers deep dives into Leibniz's mathematical thinking. The texts are prefaced by a lengthy and detailed introductory essay, in which Strickland and Lewis trace Leibniz's development of binary, place it in its historical context, and chart its posthumous influence, most notably on shaping our own computer age. (shrink)

A characterization of a property of binary relations is of finite type if it is stated in terms of ordered T-tuples of alternatives for some positive integer T. The concept was introduced informally by Knoblauch (2005). We give a clear, complete definition below. We prove that a characterization of finite type can be used to determine in polynomial time whether a binary relation over a finite set has the property characterized. We also prove a simple but useful nonexistence (...) theorem and apply it to three examples. (shrink)

For [Formula: see text], the coarse similarity class of A, denoted by [Formula: see text], is the set of all [Formula: see text] such that the symmetric difference of A and B has asymptotic density 0. There is a natural metric [Formula: see text] on the space [Formula: see text] of coarse similarity classes defined by letting [Formula: see text] be the upper density of the symmetric difference of A and B. We study the metric space of coarse similarity classes (...) under this metric, and show in particular that between any two distinct points in this space there are continuum many geodesic paths. We also study subspaces of the form [Formula: see text] where [Formula: see text] is closed under Turing equivalence, and show that there is a tight connection between topological properties of such a space and computability-theoretic properties of [Formula: see text]. We then define a distance between Turing degrees based on Hausdorff distance in the metric space [Formula: see text]. We adapt a proof of Monin to show that the Hausdorff distances between Turing degrees that occur are exactly 0, [Formula: see text], and 1, and study which of these values occur most frequently in the senses of Lebesgue measure and Baire category. We define a degree a to be attractive if the class of all degrees at distance [Formula: see text] from a has measure 1, and dispersive otherwise. In particular, we study the distribution of attractive and dispersive degrees. We also study some properties of the metric space of Turing degrees under this Hausdorff distance, in particular the question of which countable metric spaces are isometrically embeddable in it, giving a graph-theoretic sufficient condition for embeddability. Motivated by a couple of issues arising in the above work, we also study the computability-theoretic and reverse-mathematical aspects of a Ramsey-theoretic theorem due to Mycielski, which in particular implies that there is a perfect set whose elements are mutually 1-random, as well as a perfect set whose elements are mutually 1-generic. Finally, we study the completeness of [Formula: see text] from the perspectives of computability theory and reverse mathematics. (shrink)

Semantic memory encompasses one's knowledge about the world. Distributional semantic models, which construct vector spaces with embedded words, are a proposed framework for understanding the representational structure of human semantic knowledge. Unlike some classic semantic models, distributional semantic models lack a mechanism for specifying the properties of concepts, which raises questions regarding their utility for a general theory of semantic knowledge. Here, we develop a computational model of a binary semantic classification task, in which participants judged target words for (...) the referent's size or animacy. We created a family of models, evaluating multiple distributional semantic models, and mechanisms for performing the classification. The most successful model constructed two composite representations for each extreme of the decision axis (e.g., one averaging together representations of characteristically big things and another of characteristically small things). Next, the target item was compared to each composite representation, allowing the model to classify more than 1,500 words with human‐range performance and to predict response times. We propose that when making a decision on a binary semantic classification task, humans use task prompts to retrieve instances representative of the extremes on that semantic dimension and compare the probe to those instances. This proposal is consistent with the principles of the instance theory of semantic memory. (shrink)

Tylman has recently pointed out some striking conceptual and methodological analogies between philosophy and computer science. In this paper, I focus on one of Tylman’s most convincing cases, viz. the similarity between Plato’s theory of Ideas and the object-oriented programming paradigm, and analyze it in some more detail. In particular, I argue that the platonic doctrine of the Porphyrian tree corresponds to the fact that most object-oriented programming languages do not support multiple inheritance. This analysis further reinforces Tylman’s point regarding (...) the conceptual continuity between classical metaphysical theorizing and contemporary computer science. (shrink)

ABSTRACTIs the brain a digital computer? What about your own brain? This article will examine these questions, some possible answers, and what persistent disagreement on the topic might indicate. Along the way we explore the metaphor at the heart of the question and assess how observer relativity features in it. We also reflect on the role of models in scientific endeavour. By the end you should have a sense of why the question matters, what some answers to it might be, (...) and why your preferred answer is highly pertinent to any discussion. (shrink)

A central problem in the cognitive sciences is identifying the link between consciousness and neural computation. The key features of consciousness—including the emergence of representative information content and the initiation of volitional action—are correlated with neural activity in the cerebral cortex, but not computational processes in spinal reflex circuits or classical computing architecture. To take a new approach toward considering the problem of consciousness, it may be worth re‐examining some outstanding puzzles in neuroscience, focusing on differences between the cerebral (...) cortex and spinal reflex circuits. First, the mammalian cerebral cortex exhibits exascale computational power, a feature that is not strictly correlated with the number of binary computational units; second, individual computational units engage in noisy coding, allowing random electrical events to gate signaling outcomes; third, this noisy coding results in the synchronous firing of statistically random populations of cells across the neural network, at a range of nested frequencies; fourth, the system grows into a more ordered state over time, as it encodes the predictive value gained through observation; and finally, the cerebral cortex is extraordinarily energy efficient, with very little free energy lost to entropy during the work of information processing. Here, I argue that each of these five key features suggest the mammalian brain engages in probabilistic computation. Indeed, by modeling the physical mechanisms of probabilistic computation, we may find a better way to explain the unique emergent features arising from cortical neural networks. (shrink)

We formulate a restriction of Hindman’s Finite Sums Theorem in which monochromaticity is required only for sums corresponding to rooted finite paths in the full binary tree. We show that the resulting principle is equivalent to \-induction over \. The proof uses the equivalence of this Hindman-type theorem with the Pigeonhole Principle for trees \ with an extra condition on the solution tree.

Formal topology is today an established topic in the development of constructive mathematics and constructive proofs for many classical results of general topology have been obtained by using this approach. Here we analyze one of the main concepts in formal topology, namely, the notion of formal point. We will contrast two classically equivalent definitions of formal points and we will see that from a constructive point of view they are completely different. Indeed, according to the first definition the formal points (...) of the formal topology of the real numbers can be indexed by a set whereas this is not possible according to the second one. (shrink)

Evolutionary and organismal biology have become inundated with data. At the same rate, we are experiencing a surge in broader evolutionary and ecological syntheses for which tree-thinking is the staple for a variety of post-tree analyses. To fully take advantage of this wealth of data to discover and understand large-scale evolutionary and ecological patterns, computational data integration, i.e., the use of machines to link data at large scale, is crucial. The most common shared entity by which evolutionary and ecological data (...) need to be linked is the taxon to which they belong. We propose a set of requirements that a system for defining such taxa should meet for computational data science: taxon definitions should maintain conceptual consistency, be reproducible via a known algorithm, be computationally automatable, and be applicable across the Tree of Life. We argue that Linnaean names, the most prevalent means of linking data to taxa, fail to meet these requirements due to fundamental theoretical and practical shortfalls. We argue that for the purposes of data-integration we should instead use phylogenetic definitions transformed into formal logic expressions. We call such expressions “phyloreferences”, and argue that, unlike Linnaean names, they meet all requirements for effective data-integration. (shrink)

Let S2S [WS2S] espectively be the storn [weak] monadic second order theory of the binary tree T in the language of two successor functions. An S2S-formula whose free variables are just individual variables defines a relation on T (rather than on the power set of T). We show that S2S and WS2S define the same relations on T, and we give a simple characterization of these relations.

In this paper, we show that for any computable ordinal α, there exists a computable tree of rank with strong degree of categoricity if α is finite, and with strong degree of categoricity if α is infinite. In fact, these are the greatest possible degrees of categoricity for such trees. For a computable limit ordinal α, we show that there is a computable tree of rank α with strong degree of categoricity (which equals ). It follows from our proofs (...) that, for every computable ordinal, the isomorphism problem for trees of rank α is ‐complete. (shrink)