This article presents a parametrized functional interpretation. Depending on the choice of two parameters one obtains well-known functional interpretations such as Gödel's Dialectica interpretation, Diller-Nahm's variant of the Dialectica interpretation, Kohlenbach's monotone interpretations, Kreisel's modified realizability, and Stein's family of functional interpretations. A functional interpretation consists of a formula interpretation and a soundness proof. I show that all these interpretations differ only on two design choices: first, on the number of counterexamples for A which became witnesses for ¬A when defining (...) the formula interpretation and, second, the inductive information about the witnesses of A which is considered in the proof of soundness. Sufficient conditions on the parameters are also given which ensure the soundness of the resulting functional interpretation. The relation between the parametrized interpretation and the recent bounded functional interpretation is also discussed. (shrink)

La presente investigación tuvo por objetivo analizar los usos del discurso institucional de universidades chilenas autodefinidas como complejas en relación a la organización del conocimiento e iniciativas inter-transdisciplinarias relevantes informadas a nivel de estructuras estáticas y noticias en sitios web oficiales de cada una de ellas. En este contexto y a través de un Análisis Crítico del Discurso, se indaga en el despliegue de estrategias comunicativas, la producción y difusión del discurso institucional, como asimismo, su exposición y disposición en las (...) páginas web. Desde esta base, se contribuye con información cualitativa a la discusión en torno a los formatos y dispositivos de comunicación social referidos a las nociones de inter y transdisciplina en el contexto de la educación superior en el país. Los resultados dan cuenta de la emergencia, centralidad y valor comunicacional de la prospectiva inter y transdisciplinaria en el contexto universitario chileno, no obstante, también evidencian las condicionantes epistemológicas y metodológicas para su despliegue organizacional crítico y sostenible. (shrink)

Resumen: La presente investigación tuvo por objetivo analizar los usos del discurso institucional de universidades chilenas autodefinidas como complejas en relación con la organización del conocimiento e iniciativas intertransdisciplinarias relevantes informadas a nivel de estructuras estáticas y noticias en sitios web oficiales de cada una de ellas. En este contexto y mediante un Análisis Crítico del Discurso, se indaga en el despliegue de estrategias comunicativas, la producción y difusión del discurso institucional, como asimismo, su exposición y disposición en las páginas (...) web. Desde esta base se contribuye con información cualitativa a la discusión en torno a los formatos y dispositivos de comunicación social referidos a las nociones de inter y transdisciplina en el contexto de la educación superior en el país. Los resultados dan cuenta de la emergencia, centralidad y valor comunicacional de la prospectiva inter y transdisciplinaria en el contexto universitario chileno, no obstante, también evidencian las condicionantes epistemológicas y metodológicas para su despliegue organizacional crítico y sostenible.: The following investigation had as an objective to analyse the usages of the Institutional Discourse from Chilean universities self-described as complex, in relation to the Knowledge Organization and relevant inter-disciplinaries initiatives that are informed at the level of static structures and pieces of news published on each official website. In this context, and, through a Critical Discourse Analysis, the communicative strategies deployment is explored, as well as the production and broadcasting of their institutional discourse. Likewise, their exposure and disposal on web pages. On this basis, the qualitative information is contributed to the discussion around the formats and social communication devices, referred to the concepts of inter and trans-disciplines in the context of higher education in the nation. The results, reflect the emergency, centrality and communicational value of the inter and trans-disciplinary prospective in the Chilean university context. However, the epistemological and methodological conditions are evidenced for its organizational, critical, and sustainable deployment. (shrink)

In this paper, we present another case study in the general project of proof mining which means the logical analysis of prima facie non-effective proofs with the aim of extracting new computationally relevant data. We use techniques based on monotone functional interpretation developed in Kohlenbach , Oxford University Press, Oxford, 1996, pp. 225–260) to analyze Cheney's simplification 189) of Jackson's original proof 320) of the uniqueness of the best L1-approximation of continuous functions fC[0,1] by polynomials pPn of degree n. Cheney's (...) proof is non-effective in the sense that it is based on classical logic and on the non-computational principle WKL . The result of our analysis provides the first effective uniform modulus of uniqueness . Moreover, the extracted modulus has the optimal ε-dependency as follows from Kroó 331). The paper also describes how the uniform modulus of uniqueness can be used to compute the best L1-approximations of a fixed fC[0,1] with arbitrary precision. The second author uses this result to give a complexity upper bound on the computation of the best L1-approximation in Oliva 66–77). (shrink)

