Since 1993, when Hudelmaier developed an O(n log n)-space decision procedure for propositional Intuitionistic Logic, a lot of work has been done to improve the efficiency of the related proof-search algorithms. In this paper a tableau calculus using the signs T, F and Fc with a new set of rules to treat signed formulas of the kind T((A → B) → C) is provided. The main feature of the calculus is the reduction of both the non-determinism in proof-search (...) and the width of proofs with respect to Hudelmaier's one. These improvements have a significant influence on the performances of the implementation. (shrink)

We employ a recently developed methodology -- called "structural refinement" -- to extract nested sequent systems for a sizable class of intuitionistic modal logics from their respective labelled sequent systems. This method can be seen as a means by which labelled sequent systems can be transformed into nested sequent systems through the introduction of propagation rules and the elimination of structural rules, followed by a notational translation. The nested systems we obtain incorporate propagation rules that are parameterized (...) with formal grammars, and which encode certain frame conditions expressible as first-order Horn formulae that correspond to a subclass of the Scott-Lemmon axioms. We show that our nested systems are sound, cut-free complete, and admit hp-admissibility of typical structural rules. (shrink)

This paper shows how to derive nested calculi from labelled calculi for propositional intuitionistic logic and first-order intuitionistic logic with constant domains, thus connecting the general results for labelled calculi with the more refined formalism of nested sequents. The extraction of nested calculi from labelled calculi obtains via considerations pertaining to the elimination of structural rules in labelled derivations. Each aspect of the extraction process is motivated and detailed, showing that each nested calculus inherits favorable (...) proof-theoretic properties from its associated labelled calculus. (shrink)

The modal -calculus extends basic modal logic with second-order quantification in terms of arbitrarily nested fixpoint operators. Its satisfiability problem is EXPTIME-complete. Decision procedures for the modal -calculus are not easy to obtain though since the arbitrary nesting of fixpoint constructs requires some combinatorial arguments for showing the well-foundedness of least fixpoint unfoldings. The tableau-based decision procedures so far also make assumptions on the unfoldings of fixpoint formulas, e.g., explicitly require formulas to be in guarded normal form. (...) In this paper we present a tableau calculus for deciding satisfiability of arbitrary, i.e., not necessarily guarded -calculus formulas. It is based on a new unfolding rule for greatest fixpoint formulas which allows unguarded formulas to be handled without an explicit transformation into guarded form, thus avoiding a exponential blow-up in formula size. We prove soundness and completeness of the calculus, and compare it empirically to using guarded transformation instead. The new unfolding rule can also be used to handle nested star operators in PDL formulas correctly. (shrink)

We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path axioms, and for bi-intuitionistic logic. These logics do not have straightforward formalisations in the traditional Gentzen-style sequent calculus, but have all been shown to have cut-free nested sequent calculi. The proof of the interpolation theorem uses these calculi and is purely syntactic, without resorting (...) to embeddings, semantic arguments, or interpreted connectives external to the underlying logical language. A novel feature of our proof includes an orthogonality condition for defining duality between interpolants. (shrink)

In the Lambek calculus of order 2 we allow only sequents in which the depth of nesting of implications is limited to 2. We prove that the decision problem of provability in the calculus can be solved in time polynomial in the length of the sequent. A normal form for proofs of second order sequents is defined. It is shown that for every proof there is a normal form proof with the same axioms. With this normal form we (...) can give an algorithm that decides provability of sequents in polynomial time. (shrink)

Standpoint logic is a recently proposed formalism in the context of knowledge integration, which advocates a multi-perspective approach permitting reasoning with a selection of diverse and possibly conflicting standpoints rather than forcing their unification. In this paper, we introduce nested sequent calculi for propositional standpoint logics---proof systems that manipulate trees whose nodes are multisets of formulae---and show how to automate standpoint reasoning by means of non-deterministic proof-search algorithms. To obtain worst-case complexity-optimal proof-search, we introduce a novel technique in the (...) context of nested sequents, referred to as "coloring," which consists of taking a formula as input, guessing a certain coloring of its subformulae, and then running proof-search in a nested sequent calculus on the colored input. Our technique lets us decide the validity of standpoint formulae in CoNP since proof-search only produces a partial proof relative to each permitted coloring of the input. We show how all partial proofs can be fused together to construct a complete proof when the input is valid, and how certain partial proofs can be transformed into a counter-model when the input is invalid. These "certificates" (i.e. proofs and counter-models) serve as explanations of the (in)validity of the input. (shrink)

We propose a new sequent calculus for bi intuitionistic logic which sits somewhere between display calculi and traditional sequent calculi by using nested sequents. Our calculus enjoys a simple (purely syntactic) cut elimination proof as do display calculi. But it has an easily derivable variant calculus which is amenable to automated proof search as are (some) traditional sequent calculi. We first present the initial calculus and its cut elimination proof. We then present the derived (...) class='Hi'>calculus, and then present a proof search strategy which allows it to be used for automated proof search. We prove that this search strategy is terminating and complete by showing how it can be used to mimic derivations obtained from an existing calculus GBiInt for bi intuitionistic logic. As far as we know, our new calculus is the first sequent calculus for bi intuitionistic logic which uses no semantic additions like labels, which has a purely syntactic cut elimination proof, and which can be used naturally for backwards proof search. Keywords: Bi-intuitionistic logic, display calculi, proof search. (shrink)

For some modal fixed point logics, there are deductive systems that enjoy syntactic cut-elimination. An early example is the system in Pliuskevicius [15] for LTL. More recent examples are the systems by the authors of this paper for the logic of common knowledge [5] and by Hill and Poggiolesi for PDL[8], which are based on a form of deep inference. These logics can be seen as fragments of the modal mu-calculus. Here we are interested in how far this approach (...) can be pushed in general. To this end, we introduce a nested sequent system with syntactic cut-elimination which is incomplete for the modal mu-calculus, but complete with respect to a restricted language that allows only fixed points of a certain form. This restricted language includes the logic of common knowledge and PDL. There is also a traditional sequent system for the modal mu-calculus by Jäger et al. [9], without a syntactic cut-elimination procedure. We embed that system into ours and vice versa, thus establishing cut-elimination also for the shallow system, when only the restricted language is considered. (shrink)

We consider four natural deduction systems: Fitch-style systems, Gentzen-style systems (in the form of dags), general deduction Frege systems and nested deduction Frege systems, as well as dag-like Gentzen-style sequent calculi. All these calculi soundly and completely formalize classical propositional logic. -/- We show that general deduction Frege systems and Gentzen-style natural calculi provide at most quadratic speedup over nested deduction Frege systems and Fitch-style natural calculi and at most cubic speedup over Gentzen-style sequent calculi.

In het kader van de Leerstoel Rector Dhanis (UFSIA, Antwerpen) werd door een studiegroep bestaande uit artsen en verpleegkundigen, ethici en juristen, een interdisciplinaire studie ondernomen over 'klinische ethiek' en 'hoe recht en politiek omgaan met problemen die thuishoren in de klinische praktijk'. In deze bundel wordt het ethische denken in een aantal casussen betreffende neonatalen en dementerenden kritisch besproken. De adviezen van het Raadgevend Comite voor Bio-Ethiek over sterilisatie van mentaal gehandicapten en over klonering worden onderzocht op hun relevantie (...) voor de klinische praktijk. (shrink)

