Robots are increasingly being studied for use in education. It is expected that robots will have the potential to facilitate children’s learning and function autonomously within real classrooms in the near future. Previous research has raised the importance of designing acceptable robots for different practices. In parallel, scholars have raised ethical concerns surrounding children interacting with robots. Drawing on a Responsible Research and Innovation perspective, our goal is to move away from research concerned with designing features that will render robots (...) more socially acceptable by end users toward a reflective dialogue whose goal is to consider the key ethical issues and long-term consequences of implementing classroom robots for teachers and children in primary education. This paper presents the results from several focus groups conducted with teachers in three European countries. Through a thematic analysis, we provide a theoretical account of teachers’ perspectives on classroom robots pertaining to privacy, robot role, effects on children and responsibility. Implications for the field of educational robotics are discussed. (shrink)

In the context of his theory of numberings, Ershov showed that Kleene's recursion theorem holds for any precomplete numbering. We discuss various generalizations of this result. Among other things, we show that Arslanov's completeness criterion also holds for every precomplete numbering, and we discuss the relation with Visser's ADN theorem, as well as the uniformity or nonuniformity of the various fixed point theorems. Finally, we base numberings on partial combinatory algebras and prove a generalization of Ershov's theorem in this context.

A λ-theory T is a consistent set of equations between λ-terms closed under derivability. The degree of T is the degree of the set of Godel numbers of its elements. H is the $\lamda$ -theory axiomatized by the set {M = N ∣ M, N unsolvable. A $\lamda$ -theory is sensible $\operatorname{iff} T \supset \mathscr{H}$ , for a motivation see [6] and [4]. In § it is proved that the theory H is ∑ 0 2 -complete. We present Wadsworth's proof (...) that its unique maximal consistent extention $\mathscr{H}^\ast (= \mathrm{T}(D_\infty))$ is Π 0 2 -complete. In $\S2$ it is proved that $\mathscr{H}_\eta(= \lambda_\eta-\text{Calculus} + \mathscr{H})$ is not closed under the ω-rule (see [1]). In $\S3$ arguments are given to conjecture that $\mathscr{H}\omega (= \lambda + \mathscr{H} + omega-rule)$ is Π 1 1 -complete. This is done by representing recursive sets of sequence numbers as λ-terms and by connecting wellfoundedness of trees with provability in Hω. In $\S4$ an infinite set of equations independent over H η will be constructed. From this it follows that there are 2^{ℵ_0 sensible theories T such that $\mathscr{H} \subset T \subset \mathscr{H}^\ast$ and 2 ℵ 0 sensible hard models of arbitrarily high degrees. In $\S5$ some nonprovability results needed in $\S\S1$ and 2 are established. For this purpose one uses the theory H η extended with a reduction relation for which the Church-Rosser theorem holds. The concept of Gross reduction is used in order to show that certain terms have no common reduct. (shrink)

We study the cube of type assignment systems, as introduced in Giannini et al. 87–126), and confront it with Barendregt's typed gl-cube . The first is obtained from the latter through applying a natural type erasing function E to derivation rules, that erases type information from terms. In particular, we address the question whether a judgement, derivable in a type assignment system, is always an erasure of a derivable judgement in a corresponding typed system; we show that (...) this property holds only for systems without polymorphism. The type assignment systems we consider satisfy the properties ‘subject reduction’ and ‘strong normalization’. Moreover, we define a new type assignment cube that is isomorphic to the typed one. (shrink)

This collection of papers, celebrating the contributions of Swedish logician Dag Prawitz to Proof Theory, has been assembled from those presented at the Natural Deduction conference organized in Rio de Janeiro to honour his seminal research. Dag Prawitz’s work forms the basis of intuitionistic type theory and his inversion principle constitutes the foundation of most modern accounts of proof-theoretic semantics in Logic, Linguistics and Theoretical Computer Science. The range of contributions includes material on the extension of natural deduction with higher-order (...) rules, as opposed to higher-order connectives, and a paper discussing the application of natural deduction rules to dealing with equality in predicate calculus. The volume continues with a key chapter summarizing work on the extension of the Curry-Howard isomorphism, via methods of category theory that have been successfully applied to linear logic, as well as many other contributions from highly regarded authorities. With an illustrious group of contributors addressing a wealth of topics and applications, this volume is a valuable addition to the libraries of academics in the multiple disciplines whose development has been given added scope by the methodologies supplied by natural deduction. The volume is representative of the rich and varied directions that Prawitz work has inspired in the area of natural deduction. (shrink)

