The paper exposes the relevance of permuting conversions (in natural-deduction systems) to the role of such systems in the theory of meaning known as proof-theoretic semantics, by relating permuting conversion to harmony, hitherto related to normalisation only. This is achieved by showing the connection of permuting conversion to the general notion of canonicity, once applied to arbitrary derivations from open assumption. In the course of exposing the relationship of permuting conversions to harmony, a general definition of the former (...) is proposed, generalising the specific cases of disjunction and existential quantifiers considered in the literature. (shrink)

This paper gives new confluence proofs for several lambda calculi with permutation-like reduction, including lambda calculi corresponding to intuitionistic and classical natural deduction with disjunction and permutative conversions, and a lambda calculus with explicit substitutions. For lambda calculi with permutative conversion, naïve parallel reduction technique does not work, and traditional notion of residuals is required as Ando pointed out. This paper shows that the difficulties can be avoided by extending the technique proposed by Dehornoy and van Oostrom, (...) called the Z theorem: existence of a mapping on terms with the Z property concludes the confluence. Since it is still hard to directly define a mapping with the Z property for the lambda calculi with permutative conversions, this paper extends the Z theorem to compositional functions, called compositional Z, and shows that we can adopt it to the calculi. (shrink)

Inductive characterizations of the sets of terms, the subset of strongly normalizing terms and normal forms are studied in order to reprove weak and strong normalization for the simply-typed λ-calculus and for an extension by sum types with permutative conversions. The analogous treatment of a new system with generalized applications inspired by generalized elimination rules in natural deduction, advocated by von Plato, shows the flexibility of the approach which does not use the strong computability/candidate style à la Tait and (...) Girard. It is also shown that the extension of the system with permutative conversions by η-rules is still strongly normalizing, and likewise for an extension of the system of generalized applications by a rule of ``immediate simplification''. By introducing an infinitely branching inductive rule the method even extends to Gödel's T. (shrink)

A simple and complete proof of strong normalization for first- and second-order intuitionistic natural deduction including disjunction, first-order existence and permutative conversions is given. The paper follows the Tait–Girard approach via computability predicates and saturated sets. Strong normalization is first established for a set of conversions of a new kind, then deduced for the standard conversions. Difficulties arising for disjunction are resolved using a new logic where disjunction is restricted to atomic formulas.

The notions of permutable and weak-permutable convergence of a series|$\sum _{n=1}^{\infty }a_{n}$|of real numbers are introduced. Classically, these two notions are equivalent, and, by Riemann’s two main theorems on the convergence of series, a convergent series is permutably convergent if and only if it is absolutely convergent. Working within Bishop-style constructive mathematics, we prove that Ishihara’s principle BD-|$\mathbb {N}$|implies that every permutably convergent series is absolutely convergent. Since there are models of constructive mathematics in which the Riemann permutation theorem for (...) series holds but BD-|$\mathbb{N}$|does not, the best we can hope for as a partial converse to our first theorem is that the absolute convergence of series with a permutability property classically equivalent to that of Riemann implies BD-|$\mathbb {N}$|. We show that this is the case when the property is weak-permutable convergence. (shrink)

In response to the dozen essays published here, which relate my 1964 paper on “The Nature of Belief Systems in the Mass Publics” to normative requirements of democratic theory, I note, inter alia, a major misinterpretation of my old argument, as well as needed revisions of that argument in the light of intervening data. Then I address the degree to which there may be some long‐term secular change in the parameters that I originally laid out. In the final section, I (...) provide a case study of public understanding of factual trends in federal tax policy in recent decades which seems commendably veridical on average. The preferences of the public thereon add up to a remarkably clear popular mandate. But this mandate seems to disappear rather magically in the voting booth, probably due to a combination of limited contextual information on the public side, and considerable skill on the elite side in manipulating apparent political realities. (shrink)