In this article, the place and the nature of an ethical dialogue that develops within Christian healthcare institutions in Flanders, Belgium is examined. More specifically, the question is asked how Christian healthcare institutions should position themselves ethically in a context of a pluralistic society. The profile developed by Caritas Catholica Flanders must take seriously not only the external pluralistic context of our society and the internal pluralistic worldviews by personnel/employees and patients, but also the inherent inspiration of a Christian healthcare (...) institution. This article concludes with ten general orientations that could shape the ethical dialogue from a Christian inspiration in a pluralistic context. (shrink)

We establish a connection between measurement-based quantum computation and the field of mathematical logic. We show that the computational power of an important class of quantum states called graph states, representing resources for measurement-based quantum computation, is reflected in the expressive power of (classical) formal logic languages defined on the underlying mathematical graphs. In particular, we show that for all graph state resources which can yield a computational speed-up with respect to classical computation, the underlying graphs—describing the quantum correlations of (...) the states—are associated with undecidable logic theories. Here undecidability is to be interpreted in a sense similar to Gödel’s incompleteness results, meaning that there exist propositions, expressible in the above classical formal logic, which cannot be proven or disproven. (shrink)

This thesis introduces the "method of structural refinement", which serves as a means of transforming the relational semantics of a modal and/or constructive logic into an 'economical' proof system by connecting two proof-theoretic paradigms: labelled and nested sequent calculi. The formalism of labelled sequents has been successful in that cut-free calculi in possession of desirable proof-theoretic properties can be automatically generated for large classes of logics. Despite these qualities, labelled systems make use of a complicated syntax that explicitly incorporates (...) the semantics of the associated logic, and such systems typically violate the subformula property to a high degree. By contrast, nested sequent calculi employ a simpler syntax and adhere to a strict reading of the subformula property, making such systems useful in the design of automated reasoning algorithms. However, the downside of the nested sequent paradigm is that a general theory concerning the automated construction of such calculi (as in the labelled setting) is essentially absent, meaning that the construction of nested systems and the confirmation of their properties is usually done on a case-by-case basis. The refinement method connects both paradigms in a fruitful way, by transforming labelled systems into nested (or, refined labelled) systems with the properties of the former preserved throughout the transformation process. To demonstrate the method of refinement and some of its applications, we consider grammar logics, first-order intuitionistic logics, and deontic STIT logics. The introduced refined labelled calculi will be used to provide the first proof-search algorithms for deontic STIT logics. Furthermore, we employ our refined labelled calculi for grammar logics to show that every logic in the class possesses the effective Lyndon interpolation property. (shrink)

In this paper, we introduce provability multilattice logic PMLn and multilattice arithmetic MPAn which extends first-order multilattice logic with equality by multilattice versions of Peano axioms. We show that PMLn has the provability interpretation with respect to MPAn and prove the arithmetic completeness theorem for it. We formulate PMLn in the form of a nested sequent calculus and show that cut is admissible in it. We introduce the notion of a provability multilattice and develop algebraic semantics for PMLn (...) on its basis, by the method of Lindenbaum-Tarski algebras we prove the algebraic completeness theorem. We present Kripke semantics for PMLn and establish the Kripke completeness theorem via syntactical and semantic embeddings from PMLn into GL and vice versa. Last but not least, the decidability of PMLn is shown. (shrink)

In this paper, we introduce provability multilattice logic PMLn and multilattice arithmetic MPAn which extends first-order multilattice logic with equality by multilattice versions of Peano axioms. We show that PMLn has the provability interpretation with respect to MPAn and prove the arithmetic completeness theorem for it. We formulate PMLn in the form of a nested sequent calculus and show that cut is admissible in it. We introduce the notion of a provability multilattice and develop algebraic semantics for PMLn (...) on its basis, by the method of Lindenbaum-Tarski algebras we prove the algebraic completeness theorem. We present Kripke semantics for PMLn and establish the Kripke completeness theorem via syntactical and semantic embeddings from PMLn into GL and vice versa. Last but not least, the decidability of PMLn is shown. (shrink)

We see a systematic set of cut-free axiomatisations for all the basic normal modal logics formed by some combination the axioms d, t, b, 4, 5. They employ a form of deep inference but otherwise stay very close to Gentzen’s sequent calculus, in particular they enjoy a subformula property in the literal sense. No semantic notions are used inside the proof systems, in particular there is no use of labels. All their rules are invertible and the rules cut, weakening (...) and contraction are admissible. All systems admit a straightforward terminating proof search procedure as well as a syntactic cut elimination procedure. (shrink)

Neste artigo começo por argumentar que devemos ver o Big Typescript como algo muito diferente de um livro planejado para a publicação. Ele deve ser tomado meramente como uma coleção de observações, que expressam a concepção de Wittgenstein de “gramática” por volta de 1932-33, quando as observações foram reunidas. Em seguida, explico a concepção substancial de “gramática” do BT. Espero tornar claro, nesta segunda parte, que o BT e o Tractatus Logico-Philosophicus são próximos no sentido de que partilham a idéia (...) de que a linguagem tem uma estrutura que opera de acordo com regras fixas de sentido (um cálculo). (shrink)

In this paper, we present a prenex form theorem for a version of Independence Friendly logic, a logic with imperfect information. Lifting classical results to such logics turns out not to be straightforward, because independence conditions make the formulas sensitive to signalling phenomena. In particular, nested quantification over the same variable is shown to cause problems. For instance, renaming of bound variables may change the interpretations of a formula, there are only restricted quantifier extraction theorems, and slashed connectives cannot (...) be so easily removed. Thus we correct some claims from Hintikka [8], Caicedo & Krynicki [3] and Hodges [11]. We refine definitions, in particular the notion of equivalence, and sharpen preconditions, allowing us to restore those claims, including the prenex form theorem of Caicedo & Krynicki [3], and, as a side result, we obtain an application to Skolem forms of classical formulas. It is a known fact that a complete calculus for IF-logic is impossible, but with our results we establish several quantifier rules that form a partial calculus of equivalence for a general version of IF-logic reflecting general properties of information flow in games. (shrink)

An important lesson that philosophy can learn from the Turing Test and computer science more generally concerns the careful use of the method of Levels of Abstraction (LoA). In this paper, the method is first briefly summarised. The constituents of the method are “observables”, collected together and moderated by predicates restraining their “behaviour”. The resulting collection of sets of observables is called a “gradient of abstractions” and it formalises the minimum consistency conditions that the chosen abstractions must satisfy. Two useful (...) kinds of gradient of abstraction – disjoint and nested – are identified. It is then argued that in any discrete (as distinct from analogue) domain of discourse, a complex phenomenon may be explicated in terms of simple approximations organised together in a gradient of abstractions. Thus, the method replaces, for discrete disciplines, the differential and integral calculus, which form the basis for understanding the complex analogue phenomena of science and engineering. The result formalises an approach that is rather common in computer science but has hitherto found little application in philosophy. So the philosophical value of the method is demonstrated by showing how making the LoA of discourse explicit can be fruitful for phenomenological and conceptual analysis. To this end, the method is applied to the Turing Test, the concept of agenthood, the definition of emergence, the notion of artificial life, quantum observation and decidable observation. It is hoped that this treatment will promote the use of the method in certain areas of the humanities and especially in philosophy. (shrink)

