In this multiple case study, the authors compare the instruction of two high school civics teachers during the 2012 Presidential Election. Both were highly-qualified practitioners who worked in schools with one-to-one laptop initiatives, creating an environment in which access to digital technology ceased to be an issue. Although both teachers regularly used technology in their classrooms, the authors describe stark differences in the complexity and authenticity of their instruction, which the authors attribute to the teachers’ technological pedagogical content knowledge (TPCK). (...) The authors conclude by discussing implications for better understanding TPCK within civics instruction, specifically in classrooms with one-to-one laptop access. (shrink)

Under the assumption that all "rules" are recursive (ECT) the statement $\operatorname{Cont}(N^N,N)$ that all functions from N N to N are continuous becomes equivalent to a statement KLS in the language of arithmetic about "effective operations". Our main result is that KLS is underivable in intuitionistic Zermelo-Fraenkel set theory + ECT. Similar results apply for functions from R to R and from 2 N to N. Such results were known for weaker theories, e.g. HA and HAS. We extend not only (...) the theorem but the method, fp-realizability, to intuitionistic ZF. (shrink)

One of the more striking, surprising, and optimism-inducing features of the contemporary international system has been the decline of interstate war. The key question for students of international relations and comparative politics is how this happy state of affairs came about. In short, was this a universal phenomenon or did some regions play a more important and pioneering role in bringing about peaceful change? As part of the roundtable “International Institutions and Peaceful Change,” this essay suggests that Western Europe generally (...) and the European Union in particular played pivotal roles in transforming the international system and the behavior of policymakers. This helped to create the material and ideational conditions in which other parts of the world could replicate this experience, making war less likely and peaceful change more feasible. This argument is developed by comparing the experiences of the EU and the Association of Southeast Asian Nations and their respective institutional offshoots. The essay uses this comparative historical analysis to assess both regions’ capacity to cope with new security challenges, particularly the declining confidence in institutionalized cooperation. (shrink)

Euclidean geometry, as presented by Euclid, consists of straightedge-and-compass constructions and rigorous reasoning about the results of those constructions. We show that Euclidean geometry can be developed using only intuitionistic logic. This involves finding “uniform” constructions where normally a case distinction is used. For example, in finding a perpendicular to line L through point p, one usually uses two different constructions, “erecting” a perpendicular when p is on L, and “dropping” a perpendicular when p is not on L, but in (...) constructive geometry, it must be done without a case distinction. Classically, the models of Euclidean geometry are planes over Euclidean fields. We prove a similar theorem for constructive Euclidean geometry, by showing how to define addition and multiplication without a case distinction about the sign of the arguments. With intuitionistic logic, there are two possible definitions of Euclidean fields, which turn out to correspond to different versions of the parallel postulate.We consider three versions of Euclid’s parallel postulate. The two most important are Euclid’s own formulation in his Postulate 5, which says that under certain conditions two lines meet, and Playfair’s axiom, which says there cannot be two distinct parallels to line L through the same point p. These differ in that Euclid 5 makes an existence assertion, while Playfair’s axiom does not. The third variant, which we call the strong parallel postulate, isolates the existence assertion from the geometry: it amounts to Playfair’s axiom plus the principle that two distinct lines that are not parallel do intersect. The first main result of this paper is that Euclid 5 suffices to define coordinates, addition, multiplication, and square roots geometrically.We completely settle the questions about implications between the three versions of the parallel postulate. The strong parallel postulate easily implies Euclid 5, and Euclid 5 also implies the strong parallel postulate, as a corollary of coordinatization and definability of arithmetic. We show that Playfair does not imply Euclid 5, and we also give some other independence results. Our independence proofs are given without discussing the exact choice of the other axioms of geometry; all we need is that one can interpret the geometric axioms in Euclidean field theory. The independence proofs use Kripke models of Euclidean field theories based on carefully constructed rings of real-valued functions. “Field elements” in these models are real-valued functions. (shrink)

Brouwer's positions about existence (reality) and truth are examined in the light of ninety years of scientific progress. Relevant results in proof theory, recursion theory, set theory, relativity, and quantum mechanics are used to cast light on the following philosophical questions: What is real, and how do we know it? What does it mean to say a thing exists? Can things exist that we can't know about? Can things exist that we don't know how to find? What does it mean (...) to say something is true? How can we know whether something is true? Can things be true that we can't ever know to be true? (shrink)