The structure of derivations in natural deduction is analyzed through isomorphism with a suitable sequent calculus, with twelve hidden convertibilities revealed in usual natural deduction. A general formulation of conjunction and implication elimination rules is given, analogous to disjunction elimination. Normalization through permutative conversions now applies in all cases. Derivations in normal form have all major premisses of elimination rules as assumptions. Conversion in any order terminates.Through the condition that in a cut-free derivation of the sequent Γ⇒C, no (...) inactive weakening or contraction formulas remain in Γ, a correspondence with the formal derivability relation of natural deduction is obtained: All formulas of Γ become open assumptions in natural deduction, through an inductively defined translation. Weakenings are interpreted as vacuous discharges, and contractions as multiple discharges. In the other direction, non-normal derivations translate into derivations with cuts having the cut formula principal either in both premisses or in the right premiss only. (shrink)

Developing a suggestion by Russell, Prawitz showed how the usual natural deduction inference rules for disjunction, conjunction and absurdity can be derived using those for implication and the second order quantifier in propositional intuitionistic second order logic NI\. It is however well known that the translation does not preserve the relations of identity among derivations induced by the permutative conversions and immediate expansions for the definable connectives, at least when the equational theory of NI\ is assumed to consist only (...) of \- and \-equations. On the basis of the categorial interpretation of NI\, we introduce a new class of equations expressing what in categorial terms is a naturality condition satisfied by the transformations interpreting NI\-derivations. We show that the Russell–Prawitz translation does preserve identity of proof with respect to the enriched system by highlighting the fact that naturality corresponds to a generalized permutation principle. Finally we sketch how these results could be used to investigate the properties of connectives definable in the framework of higher-level rules. (shrink)

A sequent calculus is given in which the management of weakening and contraction is organized as in natural deduction. The latter has no explicit weakening or contraction, but vacuous and multiple discharges in rules that discharge assumptions. A comparison to natural deduction is given through translation of derivations between the two systems. It is proved that if a cut formula is never principal in a derivation leading to the right premiss of cut, it is a subformula of the conclusion. Therefore (...) it is sufficient to eliminate those cuts that correspond to detour and permutation conversions in natural deduction. (shrink)

The paper deals with two versions of the fragment with unit, tensor, linear implication and storage operator of intuitionistic linear logic. The first version, ILL, appears in a paper by Benton, Bierman, Hyland and de Paiva; the second one, ILL+, is described in this paper. ILL has a contraction rule and an introduction rule !I for the exponential; in ILL+, instead of a contraction rule, multiple occurrences of labels for assumptions are permitted under certain conditions; moreover, there is a different (...) introduction rule for the exponential, !I+, which is closer in spirit to the necessitation rule for the normalizable version of S4 discussed by Prawitz in his monograph “Natural Deduction”.It is relatively easy to adapt Prawitz's treatment of natural deduction for intuitionistic logic to ILL+; in particular one can formulate a notion of strong validity permitting a proof of strong normalization.The conversion rules for ILL explicitly mentioned in the paper by Benton et al. do not suffice for normal forms with subformula property, but we can show that this can be remedied by addition of a special permutation conversion plus some “satellite” permutation conversions.Some discussion of the categorical models which might correspond to ILL+ is given. (shrink)

Termination for classical natural deduction is difficult in the presence of commuting/permutative conversions for disjunction. An approach based on reducibility candidates is presented that uses non-strictly positive inductive definitions.It covers second-order universal quantification and also the extension of the logic with fixed points of non-strictly positive operators, which appears to be a new result.Finally, the relation to Parigot’s strictly positive inductive definition of his set of reducibility candidates and to his notion of generalized reducibility candidates is explained.

This paper proves the strong normalization of classical natural deduction with disjunction and permutative conversions, by using CPS-translation and augmentations. Using them, this paper also proves the strong normalization of classical natural deduction with general elimination rules for implication and conjunction, and their permutative conversions. This paper also proves that natural deduction can be embedded into natural deduction with general elimination rules, strictly preserving proof normalization.

Building on previous work by Mints, Buchholz and Schwichtenberg, a simplified version of continuous normalization for the untyped λ-calculus and Gödel’s is presented and analysed in the coalgebraic framework of non-wellfounded terms with so-called repetition constructors.The primitive recursive normalization function is uniformly continuous w.r.t. the natural metric on non-wellfounded terms. Furthermore, the number of necessary repetition constructors is locally related to the number of reduction steps needed to reach the normal form and its size.It is also shown how continuous normal (...) forms relate to derivations of strong normalizability in the typed λ-calculus and how this leads to new bounds for the sum of the height of the reduction tree and the size of the normal form.Finally, the methods are extended to an infinitary λ-calculus with ω-rule and permutative conversions and this is used to derive a strong form of normalization for an iterative version of Gödel’s system , leading to a value table semantics for number-theoretic functions. (shrink)