ABSTRACT In a recent essay, Sören Stenlund tries to align Wittgenstein’s approach to the foundations and nature of mathematics with the tradition of symbolic mathematics. The characterization of symbolic mathematics made by Stenlund, according to which mathematics is logically separated from its external applications, brings it closer to the formalist position. This raises naturally the question whether Wittgenstein holds a formalist position in philosophy of mathematics. The aim of this paper is to give a negative answer to this question, defending (...) the view that Wittgenstein always thought that there is no logical separation between mathematics and its applications. I will focus on Wittgenstein’s remarks about arithmetic during his middle period, because it is in this period that a formalist reading of his writings is most tempting. I will show how his idea of autonomy of arithmetic is not to be compared with the formalist idea of autonomy, according to which a calculus is “cut off” from its applications. The autonomy of arithmetic, according to Wittgenstein, guarantees its own applicability, thus providing its own raison d’être. RESUMO Em um recente artigo, Sören Stenlund procura alinhar a abordagem de Wittgenstein em relação aos fundamentos e à natureza da matemática com a tradição da matemática simbólica. A caracterização da matemática simbólica feita por Stenlund, de acordo com a qual a matemática é logicamente separada de suas aplicações externas, a aproxima da posição formalista. Isto naturalmente levanta a questão de se Wittgenstein defende uma posição formalista em filosofia da matemática. O objetivo deste artigo é dar uma resposta negativa a esta questão, ao defender que Wittgenstein sempre pensou não haver separação lógica entre a matemática e suas aplicações. Atenção especial será dada às observações de Wittgenstein sobre a aritmética pertencentes ao seu período intermediário, pois é neste período que uma leitura formalista de seus escritos é mais sedutora. Mostrarei como sua ideia de autonomia da aritmética não deve ser comparada à ideia formalista de autonomia, segundo a qual um cálculo é “cortado” de suas aplicações. A autonomia da aritmética, para Wittgenstein, garante ela própria sua aplicabilidade, provendo, assim, sua própria raison d’être. (shrink)

We introduce new proof systems for propositional logic, simple deduction Frege systems, general deduction Frege systems, and nested deduction Frege systems, which augment Frege systems with variants of the deduction rule. We give upper bounds on the lengths of proofs in Frege proof systems compared to lengths in these new systems. As applications we give near-linear simulations of the propositional Gentzen sequent calculus and the natural deduction calculus by Frege proofs. The length of a proof is the (...) number of lines in the proof. A general deduction Frege proof system provides at most quadratic speedup over Frege proof systems. A nested deduction Frege proof system provides at most a nearly linear speedup over Frege system where by "nearly linear" is meant the ratio of proof lengths is O) where α is the inverse Ackermann function. A nested deduction Frege system can linearly simulate the propositional sequent calculus, the tree-like general deduction Frege calculus, and the natural deduction calculus. Hence a Frege proof system can simulate all those proof systems with proof lengths bounded by O). Also we show that a Frege proof of n lines can be transformed into a tree-like Frege proof of O lines and of height O. As a corollary of this fact we can prove that natural deduction and sequent calculus tree-like systems simulate Frege systems with proof lengths bounded by O. (shrink)

The purpose of this article is to present a new theory for fixed points over arithmetic which allows the building up of fixed points in a very nested and entangled way. But in spite of its great expressive power we can show that the proof-theoretic strength of our theory—which is intensional in a meaning to be described below—is characterized by the Feferman–Schütte ordinal Γ0. Our approach is similar to the building up of fixed points over state spaces in the (...) propositional modal μ-calculus. (shrink)

ABSTRACTIn this paper, we present a generalisation of proof simulation procedures for Frege systems by Bonet and Buss to some logics for which the deduction theorem does not hold. In particular, we study the case of finite-valued Łukasiewicz logics. To this end, we provide proof systems and which augment Avron's Frege system HŁuk with nested and general versions of the disjunction elimination rule, respectively. For these systems, we provide upper bounds on speed-ups w.r.t. both the number of steps in (...) proofs and the length of proofs. We also consider Tamminga's natural deduction and Avron's hypersequent calculus GŁuk for 3-valued Łukasiewicz logic and generalise our results considering the disjunction elimination rule to all finite-valued Łukasiewicz logics. (shrink)

We consider a simple modal logic whose nonmodal part has conjunction and disjunction as connectives and whose modalities come in adjoint pairs, but are not in general closure operators. Despite absence of negation and implication, and of axioms corresponding to the characteristic axioms of _T_, _S4_, and _S5_, such logics are useful, as shown in previous work by Baltag, Coecke, and the first author, for encoding and reasoning about information and misinformation in multiagent systems. For the propositional-only fragment of such (...) a dynamic epistemic logic, we present an algebraic semantics, using lattices with agent-indexed families of adjoint pairs of operators, and a cut-free sequent calculus. The calculus exploits operators on sequents, in the style of “nested” or “tree-sequent” calculi; cut-admissibility is shown by constructive syntactic methods. The applicability of the logic is illustrated by reasoning about the muddy children puzzle, for which the calculus is augmented with extra rules to express the facts of the muddy children scenario. (shrink)

In this thesis, I deal with the notions of a condition holding for some proposition and a proposition being true in a certain number of possible worlds. These notions are called propositional quantifiers and numerical modalizers respectively. In each chapter, I attempt to dispose of a system. A system consists of: a language; axioms and rules of inference; and an interpretation. To dispose of a system is to prove its decidability and its consistency and completeness for the given interpretation. I (...) shall, in passing, make applications to de definability, translatability and other topics. In Chapter 1, I consider the system 5SQ. Its language is that of 55 with Q as a fresh unary operator. Its axioms and rules of inference are those for 85 plus the following special axiom-schemes for Q: 1) QA::>MA 2) Q A ::> L V L 3) L ::> 4) Q A ::> L Q A. 'QA' is interpreted as 'A is true in exactly one possible world.' I dispose of the system by showing that every formula in it is equivalent to one in normal form. In Chapter 2 I consider the system S5n. Its language is that of S5 but with the unary operators Qk for each non-negative integer k. Its axioms and rules are those of S5 plus the following special axiom-schemes for Qk: 1) Qk A>~Q1 A, 1˂K 2) Qk A ≡ Vki≡oQi ˄ Qk-I 3) L ˂ 4) Qk A ˂ L Qk A 5) Qo A ≡ L ~ A, 1 ≥ 0, k ≥ 1 ‘Qk A’ is interpreted as 'A is true in exactly k possible worlds.' I dispose of this system by generalising the normal forms of S5Q. In the chapters 3-5, I consider three systems which result from adding propositional quantifiers to S5. The first two systems, S5╥+ and S5╥, contain the usual axioms and rules for quantifiers. The first contains, in addition, the axiom-scheme G = )). The last, S5╥-, results from S5╥ by restricting the Scheme of Specification, viz., A > A, B free for P in A, to formulas B of the propositional calculus. To interpret these systems we must specify which propositions the variable P ranges over. For St╥-, we merely require that if p and q are propositions, then and are also propositions. For S5╥+, we also require that each possible world be describable i.e. that there be a proposition which is true in that world alone. And for S5╥, we require not that each possible world be describable but that there be a proposition which is true in just those possible worlds which are describable. Again, we dispose of the systems by normal forms. This requires that we eliminate quantifiers and nested occurrences of L by adding new symbols to the language. For S5╥+, the operators Qk suffice. For S5╥, the operators Qk suffice. For S5╥, we also require the constant g and a fresh unary operator N. For S5╥-, even greater additions are required. In the last two chapters, 6 and 7, I turn to systems which have essentially the same language as S5╥. However, ‘Qk A' is now interpreted as 'A is true in exactly k possible worlds accessible from the given world.' Different conditions on R, the relation of accessibility, lead to different axioms. In chapter 6 I consider the conditions of reflexivity, symmetry and transitivity, and in Chapter 7 the conditions of being a partial, convergent, total or dense order. I prove consistency and completeness by the method of maximally consistent systems. The method can yield decidability results, but I do not go into the matter. I have, as a rule, not given acknowledgements for well-established results or terminology. The main references are at the end of each chapter. Fuller references are in the bibliography. (shrink)

