We show that arbitrary tautologies of Johansson’s minimal propositional logic are provable by “small” polynomial-size dag-like natural deductions in Prawitz’s system for minimal propositional logic. These “small” deductions arise from standard “large” tree-like inputs by horizontal dag-like compression that is obtained by merging distinct nodes labeled with identical formulas occurring in horizontal sections of deductions involved. The underlying geometric idea: if the height, h(∂), and the total number of distinct formulas, ϕ(∂), of a given tree-like deduction ∂ of a minimal (...) tautology ρ are both polynomial in the length of ρ, |ρ|, then the size of the horizontal dag-like compression ∂ᶜ is at most h(∂)×ϕ(∂), and hence polynomial in |ρ|. That minimal tautologies ρ are provable by tree-like natural deductions ∂ with |ρ|-polynomial h(∂) and ϕ(∂) follows via embedding from Hudelmaier’s result that there are analogous sequent calculus deductions of sequent ⇒ρ. The notion of dag-like provability involved is more sophisticated than Prawitz’s tree-like one and its complexity is not clear yet. Our approach nevertheless provides a convergent sequence of NP lower approximations of PSPACE-complete validity of minimal logic. (shrink)

This paper is a continuation of dag-like proof compression research initiated in [9]. We investigate proof compression phenomenon in a particular, most transparent case of propositional DNF Logic. We define and analyze a very efficient semi-analytic sequent calculus SEQ*0 for propositional DNF. The efficiency is achieved by adding two special rules CQ and CS; the latter rule is a variant of the weakened substitution rule WS from [9], while the former one being specially designed for DNF sequents. We show that (...) dag-like SEQ*0 has good deterministic proof search strategy. Furthermore, we expose six examples showing that dag-like deducibility in SEQ*0 admits exponential-size proof compression, as compared to familiar proof systems like cutfree sequent calculi, resolution and cutting plane proof systems. (shrink)

Veloso-Pereira-Haeusler_On-what-there-must-be.

The introduction and elimination rules for material implication in natural deduction are not complete with respect to the implicational fragment of classical logic. A natural way to complete the system is through the addition of a new natural deduction rule corresponding to Peirce's formula → A) → A). E. Zimmermann [6] has shown how to extend Prawitz' normalization strategy to Peirce's rule: applications of Peirce's rule can be restricted to atomic conclusions. The aim of the present paper is to extend (...) Seldin's normalization strategy to Peirce's rule by showing that every derivation Π in the implicational fragment can be transformed into a derivation Π' such that no application of Peirce's rule in Π' occurs above applications of →-introduction and →-elimination. As a corollary of Seldin's normalization strategy we obtain a form of Glivenko's theorem for the classical {→}-fragment. (shrink)

A lógica não contém teoremas puramente existenciais: as únicas sentenças existenciaisválidas são aquelas com análogas universais válidas. Aqui, mostramos que istorealmente é assim quando corretamente interpretado: toda validade ex- istencial possuiuma análoga universal simples, que também é válida. Também caracterizamos validadesuniversais e existenciais em termos de tautologias.

Sambin [6] proved the normalization theorem for GL, the modal logic of provability, in a sequent calculus version called by him GLS. His proof does not take into account the concept of reduction, commonly used in normalization proofs. Bellini [1], on the other hand, gave a normalization proof for GL using reductions. Indeed, Sambin's proof is a decision procedure which builds cut-free proofs. In this work we formalize this procedure as a recursive function and prove its recursiveness in an arithmetically (...) formalizable way, concluding that the normalization of GL can be formalized in PA. MSC: 03F05, 03B35, 03B45. (shrink)

The relation between ex falso and disjunctive syllogism, or even the justification of ex falso based on disjunctive syllogism, is an old topic in the history of logic. This old topic reappears in contemporary logic since the introduction of minimal logic by Johansson. The disjunctive syllogism seems to be part of our general non-problematic inferential practices and superficially it does not seem to be related to or to depend on our acceptance of the frequently disputable ex falso rule. We know (...) that the acceptance of the ex falso is a sufficient condition for the acceptance of the disjunctive syllogism, but the interesting question is: is the ex falso a necessary condition for the acceptance of the disjunctive syllogism? The aim of the present paper is to discuss some possible ways to define systems that combines the preservation of the disjunctive syllogism with the rejection of the ex falso. (shrink)

