It has been known for six years that the restriction of Girard's polymorphic system $\text{\bfseries\upshape F}$ to atomic universal instantiations interprets the full fragment of the intuitionistic propositional calculus. We firstly observe that Tait's method of “convertibility” applies quite naturally to the proof of strong normalization of the restricted Girard system. We then show that each $\beta$-reduction step of the full intuitionistic propositional calculus translates into one or more $\beta\eta$-reduction steps in the restricted Girard system. As a consequence, we obtain (...) a novel and perspicuous proof of the strong normalization property for the full intuitionistic propositional calculus. It is noticed that this novel proof bestows a crucial role to $\eta$-conversions. (shrink)

We introduce a new typed combinatory calculus with a type constructor that, to each type σ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma $$\end{document}, associates the star type σ∗\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma ^*$$\end{document} of the nonempty finite subsets of elements of type σ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma $$\end{document}. We prove that this calculus enjoys the properties of strong normalization and confluence. With the aid of this star combinatory (...) calculus, we define a functional interpretation of first-order predicate logic and prove a corresponding soundness theorem. It is seen that each theorem of classical first-order logic is connected with certain formulas which are tautological in character. As a corollary, we reprove Herbrand’s theorem on the extraction of terms from classically provable existential statements. (shrink)

Commuting conversions were introduced in the natural deduction calculus as ad hoc devices for the purpose of guaranteeing the subformula property in normal proofs. In a well known book, Jean-Yves Girard commented harshly on these conversions, saying that ‘one tends to think that natural deduction should be modified to correct such atrocities.’ We present an embedding of the intuitionistic predicate calculus into a second-order predicative system for which there is no need for commuting conversions. Furthermore, we show that the redex (...) and the conversum of a commuting conversion of the original calculus translate into equivalent derivations by means of a series of bidirectional applications of standard conversions. (shrink)

It is known that there is a sound and faithful translation of the full intuitionistic propositional calculus into the atomic polymorphic system F at, a predicative calculus with only two connectives: the conditional and the second-order universal quantifier. The faithfulness of the embedding was established quite recently via a model-theoretic argument based in Kripke structures. In this paper we present a purely proof-theoretic proof of faithfulness. As an application, we give a purely proof-theoretic proof of the disjunction property of the (...) intuitionistic propositional logic in which commuting conversions are not needed. (shrink)

Edward Nelson published in 1986 a book defending an extreme formalist view of mathematics according to which there is animpassable barrierin the totality of exponentiation. On the positive side, Nelson embarks on a program of investigating how much mathematics can be interpreted in Raphael Robinson's theory of arithmetic. In the shadow of this program, some very nice logical investigations and results were produced by a number of people, not only regarding what can be interpreted inbut also what cannot be so (...) interpreted. We explain some of these results and rely on them to discuss Nelson's position. (shrink)

Edward Nelson published in 1986 a book defending an extreme formalist view of mathematics according to which there is an impassable barrier in the totality of exponentiation. On the positive side, Nelson embarks on a program of investigating how much mathematics can be interpreted in Raphael Robinson's theory of arithmetic Q. In the shadow of this program, some very nice logical investigations and results were produced by a number of people, not only regarding what can be interpreted in Q but (...) also what cannot be so interpreted. We explain some of these results and rely on them to discuss Nelson's position. (shrink)

We give an elementary proof of the strong normalization of the atomic polymorphic calculus Fat.

Suppose that it is possible to integrate real functions over a weak base theory related to polynomial time computability. Does it follow that we can count? The answer seems to be: obviously yes! We try to convince the reader that the severe restrictions on induction in feasible theories preclude a straightforward answer. Nevertheless, a more sophisticated reflection does indeed show that the answer is affirmative.

Leo Harrington showed that the second-order theory of arithmetic WKL 0 is ${\Pi^1_1}$ -conservative over the theory RCA 0. Harrington’s proof is model-theoretic, making use of a forcing argument. A purely proof-theoretic proof, avoiding forcing, has been eluding the efforts of researchers. In this short paper, we present a proof of Harrington’s result using a cut-elimination argument.

