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)

In an attempt to accommodate natural language phenomena involving nominalization and self-application, various researchers in formal semantics have proposed abandoning the hierarchical type system which Montague inherited from Russell, in favour of more flexible type regimes. We briefly review the main extant proposals, and then develop a new approach, based semantically on Aczel's notion of Frege structure, which implements a version ofsubsumption polymorphism. Nominalization is achieved by virtue of the fact that the types of predicative and propositional complements (...) are contained in the type of individuals. Russell's paradox is avoided by placing a type-constraint on lambda-abstraction, rather than by restricting comprehension. (shrink)

In a previous paper we investigated the extraction of proof-theoretic properties of natural deduction derivations from their impredicative translation into System F. Our key idea was to introduce an extended equational theory for System F codifying at a syntactic level some properties found in parametric models of polymorphic type theory. A different approach to extract proof-theoretic properties of natural deduction derivations was proposed in a recent series of papers on the basis of an embedding of intuitionistic propositional logic into a (...) predicative fragment of System F, called atomic System F. In this paper we show that this approach finds a general explanation within our equational study of second-order natural deduction, and a clear semantic justification in terms of parametricity. (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)

A class of models is presented, in the form of continuation monads polymorphic for first-order individuals, that is sound and complete for minimal intuitionistic predicate logic . The proofs of soundness and completeness are constructive and the computational content of their composition is, in particular, a β-normalisation-by-evaluation program for simply typed lambda calculus with sum types. Although the inspiration comes from Danvyʼs type-directed partial evaluator for the same lambda calculus, the use of delimited control operators is avoided. The role of (...) polymorphism is crucial – dropping it allows one to obtain a notion of model complete for classical predicate logic. (shrink)

ABSTRACT A computational logic, PLPR (Predicate Logic using Polymorphism and Recursion) is presented. Actually this logic is the object language of an automated deduction system designed as a tool for proving mathematical theorems as well as specify and verify properties of functional programs. A useful denotationl semantics and two general deduction methods for PLPR are defined. The first one is a tableau algorithm proved to be complete and also used as a guideline for building complete calculi. The second is (...) a sound and complete natural deduction system. Moreover a fixed point induction rule is introduced for formulas called continuous. The strategies for mechanizing the proofs of the final automated system are based on the previous deduction methods. As the examples of the use of the system show, the implemented theorem prover outperforms humans to a certain extent, retaining logic and calculi generality. (shrink)

As is well-known, the formal system in which Frege works in his Grundgesetze der Arithmetik is formally inconsistent, Russell’s Paradox being derivable in it.This system is, except for minor differ...

We introduce a predicative version of topos based on the notion of small maps in algebraic set theory, developed by Joyal and one of the authors. Examples of stratified pseudotoposes can be constructed in Martin-Löf type theory, which is a predicative theory. A stratified pseudotopos admits construction of the internal category of sheaves, which is again a stratified pseudotopos. We also show how to build models of Aczel-Myhill constructive set theory using this categorical structure.

Terminologically, the “topos of mu” and the “predicative self” originated in the Kyoto School and are traceable to the work of its founder NISHIDA Kitarō. The full phrase was coined by NAKAMURA Yūjirō. Conceptually, the topos of mu or place of nothingness is Nishida’s development of the Buddhist notion of anatta or no self and radiating out from that locus of emptiness is a self constituted by its predicates or the things to which it is connected by an existential (...) copula. Deeply ingrained in Western languages, metaphysics, and religion is the subjective self, in both the linguistic and psychological senses of “subjective.” That Buddhism, as reworked by the Kyota School, or Daoism, or any other non-Western tradition of thought, will catch on in the West was a puerile fantasy of some members of the first generation of environmental philosophers. There is a good chance, however, that the Western worldview may evolve toward a similar conception of the self—as ecological, relational, or systems thinking becomes ever more ingrained. We in the West may come to understand that we are constituted by our social and environmental relationships, in which we are deeply embedded and on which we are utterly dependent, such that world care is the essence of self-help. (shrink)

The main purpose of the article is to analyze the statements of philosophical Ukrainian Studies about the anthropological specifics of Ukrainian philosophical thought by means of historicalphilosophical cultural-predicative analysis. The research methodology was determined primarily by the concept of cultural attribution and translation in the dialogue of languages of historical cultures of the Poznań Methodological School (J. Topolski, W. Wrzosek, E. Domańska) and the culturological approach in historical-philosophical Ukrainian Studies (V. Horskyi, S. Rudenko). The statements of the language of (...) historical and philosophical Ukrainian studies are analyzed by means of historicalphilosophical cultural-predicative analysis. The latter is a specific humanities research strategy, which we propose as a means of studying the communicative specifics and syntactic correctness of the language of historical-philosophical theory. The study of communicative specifics takes place from the perspective of modernized versions of metaphysical, phenomenological, and dialectical logic. The first is understood as the logic of transcendental metaphysics, the second as the logic of immanent metaphysics, and the third as the logic of procedural metaphysics. Such an approach provides a qualitative and comprehensive understanding of the analyzed statements. The statements of the language of the historical-philosophical theory are generalized in its names, depending on the perspective of one of the three versions of the logic of philosophical reasoning. The offered historical-philosophical cultural-predicative analysis of communicative specifics and the syntactic correctness of the Ukrainian historical-philosophical theory statements opens new dimensions in research of the anthropological specifics of Ukrainian philosophy. (shrink)