A sequent calculus is given in which the management of weakening and contraction is organized as in natural deduction. The latter has no explicit weakening or contraction, but vacuous and multiple discharges in rules that discharge assumptions. A comparison to natural deduction is given through translation of derivations between the two systems. It is proved that if a cut formula is never principal in a derivation leading to the right premiss of cut, it is a subformula of the conclusion. Therefore (...) it is sufficient to eliminate those cuts that correspond to detour and permutation conversions in natural deduction. (shrink)

The following conversation examines the role of the university in our present moment and examines the necessity of anti-colonial praxis in the academy. The dialogue takes as its starting point the long history of white, heteropatriarchal capitalist supremacy that has oriented the institutional production of knowledge and considers its present permutations in such practices as diversity initiatives in teaching and hiring. The discussants in turn reflect on their own approaches and strategies for enacting liberatory pedagogy in light of the contingent, (...) historical, and material limitations of higher education today. (shrink)

This essay in the comparative metaphysic of nothingness begins by pondering why Leibniz thought of the converse question as the preeminent one. In Eastern philosophical thought, like the numeral ‘zero’ that Indian mathematicians first discovered, nothingness as non-being looms large and serves as the first quiver on the imponderables they seem to have encountered. The concept of non-being and its permutations of nothing, negation, nullity, etc., receive more sophisticated treatment in the works of grammarians, ritual hermeneuticians, logicians, and their dialectical (...) adversaries variously across Jaina and Buddhist schools. The present analysis follows the function of negation/the negative copula, nãn, and dialetheia in grammar and logic, then moves onto ontologies of non-existence and extinction and further suggestive tropes that tend to arrest rather than affirm the inexorable being-there of something., namely, ‘Thinking Negation in Early Hinduism and Classical Indian Philosophy’ ; and ‘Negation, Non-existents, and a Distinctive Pramāṇa in the Nyāya-Mīmāṃsā’ ).After a discussion of interests in being, non-being and nothingness in contemporary metaphysics, the article examines Heidegger’s extensive treatment of nothingness in his 1929 inaugural Freiburg lecture, ‘Was ist Metaphysik?’, published later as ‘What is Metaphysics?’ The essay however distances itself from any pretensions toward a doctrine of ‘Metaphysical’ at ‘Nihilism’. (shrink)

Ramseyan humility is the thesis that we cannot know which properties realize the roles specified by the laws of completed physics. Lewis seems to offer a sceptical argument for this conclusion. Humean fundamental properties can be permuted as to their causal roles and distribution throughout spacetime, yielding alternative possible worlds with the same fundamental structure as actuality, but at which the totality of available evidence is the same. On the assumption that empirical knowledge requires evidence, we cannot know which of (...) these worlds is actual. However, Lewis also appeals to a range of familiar semantic principles when framing his argument, which leads some authors to suppose that he can also plausibly be interpreted as offering a purely semantic argument for humility in addition. In this paper I grant that these arguments are Lewisian, but argue that Lewis is also committed to a theory of mind that licenses a purely metaphysical argument for humility based on the idea that mental properties supervene on fundamental structure. Given that knowing which x is the F requires knowing that a is the F, the supposition that we could come to know which properties actually occupy the fundamental roles entails differences in mental properties between worlds with the same fundamental structure, violating supervenience. Humility follows right away, without any further epistemic or semantic principles. This argument is immune to almost every way of rebutting the sceptical and semantic arguments; conversely, almost every way of rebutting the metaphysical argument tells equally against the others. (shrink)