A partir da temática abordada no filme Gattaca - a experiência genética , que trata de uma sociedade adepta da eugenia; mostraremos quais são as implicações morais que essa prática pode ocasionar em uma sociedade, bem como as diversas discriminações. Em contra-argumento a essa prática, abordaremos a teoria de Peter Singer em prol do princípio da igual consideração de interesses, demonstrando que dessa maneira teríamos sociedades menos discriminatórias. Enfim, queremos mostrar que caso não nos alertemos para as questões abordadas por (...) Singer, nós, agentes morais, faremos emergir uma sociedade preconceituosa, tal como vemos no filme Gattaca.: From selected themes in the movie Gattaca - A genetic experiment that describes a eugenics society, we will show what are the moral implications of the eugenic practice to the society as well as its several kinds of discrimination. We will argue against such practice by appropriating Peter Singer’s theory on behalf of the principle of equal consideration of interests by showing that societies based on it would be less discriminatory. Finally, we show that if we do not consider the issues raised by Singer we, moral agents, will make emerge a prejudiced society similar to that narrated by the movie Gattaca. Key words : Moral, Equality, Eugenie, discrimination. (shrink)

O estudo visa evidenciar o lugar que os princípios primeiros ocupam na filosofia moral de Alasdair MacIntyre, bem como o conceito de teleologia a eles articulado. Consistirá, no estudo panorâmico das categorias centrais da ética das virtudes de MacIntyre, onde ele constrói sua teoria da racionalidade das tradições que, por sua vez, é essencial para sua compreensão da retomada da ética aristotélica das virtudes e o papel dos princípios primeiros na sua filosofia moral. A partir destes, o desenvolvimento do artigo (...) se dá com a identificação do lugar que os primeiros princípios ocupam na filosofia moral de MacIntyre, como também a relevância que eles têm para o desenvolvimento de sua teoria do resgate da ética aristotélica. (shrink)

Frege’s Grundgesetze der Arithmetik is formally inconsistent. This system is, except for minor differences, second-order logic together with an abstraction operator governed by Frege’s Axiom V. A few years ago, Richard Heck showed that the ramified predicative second-order fragment of the Grundgesetze is consistent. In this paper, we show that the above fragment augmented with the axiom of reducibility for concepts true of only finitely many individuals is still consistent, and that elementary Peano arithmetic (and more) is interpretable in this (...) extended system. (shrink)

The present paper draws a contrast between the notions of τὸ παρ’ ἡμᾶς and τὸ ἐφ’ ἡμῖν to the effect that, according to Chrysippus, each has a different role to play and different requirements to meet, the former being especially tailored to suit the exigencies of praise and blame taken as exhortations, the latter those of desert and justice in praising and blaming as well as honoring and punishing.

Nowadays, football goalkeepers play an important role in the team's organization, namely, considering the offensive and defensive processes. The purpose of our investigation focuses on the notational and T-pattern analysis of the offensive and defensive actions of elite young football GKs. The participating GKs presented 8 years of experience in the specific position, were internationally selected for the national team of Portugal, and competed in the national U-17 championship of Portugal. Thirty football matches were observed. The observational sample consisted of (...) defensive actions and offensive actions. Two observational instruments were used to codify the actions: the observation system of defensive technical-tactical actions of GKs and the observation system of offensive technical-tactical actions of GKs. Both instruments underwent a validation process, and inter- and intra-observer reliability was tested. The codification of the actions was performed with the LINCE program, and later the data were exported to Microsoft Excel and THEME 5.0. The notational data were analyzed in SPSS, and T-pattern detection analysis was performed in THEME 5.0. The predominant actions of young observed GKs were fundamentally goal defense and participation in the team's offensive process construction through actions performed with the foot and hand. The analysis of T-patterns allowed to identify T-pattern actions in the defensive actions of goal defense and exit of the goal, as well as related to the defensive set pieces. In the offensive process, the analysis of T-patterns reinforced the participation of the GK in the team's first phase of construction and in the execution of goal kicks and actions that start as a result of the actions of the opponent. The GK's defensive actions are mostly focused on the objective of goal defense and offensive actions with the hands and feet are important for their participation in positional attack construction. Our study contributes to a better knowledge of the GK's actions in the competition and is relevant to be considered by the specific position coaches in the training process organization. (shrink)