The pain -- I thought church would be different -- The pain goes so deep -- Where does all this pain come from? -- Nobody sees me -- I feel beat up in church -- I live in shame all the time -- I feel used -- I can't forgive -- The hope -- Will I ever get past the pain? -- Why do I feel so unsafe in church? -- I can't keep up with all the rules -- What's (...) wrong with these people? -- I just need to be perfect -- The church doesn't seem to care -- How do I find a good church? -- Hope beyond the pain -- Demonic lies and doctrines -- Learning to live in the kingdom of light. (shrink)

Western Australia has recently assumed an unaccustomed centrality in the minds of Australian policymakers. The recent resource boom briefly propelled WA to the forefront of national economic affairs. While this proved a relatively short-lived prominence, the emergence of WA at the centre of a putative ‘Indo-Pacific’ region promises to give it a more enduring strategic significance. This paper details how geopolitical and geoeconomic forces have shaped WA’s developmental history, and why they are likely to do so in the future as (...) well. (shrink)

This article answers two questions (posed in the literature), each concerning the guaranteed existence of proofs free of double negation. A proof is free of double negation if none of its deduced steps contains a term of the formn(n(t)) for some term t, where n denotes negation. The first question asks for conditions on the hypotheses that, if satisfied, guarantee the existence of a double-negation-free proof when the conclusion is free of double negation. The second question asks about the existence (...) of an axiom system for classical propositional calculus whose use, for theorems with a conclusion free of double negation, guarantees the existence of a double-negation-free proof. After giving conditions that answer the first question, we answer the second question by focusing on the Lukasiewicz three-axiom system. We then extend our studies to infinite-valued sentential calculus and to intuitionistic logic and generalize the notion of being double-negation free. The double-negation proofs of interest rely exclusively on the inference rule condensed detachment, a rule that combines modus ponens with an appropriately general rule of substitution. The automated reasoning program Otter played an indispensable role in this study. (shrink)

We use Herbrand’s theorem to give a new proof that Euclid’s parallel axiom is not derivable from the other axioms of first-order Euclidean geometry. Previous proofs involve constructing models of non-Euclidean geometry. This proof uses a very old and basic theorem of logic together with some simple properties of ruler-and-compass constructions to give a short, simple, and intuitively appealing proof.

Legal structures may form barriers to, or enablers of, adoption of precision agriculture management with small autonomous agricultural robots. This article develops a conceptual regulatory framework for small autonomous agricultural robots, from a practical, self-contained engineering guide perspective, sufficient to get working research and commercial agricultural roboticists quickly and easily up and running within the law. The article examines the liability framework, or rather lack of it, for agricultural robotics in EU, and their transpositions to UK law, as a case (...) study illustrating general international legal concepts and issues. It examines how the law may provide mitigating effects on the liability regime, and how contracts can be developed between agents within it to enable smooth operation. It covers other legal aspects of operation such as the use of shared communications resources and privacy in the reuse of robot-collected data. Where there are some grey areas in current law, it argues that new proposals could be developed to reform these to promote further innovation and investment in agricultural robots. (shrink)