This essay in the comparative metaphysic of nothingness begins by pondering why Leibniz thought of the converse question as the preeminent one. In Eastern philosophical thought, like the numeral 'zero' (śūnya) that Indian mathematicians first discovered, nothingness as non-being looms large and serves as the first quiver on the imponderables they seem to have encountered (e.g., 'In the beginning was neither non-being nor being: what was there, bottomless deep?' RgVeda X.129). The concept of non-being and its permutations of nothing, negation, (...) nullity, etc., receive more sophisticated treatment in the works of grammarians, ritual hermeneuticians, logicians, and their dialectical adversaries variously across Jaina and Buddhist schools. The present analysis follows the function of negation/the negative copula, nãn, and dialetheia in grammar and logic, then moves onto ontologies of non-existence and extinction and further suggestive tropes that tend to arrest rather than affirm the inexorable being-there of something. After a discussion of interests in being (existence), non-being and nothingness in contemporary metaphysics, the article examines Heidegger’s extensive treatment of nothingness in his 1929 inaugural Freiburg lecture, 'Was ist Metaphysik?', published later as 'What is Metaphysics?' The essay however distances itself from any pretensions toward a doctrine of Metaphysical Nihilism. (shrink)

This essay in the comparative metaphysic of nothingness begins by pondering why Leibniz thought of the converse question as the preeminent one. In Eastern philosophical thought, like the numeral 'zero' (śūnya) that Indian mathematicians first discovered, nothingness as non-being looms large and serves as the first quiver on the imponderables they seem to have encountered (e.g., 'In the beginning was neither non-being nor being: what was there, bottomless deep?' RgVeda X.129). The concept of non-being and its permutations of nothing, negation, (...) nullity, etc., receive more sophisticated treatment in the works of grammarians, ritual hermeneuticians, logicians, and their dialectical adversaries variously across Jaina and Buddhist schools. The present analysis follows the function of negation/the negative copula, nãn, and dialetheia in grammar and logic, then moves onto ontologies of non-existence and extinction and further suggestive tropes that tend to arrest rather than affirm the inexorable being-there of something. After a discussion of interests in being (existence), non-being and nothingness in contemporary metaphysics, the article examines Heidegger’s extensive treatment of nothingness in his 1929 inaugural Freiburg lecture, 'Was ist Metaphysik?', published later as 'What is Metaphysics?' The essay however distances itself from any pretensions toward a doctrine of Metaphysical Nihilism. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:Hume on Human Excellence Marie A. Martin Hume was, in important respects, still verymuch a part ofthe classical ethical tradition. This is something we tend to overlook because we come out of a distinctly modern moral tradition, and we normally approach Hume looking for answers to a set of questions that are distinct, and often far removed, from the central questions of the classical tradition. Yet, the classical aspects (...) of Hume's ethics are not irrelevant to contemporary moral debates. There is evidence in recent years of a growing discontent with all the permutations of the two dominant strands of contemporary moral thought, Kantianism and utilitarianism. The sort of radical critique found in the works of Maclntyre, the increasing popularity of communitarian theories, and the resurgence of interest in virtue ethics in general, and Aristotelianism in particular, are all indications of this discontent. What I wish to suggest is that Hume's moral thought might prove a rich source for those who are dissatisfied with the direction ofmodern moral theory, and especially for those who believe that there is something within the classical tradition of virtue ethics worth salvaging. For Hume is a virtue ethicist, albeit one in modern dress, who, poised between the ancients and moderns, self-consciously chose to align himself with the ancient tradition, asserting its superiority over the modern. The ancient moralists are, Hume claims, the "best models,"1 morals being the one science "inwhich theyare not surpassed by the moderns" (E 330). The aim of this paper is to take an initial step towards refocusing our view on the largely neglected classical aspects of Hume's moral thought. The relationship between Hume's moral thought and the classical tradition is both extensive and complex, and I do not pretend to do anything more in this paper than present the tip of the iceberg. But the tip I shall examine is central to all that lies below; it is Hume's conception ofhuman excellence. Virtue or Human Excellence Perhaps Hume's most complete description ofhuman excellence occurs in the conclusion ofAn Enquiry Concerning the Principles ofMorals. Hume presents us with the fictional character, Cleanthes, as one whom "a philosopher might select... as a model ofperfect virtue" (E 270). He is, Hume claims, "a man ofhonour andhumanity," one ofwhom "[e]very one, who has anyintercourse... is sure offair and kind treatment." His Volume XVIII Number 2 383 MARIE A. MARTIN "assiduous application... [and] quick penetration... prognosticate the greatest honours and advancement." His company is enjoyed by all because he has "so much wit with good manners; so much gallantry without affectation" and "so much ingenious knowledge." His "cheerfulness... runs through the whole tenor ofhislife, and preserves a perpetual serenity on his countenance, and tranquillity ofhis soul." Finally, "[h]e has met with severe trials, misfortunes as well as dangers; and by his greatness ofmind, was still superior to all ofthem" (E 269-70). In the Treatise, Hume offers a less specific, yet similar portrait of human excellence: when we enumerate the good qualities of any person, we always mention those parts ofhis character, which renderhim a safe companion, an easy friend, a gentle master, an agreeable husband, or an indulgent father. We consider him with all hisrelations in society; andlove orhate him, according as he affects those, who have any immediate intercourse with him. And 'tis a most certain rule, that if there be no relation oflife, in which I cou'd not wish to stand to aparticular person, his character must so far be allow'd to be perfect. If he be as little wanting to himselfas to others, his character is entirely perfect.2 Although there are numerous passages throughout Hume's works that paint the same general picture, I will offer only one more, his description of an ideally virtuous disposition from his essay, The Sceptic: that which leads to action and employment, renders us sensible to the social passions, steels the heart against the assaults offortune, reduces the affections to ajustmoderation, makes our own thoughts an entertainment to us, and inclines us rather to the pleasure of society and conversation, than to those ofthe senses.3 What is common to all these descriptions... (shrink)

