The present paper intends to draw the conception of language implied in the technique of word embeddings that supported the recent development of deep neural network models in computational linguistics. After a preliminary presentation of the basic functioning of elementary artificial neural networks, we introduce the motivations and capabilities of word embeddings through one of its pioneering models, word2vec. To assess the remarkable results of the latter, we inspect the nature of its underlying mechanisms, which have been characterized as the (...) implicit factorization of a word-context matrix. We then discuss the ordinary association of the “distributional hypothesis” with a “use theory of meaning,” often justifying the theoretical basis of word embeddings, and contrast them to the theory of meaning stemming from those mechanisms through the lens of matrix models (such as vector space models and distributional semantic models). Finally, we trace back the principles of their possible consistency through Harris’s original distributionalism up to the structuralist conception of language of Saussure and Hjelmslev. Other than giving access to the technical literature and state of the art in the field of natural language processing to non-specialist readers, the paper seeks to reveal the conceptual and philosophical stakes involved in the recent application of new neural network techniques to the computational treatment of language. (shrink)

We introduce a new simple way of defining the forcing method that works well in the usual setting under FA, the Foundation Axiom, and moreover works even under Aczel's AFA, the Anti-Foundation Axiom. This new way allows us to have an intuition about what happens in defining the forcing relation. The main tool is H. Friedman's method of defining the extensional membership relation ∈ by means of the intensional membership relation ε .Analogously to the usual forcing and the usual generic (...) extension for FA-models, we can justify the existence of generic filters and can obtain the Forcing Theorem and the Minimal Model Theorem with some modifications. These results are on the line of works to investigate whether model theory for AFA-set theory can be developed in a similar way to that for FA-set theory.Aczel pointed out that the quotient of transition systems by the largest bisimulation and transition relations have the essentially same theory as the set theory with AFA. Therefore, we could hope that, by using our new method, some open problems about transition systems turn out to be consistent or independent. (shrink)

The thesis according to which the meaning of a mathematical sentence is given by its proof was held by both Wittgenstein and the intuitionists, following Heyting and Dummett. In this paper, we clarify the meaning of this thesis for Wittgenstein, showing how his position differs from that of the intuitionists. We show how the thesis originates in his thoughts, from the middle period, about proofs by induction, and we sketch his answers to a number of objections, including the idea that, (...) given the particular meaning he gives to this thesis, he cannot account for mathematical conjectures. We conclude by showing how his views find a favourable echo today in the paradigm of “proposition-as-type” and extensions of the Curry-Howard isomorphism from which this paradigm originates. (shrink)

This article provides a survey of key papers that characterise computable functions, but also provides some novel insights as follows. It is argued that the power of algorithms is at least as strong as functions that can be proved to be totally computable in type-theoretic translations of subsystems of second-order Zermelo Fraenkel set theory. Moreover, it is claimed that typed systems of the lambda calculus give rise naturally to a functional interpretation of rich systems of types and to a hierarchy (...) of ordinal recursive functionals of arbitrary type that can be reduced by substitution to natural number functions. (shrink)

We propose an extension of minimal intuitionistic predicate logic, based on delimited control operators, that can derive the predicate-logic version of the double-negation shift schema, while preserving the disjunction and existence properties.