A theory of magnitudes involves criteria for their equivalence, comparison and addition. In this article we examine these aspects from an abstract viewpoint, by focusing on the so-called De Zolt’s postulate in the theory of equivalence of plane polygons (“If a polygon is divided into polygonal parts in any given way, then the union of all but one of these parts is not equivalent to the given polygon”). We formulate an abstract version of this postulate and derive it from some (...) selected principles for magnitudes. We also formulate and derive an abstract version of Euclid’s Common Notion 5 (“The whole is greater than the part”), and analyze its logical relation to the former proposition. These results prove to be relevant for the clarification of some key conceptual aspects of Hilbert’s proof of De Zolt’s postulate, in his classicalFoundations of Geometry(1899). Furthermore, our abstract treatment of this central proposition provides interesting insights for the development of a well-behaved theory ofcompatiblemagnitudes. (shrink)

_Seeing the World through Children’s Eyes_ brings an overarching emphasis on ‘seeing’ to early years research and provides an opportunity to see and hear from leading researchers in the field concerning how they work with visual methodologies in their early years research.

Standard models of adolescent risk taking posit that the cognitive abilities of adolescents and adults are equivalent, and that increases in risk taking that occur during adolescence are the result of socio emotional differences in impulsivity, sensation seeking, and lack of self-control. Fuzzy-trace theory incorporates these socio emotional differences. However, it predicts that there are also cognitive differences between adolescents and adults, specifically that there are developmental increases in gist-based intuition that reflects understanding. Gist understanding, as opposed to verbatim-based analysis, (...) generally has been hypothesized to have a protective effect on risk taking in adolescence. Gist understanding is also an essential element of informed consent regarding risks in medical decision- making. Evidence thus supports the argument that adolescents’ status as mature minors should be treated as an exception rather than a presumption, because accuracy in verbatim analysis is not mature gist understanding. Use of the exception should be accompanied by medical experts’ input on the bottom-line gist of risks involved in treatment. (shrink)

Introducing Dialogic Pedagogy presents some of the ideas of Russian philosopher Mikhail Bakhtin concerning dialogism in a way that will engage and inspire those studying early childhood education. By translating the growing body of dialogic scholarship into a practical application of teaching and learning with very young children, this book provides readers with alternative ways of examining, engaging and reflecting on practice in the early years to provoke new ways of understanding and enacting pedagogy. This text combines important theoretical ideas (...) with a practical application to support practitioners who are keen to promote creativity and agency through ethical self-other relations. It provides unique insights into the amazing world of the youngest child, and offers enriched understandings of the profound impact of adults in their journey of becoming (or bildung). Key points covered include: Investigating dialogic philosophy and its application to early childhood education, with an emphasis on notions of justice, democracy, ethics and answerability Considering the relationship between dialogism and pedagogical approaches Theorising a range of approaches to relevant early childhood practice, as pedagogy This accessible and readable guide offers sound theoretical principles with practical suggestions for early years' settings. The book is supplemented by an extensive online video resource website that will bring these revolutionary ideas to life.. (shrink)

The foundation of the Christian counselling movement -- Christian counselling in the UK -- The aims of Christian counselling -- Integrating psychological and biblical truth -- Sigmund Freud--the founding father of psychotherapy -- The individual psychology of Alfred Adler -- Abraham Maslow--the man with new age tendencies -- Carl Rogers--a man who believed in himself -- Albert Ellis--the aggressive atheist -- The Bible's verdict on psychological 'truth' -- The case against Larry Crabb -- Self-esteem: the secular foundation -- Self-esteem and (...) the Christian counselling movement -- Self-esteem dogma in the light of scripture. (shrink)