Jones and Coleman are among a handful of otherwise normal as a child and the number 5 was red and 6 was green. This the- people who have synesthesia. They experience the ordinary ory does not answer why only some people retain such vivid world in extraordinary ways and seem to inhabit a mysterious sensory memories, however. You might _think _of cold when you no-man’s-land between fantasy and reality. For them the sens- look at a picture of an ice (...) class='Hi'>cube, but you probably do not feel es—touch, taste, hearing, vision and smell—get mixed up in- cold, no matter how many encounters you may have had with stead of remaining separate. ice and snow during your youth. Modern scientists have known about synesthesia since Another prevalent idea is that synesthetes are merely being 1880, when Francis Galton, a cousin of Charles Darwin, pub- metaphorical when they describe the note C flat as “red” or say lished a paper in _Nature _on the phenomenon. But most have that chicken tastes “pointy”—just as you and I might speak of brushed it aside as fakery, an artifact of drug use (LSD and a “loud” shirt or “sharp” cheddar cheese. Our ordinary lan- mescaline can produce similar effects) or a mere curiosity. guage is replete with such sense-related metaphors, and perhaps About four years ago, however, we and others began to un- synesthetes are just especially gifted in this regard. cover brain processes that could account for synesthesia. Along We began trying to find out whether synesthesia is a gen- the way, we also found new clues to some of the most mysteri- uine sensory experience in 1999. This deceptively simple ques- ous aspects of the human mind, such as the emergence of ab- tion had plagued researchers in this field for decades. One nat- stract thought, metaphor and perhaps even language. ural approach is to start by asking the subjects outright: “Is this A common explanation of synesthesia is that the affected just a memory, or do you actually see the color as if it were right people are simply experiencing childhood memories and asso- in front of you?” When we tried asking this question, we did ciations.. (shrink)

We apply linear algebra to the study of the inconsistent figure known as the Crazy Crate. Disambiguation by means of occlusions leads to a class of sixteen such figures: consistent, complete, both and neither. Necessary and sufficien conditions for inconsistency are obtained.

Experimental Phenomenology is a book on learning phenomenology by doing it. The format follows the progression of a number of thought-experiments which mark out the procedures and directions of phenomenological inquiry. Making use of examples of familiar optical illusions and multi-stable drawings, such as the well-known Necker cube, Professor Ihde illustrates by way of careful and disciplined step-by-step analyses how some of the main methodological procedures and epistemological concepts of phenomenology assume concrete relevance in the project of doing phenomenology. (...) Such formidable phenomenological fare as epoche, noetic and noematic analysis, apodicticity, adequacy, sedimentation, imaginative variation, field, and fringe are rendered into the currency of a quotidian commerce with the perceptual world. (shrink)

. It is shown that the properties of so-called consequential implication allow to construct more than one aristotelian square relating implicative sentences of the consequential kind. As a result, if an aristotelian cube is an object consisting of two distinct aristotelian squares and four distinct “semiaristotelian” squares sharing corner edges, it is shown that there is a plurality of such cubes, which may also result from the composition of cubes of lower complexity.

We study the computational content of the Brouwer Fixed Point Theorem in the Weihrauch lattice. Connected choice is the operation that finds a point in a non-empty connected closed set given by negative information. One of our main results is that for any fixed dimension the Brouwer Fixed Point Theorem of that dimension is computably equivalent to connected choice of the Euclidean unit cube of the same dimension. Another main result is that connected choice is complete for dimension greater (...) than or equal to two in the sense that it is computably equivalent to Weak Kőnig’s Lemma. While we can present two independent proofs for dimension three and upward that are either based on a simple geometric construction or a combinatorial argument, the proof for dimension two is based on a more involved inverse limit construction. The connected choice operation in dimension one is known to be equivalent to the Intermediate Value Theorem; we prove that this problem is not idempotent in contrast to the case of dimension two and upward. We also prove that Lipschitz continuity with Lipschitz constants strictly larger than one does not simplify finding fixed points. Finally, we prove that finding a connectedness component of a closed subset of the Euclidean unit cube of any dimension greater than or equal to one is equivalent to Weak Kőnig’s Lemma. In order to describe these results, we introduce a representation of closed subsets of the unit cube by trees of rational complexes. (shrink)