continent. 1.3 (2011): 201-207. “Poetry is experience, linked to a vital approach, to a movement which is accomplished in the serious, purposeful course of life. In order to write a single line, one must have exhausted life.” —Maurice Blanchot (1982, 89) Nikos Karouzos had a communist teacher for a father and an orthodox priest for a grandfather. From his four years up to his high school graduation he was incessantly educated, reading the entire private library of his granddad, comprising mainly (...) the Orthodox Church Fathers and the ancient classics. Later on in his life he sold the library for money, only to buy a little more time before he went broke again: “I carry sorrow like a cage/ I got no birds/ as I come back from her hair/ I see the profit emptied/ cool from terror.” (1993, Ι, 101) Nowadays—and ridiculously recently—we are more than apt to speak of a certain insouciance pertaining to the Greek form of expenditure: expenditure without any type of investment, sometimes not (even) symbolic. In the vaults of the European unconscious, this imprudent stance still conjures a “capital punishment” in the form of de-capitation, reflecting back the fear of excess and the terror of its consequences.1 Thus the Greek way of living is very close to what a stranger could have termed as “the Greek way of dying.” Yet, what is not often understood is that the Greek esprit , the same one that invented the maxim μηδ?ν ?γαν (“nothing in excess”), does not experience death solely as an imminent fear of bankruptcy. For it miraculously combines its unconditional acceptance with the promise of a resurrection that is always there in the scents of Spring, from Dionysus to the orthodox Christ: “Everyone resurrects himself through dying [….] Resurrection is the switching of mortalities.” (2002, 94) Hence, if an entire library was imprudently traded for a plate with seven olives, a sliced tomato and some fresh goat cheese, let us not be fooled: this is not the meal of the pauper, but that of “an aristocrat from God” (1993, II, 491) feeding his eloquent loudmouth, ridiculously cut open in an otherwise rock-solid caput . *** To speak of the Greek experience is to speak about a half-dead language that still utters in life what is seemingly excluded from it and thus forbidden to be talked about: death. Death as anything that is out of this world, as something that will never return . Still, along with an experience of death that recently waned as a worn-out academic fashion, the Greek experience is dead too. Nearly 2300 years of written words separating Homer from the fall of Byzantium equal 500 books on a library traded for money: “I am with the killed. Hence my deepest solitude. I do not feel this tremendous macho society, beyond from the fact that it is a ruthlessly consuming one. It is me who pays all the time .” (2002, 57) Let us do the math and see how much this dealing with the Greek experience is costing the poet and how much dealing with the Greek experience might cost us today. *** “I do not guarantee a single word.” (Karouzos, 1993, II, 454) Through its various dialects and forms, the Greek language speaks through an incessant historical dissemination. Anyone who is aware of this terrifying polymorphy and still calls himself a poet, must stand against a white sheet of paper, pen-in-hand, with a very particular duty: to be as fully inconsistent as possible. In the formally ironic uniqueness of the poem, the poet functions as “a band-aid for lesser and greater antinomies.” (1993, I, 251) Of course these antinomies are not exhausted in language—they are historical, political and, alas, existential. Yet, beyond appearances , it is language that ruthlessly encodes them through history, submitting the poet to the temptation of placing them one next to the other on a single white sheet. The closer their neighboring, the greater the scattering of the writer in the ironic uniqueness of the paper. In a work where poetic license is described as a “freedom-impasse” (2002, 51), this task is undertaken in full conscience of its personal consequences: “what I am interested in is to escape my individuality (envisioning the non-ego) […] Nevertheless, my dissociations never achieve duration.” (2002, 74-75) Hence, though poetry is the “deserted direction of will,” (1998, 62) the stance of the poet is not that of a Nietzschean “great man.”2 Whereas drunkenness provides a thread between the poem and the excess it both presupposes and infuses (“Poetry always enlarges. ‘Drunkenness’ is nothing more than that,” (2002, 85)), whereas language flashes in loudmouth spurts of déraison (“When I am alone I do something else. I utter words. For example, while having my ouzo and listening to music I am most likely capable of randomly shouting ‘Electricity!’” (2002, 138)), the poet never gives in to the double affirmation that would eventually risk the “element of pleasure in discourse.” (2002, 80)” It is exactly because the gap of the antinomies is so vast that poetry is not meant to be written with a hammer. Neither does writing consist in a reevaluation of those elements. In short, poetry is not an affirmation of difference, but the surprising beauty of chiming antinomies. We might never transcend them, but it is up to us to put them together. Yet again, this voisinage is not to be identified with the necessity of chance as an eternal return.4 On the contrary it is a return from that very return : Let us treat Yes as a No to No and No as a Yes […] And let us not forget that this pissed affirmation crumbled down Nietzsche’s intellect in the dark paths of this world. (2002, 88) This return from the “vicious circle” should in no way be taken as a form of artistic prudence. Rather it can be seen as a dribble of demonic inconsistency as Dionysus transforms himself into a Christ that is in turn de-theologized: “Who can forbid that? Every man is capable of his own theology, nothing can stop him.” (2002, 73-74) This is a turn towards an existential vision of the world, historically coinciding with a particular political defeat of the Left, to which the poet devoted all his life: after the defeat of the popular front I raised the question “why do we exist?” while others were asking “why we failed.” (2002, 57)5 But most of all it is a return to poetry that exceeds the existential question itself, going beyond the issue of faith. Poetry comes in as a question of return after a defeat that is confessed in full profanity. Though it accepts the necessity of the defeat, it does not affirm it. Though it negates it, the negation is not in the name of a promise to be delivered in the kingdom of heavens. Following a historical and existential defeat, poetry is born post mortem . It signals a return to Christ as “groundless religiousness in the surprise of the real as such” (2002, 72) which is at once a return to the refuge of childhood. It is not a question of endurance towards an eternal return. Rather it is a question on the possibility of an existential return. Returning in a world as someone who cannot enjoy any returns exactly because he is averse to guarantees. A return without returns. *** PHOTOCOPY OF HAPPINESS When I was young I used to pin down cicadas and step on ant nests. I used to stand there silent for hours. With threads I decapitated bees. Now I am a dead man breathing. (Karouzos, 1993, II, 336.) The return to the “paradise of childhood” (2002, 68) constitutes the devouring refuge of its own memory when defeat becomes the synonym of adulthood. The political struggles of a young communist in a country torn up by a civil war right after World War II fraught with incarcerations and exiles. Historically they resulted in the defeat of the communist movement in Greece and opened up a long turbulent road that would peak in the dictatorship of 1967. Existentially they led to a series of disillusionments: mental breakdown, divorce, abandonment of studies in law school. To the question “why do we exist” the answer was poetry. Still this exposé should not be read as a sweeping chronography of a man. For it actually happens to coincide with the historical fate of a nation that after its modern constitution never stopped dreaming of the glories of its past youth, in a present that was (and is) sweepingly disappointing. But isn’t this return to youth finally a way of compensating for a loss of youth that necessarily results in a losing adulthood? Will Greeks, the eternal children of Plato and Nietzsche, ever learn? How to return without dying, how to remember without wasting time? WE ARE IN THE OPEN MEANING Living the coldest mauve night right across Parthenon I went to take a piss on some foliage and I was enjoying the foliage as it was steaming. (Karouzos, 1993, II, 340) Beyond the historical tragedies of modern Greece and away from any personal disappointments, the relation that this land holds with language and history is mediated through the Greek light—whose omnipresence is the very condition of its transcendence. All historical contradictions from Dionysus to Christ took place under this light; all those disseminated dialects were spoken beneath its warmth. To paraphrase Lévinas,6 light is both the condition of the world and of our withdrawal from it—a withdrawal towards the invisibility of God, of the dead, of meta-physics, resulting from the temptation that all is still here, behind this light the visibility of which they once evaded: “birds, the allurement of God.” (1993, I, 17) Under that luminous sky, if Greeks can do anything at all, it is to envision a return that will never come. All they can do is write poetry—which is doing nothing; other than lending an ear to a disseminated language whispering a unity that cannot be promised, as an adulthood in defeat is ready to recognize. Trying “to trap the invisible in visibility” (1993, II, 483) they forget that they have grown up and one day they die—with the promise of return. Hence an additional meaning must be given to this return to childhood. It does not signal salvation but rather its promise. To the ears of an aged continent it means that the return to/of poetry is a losing game, a return without returns. “Europe, Europe… you are nothing more than the continuation of Barabbas.” (1993, I, 295) *** “Life is not there to verify theories.”7 The records show that Karouzos was finally given a second-class pension from the Greek government, at the time when he was being recognized by the literary press as one of Greece’s major contemporary poets. Being neither a bourgeois nor a nobelist, he proclaimed himself to be an anarcho-communist, unconditionally faithful to the utopia of a classless society. He also drank, heavily. “Capitalism made an animal out of man/ Marxism made an animal out of truth/ Shut up.” (1993, II, 369) Perhaps one of the most scandalous divides of our times has been the one between the living and the dead, the latent prohibition that the living should not be concerned with the dead based on the mere impossibility of the dead to be concerned with the living in the first place. What adds to this scandal is that this divide abuses anything that cannot return to us by subsuming it under the same futility. Hence death is no longer “loss” in the usual sense. It no more refers to the things we lost but to our “loss” (of time, money and well-being) as we insist to dwell on them. Death is a waste —of time. It is this waste that we find in the insouciance of Greek expenditure; the waste in dealing with a language that most of its historical part is no longer spoken (a dead language); the waste in translating a poet who is ex definitio untranslatable; the waste of his vision, his money, his life. The waste of dealing with anything that cannot return and that cannot bring in any returns . But it is also the waste of life that poetry itself presupposes, the waste of dealing with invisibility, with anything that is out of this world and thus invokes the fear of death that is in turn—and surprisingly— nowhere to be found. Instead of death, what is there, beyond the light, is the being without us (to recall the Lévinasian il y a ), the mumble of our own nothingness which constitutes the price to be paid for writing poetry under an evergreek light. To understand this to-and-fro, is to realize that poetry is something out of this world that nevertheless takes place in this world, by virtue of this world. But to ridiculously equate this to-and-fro with death as non-existence, is to exile poetry along with its own possibility from this same old world: I do not believe that poetry will ever disappear from this world. […] But I am also sure that it does not have many chances of playing, as you say, a redemptive role in our vertiginous technological future. Without being endangered as a creative need, it will be placed on the side of history. (2002, 32) It is mainly there that we would like to locate the meaning of Nikos Karouzos’s poetry today. If we are willing to include the Greek original it is because we consider that it will be both a waste of time for us to do so (since most of you cannot read Greek) and because it might induce you to the even larger waste of learning it. We would additionally be glad if this small introduction served as an equally wasteful, academically useless piece of reading, gesturing towards a taboo of investing in anything Greek—that is in anything dead among the living, in anything that will never come back and maybe was never here in the first place. This is the only way to reserve for ourselves the possibility of poetry and preserve the light of its promise. “To return: that is the miracle.” (1993, I, 17) Athens, Greece July 10, 2011 NOTES 1 “ Capitale (a Late Latin word based on caput “head”) emerged in the twelfth to thirteenth centuries in the sense of funds, stock of merchandise, sum of money or money carrying interest.[…] The word and the reality it stood for appear in the sermons of St. Bernardino of Siena (1380-1444) ‘… quamdam seminalem rationem lucrosi quam communiter capitale vocamus ’, ‘that prolific cause of wealth that we commonly call capital’” (Braudel, 1992, 232-233). 2 “A great man – a man whom nature has constructed and invented in the grand style – what is he? First : there is a long logic in all of his activity, hard to survey because of its length, and consequently misleading; he has the ability to extend his will across great stretches of his life and to despise and reject everything petty about him, including even the fairest, ‘divinest’ things in the world.” (Nietzsche, 1968, 505, §962) 3 Cf. Deleuze, 1986, 186-9. 4 “Return is the being of becoming, the unity of multiplicity, the necessity of chance: the being of difference as such or the eternal return.” (Deleuze, 189)5 In this 1982 interview Karouzos refers to the defeat of the communist movement in Greece after the civil war of 1946-1949 between the Governmental Army and the Democratic Army of Greece, the military division of the Greek communist party. Karouzos’s father was a member of the communist National Liberation front (EAM) members of which formed the mainl resistance movement (ELAS) in Greece during WWII. The poet was a member of the United Panhellenic Organization of Youth (EPON), which was a youth division of EAM. After the end of the war, ELAS was called to disarmament in view of the formation of a National Army. The members of EAM resigned from the government of national unity and a series of protests led to a 3 year civil war between ELAS and the Government Army. After the defeat of ELAS the Communist party was outlawed and many communists were exiled in deserted Greek islands. Karouzos, who took action in the Greek resistance and was active during the Greek civil war, was exiled in Icaria on 1947 and in Makronisos on 1953 where he was called two years earlier to do his military service. 6 “Existence in the world qua light, which makes desire possible, is then, in the midst of being, the possibility of detaching oneself from being. To enter into being is to link up with objects; it is in effect a bond that is already tainted with nullity. It is already to escape anonymity. In this world where everything seems to affirm our solidarity with the totality of existence, where we are caught up in the gears of a universal mechanism, our first feeling, our ineradicable illusion, is a feeling or illusion of freedom. To be in the world is this hesitation, this interval in existing, which we have seen in the analyses of fatigue and the present.” (Lévinas, 1988,43-4) 7from a TV interview. THE POETRY OF NIKOS KAROUZOS From Redwriter [ Ερυθρογρ?φος ], in Collected Works, Vol . II, Athens: Ikaros. 1993, 463-4. [Athens: Apopeira, 1990, 9-10.] JESUS ANTI-OEDIPUS* Why were we once saving till the fifth day the Paschal lamb? The scriptures say: with this victim’s meat we ought to cleanse all of our senses. To give life to the whitest wave miraculous odors in the extension of the chest. Ideals to death. For us to witness the illustrious dawns of Absinthe and for the soul to be a deeply carved ornament on the fore we named will. Then many deer running amidst the evergreen growth with watery hymns, then, the unintended angels descending with heights spiraling in their momentum offer themselves to the luminous Adventure. Whence the need for speech and our sufferings covered with flags like the glorified dead. An incorporeal finger pointing at the flamboyant and fragrant holocausts within the tired horizons and the exhausted breadths with joys of the mistletoe on fire and shivering all of the green-leaved love. Something would have chirped again had we not driven it away— maybe the ewe’s grass. Something would have called us to the eternal resurrection— maybe the grace of spring. But now our heart is fiercely blinded, withdrawn to the appearances of Hades. Silence and ice incessantly cover the Infant Spirit in thatched times. While the cherry trees are dreaming faintly glowing in absolute darkness there’s nothing the Babylonians can contemplate in labs with automatic colored lights. How to rejoice now in the fifth day of the lamb? We have forked the stars. We’ve gradually become supposedly sublime with plucked chimeras in our hands. Avenged relentlessly by science. *Though the poem appears in a 1990 collection, it was actually written in 1968. Hence the reader must be aware in not associating Karouzos’ Anti-Oedipus with the famous 1972 work of Deleuze and Guattari, given that the former precedes the latter. ΙΗΣΟΥΣ ΑΝΤΙ-ΟΙΔΙΠΟΥΣ Γιατ? κρατο?σαμε κ?ποτε ?ς την π?μπτη μ?ρα το πασχαλιν? πρ?βατο; Τα κε?μενα λ?νε: μ’ αυτο? του θ?ματος το κρ?ας ?πρεπε να καθαρ?σουμε ?λες τις αισθ?σεις. Για να δ?σουμε κ?μα στη ζω? λευκ?τατο θαυμ?σιες ευωδι?ς στην ?κταση του στ?θους. Ιδανικ? στο χ?ρο. Για να βλ?πουμε τα λαμπρ? χαρ?ματα του ?ψινθου και να ’ναι η ψυχ? στ?λισμα βαθυχ?ρακτο της πλ?ρης που την ε?παμε θ?ληση. Τ?τε πολλ?ς δορκ?δες τρ?χοντας αν?μεσα στην καταπρ?σινη φ?ση με τους υδ?τινους ?μνους, τ?τε, κατεβα?νοντας οι αθ?λητοι ?γγελοι με κυλινδο?μενο το ?ψος στην ορμ? τους χαρ?ζονται της αστραφτερ?ς Περιπ?τειας. ?θεν η μιλι? γι’ αυτ? χρει?ζεται και τα δειν? σκεπ?ζονται ωσ?ν τους τιμημ?νους νεκρο?ς με σημα?ες. Ασ?ματο δ?χτυλο δε?χνει τα φλογ?δη και μοσχοβ?λα ολοκαυτ?ματα στους κουρασμ?νους ορ?ζοντες στα εξουθενωμ?να πλ?τη καθ?ς αν?βουν οι χαρ?ς του νερα?δ?ξυλου και τρ?μει ολ?κληρη η πρασιν?φυλλη αγ?πη. Κ?τι θα κελαηδο?σε π?λι αν δεν το δι?χναμε— μπορε? της προβατ?νας το χορτ?ρι. Κ?τι θα μας καλο?σε στην απ?ραντη αν?σταση— μπορε? του ?αρος η χ?ρη. Μα η καρδι? μας ?γρια τυφλ?θηκε π?ρασε στα φαιν?μενα του ?δη. Σιγ? και π?γος αδι?κοπα σκεπ?ζει στους αχυρ?νιους καιρο?ς το Ν?πιο Πνε?μα. Την ?ρα που ονειρε?ονται οι βυσσινι?ς και λ?μπουν αμυδρ? μεσ’ στο απλ?τατο σκοτ?δι τ?ποτα δε στοχ?ζονται οι βαβυλ?νιοι στα εργαστ?ρια με τ’ αυτ?ματα χρωματιστ? φ?τα. Π?ς να χαρο?με πια την π?μπτη μ?ρα του προβ?του; Φουρκ?σαμε τ’ αστ?ρια. Γ?ναμε σιγ?-σιγ? δ?θεν υπ?ροχοι με μαδημ?νες χ?μαιρες στα χ?ρια. Μας ν?μεται σκληρ? η επιστ?μη. From: Redwriter [Ερυθρογρ?φος], in Collected Works, Vol. II, Athens: Ikaros. 1993, 472. [Athens: Apopeira, 1990, 18.] DIALECTΙCS OF SPRING Christ the straight angle; Christ the Pythagorean theorem. Christ the infinitesimal calculus from above the blessed Sets Christ. Christ the tessellation of massive particles Christ the zero mass. Hence we spray numbers and fields of lust. We are carabineers of diseased logic plus something— Observed means observer and Hekate The darkness luminous and light in the dark Astarte banqueters demons from today. ΔΙΑΛΕΚΤΙΚΗ ΤΟΥ ΕΑΡΟΣ Χριστ?ς η ορθ? γων?α· Χριστ?ς το πυθαγ?ριο θε?ρημα. Χριστ?ς ο απειροστικ?ς λογισμ?ς ?νωθεν ?λβια Χριστ?ς τα Σ?νολα. Χριστ?ς η ψηφιδογραφ?α στα μαζικ? σωμ?τια Χριστ?ς η μ?ζα μηδ?ν. ?ρα ψεκ?ζουμε αριθμο?ς και πεδ?α λαγνε?ας. Ε?μαστε τυφεκιοφ?ροι νοσο?σης λογικ?ς και κ?τι-- παρατηρο?μενο σημα?νει παρατηρητ?ς και Εκ?τη σκ?τος το π?μφωτο και φως εν τ? σκοτ?? η Αστ?ρτη συνδαιτημ?νες δα?μονες απ’ ?ρτι. From: Redwriter [Ερυθρογρ?φος], Athens: Apopeira, 1990, 18. [1993, II, 472]. CREDO (as we are used to say in Latin) Α I believe in one Poet expelled from heavens / fugitive from the god and vagabond, Empedocles / and here on earth / exile on the earth etc. of Baudelaire /. Β I believe in one Computer inside thunder and through matter. Γ Suffering undefiled / substantive / the Poet uplifts himself slow-burning suicidal implying lengthy sleeps. Δ Cutting down on prospective mistakes. Ε Of all things visible and invisible officiating the onion-peelings. Ζ The Poet has nothing / see the departed /. Η I believe in one Poet that says: madness I enjoy; he ridicules existence; let me light up from my mana. Θ Syntax he doesn’t care about when musicality commands him. Along with still more licenses, and Ts are played according to the concept sound anywhere. E.g. the winters here, he winters there; it will not come—I will not rest, etc. etc. Ι The Poet exercises thought until it’s stripped down. Κ And if he’s Greek he must always study the fineness of Attica, in light, mountains, fields and sea. For this fineness teaches language. Λ And if he’s deeply destined the Poet expresses the unexplainable of the explained; he happens to be a rightful heir to the scientist and his predecessor. Μ On the froth he does not last; the Poet blusters at the bottom of the pot. Ν Flamebred and never redeemed. Ξ The Poet must sometimes say: what a consumption of presence — be a bit lonely for a change! Ο The Poet is twilit. Π He is susceptible of deaths and resurrections. Ρ He looks from the corner of his eye and exists in a glance. Σ He follows behind the mother. Τ Eveningless when it comes to age. Υ I believe in one Poet who says: let the purities coincide. Until the Corinth of the Universe or even further. Φ In a higher despair. Χ In a brighter quintessence. Ψ In one sensation that lifts off. Ω Forgiving everyone. CREDO (ως ε?θισται να λ?με λατινιστ?) Α Πιστε?ω εις ?να Ποιητ?ν εκτ?ς ουρανο? / φυγ?ς θε?θεν και αλ?της, Εμπεδοκλ?ς / και επ? της γης / εξ?ριστος π?νω στη γη κ.λπ. του Βωδελα?ρου /. Β Πιστε?ω εις ?να Υπολογιστ?ν εντ?ς κεραυνο? και δια της ?λης. Γ Υποφ?ροντας ?χραντα / ουσιαστικ?ν / ο Ποιητ?ς ανατε?νεται βραδυφλεγ?ς αυτ?χειρας εξυπακο?οντας πολ?ωρους ?πνους. Δ Τα υποψ?φια λ?θη λιγοστε?οντας. Ε Ορατ?ν τε π?ντων και αορ?των ιερουργ?ντας την αποκρομμ?ωση. Ζ Ο Ποιτ?ς ?χει τ?ποτα / βλ?πε τους αναχωρ?σαντες /. Η Πιστε?ω εις ?να Ποιητ?ν που λ?ει: η τρ?λα μ’ αρ?σει· γελοιοποιε? την ?παρξη· ας αν?ψω απ’ τη μ?να μου. Θ Συνταχτικ? δεν το γνοι?ζεται στην προσταγ? της μουσικ?τητας. Μαζ? και μ’ ?λλες ακ?μη λευτερι?ς, και τα νυ πα?ζονται κατ? την ?ννοια ?χος οπουδ?ποτε. Π.χ. τον χειμ?να εδ?, το χειμ?να εκε?· δε θ? ’ρθει – δεν θα καταλαγι?σουμε, κ. λπ. κ.λπ. Ι Ο Ποιητ?ς γυμν?ζει τη σκ?ψη σε απογ?μνωση. Κ Κι αν ε?ναι ?λληνας οφε?λει να σπουδ?ζει π?ντοτε της Αττικ?ς τη λεπτ?τητα, σε φως, βουν?, χωρ?φια και θ?λασσα. Διδ?σκει γλ?σσα η λεπτ?τητα το?τη. Λ Κι αν ε?ναι βαθι? πεπρωμ?νος ο Ποιητ?ς εκφρ?ζει το ανεξ?γητο του εξηγητο?· τυγχ?νει ν?μιμος δι?δοχος του επιστ?μονα και προκ?τοχ?ς του. Μ Στον αφρ? δεν ?χει δι?ρκεια· στο πατοκ?ζανο μα?νεται ο Ποιητ?ς. Ν Φλογοδ?αιτος και ποτ? ξελυτρωμ?νος. Ξ Ο Ποιητ?ς κ?ποτε πρ?πει να λ?ει: μεγ?λη καταν?λωση παρουσ?ας – γενε?τε και λ?γο μοναξι?ρηδες! Ο Ο Ποιητ?ς ε?ναι αμφ?φλοξ. Π Επιδ?χεται θαν?τους και αναστ?σεις. Ρ Ακροθωρ?ζει και υπ?ρχει σε ξαφνοκο?ταγμα. Σ Ε?ναι ουραγ?ς της μητ?ρας. Τ Αν?σπερος απ? ηλικ?α. Υ Πιστε?ω εις ?να Ποιητ?ν που λ?ει: να συμπ?σουν οι αγν?τητες. Μ?χρι την Κ?ρινθο του Σ?μπαντος ? μακρ?τερα. Φ Σε αν?τερη απελπισ?α. Χ Σε φαειν?τερη πεμπτουσ?α. Ψ Σε μια α?σθηση που πτηνο?ται. Ω Συγχωρ?ντας τους π?ντες. From Large Sized Logic [ Λογικ? μεγ?λου σχ?ματος ], Athens: Erato, 1989, n.p. [1993, II, 521-3]. (shrink)