We upgrade [3] to a complete proof of the conjecture NP = PSPACE that is known as one of the fundamental open problems in the mathematical theory of computational complexity; this proof is based on [2]. Since minimal propositional logic is known to be PSPACE complete, while PSPACE to include NP, it suffices to show that every valid purely implicational formula ρ has a proof whose weight and time complexity of the provability involved are both polynomial in the weight of (...) ρ. As is [3], we use proof theoretic approach. Recall that in [3] we considered any valid ρ in question that had a “short” tree-like proof π in the Hudelmaier-style cutfree sequent calculus for minimal logic. The “shortness” means that the height of π and the total weight of different formulas occurring in it are both polynomial in the weight of ρ. However, the size, and hence also the weight, of π could be exponential in that of ρ. To overcome this trouble we embedded π into Prawitz’s proof system of natural deductions containing single formulas, instead of sequents. As in π, the height and the total weight of different formulas of the resulting tree-like natural deduction ∂1 were polynomial, although the size of ∂1 still could be exponential, in the weight of ρ. In our next, crucial move, ∂1 was deterministically compressed into a “small”, although multipremise, dag-like deduction ∂ whose horizontal levels contained only mutually different formulas, which made the whole weight polynomial in that of ρ. However, ∂ required a more complicated verification of the underlying provability of ρ. In this paper we present a nondeterministic compression of ∂ into a desired standard dag-like deduction ∂0 that deterministically proves ρ in time and space polynomial in the weight of ρ.2 Together with [3] this completes the proof of NP = PSPACE.Natural deductions are essential for our proof. Tree-to-dag horizontal compression of π merging equal sequents, instead of formulas, is not sufficient, since the total number of different sequents in π might be exponential in the weight of ρ – even assuming that all formulas occurring in sequents are subformulas of ρ. On the other hand, we need Hudelmaier’s cutfree sequent calculus in order to control both the height and total weight of different formulas of the initial tree-like proof π, since standard Prawitz’s normalization although providing natural deductions with the subformula property does not preserve polynomial heights. It is not clear yet if we can omit references to π even in the proof of the weaker result NP = coNP. (shrink)

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

We present a categorical/denotational semantics for the Lambek Syntactic Calculus , indeed for a λlD-typed version Curry-Howard isomorphic to it. The main novelty of our approach is an abstract noncommutative construction with right and left adjoints, called sequential product. It is defined through a hierarchical structure of categories reflecting the implicit permission to sequence expressions and the inductive construction of compound expressions. We claim that Lambek's noncommutative product corresponds to a noncommutative bi-endofunctor into a category, which encloses all categories of (...) such hierarchical structure. A soundness theorem for LSC is shown with respect to this semantical framework. (shrink)

One of the main problems in computer science is to ensure that programs are implemented in such a way that they satisfy a given specification. There are many studies about methods to prove correctness of programs. This work presents a method, belonging to the constructive synthesis or proofs-as-programs paradigm, that comes from the Curry-Howard isomorphism and extracts the computational contents of intuitionist proofs. The synthesis process proposed produces a program in an imperative language from a proof in many-sorted intuitionist logic, (...) where the axioms define the abstract data types, using Natural Deduction as deductive system. It is proved the correctness, as well as the completeness of the method regarding the Heyting arithmetic with ω-rule . A discussion about the use of the finitary induction instead of computational ω-rule concludes the work. (shrink)

In our previous work we proved the conjecture NP = PSPACE by advanced proof theoretic methods that combined Hudelmaier’s cut-free sequent calculus for minimal logic with the horizontal compressing in the corresponding minimal Prawitz-style natural deduction. In this Addendum we show how to prove a weaker result NP = coNP without referring to HSC. The underlying idea is to omit full minimal logic and compress only “naive” normal tree-like ND refutations of the existence of Hamiltonian cycles in given non-Hamiltonian graphs, (...) since the Hamiltonian graph problem in NPcomplete. Thus, loosely speaking, the proof of NP = coNP can be obtained by HSC-elimination from our proof of NP = PSPACE. (shrink)

The Great Psychotherapy Debate: Models, Methods, and Findings comprehensively reviews the research on psychotherapy to dispute the commonly held view that the benefits of psychotherapy are derived from the specific ingredients contained in a given treatment (medical model). The author reviews the literature related to the absolute efficacy of psychotherapy, the relative efficacy of various treatments, the specificity of ingredients contained in established therapies, effects due to common factors, such as the working alliance, adherence and allegiance to the therapeutic protocol, (...) and effects that are produced by different therapists. In each case, the evidence convincingly corroborates the contextual model and disconfirms the prevailing medical model. (shrink)

The second edition of The Great Psychotherapy Debate has been updated and revised to include a history of healing practices, medicine, and psychotherapy, an expanded theoretical presentation of the contextual model, an examination of therapist effects, and a thorough review of the research on common factors such as the alliance, expectations, and empathy.

Truth depends in some sense on reality. But it is a rather delicate matter to spell this intuition out in a plausible and precise way. According to the theory of truth-making this intuition implies that either every truth or at least every truth of a certain class of truths has a so-called truth-maker, an entity whose existence accounts for truth. This book aims to provide several ways of assessing the correctness of this controversial claim. This book presents a detailed introduction (...) to the theory of truth-making, which outlines truth-maker relations, the ontological category of truth-making entities, and the scope of a truth-maker theory. The essays brought together here represent the most important articles on truth-making in the last three decades as well as new essays by leading researchers in the field of the theory of truth and of truth-making. (shrink)