Schwichtenberg showed that the System T definable functionals are closed under a rule-like version Spector’s bar recursion of lowest type levels 0 and 1. More precisely, if the functional Y which controls the stopping condition of Spector’s bar recursor is T-definable, then the corresponding bar recursion of type levels 0 and 1 is already T-definable. Schwichtenberg’s original proof, however, relies on a detour through Tait’s infinitary terms and the correspondence between ordinal recursion for α < ε₀ and primitive recursion over (...) finite types. This detour makes it hard to calculate on given concrete system T input, what the corresponding system T output would look like. In this paper we present an alternative (more direct) proof based on an explicit construction which we prove correct via a suitably defined logical relation. We show through an example how this gives a straightforward mechanism for converting bar recursive definitions into T-definitions under the conditions of Schwichtenberg’s theorem. Finally, with the explicit construction we can also easily state a sharper result: if Y is in the fragment Tᵢ then terms built from BR^ℕ,σ for this particular Y are definable in the fragment T_i+max{1,level(σ)}+2. (shrink)

We present a new functional interpretation, based on a novel assignment of formulas. In contrast with Gödel’s functional “Dialectica” interpretation, the new interpretation does not care for precise witnesses of existential statements, but only for bounds for them. New principles are supported by our interpretation, including the FAN theorem, weak König’s lemma and the lesser limited principle of omniscience. Conspicuous among these principles are also refutations of some laws of classical logic. Notwithstanding, we end up discussing some applications of the (...) new interpretation to theories of classical arithmetic and analysis. (shrink)

This article presents an analysis of Gödel's dialectica interpretation via a refinement of intuitionistic logic known as linear logic. Linear logic comes naturally into the picture once one observes that the structural rule of contraction is the main cause of the lack of symmetry in Gödel's interpretation. We use the fact that the dialectica interpretation of intuitionistic logic can be viewed as a composition of Girard's embedding of intuitionistic logic into linear logic followed by de Paiva's dialectica interpretation of linear (...) logic. We then investigate the various properties of the dialectica interpretation, such as the characterisation theorem, and variants of Gödel's interpretation within the linear logic context. The role of contraction in extensions to classical logic, arithmetic and analysis is also discussed. (shrink)

We show that Spector's “restricted” form of bar recursion is sufficient (over system T) to define Spector's search functional. This new result is then used to show that Spector's restricted form of bar recursion is in fact as general as the supposedly more general form of bar recursion. Given that these two forms of bar recursion correspond to the (explicitly controlled) iterated products of selection function and quantifiers, it follows that this iterated product of selection functions is T‐equivalent to the (...) corresponding iterated product of quantifiers. (shrink)

This article presents an analysis of Gödel's dialectica interpretation via a refinement of intuitionistic logic known as linear logic. Linear logic comes naturally into the picture once one observes that the structural rule of contraction is the main cause of the lack of symmetry in Gödel's interpretation. We use the fact that the dialectica interpretation of intuitionistic logic can be viewed as a composition of Girard's embedding of intuitionistic logic into linear logic followed by de Paiva's dialectica interpretation of linear (...) logic. We then investigate the various properties of the dialectica interpretation, such as the characterisation theorem, and variants of Gödel's interpretation within the linear logic context. The role of contraction in extensions to classical logic, arithmetic and analysis is also discussed. (shrink)

In this article we study applications of the bounded functional interpretation to theories of feasible arithmetic and analysis. The main results show that the novel interpretation is sound for considerable generalizations of weak König’s Lemma, even in the presence of very weak induction. Moreover, when this is combined with Cook and Urquhart’s variant of the functional interpretation, one obtains effective versions of conservation results regarding weak König’s Lemma which have been so far only obtained non-constructively.

It is well known that for a given continuous function f : [0, 1] → ℝ and a number n there exists a unique polynomial pn ∈ Pn which best L1-approximates f. We establish the first upper bound on the complexity of the sequence n∈ ℕ, assuming f is polynomial-time computable. Our complexity analysis makes essential use of the modulus of uniqueness for L1-approximation presented in [13].