Against the backdrop of the frequent comparison of theories of truth in the literature on semantic paradoxes with regard to which inferences and metainferences are deemed valid, this paper develops a novel approach to defining a binary predicate for representing the valid inferences and metainferences of a theory within the theory itself under the assumption that the theory is defined with a classical meta-theory. The aim with the approach is to obtain a tool which facilitates the comparison between a theory (...) and its competitors within the theory itself, thereby expressing the disagreement between the theories within the theories. After discussing what we can and should require of an object-linguistic representation of a theory for that purpose, this paper proposes to restrict the representation of valid metainferences to locally valid metainferences, a requirement which turns out to be \-consistent and conservative over classical first-order arithmetic. This approach is then applied to four theories definable on strong Kleene models using a labelled nested sequent calculus. (shrink)

This thesis is about the metaphysics of logic. I argue against a view I refer to as ‘logical realism’. This is the view that the logical constants represent a particular kind of metaphysical structure, which I dub ‘logico-metaphysical structure’. I argue instead for a more metaphysically lightweight view of logic which I dub ‘logical expressivism’. -/- In the first part of this thesis (Chapters I and II) I argue against a number of arguments that Theodore Sider has given for logical (...) realism. In Chapter I, I present an argument of his to the effect that logico-metaphysical structure provides the only good explanation of the semantic determinacy of the logical constants. I argue that other explanations are possible. In Chapter II, I present another argument of his to the effect that logico-metaphysical structure is something that comes along with ontological realism: the view that there is a non-language-relative fact of the matter about what exists. I argue that the connection between logical and ontological realism is not as close as Sider makes it out to be. -/- In the second part of this thesis (Chapters III – V) I set out a positive view of the logical constants that can explain both why their meanings are semantically determinate, and why they form part of our vocabulary. On that view, the primary bearers of logical structure are propositional attitudes, and the logical constants are in our language as vehicles for the expression of logically complex propositional attitudes. In Chapter III, I set out an expressivist theory of propositional logic. In Chapter IV, I use this theory to explain how the logical connectives end up having determinate meanings. In Chapter V, I extend the expressivist theory to predicate logic. (shrink)