In ‘Reichenbach's cubical universe and the problem of the external world’, Elliott Sober attempts a refutation of solipsism à la Reichenbach. I here contrast Sober's line of argument with observati...

The debates about human free will are traditionally the concern of metaphysics but neuroscientists have recently entered the field arguing that acts of the will are determined by brain events themselves causal products of other events. We examine that claim through the example of free or voluntary switch of perception in relation to the Necker cube. When I am asked to see the cube in one way, I decide whether I will follow the command (or do as I (...) am asked) using skills that reason and language give to me and change my brain states accordingly. The voluntary shift of perspective in seeing the Necker cube this way or that exemplifies the top-down control exercised by a human being on the basis of the role of language and meaning in their activity. It also indicates the lived story that is at the centre of each human consciousness. In the third part of this essay, three arguments are used to undermine metaphysical objections to the very idea of top-down self control. (shrink)

Universality of generalized Alexandroff's cube plays essential role in theory of absolute retracts for the category of , -closure spaces. Alexandroff's cube. is an , -closure space generated by the family of all complete filters. in a lattice of all subsets of a set of power .Condition P(, , ) says that is a closure space of all , -filters in the lattice ( ).

In the paper [2] the following theorem is shown: Theorem (Th. 3,5, [2]), If =0 or = or , then a closure space X is an absolute extensor for the category of , -closure spaces iff a contraction of X is the closure space of all , -filters in an , -semidistributive lattice.In the case when = and =, this theorem becomes Scott's theorem.

Pure Type Systems, PTSs, were introduced as a generalization of the type systems of Barendregt's lambda cube and were designed to provide a foundation for actual proof assistants which will verify proofs. Systems of illative combinatory logic or lambda calculus, ICLs, were introduced by Curry and Church as a foundation for logic and mathematics. In an earlier paper we considered two changes to the rules of the PTSs which made these rules more like ICL rules. This led to (...) four kinds of PTSs. Most importantly PTSs are about statements of the form M:A, where M is a term and A a type. In ICLs there are no explicit types and the statements are terms. In this paper we show that for each of the four forms of PTS there is an equivalent form of ICL, sometimes if certain conditions hold. (shrink)

Pure Type Systems, PTSs, introduced as a generalisation of the type systems of Barendregt's lambda-cube, provide a foundation for actual proof assistants, aiming at the mechanic verification of formal proofs. In this paper we consider simplifications of some of the rules of PTSs. This is of independent interest for PTSs as this produces more flexible PTS-like systems, but it will also help, in a later paper, to bridge the gap between PTSs and systems of Illative Combinatory Logic. First (...) we consider a simplification of the start and weakening rules of PTSs, which allows contexts to be sets of statements, and a generalisation of the conversion rule. The resulting Set-modified PTSs or SPTSs, though essentially equivalent to PTSs, are closer to standard logical systems. A simplification of the abstraction rule results in Abstraction-modified PTSs or APTSs. These turn out to be equivalent to standard PTSs if and only if a condition (*) holds. Finally we consider SAPTSs which have both modifications. (shrink)