We show that the types of the witnesses in the Herbrand functional interpretation can be simplified, avoiding the use of “sets of functionals” in the interpretation of implication and universal quantification. This is done by presenting an alternative formulation of the Herbrand functional interpretation, which we show to be equivalent to the original presentation. As a result of this investigation we also strengthen the monotonicity property of the original presentation, and prove a monotonicity property for our alternative definition.

We show how two iterated products of selection functions can both be used in conjunction with systemTto interpret, via the dialectica interpretation and modified realizability, full classical analysis. We also show that one iterated product is equivalent over systemTto Spector’s bar recursion, whereas the other isT-equivalent to modified bar recursion. Modified bar recursion itself is shown to arise directly from the iteration of a different binary product of ‘skewed’ selection functions. Iterations of the dependent binary products are also considered but (...) in all cases are shown to beT-equivalent to the iteration of the simple products. (shrink)

We present a refinement ofthe bounded modified realizability which provides both upper and lower bounds for witnesses. Our interpretation is based on a generalisation of Howard/Bezem's notion of strong majorizability. We show how the bounded modified realizability coincides with our interpretation in the case when least elements exist . The new interpretation, however, permits the extraction of more accurate bounds, and provides an ideal setting for dealing directly with data types whose natural ordering is not well-founded.

This paper presents an algebraic framework for investigating proposed translations of classical logic into intuitionistic logic, such as the four negative translations introduced by Kolmogorov, Gödel, Gentzen and Glivenko. We view these asvariant semanticsand present a semantic formulation of Troelstra’s syntactic criteria for a satisfactory negative translation. We consider how each of the above-mentioned translation schemes behaves on two generalisations of Heyting algebras: bounded pocrims and bounded hoops. When a translation fails for a particular class of algebras, we demonstrate that (...) failure via specific finite examples. Using these, we prove that the syntactic version of these translations will fail to satisfy Troelstra’s criteria in the corresponding substructural logical setting. (shrink)

This article systematically investigates so-called “truth variants” of several functional interpretations. We start by showing a close relation between two variants of modified realizability, namely modified realizability with truth and q-modified realizability. Both variants are shown tobe derived from a single “functional interpretation with truth” of intuitionistic linear logic. This analysis suggests that several functional interpretations have truth and q-variants. These variants, however, require a more involved modification than the ones previously considered. Following this lead we present truth and q-variants (...) of the Diller-Nahm interpretation, the bounded modified realizability and the bounded functional interpretation. (shrink)

The author provides an original reflection on the notion of selfhood as intersubjective, taking the form of phenomenological reflections on the building blocks of the perennial philosophy, recasting Aristotelian-Thomistic metaphysics from the perspective of a phenomenology.

Este artículo aborda la recepción temprana del filósofo esloveno Slavoj Žižek en el debate teórico chileno entre los años 1998-2013. El interés de este articulo no consiste meramente en enlistar las menciones a Žižek en el contexto local, sino problematizar los intereses históricos de las escenas teóricas locales y el alcance político de la teoría materialista dialéctica de Žižek, considerando que esta recepción se masifica al aproximarse el movimiento estudiantil del 2011 bajo la necesidad de acudir a nuevos referentes teóricos (...) para entender la realidad contingente. (shrink)

Metaphysics is not often spoken of as a venue for dialogue about anything, let alone culture or religion, which are more readily associated with phenomenology or hermeneutics in contemporary thinking. This collection of essays, however, by the late Boston College philosopher Oliva Blanchette, maintains the absolute necessity of metaphysics as a prerequisite for examining any particular 'realm of being,' in all areas of human inquiry, from the particular sciences to historical cultures and religions. Blanchette proposes metaphysics as a fundamental (...) and necessary level of intelligence presupposed in any exercise of judgment, discourse, or dialogue, among rational beings. At the same time, he defends the idea that dialogue is the first and most fundamental form in which such reasoning takes place in human experience, on a radically intersubjective level through language. (shrink)