Este dossiê representa a continuidade de um projecto centrado no património dos agentes ligados à produção, circulação e recepção do livro. A partir da história e dos espólios de empresas editoriais e de coleccionadores, bibliófilos e/ou divulgadores, a introdução problematizante e os depoimentos convocam a memória dos agentes e debatem as ameaças que pendem sobre essa herança cultural riquíssima e possíveis soluções. As boas práticas de vários países impõem uma reflexão inadiável para o contexto português: que vias de cooperação inter-institucional (...) concretas para garantir o depósito, tratamento e comunica­ção duma dimensão fulcral do património e da memória colectiva. A relevância desta ques­tão deve-se a estar inextricavelmente ligada a um reconhecimento sustentável do estatuto patrimonial e histórico dos acervos dos editores e doutros agentes ligados à edição e ao livro enquanto espaços vitais para a construção da cultura impressa e para a história do livro e da edição. Os depoimentos referidos são de Carlos da Veiga Ferreira, Fernando Paulouro Neves e Francisco Pedro Lyon de Castro. (shrink)

RESUMO O presente ensaio aborda o período anterior às obras tidas como as diferentes reescrições da Doutrina da Ciência, de J. G. Fichte, e aí tenta não só perceber a origem da necessidade de um princípio da identidade, como ela surge aquando das primeiras ocorrências do mesmo, mas também discernir os primeiros passos de todo o problema da possibilidade de um princípio absoluto de toda a filosofia, que sempre animaria a empresa. O foco em questão é a «Aenesidemus-Rezension», onde Fichte (...) junta a sua voz ao aceso diálogo já anteriormente entabulado por K. L. Reinhold e G. E. Schulze, e, na necessidade de repensar o princípio da consciência do primeiro, e as críticas a este feitas pelo segundo, é trazido à convicção da necessidade de um novo princípio absoluto; mas onde, e é este o fulcro do presente ensaio, Fichte percebe a insuficiência filososófica do sistema reinholdiano como uma insuficiência de linguagem, e portanto todo o problema como um problema que depende intimamente de uma apoditicidade linguística, e daí parte para a proposta de uma nova terminologia nacional, uma linguagem filosófica sistematicamente certa e inequívoca, à altura de um sistema filosófico regido por um princípio absoluto – um problema que viria a ocupar as cogitações de toda a geração de jovens pensadores em torno do professor de Jena. ABSTRACT This essay approaches the period prior to the works considered as the different versions of the Doctrine of Science, by J. G. Fichte, and aims not only at discerning the origin of the need for a principle of identity, but also at retracing the first steps of the whole problem of the possibility of an absolute principle of all philosophy. The focus shall be the «Aenesidemus-Rezension», where Fichte joins his voice to the heated argument previously struck by K. L. Reinhold and G. E. Schulze, and, urged to rethink Reinhold's principle of consciousness and the criticism raised by Schulze, is brought to believe the necessity for a new absolute principle; but where, and this is the fundamental idea of this essay, Fichte realizes the philosophical insufficiency of Reinhold's system as a language-related insufficiency, and therefore the whole problem as one intimately dependent on a linguistic apodicticity, and moves on to propose a new national terminology, a systematically certain and unequivocal philosophical language, which might meet the demands of a philosophical system ruled by an absolute principle – a problem which would soon be in the agenda of a whole generation of young idealists around the Professor of Jena. (shrink)