After giving a short summary of the traditional theory of the syllogism, it is shown how the square of opposition reappears in the much more powerful concept logic of Leibniz. Within Leibniz’s algebra of concepts, the categorical forms are formalized straightforwardly by means of the relation of concept-containment plus the operator of concept-negation as ‘S contains P’ and ‘S contains Not-P’, ‘S doesn’t contain P’ and ‘S doesn’t contain Not-P’, respectively. Next we consider Leibniz’s version of the so-called Quantification of (...) the Predicate which consists in the introduction of four additional forms ‘Every S is every P’, ‘Some S is every P’, ‘Every S isn’t some P’, and ‘Some S isn’t some P’. Given the logical interpretation suggested by Leibniz, these unorthodox propositions also form a Square of Opposition which, when added to the traditional Square, yields a “Cube of Opposition”. Finally it is shown that besides the categorical forms, also the non-categorical forms can be formalized within an extension of Leibniz’s logic where “indefinite concepts” X, Y, Z\ function as quantifiers and where individual concepts are introduced as maximally consistent concepts. (shrink)

Pure Type Systems, PTSs, introduced as a generalisation of the type systems of Barendregt's lambda-cube, provide a foundation for actual proof assistants, aiming at the mechanic verification of formal proofs. In this paper we consider simplifications of some of the rules of PTSs. This is of independent interest for PTSs as this produces more flexible PTS-like systems, but it will also help, in a later paper, to bridge the gap between PTSs and systems of Illative Combinatory Logic. First (...) we consider a simplification of the start and weakening rules of PTSs, which allows contexts to be sets of statements, and a generalisation of the conversion rule. The resulting Set-modified PTSs or SPTSs, though essentially equivalent to PTSs, are closer to standard logical systems. A simplification of the abstraction rule results inion-modified PTSs or APTSs. These turn out to be equivalent to standard PTSs if and only if a condition holds. Finally we consider SAPTSs which have both modifications. (shrink)

We re-examine the problem of existential import by using classical predicate logic. Our problem is: How to distribute the existential import among the quantified propositions in order for all the relations of the logical square to be valid? After defining existential import and scrutinizing the available solutions, we distinguish between three possible cases: explicit import, implicit non-import, explicit negative import and formalize the propositions accordingly. Then, we examine the 16 combinations between the 8 propositions having the first two kinds of (...) import, the third one being trivial and rule out the squares where at least one relation does not hold. This leads to the following results: (1) three squares are valid when the domain is non-empty; (2) one of them is valid even in the empty domain: the square can thus be saved in arbitrary domains and (3) the aforementioned eight propositions give rise to a cube, which contains two more (non-classical) valid squares and several hexagons. A classical solution to the problem of existential import is thus possible, without resorting to deviant systems and merely relying upon the symbolism of First-order Logic (FOL). Aristotle’s system appears then as a fragment of a broader system which can be developed by using FOL. (shrink)

Various arguments have been put forward to show that Zeno-like paradoxes are still with us. A particularly interesting one involves a cube composed of colored slabs that geometrically decrease in thickness. We first point out that this argument has already been nullified by Paul Benacerraf. Then we show that nevertheless a further problem remains, one that withstands Benacerraf s critique. We explain that the new problem is isomorphic to two other Zeno-like predicaments: a problem described by Alper and Bridger (...) in 1998 and a modified version of the problem that Benardete introduced in 1964. Finally, we present a solution to the three isomorphic problems. (shrink)

Various arguments have been put forward to show that Zeno-like paradoxes are still with us. A particularly interesting one involves a cube composed of colored slabs that geometrically decrease in thickness. We first point out that this argument has already been nullified by Paul Benacerraf. Then we show that nevertheless a further problem remains, one that withstands Benacerraf’s critique. We explain that the new problem is isomorphic to two other Zeno-like predicaments: a problem described by Alper and Bridger in (...) 1998 and a modified version of the problem that Benardete introduced in 1964. Finally, we present a solution to the three isomorphic problems. (shrink)

In 1929 Tarski showed how to construct points in a region-based first-order logic for space representation. The resulting system, called the geometry of solids, is a cornerstone for region-based geometry and for the comparison of point-based and region-based geometries. We expand this study of the construction of points in region-based systems using different primitives, namely hyper-cubes and regular simplexes, and show that these primitives lead to equivalent systems in dimension n ≥ 2. The result is achieved by adopting a single (...) set of definitions that works for both these classes of figures. The analysis of our logics shows that Tarski’s choice to take sphere as the geometrical primitive might be intuitively justified but is not optimal from a technical viewpoint. (shrink)