continent. 1.4 (2011): 286—310. This mad play of writing —Stéphane Mallarmé Somewhere in between mathematics and theory, light and dark, physicality and projection, oscillates the poetry of Alessandro De Francesco. The texts hold no periods or commas, not even a capital letter for reference. Each piece stands as an individual construction, and yet the poetry flows in and out of the frame. Images resurface from one poem to the next, haunting the reader with reincarnations of an object lost in the (...) grass or a representation of a pear in a Dutch still life, embedded in cycles of cinematic close ups and multiple dimensions. As a whole, De Francesco’s oeuvre suggests, to use the title of one of his works, a redefinition —linguistic, epistemological, personal. The poem The End (un’agenda) (The End (an agenda)) opens with a quote by literary theorist Maurice Blanchot, which may be translated as follows: Speaking is not seeing. Speaking frees thought from this optical imperative that in the Western tradition, for thousands of years, has subjugated out approach to things, and induced us to think under the guaranty of light or under the threat of its absence.[1] In writing, De Francesco seeks to redefine our approach to things. His poems, like Blanchot’s writings, speak to both illuminate and to obscure. The reader hangs in an absence of reality within language that necessitates an attempt at interpretation, yet renders such a search ultimately futile. De Francesco draws the anonymous images that appear in this poem from the city of Paris, his current home. The fragmented narrative depicts an inner doubt of realness, calling for a confirmation of a physical existence beyond verbalization and cogitation. Cyclical references to film throw into question the reliability of the reality he creates. The light, sometimes red and safe, other times absent and murky, cannot necessarily be trusted as a guaranteed means of illumination. Blanchot’s distinction between language and visualization, and the relationship of each to reality, though linked specifically to The End (un’agenda) , can be a lens through which to read any of the three works that follow. assente obliqua (absent oblique) is composed of descriptions of six still life paintings, ranging from Dutch masterpieces of the seventeenth century to 1960s minimalism. The actual images of the paintings are absent, and the text is the sole source and object of a virtual reality created around the artwork. “Absent oblique” refers to the light source placed outside of the frame, which both informs and distracts viewing of the scene. Although mere description can be unreliable and unsatisfying in its necessary limitation, the representational act of description is shown as more than just a human want. It is a need, a means by which to grapple with an unsure reality. As the illustrations progress, they descend into abstraction and chaos. The precariously placed plate triggers the movement: the bottle bursts and the objects collapse into the movement of a tracking film camera. corpo estraneo in moto ascensionale (foreign body in ascending motion) is prose poetry in action. Its objective tone of description is skewed by the subjectivity of the narrative as horrific images are relayed in fragmented but matter-of-fact manner. A “foreign body” is both a mass of cancerous cells, and a corporeal description, and the poem takes the reader on a journey back and forth between the two, destination unclear. Beyond a questioning of the real, corpo estraneo in moto ascensionale is an examination of the possible. De Francesco’s poetry becomes a camera obscura through which to observe the constant flux of light and dark that blurs our reality. His work is colored by the idea of apo koinou , a Greek term meaning “from the common” that involves a construction of two clauses with a shared word or phrase. Through such melting of meaning, De Francesco creates a fluid ambiguity that is nonetheless grounded in bodily concepts. In assente obliqua , the reader is confronted with a description of a still life that rapidly transforms into a more chilling scene: the membrane of the mushroom in the basket emerges behind the white cloth a body could hide itself that asks for help In the realm of pure description, there is a mushroom that peeks out from behind a white cloth in a basket. Behind the white cloth, too, there could be a body, hiding, asking for help. Such an elision elicits disorienting mistrust in temporality, but also expands the planar possibilities of syntactical meaning. A white cloth is not merely a construct in still life painting, but veil that both shields and reveals potential mysteries. It is a proposed alternative to a traditional Western binary of subjectivity and objectivity. The apo koinou construction is rare in modern English, having slipped out of use after its resurgence in Old English poetry. De Francesco reintroduces this blur of object and subject relations into a modern light. He draws inspiration from a device used by Gruppo 63 founder and avant-garde poet Antonio Porta tended toward repetition of phrases in third person perspective. In Italian, it is perfectly grammatically correct to omit the subject, including only a verb conjugation. Gender, even humanity unknown, the subject dissolves into the action, thus giving to the poetry the power to change the reader’s perception of who or what is actually acting. To further push the relative boundaries of experience, De Francesco expands his written poetry into what he calls “reading environments.” In these sound experiments, De Francesco’s voice reading his poetry is manipulated by real time digital voice processing. The written is transformed to the spoken, and then injected with currents of electric sound. “At each activation of word in the darkness,” (from The End (un’agenda) ) language is permutated into a nonphysical yet all-encompassing being. In these projects, realized all over Europe, De Francesco continues his examination of the word’s potency beyond the page and into an “n-dimensional space,” where the lines between nature and affect are intertwined. To publish excerpts of De Francesco’s oeuvre is to show screen shots of full-length film, to read pull quotes from a philosophy treatise. In these poems, there are questions, not to be answered, but to be questioned again. The words will oscillate in and out of the square construction found in his poems, out of the borders of the page, out of the rectangle of the laptop screen. NOTES (1) Blanchot, Maurice. The Infinite Conversation . Trans. Susan Hanson. Minneapolis: University of Minnesota Press, 1993. 27. EDITORS' NOTE The .pdf above contains about twenty pages of translation and the original Italian poetry. Below we provide only a brief account. The End (an agenda) Parler, ce n’est pas voir. Parler libère la pensée de cette exigence optique qui, dans la tradition occidentale, soumet depuis des millénaires notre approche des choses et nous invite à penser sous la garantie de la lumière ou sous la menace de l’absence de lumière. —Maurice Blanchot in this n-dimensional space i could spy on myself from the cracks while going back and forth from the summer to the wardrobe from the night to the parking lot but something filters in through the half-closed shutters becomes an event enunciation we stay without explanation like parallel curves on the back of a solid growing older she enters the garden always repeats certain phrases the elevator to be redone the neighbor’s music the steps the pavement furls like the leaves of a fern when touched she is framed from behind while she moves rocking she covers distances slowly a bag overflows from the wardrobe something stirs inside but then the suitcase comes open not even by my hand it’s the objects that are starting to filter out the little red haired monster watches idling the appointments written on one of your agendas two years old still seem urgent each letter holds itself upright on the page with flourishes and arabesques each angle has its own geography i’m trying to describe the path the fingers trace on the carpet the zipper takes the opposite route we are suspended on the stairs above the water in the center is the summer seen from above the darkness of the city passes from one headlight to the next the surfaces of our arms cohere and are shiny underneath the blinking of a sign each pore is an open expanse the body dreams the hair gives form to the possible some daring swimmers were throwing themselves into the seine they swam upstream up to the first quay look there could exist behind the screen a room where even when the lamp is out and the curtains drawn even when the suitcase wasn’t closed everything seemed red everything calm construction of a four-dimensional tetrahedron by R. Courant – H. Robbins, What is Mathematics? Oxford University Press, 1941  . (shrink)