RESUMO A história do estatuto, bem como da posição da memória entre semelhantes forças, desde a formação do conceito moderno da antropologia, durante toda a tradição leibniz-wolffinana, e até Kant, é uma história de mudança ascendente, de cristalização de ambos os predicados desta faculdade, e também uma de grande influência sobre a história do próprio pensamento antropológico. O presente ensaio propõe-se analisar como Kant receberia essa evolução, e como ele sobre ela actuaria. Isto é, centrando-nos nas “Lições de Antropologia”, e (...) sobre a “Antropologia num Enfoque Pragmático”, queremos indagar até que ponto Kant daria continuidade à referida tradição, mas, sobretudo, a partir de onde este com ela rompe, talhando ele próprio um novo capítulo nessa história, e também na história da antropologia; mais concretamente, importa conhecer a posição de Kant em relação a Platner ou Hume e suas concepções de memória, sua cisão em relação a estes, e sua proposta de todo um reposicionamento, e também revalorização do estatuto da memória entre faculdades da alma; e, por fim, perceber como Kant traz estes propósitos a bom porto, a saber, por meio da memória judiciosa, a única que abre não só para as ciências, mas também para a faculdade de imaginação produtiva, e para a poesia, e portanto também a única capaz de unir inferiores e superiores faculdades da alma, e instaurar harmonia entre estas. ABSTRACT The history of the status, as well as the position of memory among similar forces, since the genesis of the modern concept of anthropology, during the Leibniz-Wolffian tradition, and until Kant, is a history of ascending transformation, a crystallization of both this faculty’s attributes, and also one of great influence on the history of anthropological thought itself. The present essay aims at analyzing how Kant would receive that evolution, and how he would act upon it. That is, by focusing on the “Lectures on Anthropology”, and on “Anthropology on a Pragmatic Point of View”, we wish to inquire to what extent Kant would resume the aforementioned tradition, but, above all, from which point he breaks with it, thus carving he himself a new chapter in that history, and also in the history of anthropology; namely, it is our objective to ascertain Kant’s position regarding Platner or Hume and their conceptions of memory, his scission from the latter two, and his proposition of a whole repositioning, and also revaluation of the status of memory among faculties of the soul; and finally, understanding how Kant succeeds in these purposes, namely, through the concept of judicious memory, the only one which enables not only sciences, but also the productive faculty of imagination, and hence poetry, and therefore the only one able to unite both inferior and superior faculties of the soul and to sow harmony between the latter. (shrink)

RESUMO: Fruto de longa maturação filosófica desde a sua estada em Jena, e instado a isso pelas influências de Karl L. Reinhold e Johann G. Fichte, o poeta Novalis produz, a partir do outono de 1795, um conjunto de anotações fragmentárias sobre a filosofia de Fichte, hoje conhecidas como Fichte-Studien. De entre os importantes temas aí abordados, um revela-se particularmente interessante: o tema do estatuto da Filosofia no seio do problema da autocompreensão do Eu -, e mais concretamente, o necessário (...) pensar da filosofia sobre si própria, as alterações que no processo têm de sobrevir à própria filosofia e a repercussão disto na compreensão de si próprio do Eu. Nesta senda, o seguinte ensaio propõe-se mostrar como, para Novalis, a filosofia é o natural pensar do homem, e como para além disto é a própria filosofia, com o decorrer do seu pensamento sobre si própria, que molda o curso da compreensão de si próprio do Eu: quer tendo com o Eu uma origem comum, nascendo com ele, lançando-o para o mundo e cindindo a união originária em que ele de outro modo sempre estaria, quer, por fim, afirmando-se como carência deste, ou como algo por que o Eu e a própria filosofia têm de passar no seu curso, para que possam experienciar a perda, e almejar à recuperação dessa origem. ABSTRACT: Fruit of a long philosophical maturation that began with his stay in Jena, and encouraged by the influence of Karl L. Reinhold and Johann G. Fichte, the poet Novalis produced, from autumn 1795 on, a set of fragmentary notes on the philosophy of Fichte. These are now known as Fichte-Studien. Among the important issues treated in the notes, one appears particularly interesting: the treatment of the theme of philosophy within the problem of the self-understanding of the "I" - and, more specifically, the need for philosophy to think about itself, about the changes that must come upon philosophy during this process, and about the impact of these on the self-understanding of the "I". The present article aims to show how, for Novalis, philosophy is the natural thought of man. Furthermore, it aims to show how philosophy, in the course of its thought on itself, shapes the course of the self-understanding of the "I", having with the "I" a common origin, being born with it, launching it into the world, cleaving the original union in which it otherwise would always be, and finally asserting itself as a lack of this union, something through which the "I" and philosophy itself must pass in their course so they can experience this loss and aim to recover its source. (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)