Reuben Louis Goodstein (1912-1985) foi aluno de Wittgenstein em Cambridge de 1931 a 1934. Neste artigo, faço uma breve descrição de seu trabalho na lógica matemática, no qual se percebe a influência das idéias de Wittgenstein, inclusive a substituição, em seu cálculo equacional, da indução matemática por uma regra de unicidade de uma função definida por uma função recursiva. Esse último aspecto se encontra no Big Typescript de Wittgenstein. Também mostro que as idéias fundamentais do cálculo equacional podem ser encontradas (...) não apenas no período intermediário, mas, in nuce, nas observações sobre matemática do Tractatus Logico-philosophicus. A partir disso, procuro desenvolver um argumento contra uma leitura corrente daquele livro, o assim chamado “Novo Wittgenstein”. Outra conexão entre Goodstein e Wittgenstein se encontra na rejeição da teoria da quantificação; na parte final do artigo, recorro às observações críticas de Goodstein sobre a Lei do Terceiro Excluído (que também incluem uma crítica a Brouwer e à sua rejeição “pela metade” dessa lei) para lançar luz sobre as observações do próprio Wittgenstein a esse respeito. (shrink)

The epsilon calculus is a logical formalism developed by David Hilbert in the service of his program in the foundations of mathematics. The epsilon operator is a term-forming operator which replaces quantifiers in ordinary predicate logic. Specifically, in the calculus, a term εx A denotes some x satisfying A(x), if there is one. In Hilbert's Program, the epsilon terms play the role of ideal elements; the aim of Hilbert's finitistic consistency proofs is to give a procedure which removes (...) such terms from a formal proof. The procedures by which this is to be carried out are based on Hilbert's epsilon substitution method. The epsilon calculus, however, has applications in other contexts as well. The first general application of the epsilon calculus was in Hilbert's epsilon theorems, which in turn provide the basis for the first correct proof of Herbrand's theorem. More recently, variants of the epsilon operator have been applied in linguistics and linguistic philosophy to deal with anaphoric pronouns. (shrink)