Cube Living 221A is the most recent iteration of the Cube Living project, initiated in 2008. It appropriates the language, media and social practices of real estate development campaigns to engage in speculation about spatial ontologies, examining how social, legal and financial conventions determine the creation of space in our cities.This paper describes the staging and production process by which Cube Living 221A performs the creation of a spatial commodity. Drawing on the concepts presented in Žižek’s 2009 (...) talk “Architectural Parallax: Spandrels and Other Phenomena of Class Struggle”, it goes on to speculate that urban real estate development results in an architectural parallax: real estate property must function simultaneously as a financial asset and also as a residence. Similarly, the property owner must play simultaneous but irreconcilable roles as both investor and citizen. The Cube object can be regarded as a spandrel at the hinge of this parallax. (shrink)

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.

"Hungarian Cubes" proposes an aesthetical typology of the ornamentation of cubic houses from the 1960s 70s in Hungary. The book is based on the artistic project Magyar Kocka Hungarian Cube, which German-Hungarian artist Katharina Roters is pursuing since 2005. The origins of the Hungarian Cube, a standardized type of residential house, date back to the 1920s, when the cube as prototype of a radically functional design first appeared in plans for single-family homes in Budapest s suburbs and (...) also in social housing projects. During Hungary s communist era after WW II, many villages were rebuilt on uniform schemes of single-family homes and the "Magyar Kocka "or "Kadar Kocka, " as they were also named after Hungary s communist president Janos Kadar became ubiquitous. A unique characteristic of this housing type is the ornamental decoration of its facades. The facade thereby became an opportunity of both individual and collective expression within uniformity. The ornament is not merely an aesthetic sign. It rather creates meaningful identity and distinguishes the appearance of entire dwellings across the country. Often this individualized ornament can also be read as an act of subversion against the pressure of conformity in the socialist system. Katharina Roters has been investigating and documenting this previously neglected ornamental phenomenon since 2005 from an artistic point of view. The houses are shown in her images cleaned of all surplus information, fences and railings, antennas, road signs, electric power lines. Only by this deletion of additions to each house the project can reach beyond a merely archival nature and the photograph becomes a document of aesthetic typology. The book combines the serial composition of Roters s images with essays on various aspects of this architectural phenomenon. ". (shrink)

In Russell''s Ramified Theory of Types RTT, two hierarchical concepts dominate:orders and types. The use of orders has as a consequencethat the logic part of RTT is predicative.The concept of order however, is almost deadsince Ramsey eliminated it from RTT. This is whywe find Church''s simple theory of types (which uses the type concept without the order one) at the bottom of the Barendregt Cube rather than RTT. Despite the disappearance of orders which have a strong correlation with predicativity, (...) predicative logic still plays an influential role in Computer Science.An important example is the proof checker Nuprl, which is basedon Martin-Löf''s Type Theory which uses type universes. Those type universes,and also degrees of expressions in AUTOMATH, are closely related toorders. In this paper, we show that orders have not disappeared from modern logic and computer science, rather, orders play a crucial role in understanding the hierarchy of modern systems. In order to achieve our goal, we concentrate on a subsystem of Nuprl.The novelty of our paper lies in: (1) a modest revival of Russell's orders, (2) the placing of the historical system RTT underlying the famous Principia Mathematica in a context with a modern system of computer mathematics (Nuprl) and modern type theories (Martin-Löf''s type theory and PTSs), and (3) the presentation of acomplex type system (Nuprl) as a simple and compact PTS. (shrink)

This paper presents the topological arrangements in four geometrical figures of modal propositions and their derivative relations by means of Peirce's gamma graphs and their rules of transformation. The idea of arraying the gamma graphs in a geometric and symmetrical order comes from Peirce himself who in a manuscript drew two cubes in which he presented the derivative relations of some gamma graphs. Therefore, Peirce's insights of a topological order of gamma graphs are extended here backwards from the cube (...) to the line and the square; and then forwards from the cube to the four-dimensional polyhedron. (shrink)