A long-standing question in cognitive science is how high-level knowledge is integrated with sensory input. For example, listeners can leverage lexical knowledge to interpret an ambiguous speech sound, but do such effects reflect direct top-down influences on perception or merely postperceptual biases? A critical test case in the domain of spoken word recognition is lexically mediated compensation for coarticulation (LCfC). Previous LCfC studies have shown that a lexically restored context phoneme (e.g., /s/ in Christma#) can alter the perceived place of (...) articulation of a subsequent target phoneme (e.g., the initial phoneme of a stimulus from a tapes-capes continuum), consistent with the influence of an unambiguous context phoneme in the same position. Because this phoneme-to-phoneme compensation for coarticulation is considered sublexical, scientists agree that evidence for LCfC would constitute strong support for top–down interaction. However, results from previous LCfC studies have been inconsistent, and positive effects have often been small. Here, we conducted extensive piloting of stimuli prior to testing for LCfC. Specifically, we ensured that context items elicited robust phoneme restoration (e.g., that the final phoneme of Christma# was reliably identified as /s/) and that unambiguous context-final segments (e.g., a clear /s/ at the end of Christmas) drove reliable compensation for coarticulation for a subsequent target phoneme. We observed robust LCfC in a well-powered, preregistered experiment with these pretested items (N = 40) as well as in a direct replication study (N = 40). These results provide strong evidence in favor of computational models of spoken word recognition that include top–down feedback. (shrink)

Luthra, Peraza-Santiago, Beeson, Saltzman, Crinnion, and Magnuson (2021) present data from the lexically mediated compensation for coarticulation paradigm that they claim provides conclusive evidence in favor of top-down processing in speech perception. We argue here that this evidence does not support that conclusion. The findings are open to alternative explanations, and we give data in support of one of them (that there is an acoustic confound in the materials). Lexically mediated compensation for coarticulation thus remains elusive, while prior data (...) from the paradigm instead challenge the idea that there is top-down processing in online speech recognition. (shrink)

Constructive set theory a' la Myhill-Aczel has been extended in (Cantini and Crosilla 2008, Cantini and Crosilla 2010) to incorporate a notion of (partial, non--extensional) operation. Constructive operational set theory is a constructive and predicative analogue of Beeson's Inuitionistic set theory with rules and of Feferman's Operational set theory (Beeson 1988, Feferman 2006, Jaeger 2007, Jaeger 2009, Jaeger 1009b). This paper is concerned with an extension of constructive operational set theory (Cantini and Crosilla 2010) by a uniform operation (...) of Transitive Closure, \tau. Given a set a, \tau produces its transitive closure \tau a. We show that the theory ESTE of (Cantini and Crosilla 2010) augmented by \tau is still conservative over Peano Arithmetic. (shrink)

Qu'est-ce que l'ironie? Quelles en sont les formes? Quels en sont les pièges aussi? Autant de délicates questions auxquelles l'auteur répond, non sans ironie lui-même, avec l'aide d'une infinité d'exemples qui montrent son immense culture, musicale aussi bien que philosophique. Sommairement, qu'est-ce que l'ironie, sinon la conscience, mais une bonne conscience joyeuse, ce en quoi elle se distingue de l'hypocrisie? Pas d'humour sans amour, ni d'ironie sans joie. L'ironie, en somme, sauve ce qui peut être sauvé. Elle est mortelle aux (...) illusions ; partout elle tisse les toiles d'araignée où se prendront les pédants, les vaniteux et les grotesques. " Ironie, vraie liberté! ", s'écrie Proudhon au fond de sa cellule de Sainte-Pélagie. L'ironie remet tout en question ; par ses interrogations indiscrètes elle ruine toute définition, dérange à tout moment la pontifiante pédanterie prête à s'installer dans une déduction satisfaite. Grâce à l'ironie, la pensée respire plus légèrement quand elle s'est reconnue, dansante et grinçante, dans le miroir de la réflexion. (shrink)

Qu'est-ce que l'ironie? Quelles en sont les formes? Quels en sont les pièges aussi? Autant de délicates questions auxquelles l'auteur répond, non sans ironie lui-même, avec l'aide d'une infinité d'exemples qui montrent son immense culture, musicale aussi bien que philosophique. Sommairement, qu'est-ce que l'ironie, sinon la conscience, mais une bonne conscience joyeuse, ce en quoi elle se distingue de l'hypocrisie? Pas d'humour sans amour, ni d'ironie sans joie. L'ironie, en somme, sauve ce qui peut être sauvé. Elle est mortelle aux (...) illusions ; partout elle tisse les toiles d'araignée où se prendront les pédants, les vaniteux et les grotesques. " Ironie, vraie liberté! ", s'écrie Proudhon au fond de sa cellule de Sainte-Pélagie. L'ironie remet tout en question ; par ses interrogations indiscrètes elle ruine toute définition, dérange à tout moment la pontifiante pédanterie prête à s'installer dans une déduction satisfaite. Grâce à l'ironie, la pensée respire plus légèrement quand elle s'est reconnue, dansante et grinçante, dans le miroir de la réflexion. (shrink)

Consistency with the formal Church’s thesis, for short CT, and the axiom of choice, for short AC, was one of the requirements asked to be satisfied by the intensional level of a two-level foundation for constructive mathematics as proposed by Maietti and Sambin From sets and types to topology and analysis: practicable foundations for constructive mathematics, Oxford University Press, Oxford, 2005). Here we show that this is the case for the intensional level of the two-level Minimalist Foundation, for short MF, (...) completed in 2009 by the second author. The intensional level of MF consists of an intensional type theory à la Martin-Löf, called mTT. The consistency of mTT with CT and AC is obtained by showing the consistency with the formal Church’s thesis of a fragment of intensional Martin-Löf’s type theory, called \, where mTT can be easily interpreted. Then to show the consistency of \ with CT we interpret it within Feferman’s predicative theory of non-iterative fixpoints \ by extending the well known Kleene’s realizability semantics of intuitionistic arithmetics so that CT is trivially validated. More in detail the fragment \ we interpret consists of first order intensional Martin-Löf’s type theory with one universe and with explicit substitution rules in place of usual equality rules preserving type constructors -rule which is not valid in our realizability semantics). A key difficulty encountered in our interpretation was to use the right interpretation of lambda abstraction in the applicative structure of natural numbers in order to model all the equality rules of \ correctly. In particular the universe of \ is modelled by means of \-fixpoints following a technique due first to Aczel and used by Feferman and Beeson. (shrink)