This handbook with exercises reveals the mathematical beauty of formalisms hitherto mostly used for software and hardware design and verification.

Two years ago, a nest box outside my window held a pair of Violet-Green Swallow. I counted six swallows fledge from the box and take their first flights in the July rain. Leaving the roof of the nest box, they flew in little loops out over the water, trying out their wings. I watched them from the dock, their bodies suspended in the air between the raindrops. This experience was the inspiration for what I call ‘nest-works’ – for poetic wilding (...) of all-too-human spaces. Nest-works began with an experimental panel for the 2021 College Art Association Conference, called ‘Co-Making this World’. The experimental session was modelled after the nest of a bird, a Black-Capped Chickadee. As this cavity-nester builds a home of disparate materials, the panel of artist-researchers built a session of disparate theories and practices, as we considered relationships with world-systems that are in the process of making (such as the nest of the chickadee). For Technoetic Arts, we weave a new nest-work of research material, as we consider new models for knowledge and creative production. This nest-work is an entanglement of short essays made by artists working with a common pattern, framing eco-poetics on collaborative and participatory processes with the non-human/more-than-human. (shrink)

A mathematical model in science can be formulated as a counterfactual conditional, with the model’s assumptions in the antecedent and its predictions in the consequent. Interestingly, some of these models appear to have assumptions that are metaphysically impossible. Consider models in ecology that use differential equations to track the dynamics of some population of organisms. For the math to work, the model must assume that population size is a continuous quantity, despite that many organisms are necessarily discrete. This means our (...) counterfactual representation of the model can have an impossible antecedent, giving us a counterpossible. Analogous counterpossibles arise in other sciences, as we’ll see. According to a prominent view in counterfactual semantics, the vacuity thesis, all counterpossibles are vacuously true, that is, true merely because their antecedents are necessarily false. But some counterpossible formulations of differential equation models in science are not all vacuously true—some are non-vacuously true, and some are false. I go on to show how an alternative semantics, one that employs impossible worlds, can deliver this judgment. (shrink)