In the late 1930's Blondel precipitated a debate over the question of a Christian philosophy in a series of articles on St. Augustine insisting on the philosophical nature of the saint's thought. Rationalist historian of philosophy Bréhier objected to the very idea of a Christian philosophy. Other historians like Gilson allowed that a philosophy could be characterized loosely as Christian when it was associated with Christian thought, as in the Middle Ages. But Blondel argued against both of these positions as (...) presupposing a separation between philosophy and religion that allowed only for a false hybridization between the two when they were juxtaposed. His own approach to philosophy had been to show a necessary intersection between the two in the question about the ultimate meaning of human action as it relates to God in his infinite transcendence, as this had long been understood in the Catholic tradition, that is, as relating to something supernatural in the strictest sense, something bound to appear as scandalous and paradoxical to reason alone. The present article examines how he first came to his philosophical method for dealing with this question in the 1890's and how he later used this method in defending the idea of a philosophy that was integrally rational and Catholic in the strict sense of both terms. /// Na década de 1930, Maurice Blondel desencadeou um importante debate acerca da questão da chamada Filosofia Cristã mediante uma série de artigos sobre Santo Agostinho, os quais insistiam em particular sobre a natureza filosófica do pensamento do grande santo. Bréhier, um historiador da Filosofia de tendência racionalista, objectou à própria ideia de uma Filosofia Cristã. Outros historiadores, tais como E. Gilson, concediam que uma Filosofia poderia ser vagamente caracterizada como Cristã quando a mesma esteja associada com o pensamento cristão, como era o caso na Idade Média. Mas Blondel argumentava contra estas duas posições na medida em que achava que as mesmas pressuponham a separação entre Filosofia e Religião, separação esta que permitia apenas uma falsa hibridização entre as duas quando as mesmas eram justapostas. A sua posição pessoal em relação à Filosofia defendia que entre esta e a Religião existia uma intersecçdo necessária acerca da questão relativa ao sentido ultimo da acçdo humana na medida em que esta remete para Deus na sua infinita transcendência, tal como esta era desde há muito compreendida na tradição Católica, ou seja, enquanto que remetendo para algo sobrenatural no sentido mais estrito, algo destinado a aparecer como escandaloso e paradoxal à razão enquanto que entregue a si mesma. O presente artigo examina de que modo Blondel primeiro chegou ao seu método filosófico no tratamento desta questão na década de 1890 e de como ele mais tarde usou este método para defender a ideia de uma Filosofia que é integralmente racional e católica no sentido mais estrito de ambos os termos. (shrink)

Um das achtzehnte Jahrhundert herum zogen verschiedene Denker dem Staat eine auch heute noch vielbeachtete Grenze: Religion ist Privatsache. Fragen der Religion lägen jenseits dessen, wo der Staat legitimerweise wirken könne. Diese Forderung nach einer Trennung von Staat und Religion wird heute wesentlich als eine Frage der Gewissensfreiheit gedeutet. Wo wir Gewissensfreiheit missachten, erlegen wir Individuen unzumutbare Gewissensnöte auf Der Laizismus bewahrt damit die Unverletzlichkeit religiöser Einstellungen. Gewissensfragen gibt es jedoch nicht nur in der Religion. Es gibt sie auch in (...) der Moral, und sogar in individuellen Lebensperspektiven und Weltanschauungen jenseits von Religion und Moral. Wer Denkern wie Jefferson und Humboldt folgen will, muss daher weiter gehen. Der Aufsatz entwickelt die Konsequenzen für einen in Hobbes und Locke gründenden Kontraktualismus. Ich deute Gewissensgründe als politischen Zustimmungsvorbehalt, der dem kontraktualistischen Gemeinwesen strikte Neutralität abverlangt. Gewissensfreiheit zu missachten zerstört daher das politische, das „Locke'sche" Vertrauen, welches das Gemeinwesen trägt. *—————* Around the eighteenth century, several theorists came to advocate the separation of religion and state. In various ways they argued that all that concerns religion lies beyond the sphere of the state's activity. This "wall of separation" is today often understood as a matter offreedom of conscience. Wherefreedom of conscience is infringed, man 's soul is burdened beyond what the individual can bear. The separation of religion and state thus protects the inviolability of religious attitudes. However, matters of conscience are not exclusively religious. They can be moral, or even pertaining to individual worldviews beyond morality or religion. Those who want to follow thinkers like Jefferson or Humboldt must therefore go beyond their call. This paper investigates the consequences for contractarianism in the spirit of Hobbes and Locke. I suggest conscientious reservations are implied conditions for contractarian consent which oblige the commonwealth to strict neutrality in matters offreedom of conscience. To infringe uponfreedom of conscience thus destroys the band ofthe commonwealth, i.e., political, "Lockean" trust. -/- . (shrink)