Big Ideas for Little Kids includes everything a teacher, a parent, or a college student needs to teach philosophy to elementary school children from picture books. Written in a clear and accessible style, the book explains why it is important to allow young children access to philosophy during primary-school education. Wartenberg also gives advice on how to construct a "learner-centered" classroom, in which children discuss philosophical issues with one another as they respond to open-ended questions by saying whether they agree (...) or disagree with what others have said. (shrink)

In 'Een handvol filosofen' staan de filosofen centraal die sinds de oprichting van de Vrije Universiteit in 1880 aan deze instelling verbonden zijn geweest. Het gaat hierbij niet alleen om de inhoud van hun werk, maar ook om de personen zelf. Er waren filosofiedocenten die zich met de universiteit identificeerden en zich volledig konden ontplooien. Er waren er echter ook voor wie dit niet gold, die geïsoleerd of in gewetensnood raakten. Veel filosofiestudenten waren actief betrokken bij wat er in hun (...) faculteit gebeurde. Zij namen initiatieven, protesteerden soms tegen de gang van zaken en kozen partij in conflictsituaties. Sinds het eind van de jaren zestig van de twintigste eeuw verloor de Vrije Universiteit geleidelijk haar christelijk karakter. Tegenwoordig werken alle stafleden vanuit hun eigen motivatie mee aan een hoofdzakelijk seculier geworden universiteit, die ruimte biedt voor religieuze en levensbeschouwelijke diversiteit. (shrink)

Modern scholars have been concerned with the hostility shown to Alexander by the Hellenistic schools of philosophy. Two literary portraits have been distinguished, the Peripatetic and the Stoic, the former deriving from Theophrastus' book on Callisthenes, or starting with this work the Peripatetics worked out a theory of and applied it to Alexander, in order to belittle his achievements. It was a case of giving sophisticated expression to the kind of crude resentment expressed by Demades.

English summary: Marc Andre Wiegand analyzes the neo-Kantian premises of Gustav Radbruch's legal philosophy.

The locus classicus for Plutarch's own views on his methods is in the Alexander He has begun by asking for the indulgence of his readers if they do not find all the exploits of Alexander and Caesar recounted by the biographer or if they discover him not reporting some famous incident in detail (); and he goes on to compare his own search for evidence which will indicate the kind of soul, with the activity of the painter, who, in order (...) to create a likeness, concentrates on the eyes and pays little attention to the other parts. Commentators and critics have been right to take this as a key text for the purpose of understanding Plutarch's attitude towards his biographical work; nevertheless there are other passages in the Lives where we can at least glimpse his attitude to his subject, and we can only see the Alexander-remarks in correct perspective if we take these other passages into account. I propose therefore, starting with the Alexander, to see how far these critical remarks apply to Plutarch's theory and practice elsewhere in the Lives. (shrink)

Shrek! focuses on an issue in the philosophy of language, a relatively new area of philosophical investigation that first emerged during the twentieth century. Some philosophers disagree with the claim that you cannot separate the descriptive and evaluative elements of linguistic statements. This is because they take descriptive statements to be the basic elements of language, to which our subjective attitudes get attached later in a contingent manner. At its most basic level language presents a symbolic picture of facts in (...) the world. Shrek! presents what philosophers call a thought experiment that purports to show that the descriptive and evaluative contents of sentences are really distinct. The chapter ends by suggesting how to discuss the philosophy of language with children. (shrink)

In Daniel Manus Pinkwater's quirkily illustrated book, The Big Orange Splot, a strange accident leads a man to change his life. The book presents an important claim that the existentialists and other philosophers have embraced: That the life of conformity is one that people ought to avoid, despite its attractiveness. Instead of living a life just like everyone else and fulfilling expectations that others have for us, our lives should resemble the transformed facades of all the homes on Mr. Plumbean's (...) street: reflections of our own, individual dreams. (shrink)

The chapter talks about Shel Silverstein's The Giving Tree, which is a favorite of many children, adults, and teachers. The story of a relationship between a boy and a tree is charming for, despite the vicissitudes of the relationship, the two end up together at the end, with the boy — now an old man — sitting contentedly on the tree — itself reduced to a mere stump. The book raises an important issue in the field of environmental ethics. It (...) asks us to recognize that between childhood and old age, people operating within the Western tradition of ethics are not mindful of the value that the non‐human beings in their environment have for them as well as for future generations. Harkening to such warnings, environmental ethicists have attempted to raise important issues about our relationship with the other beings that make up our world. (shrink)