Online research in philosophy

Hoare's Iteration Rule is a principle of reasoning that is used to derive correctness assertions about the effects of implementing a while-command. We show that the propositional modal logic of this type of command is axiomatised by Hoare's rule in conjunction with two additional axioms. The proof also establishes decidability of the logic. The paper concludes with a discussion of the relationship between the logic of while and Segerberg's axiomatisation of propositional dynamic logic.

The new concept of lambda calculi with monotone inductive types is introduced byhelp of motivations drawn from Tarski's fixed-point theorem (in preorder theory) andinitial algebras and initial recursive algebras from category theory. They are intendedto serve as formalisms for studying iteration and primitive recursion ongeneral inductively given structures. Special accent is put on the behaviour ofthe rewrite rules motivated by the categorical approach, most notably on thequestion of strong normalization (i.e., the impossibility of an infinitesequence of successive rewrite steps). It is shown that this key propertyhinges on the concrete formulation. The canonical system of monotone inductivetypes, where monotonicity is expressed by a monotonicity witness beinga term expressing monotonicity through its type, enjoys strong normalizationshown by an embedding into the traditional system of non-interleavingpositive inductive types which, however, has to be enriched by the parametricpolymorphism of system F. Restrictions to iteration on monotone inductive typesalready embed into system F alone, hence clearly displaying the differencebetween iteration and primitive recursion with respect to algorithms despitethe fact that, classically, recursion is only a concept derived from iteration.

Recent cognitive accounts of the imagination propose that imagining and believing are in the same “code”. According to the single code hypothesis, cognitive mechanisms that can take input from both imagining and from believing will process imagination-based inputs (“pretense representations”) and isomorphic beliefs in much the same way. In this paper, I argue that the single code hypothesis provides a unified and independently motivated explanation for a wide range of puzzles surrounding fiction.

This volume brings together specially written essays by leading researchers on the propositional imagination. This is the mental capacity we exploit when we imagine that Holmes has a bad habit or that there are zombies. It plays an essential role in philosophical theorizing, engaging with fiction, and indeed in everyday life. The Architecture of the Imagination capitalizes on recent attempts to give a cognitive account of this capacity, extending the theoretical picture and exploring the philosophical implications.

We prove that PTIME generalized quantifiers are closed under Boolean operations, iteration, cumulation and resumption.

Any finite support iteration of posets with precalibre ℵ 1 which has the length of cofinality greater than ω 1 yields a model for the dual Borel conjecture in which the real line is covered by ℵ 1 strong measure zero sets.

We show that every sufficiently iterable countable mouse has a unique iteration strategy whose associated iteration maps are lexicographically minimal. This enables us to extend the results of [3] on the good behavior of the standard parameter from tame mice to arbitrary mice.

It is shown, assuming the existence of a Woodin cardinal δ, that every tree ordering on some limit ordinal $\lambda < \delta$ with a cofinal branch is the tree ordering of some iteration tree on V.