Expressives are words that convey speakers’ attitudes towards a particular object or situation. Consider two examples:Attributive: That f**khead Jeremy forgot the turkey.Predicative: Jeremy is a f**khead. In both examples the word f**khead communicates some expressive content - the negative attitude of the speaker. However, only in Predicative does it appear to contribute to the truth-conditional content. The task is to explain the semantics of the word f**khead when it seemingly behaves wildly differently in different syntactic positions. In this (...) paper I consider several good candidates for dealing with f**khead occurring in Predicative position: Expressivist and Descriptive approaches that treat f**khead in Predicative as purely descriptive; and Expressive-Contextualism that treats Predicative as communicating to both expressive and descriptive dimensions. I show that none of the options fully capture the meaning of f**khead. Treating Predicative as purely descriptive leaves out the highly important expressive element, whilst Contextualist semantics does not seem as a suitable descriptive theory for expressives. I finally present a novel hybrid account that combines Expressivist semantics with Relativism. I call this view Expressive-Relativism. I show that by adopting Expressive-Relativism we can not only explain the relationship of f**khead in Attributive and Predicative, but also give a suitable descriptive theory that captures the truth-conditions of Predicative. (shrink)

An ω-model (a model in which all natural numbers are standard) of the predicative fragment of Quine's set theory "New Foundations" (NF) is constructed. Marcel Crabbe has shown that a theory NFI extending predicative NF is consistent, and the model constructed is actually a model of NFI as well. The construction follows the construction of ω-models of NFU (NF with urelements) by R. B. Jensen, and, like the construction of Jensen for NFU, it can be used to construct (...) α-models for any ordinal α. The construction proceeds via a model of a type theory of a peculiar kind; we first discuss such "tangled type theories" in general, exhibiting a "tangled type theory" (and also an extension of Zermelo set theory with Δ 0 comprehension) which is equiconsistent with NF (for which the consistency problem seems no easier than the corresponding problem for NF (still open)), and pointing out that "tangled type theory with urelements" has a quite natural interpretation, which seems to provide an explanation for the more natural behaviour of NFU relative to the other set theories of this kind, and can be seen anachronistically as underlying Jensen's consistency proof for NFU. (shrink)

In the paper we survey the known connections between theories that extend a common base theory with typed truth axioms on the one hand and predicative set-existence assumptions on the other. How general can the mutual reductions between truth and comprehension be taken to be? In trying to address this question, we consider classical, positive truth and predicative comprehension as operations on theories.

This essay examines how Husserl stretches the bounds of his philosophy of meaning, according to which all propositions are categorical, to account for existential propositions, which seem to lack predicates. I examine Husserl’s counterintuitive conclusion that an existential proposition does possess a predicate and I explore his endeavor to pinpoint what that predicate is. This goal is accomplished in three stages. First, I examine Husserl’s standard theory of predication and categorial intuition from his 1901 Logical Investigations. Second, I show how (...) Husserl imposes those 1901 insights to uncover the predicate of the existential proposition in unpublished manuscripts and lectures. He determines that the existential proposition predicates of the subject, that it corresponds to an actual object. This analysis reveals that Husserl’s descriptions of existential propositions from the late 1890s employed both static and genetic methodologies. In those texts, he carefully untangles and clarifies the co-enmeshed passive and active moments of consciousness and shows that the passive givenness of certain circumstances is the condition of possibility for our active verifying of propositions. Finally, I execute a critical assessment of Husserl’s thought to reveal that, while his insights about existential propositions are largely correct, they are augmented by re-construing them within the context of his mature philosophy. Only by renouncing his metaphysical neutrality and by accounting for intersubjectivity, can Husserl properly clarify existential propositions. (shrink)

In this article, we address the problem of how people understand predicative metaphors such as “The rumor flew through the office,” and argue that predicative metaphors are understood as indirect (or two-stage) categorizations. In the indirect categorization process, the verb (e.g., fly) of a predicative metaphor evokes an intermediate entity, which in turn evokes a metaphoric category of actions or states (e.g., “to spread rapidly and soon disappear”) to be attributed to the target noun (e.g., rumor), rather (...) than directly evoking a metaphoric category as argued by CitationGlucksberg's (2001) categorization theory. We test our argument using two experiments, namely, offline comprehension and online priming. The offline comprehension experiment showed that interpretation of predicative metaphors had greater overlap with words indirectly associated with the verb than those directly associated with the verb. The online priming experiment demonstrated that indirectly associated words were activated during predicative metaphor comprehension, but directly associated words were not. These results provide convergent evidence for our argument, and thus the psychological validity of two-stage categorization as a process of predicative metaphor comprehension was confirmed. (shrink)

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)

In [1] Todorov has shown by means of axiomatic set theory that there exists a nonstandard function Δ: *ℝn → * ℂ such that for all continuous functions φ: ℝn → ℂ, equation image.Here *ℝ and *ℂ are the set of the nonstandard real numbers and the set of the nonstandard complex numbers, respectively, and *φ: *ℝn → *ℂ is the nonstandard extension of φ In the present note we want to prove an analogous theorem by predicative means only.

I argue that a tripartite analysis of simple statements such as “Bucephalus is a horse”, according to which they divide into two terms and a copula, requires the notion of a repeatable: something such that more than one particular can literally be it. I pose a familiar dilemma with respect to repeatables, and turn to Avicenna for a solution, who discusses a similar dilemma concerning quiddities. I conclude by describing how Avicenna’s quiddities relate to repeatables, and how both quiddities and (...) repeatables may contribute to a tripartite analysis of predication. (shrink)