Recluses, ermites ou engagées dans le monde, les saintes travesties sont nombreuses jusqu’à la fin du Moyen Âge. Ayant valeur de transgression et/ou d’initiation, le travestissement permet à Thècle, Pélagie, Marguerite, Marine ou Eugénie de redéfinir non seulement la notion de virginité mais d’affirmer une sainteté au nom d’une intégrité qui dérange les catégories sexuées et renverse les notions de genre. D’autres, comme Galla, Paula ou Wilgeforte, délivrent de l’antagonisme des sexes. Et toutes, jusqu’à Jeanne d’Arc, bouleversent la destinée des (...) femmes en perturbant l’ordre temporel des hommes. Ainsi apparaît la conquête d’un nouveau corps à travers la mission chrétienne et l’expérience mystique, qui déjoue la nature de femme et les vertus masculines. (shrink)

Recluses, ermites ou engagées dans le monde, les saintes travesties sont nombreuses jusqu’à la fin du Moyen Âge. Ayant valeur de transgression et/ou d’initiation, le travestissement permet à Thècle, Pélagie, Marguerite, Marine ou Eugénie de redéfinir non seulement la notion de virginité mais d’affirmer une sainteté au nom d’une intégrité qui dérange les catégories sexuées et renverse les notions de genre. D’autres, comme Galla, Paula ou Wilgeforte, délivrent de l’antagonisme des sexes. Et toutes, jusqu’à Jeanne d’Arc, bouleversent la destinée des (...) femmes en perturbant l’ordre temporel des hommes. Ainsi apparaît la conquête d’un nouveau corps à travers la mission chrétienne et l’expérience mystique, qui déjoue la nature de femme et les vertus masculines. (shrink)

Goodman’s theorem states that HAω+AC+RDC is conservative over HA. The same result applies to the extensional case, that is, E-HAω+AC+RDC is also conservative over HA. This is due to Beeson. In this article, we modified the Goodman realizability and provide a new proof of the extensional case.

A free logic is one in which a singular term can fail to refer to an existent object, for example, `Vulcan' or `5/0'. This essay demonstrates the fruitfulness of a version of this non-classical logic of terms (negative free logic) by showing (1) how it can be used not only to repair a looming inconsistency in Quine's theory of predication, the most influential semantical theory in contemporary philosophical logic, but also (2) how Beeson, Farmer and Feferman, among others, use (...) it to provide a natural foundation for partial functions in programming languages. Vis à vis (2), the question is raised whether the Beeson-Farmer-Feferman approach is adequate to the treatment of partial functions in all programming languages. Gumb and the author say No, and suggest a way of handling the refractory cases by means of positive free logic. Finally, Antonelli's solution of a problem associated with the Gumb-Lambert proposal is mentioned. (shrink)

This paper presents a novel proof of the conservativity of the intuitionistic theory of strictly positive fixpoints, $$\widehat{{\textrm{ID}}}{}_{1}^{{\textrm{i}}}{}$$ ID ^ 1 i, over Heyting arithmetic ($${\textrm{HA}}$$ HA ), originally proved in full generality by Arai (Ann Pure Appl Log 162:807–815, 2011. https://doi.org/10.1016/j.apal.2011.03.002). The proof embeds $$\widehat{{\textrm{ID}}}{}_{1}^{{\textrm{i}}}{}$$ ID ^ 1 i into the corresponding theory over Beeson’s logic of partial terms and then uses two consecutive interpretations, a realizability interpretation of this theory into the subtheory generated by almost negative fixpoints, (...) and a direct interpretation into Heyting arithmetic with partial terms using a hierarchy of satisfaction predicates for almost negative formulae. It concludes by applying van den Berg and van Slooten’s result (Indag Math 29:260–275, 2018. https://doi.org/10.1016/j.indag.2017.07.009) that Heyting arithmetic with partial terms plus the schema of self realizability for arithmetic formulae is conservative over $${\textrm{HA}}$$ HA. (shrink)