It is well known that Frege's system in the Grundgesetze der Arithmetik is formally inconsistent. Frege's instantiation rule for the second-order universal quantifier makes his system, except for minor differences, full (i.e., with unrestricted comprehension) second-order logic, augmented by an abstraction operator that abides to Frege's basic law V. A few years ago, Richard Heck proved the consistency of the fragment of Frege's theory obtained by restricting the comprehension schema to predicative formulae. He further conjectured that the more encompassing Δ₁¹-comprehension (...) schema would already be inconsistent. In the present paper, we show that this is not the case. (shrink)

We construct a weak second-order theory of arithmetic which includes Weak König's Lemma (WKL) for trees defined by bounded formulae. The provably total functions (with Σ b 1 -graphs) of this theory are the polynomial time computable functions. It is shown that the first-order strength of this version of WKL is exactly that of the scheme of collection for bounded formulae.

It is well known that Frege's system in the Grundgesetze der Arithmetik is formally inconsistent. Frege's instantiation rule for the second-order universal quantifier makes his system, except for minor differences, full (i.e., with unrestricted comprehension) second-order logic, augmented by an abstraction operator that abides to Frege's basic law V. A few years ago, Richard Heck proved the consistency of the fragment of Frege's theory obtained by restricting the comprehension schema to predicative formulae. He further conjectured that the more encompassing Δ11-comprehension (...) schema would already be inconsistent. In the present paper, we show that this is not the case. (shrink)

We show how to interpret intuitionistic propositional logic into a predicative second-order intuitionistic propositional system having only the conditional and the universal second-order quantifier. We comment on this fact. We argue that it supports the legitimacy of using classical logic in a predicative setting, even though the philosophical cast of predicativism is nonrealistic. We also note that the absence of disjunction and existential quantifications allows one to have a process of normalization of proofs that avoids the use of "commuting conversions.".

In "'Yes" and "No'" (2000), Ian Rumfitt proposed bilateralism--a use-based account of the logical words, according to which the sense of a sentence is determined by the conditions under which it is asserted and denied. One of Rumfitt's key claims is that bilateralism can provide a justification of classical logic. This paper raises a techical problem for Rumfitt's proposal, one that seems to undermine the bilateralist programme.

We prove that the (non-intuitionistic) law of the double negation shift has a bounded functional interpretation with bar recursive functionals of finite type. As an application. we show that full numerical comprehension is compatible with the uniformities introduced by the characteristic principles of the bounded functional interpretation for the classical case.

We introduce a herbrandized functional interpretation of a first-order semi-intuitionistic extension of Heyting Arithmetic and study its main properties. We then extend the interpretation to a certain system of second-order arithmetic which includes a (classically false) formulation of the FAN principle and weak König's lemma. It is shown that any first-order formula provable in this system is classically true. It is perhaps worthy of note that, in our interpretation, second-order variables are interpreted by finite sets of natural numbers.

In Frege’s logicism, numbers are logical objects in the sense that they are extensions of certain concepts. Frege’s logical system is inconsistent, but Richard Heck showed that its restriction to predicative quantification is consistent. This predicative fragment is, nevertheless, too weak to develop arithmetic. In this paper, I will consider an extension of Heck’s system with impredicative quantifiers. In this extended system, both predicative and impredicative quantifiers co-exist but it is only permissible to take extensions of concepts formulated in the (...) predicative fragment of the language. This system is consistent. Moreover, it proves the principle of reducibility applied to concepts true of only finitely many objects. With the aid of this form of reducibility, it is possible to develop arithmetic in a thoroughly Fregean way. (shrink)