The study of cases of illusory or unstable perception of some visual stimuli allows exploration of the psychology of perception of the surrounding world. The wired construction known as “Necker cube” is one such stimulus: it can be perceived as a cube whose front face is seen higher than the back face or vice versa. The switch can occur intentionally or spontaneously. The investigations were focused on switching parameters, relation of the switching to eye position, pre-history, and environment. (...) Here we define that the kernel of the problem is recognizing the 2D drawing as a 3D Necker cube. To this end, we have expanded Gestalt's psychology methods that allow us to recognize 2D figures in drawings for recognizing 3D figure in a flat drawing (including the Necker cube). The presented algorithm for recognizing the cube based on the imitation principle allowed the development of the model of switching between two possible perceptions of the Necker cube. The paper shows that the predictions are in conformity with previously available experimental data. The results confirm the imitation principle of perception, and suggest expanding our research on perception to a wider class of 3D figures, opening a window into the internal processes of perception. (shrink)

RésuméLa sémiotique a inventé ou utilisé plusieurs modèles logiques pour représenter la structure élémentaire de la signification. Le carré sémiotique est sans doute l’un des plus célèbres de ces modèles. Il faut se demander, devant l’importance des phénomènes triadiques, si les modèles dyadiques sont (toujours) adaptés à leur description ou s’il ne faudrait pas se tourner (aussi) vers des modèles triadiques. Or, les modèles triadiques de la structure élémentaire de la signification nous apparaissent bien moins nombreux. À notre connaissance, seule (...) la sémiotique de Peirce et le templum de Boudon occupent cet espace autrement laissé vacant. Nous voulons ici à la fois présenter et exemplifier le templum et le compléter, en nous inspirant du carré sémiotique, pour le faire évoluer vers un « prisme sémiotique ». Nous proposerons également d’autres modèles logiques, comme le pentalemme et le cube sémiotiques. Au passage, nous étudierons plusieurs questions et problèmes – dont la décidabilité – entourant les modèles logiques. Nous ferons quelques applications sommaires de certains modèles, sur le temps, l’espace et la transcendance principalement. (shrink)

This paper examines an annotation in Newton’s hand found by H. W. Turnbull in David Gregory’s papers in the Library of the Royal Society. It will be shown that Gregory asked Newton to explain to him how the trajectories of a body accelerated by an inverse-cube force are determined in a corollary in the Principia: an important topic for gravitation theory, since tidal forces are inverse cube. This annotation opens a window on the more hidden mathematical methods which (...) Newton deployed in his magnum opus. The received view according to which the Principia are written in a geometric style with no help from calculus techniques must be revised. (shrink)

"Out of the box! ". Qui n'a pas entendu cette injonction destinée à ceux que l'on somme d'être créatif? Si nos sens délimitent sans peine des murs et des portes, de quoi se compose la boîte de laquelle on nous enjoint de sortir? Qui la construit et à quoi sert-elle? Nous avons pris au sérieux ce banal mot d'ordre managérial et avons bâti une théorie sur l'innovation. Ce n'est pas une "boîtes" que nous avons identifiée, mais trois "cubes" qui formatent (...) nos identités, nos usages et nos objets. Sujet, verbe, objet tout marché fonde en même temps un récit et s'appuie sur la même grammaire que nous avons apprise sur les bancs d'école. Les neufs dimensions réunies par les trois cubes sont des productions historiques. Elles sont le produit d'un nombre impressionnant d'acteurs : Etats, organismes administratifs, partis politiques, arts, aménagement du territoire, syndicats patronaux ou ouvriers, associations de consommateurs, médias, médecine, droit, formation, police, langue, leaders d'opinion, structures faîtières, etc. Le lecteur découvrira que l'innovation exprime un paradoxe : l'innovation est nécessaire pour les entreprises ; elle aussi est un danger pour ces dernières ; elle doit enfin être domestiquée et "cubée" pour organiser une concurrence. Si l'innovation était débridée, aucun marché n'y résisterait... Trois cubes comme paradoxes de la créativité et de la liberté ; il faut bien des murs, savoir de quoi ils sont faits et où ils sont érigés pour s'évader de temps en temps. (shrink)