Because of the “all-or-none” character of nervous activity, neural events and the relations among them can be treated by means of propositional logic. It is found that the behavior of every net can be described in these terms, with the addition of more complicated logical means for nets containing circles; and that for any logical expression satisfying certain conditions, one can find a net behaving in the fashion it describes. It is shown that many particular choices among possible neurophysiological assumptions (...) are equivalent, in the sense that for every net behaving under one assumption, there exists another net which behaves under the other and gives the same results, although perhaps not in the same time. Various applications of the calculus are discussed. (shrink)

A nested mode ontology allows one to make sense of apparently contradictory Christological claims such as that Christ knows everything and there are some things Christ does not know.

We give a novel proof that primitive recursive functions are closed under nested simple recursion. This new presentation is supplied with a detailed proof which can be easily formalized in small fragments of Peano Arithmetic.

Although Aristotle (Metaphysics, Book IV, Chapter 2) was perhaps the first person to consider the part-whole relationship to be a proper subject matter for philosophic inquiry, the Polish logician Stanislow Lesniewski [15] is generally given credit for the first formal treatment of the subject matter in his Mereology.1 Woodger [30] and Tarski [24] made use of a specific adaptation of Lesniewski's work as a basis for a formal theory of physical things and their parts. The term 'calculus of individuals' (...) was introduced by Leonard and Goodman [14] in their presentation of a system very similar to Tarski's adaptation of Lesniewski's Mereology. Contemporaneously with Lesniewski's development of his Mereology, Whitehead [27] and [28] was developing a theory of extensive abstraction based on the two-place predicate, 'x extends over y\ which is the converse of 'x is a part of y\ This system, according to Russell [22], was to have been the fourth volume of their Pήncipia Mathematica, the never-published volume on geometry. Both Lesniewski [15] and Tarski [25] have recognized the similarities between Whitehead's early work and Lesniewski's Mereology. Between the publication of Whitehead's early work and the publication of Process and Reality [29], Theodore de Laguna [7] published a suggestive alternative basis for Whitehead's theory. This led Whitehead, in Process and Reality, to publish a revised form of his theory based on the two-place predicate, 'x is extensionally connected with y\ It is the purpose of this paper to present a calculus of individuals based on this new Whiteheadian primitive predicate. (shrink)

The calculus of Natural Calculation is introduced as an extension of Natural Deduction by proper term rules. Such term rules provide the capacity of dealing directly with terms in the calculus instead of the usual reasoning based on equations, and therefore the capacity of a natural representation of informal mathematical calculations. Basic proof theoretic results are communicated, in particular completeness and soundness of the calculus; normalisation is briefly investigated. The philosophical impact on a proof theoretic account of (...) the notion of meaning is considered. (shrink)