We present a functional interpretation of Peano arithmetic that uses Gödel’s computable functionals and which systematically injects uniformities into the statements of finite-type arithmetic. As a consequence, some uniform boundedness principles are interpreted while maintaining unmoved the -sentences of arithmetic. We explain why this interpretation is tailored to yield conservation results.

We define a notion of realizability, based on a new assignment of formulas, which does not care for precise witnesses of existential statements, but only for bounds for them. The novel form of realizability supports a very general form of the FAN theorem, refutes Markov's principle but meshes well with some classical principles, including the lesser limited principle of omniscience and weak König's lemma. We discuss some applications, as well as some previous results in the literature.

_Objetivo:_ conocer las opiniones de los ancianos sobre la vacuna anti-covid y su posible rechazo. _Metodología:_ se trata de un estudio exploratorio y cualitativo, realizado en un pequeño municipio, en el extremo Norte de Mato Grosso, Brasil. La recolección de datos ocurrió en marzo de 2021, a través de una entrevista semiestructurada. Para el análisis de datos se utilizó el software ATLAS.ti®. _Resultados:_ la mayoría de los ancianos mostró aceptación y deseo de ser inmunizados, pero aquellos con baja escolaridad mostraron (...) mayor rechazo a la vacuna, lo que fue percibido por los demás ancianos como una irresponsabilidad. Los participantes mencionan que toda persona tiene derecho a elegir. _Conclusiones:_ aunque los ancianos tenían una opinión positiva sobre la vacuna, se deben intensificar las acciones educativas, especialmente entre aquellos con baja escolaridad, para que la conducta de rechazo, si prevalece incluso después de diálogos y aclaraciones, no influya a terceros y ponga en peligro la salud de la comunidad. (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.

In the course of ten short sections, we comment on Gödel's seminal dialectica paper of fifty years ago and its aftermath. We start by suggesting that Gödel's use of functionals of finite type is yet another instance of the realistic attitude of Gödel towards mathematics, in tune with his defense of the postulation of ever increasing higher types in foundational studies. We also make some observations concerning Gödel's recasting of intuitionistic arithmetic via the dialectica interpretation, discuss the extra principles that (...) the interpretation validates and comment on extensionality and higher order equality. The latter sections focus on the role of majorizability considerations within the dialectica and related interpretations for extracting computational information from ordinary proofs in mathematics. (shrink)

Every model of IΔ0 is the tally part of a model of the stringlanguage theory Th-FO . We show how to “smoothly” introduce in Th-FO the binary length function, whereby it is possible to make exponential assumptions in models of Th-FO. These considerations entail that every model of IΔ0 + ¬exp is a proper initial segment of a model of Th-FO and that a modicum of bounded collection is true in these models.

Emotional intelligence is a psychological skill that aids athletes in the control of emotions and optimization of sports performance. The present study investigated the psychometric properties of the Self-Report Emotional Intelligence Test in 508 Brazilian youth and adult athletes. Data analysis was conducted through Exploratory and Confirmatory Factor Analysis, Cronbach’s alpha, composite reliability and Pearson’s Correlation. EFA revealed the one-factor model with 26 items with the best adjustment. CFA confirmed the one-factor model with 26 items with best greater fit. No (...) evidence of invariance was found, suggesting that the SSEIT must be used with caution when comparing gender and age groups. The external validity was found in the correlation of EI and cognitive anxiety and self-confidence. It is concluded that the Brazilian version of SSEIT for the sports context presented acceptable psychometric properties, however, showed limitations that should be explored in the future. (shrink)

Let be the fragment of elementary Peano arithmetic in which induction is restricted to -formulas. More than three decades ago, Parsons showed that the provably total functions of are exactly the primitive recursive functions. In this paper, we observe that Parsons' result is a consequence of Herbrand's theorem concerning the -consequences of universal theories. We give a self-contained proof requiring only basic knowledge of mathematical logic.

We show how to interpret weak Kőnig's lemma in some recently defined theories of nonstandard arithmetic in all finite types. Two types of interpretations are described, with very different verifications. The celebrated conservation result of Friedman's about weak Kőnig's lemma can be proved using these interpretations. We also address some issues concerning the collecting of witnesses in herbrandized functional interpretations.

We formulate schemes and of the “typical” ∀∑ 1 b -sentences that are provable in T 2 1, respectively T 2 2. As an application, we reprove a recent result of Buss and Krajíček which describes witnesses for the ∀∑ 1 b -sentences provable in T 2 1 in terms of solutions to PLS-problems.

We formulate schemes and of the “typical” ∀∑ 1 b -sentences that are provable in T 2 1 , respectively T 2 2 . As an application, we reprove a recent result of Buss and Krajíček which describes witnesses for the ∀∑ 1 b -sentences provable in T 2 1 in terms of solutions to PLS-problems.

In the course of ten short sections, we comment on Gödel's seminal dialectica paper of fifty years ago and its aftermath. We start by suggesting that Gödel's use of functionals of finite type is yet another instance of the realistic attitude of Gödel towards mathematics, in tune with his defense of the postulation of ever increasing higher types in foundational studies. We also make some observations concerning Gödel's recasting of intuitionistic arithmetic via the dialectica interpretation, discuss the extra principles that (...) the interpretation validates and comment on extensionality and higher order equality. The latter sections focus on the role of majorizability considerations within the dialectica and related interpretations for extracting computational information from ordinary proofs in mathematics. (shrink)

Brazil stands out at the global level for having implemented several policies intending to promote agroecology as a productive paradigm for small-holder farmers. However, the impacts of this process of institutionalization of agroecology still lack research and debates that evaluate the effectiveness of these policies. In this paper, we assess and discuss the impacts of a policy specifically focused on education in agroecology, the support to the establishment of Centers for the Study of Agroecology and Organic Production (NEAs) in more (...) than 150 higher education institutions throughout Brazil. NEAs bring together teachers, researchers, and students who engage in teaching, research, and extension activities in partnerships with peasant farmers, their organizations, and rural extension workers. The hypothesis that guides our analysis is that this support to establish NEAs allowed redistribution of symbolic power in the universities where they were established, supporting agroecology to gain greater legitimacy inside and outside the university field. Based on an in-depth study of four NEAs, performed through participant observation and documentary analysis, the NEAs are evaluated from the perspective of social fields in dispute, first in a university sphere, but also from the perspective of training people in integrative and transdisciplinary thinking that will contest the industrial-corporate food regime. Our findings suggest that the State support to university groups dedicated to the promotion of agroecology has allowed the construction of what we have named agroecological spaces, which symbolically dispute the dominant paradigms in educational institutions, supporting the constitution of material and immaterial agroecological territories. (shrink)

We introduce a class of models of the bounded arithmetic theoryPV n . These models, which are generated by their tally part, have a curious feature: they have end-extensions or satisfyB∑ n b only in case they are closed under exponentiation. As an application, we show that if then the polynomial hierarchy does not collapse.

Recently, Feferman and Hellman (and Aczel) showed how to establish the existence and categoricity of a natural number system by predicative means given the primitive notion of a finite set of individuals and given also a suitable pairing function operating on individuals. This short paper shows that this existence and categoricity result does not rely (even indirectly) on finite-set induction, thereby sustaining Feferman and Hellman's point in favor of the view that natural number induction can be derived from a very (...) weak fragment of finite-set theory, so weak that finite-set induction is not assumed. Many basic features of finiteness fail to hold in these weak fragments, conspicuously the principle that finite sets are in one-one correspondence with a proper initial segments of a (any) natural number structure. In the last part of the paper, we propose two prima facie evident principles for finite sets that, when added to these fragments, entail this principle. (shrink)