We introduce an extension of the propositional calculus to include abstracts of predicates and quantifiers, employing a single rule along with a novel comprehension schema and a principle of extensionality, which are substituted for the Bernays postulates for quantifiers and the comprehension schemata of ZF and other set theories. We prove that it is consistent in any finite Boolean subset lattice. We investigate the antinomies of Russell, Cantor, Burali-Forti, and others, and discuss the relationship of the system to other set-theoretic (...) systems ZF, NBG, and NF. We discuss two methods of axiomatizing higher order quantification and abstraction, and then very briefly discuss the application of one of these methods to areas of mathematics outside of logic. (shrink)

In [Waragai & Shidori, 2007], a system of paraconsistent logic called PCL1, which takes a similar approach to that of da Costa, is proposed. The present paper gives further results on this system and its related systems. Those results include the concrete condition to enrich the system PCL1 with the classical negation, a comparison of the concrete notion of “behaving classically” given by da Costa and by Waragai and Shidori, and a characterisation of the notion of “behaving classically” given by (...) Waragai and Shidori. (shrink)

This paper is a sequel to Beall (2011), in which I both give and discuss the philosophical import of a result for the propositional (multiple-conclusion) logic LP+. Feedback on such ideas prompted a spelling out of the first-order case. My aim in this paper is to do just that: namely, explicitly record the first-order result(s), including the collapse results for K3+ and FDE+.

Traditional combinatory logic uses combinators S and K to represent all Turing-computable functions on natural numbers, but there are Turing-computable functions on the combinators themselves that cannot be so represented, because they access internal structure in ways that S and K cannot. Much of this expressive power is captured by adding a factorisation combinator F. The resulting SF-calculus is structure complete, in that it supports all pattern-matching functions whose patterns are in normal form, including a function that decides structural equality (...) of arbitrary normal forms. A general characterisation of the structure complete, confluent combinatory calculi is given along with some examples. These are able to represent all their Turing-computable functions whose domain is limited to normal forms. The combinator F can be typed using an existential type to represent internal type information. (shrink)

This paper presents and defends a way to add a transparent truth predicate to classical logic, such that and A are everywhere intersubstitutable, where all T-biconditionals hold, and where truth can be made compositional. A key feature of our framework, called STTT (for Strict-Tolerant Transparent Truth), is that it supports a non-transitive relation of consequence. At the same time, it can be seen that the only failures of transitivity STTT allows for arise in paradoxical cases.

the world of phenomena is immensely large this means we can perceive only part of the world. We see, feel and hear parts of reality, not the whole of it, and it seems that a sentence containing a verb of perception like 'John sees a house burn' is most naturally treated as saying that the subject sees an incomplete world in which the embedded sentence is true (see Barwise (1981) for this analysis). But if we want to analyse perception verbs (...) thus, we must introduce some form of incompleteness into our formal system, the.. (shrink)

RésuméUn paradigme en vogue en informatique théorique exploite l'analogie entre les formules et les types et traite une deduction Al… An→ B comme une opération plurisortale. On propose ici d'étendre cette analogie aux déductions de la forme Al… An→, où la place à droite de la flèche est vide. D'un point de vue logique, une telle déduction constitue une réfutation de la conjonction desformules qui se trouvent à gauche de la flèche. On défend l'idée qu'ilfaut, selon ce paradigme étendu, interpréter (...) la flèche comme assignant à n'importe quelle séquence al… an, où aiest de type Ai, le type des valeurs de vérite correspondantes. Pour que cela fonctionne, cependant, il faut abandonner la règle structurale de l'affaiblissement à droite de la flèche. La négation de A est alors interprétée comme l'ensemble puissance de A et la complétude fonctionnelle habituelle s'identifie au schème de compréhension avec extensionnalitè. (shrink)

Cet article s'ajoute à la liste déjà longue de ceux qui traitent des rapports entre la théorie russellienne des descriptions définies et la théorie ramifiée des types. Seule la prétention d'aborder cette question dans une perspective nouvelle justifie ici sa présence: d'une part, la théorie des descriptions définies sera resituée dans le contexte initial et souvent méconnu de la théorie des expressions dénotantes et d'autre part, c'est à la logique intensionnelle de Russell, objet d'une méconnaissance au moins égale, que nous (...) nous intéresserons. De plus, c'est du point de vue de la théorie de la signification et non pas du point de vue ontologique, génético-historique ou logico-mathematique que nous nous proposons de traiter de ces rapports. (shrink)

Smullyan in [Smu61] identified the recursion theoretic essence of incompleteness results such as Gödel's first incompleteness theorem and Rosser's theorem. Smullyan showed that, for sufficiently complex theories, the collection of provable formulae and the collection of refutable formulae are effectively inseparable—where formulae and their Gödel numbers are identified. This paper gives a similar treatment for proof speed-up. We say that a formal system S1is speedable over another system S0on a set of formulaeAiff, for each recursive functionh, there is a formulaαinAsuch (...) that the length of the shortest proof ofαin S0is larger thanhof the shortest proof ofαin S1. We characterize speedability in terms of the inseparability by r.e. sets of the collection of formulae which are provable in S1but unprovable in S0from the collectionA–where again formulae and their Gödel numbers are identified. We provide precise definitions of proof length, speedability and r.e. inseparability below.We follow the terminology and notation of [Rog87] with borrowings from [Soa87]. Below,ϕis an acceptable numbering of the partial recursive functions [Rog87] andΦa complexity measure associated withϕ[Blu67], [DW83]. (shrink)

By language we understand a lower predicate calculus with identity and (perhaps) relation and function symbols. It is convenient to allow for more than one sort of variable. Now each individual constant (if there are any) is of a specified sort, the formal expressions R(t1, … tn), f(t1,…, tn) are well formed only if the terms t1, …, tn are of specified sorts determined by the relation symbol R and the function symbol f, and the term f(t1, …, tn) (if (...) well formed) is of a sort determined by f. We admit s = t as well formed, no matter what the sorts of s and t. (shrink)

Arguments to the effect that Church's thesis is intrinsically unprovable because proof cannot relate an informal, intuitive concept to a mathematically defined one are unconvincing, since other 'theses' of this kind have indeed been proved, and Church's thesis has been proved in one direction. However, though evidence for the truth of the thesis in the other direction is overwhelming, it does not yet amount to proof.

The form of nominalism known as 'mathematical fictionalism' is examined and found wanting, mainly on grounds that go back to an early antinominalist work of Rudolf Carnap that has unfortunately not been paid sufficient attention by more recent writers.

is a fragment of first-order aritlimetic so weak that it cannot prove the totality of an iterated exponential fimction. Surprisingly, however, the theory is remarkably robust. I will discuss formal results that show that many theorems of number theory and combinatorics are derivable in elementary arithmetic, and try to place these results in a broader philosophical context.

Formal approaches that aim at representing human reasoning should be evaluated based on how humans actually reason. One way of doing so is to investigate whether psychological findings of human reasoning patterns are represented in the theoretical model. The computational logic approach discussed here is the so-called weak completion semantics which is based on the three-valued ᴌukasiewicz logic. We explain how this approach adequately models Byrne’s suppression task, a psychological study where the experimental results show that participants’ conclusions systematically deviate (...) from the classical logically correct answers. As weak completion semantics is a novel technique in the field of computational logic, it is important to examine how it corresponds to other already established non-monotonic approaches. For this purpose we investigate the relation of weak completion with respect to completion and three-valued stable model semantics. In particular, we show that well-founded semantics, a widely accepted approach in the field of non-monotonic reasoning, corresponds to weak completion semantics for a specific class of modified programs. (shrink)

In this paper we describe the well-founded initial segment of the free Heyting algebra ������α on finitely many, α, generators. We give a complete classification of initial sublattices of ������₂ isomorphic to ������₁ (called 'low ladders'), and prove that for 2 < α < ω, the height of the well-founded initial segment of ������α.

A common and much-explored thought is Łukasiewicz's idea that the future is ‘indeterminate’—i.e., ‘gappy’ with respect to some claims—and that such indeterminacy bleeds back into the present in the form of gappy ‘future contingent’ claims. What is uncommon, and to my knowledge unexplored, is the dual idea of an overdeterminate future—one which is ‘glutty’ with respect to some claims. While the direct dual, with future gluts bleeding back into the present, is worth noting, my central aim is simply to sketch (...) and briefly explore an alternative glutty-future view, one that is conservative—indeed, entirely classical—with respect to the present. The structure of the paper runs as follows. §1 briefly sketches the target gap picture of an indeterminate future yielding gappy claims at the present. §2 presents the direct dual idea—a glut picture of an overdeterminate future yielding glutty claims at present. §3 sketches the central idea, a more interesting glut picture in which the future contains contradictory states but the present remains entirely classical. §4 contains a general defence of the idea, leaving it open as to whether the gappy-future view enjoys substantive virtues over the proposed glutty-future view of §3. (shrink)

In a previous paper the concept of disease was fuzzy-logically analyzed and a sketch was given of a prototype resemblance theory of disease (Sadegh-Zadeh (2000). J. Med. Philos., 25:605–38). This theory is outlined in the present paper. It demonstrates what it means to say that the concept of disease is a nonclassical one and, therefore, not amenable to traditional methods of inquiry. The theory undertakes a reconstruction of disease as a category that in contradistinction to traditional views is not based (...) on a set of common features of its members, that is individual diseases, but on a few best examples of the category, called its prototypes, and a similarity relationship such that a human condition is considered a disease if it resembles a prototype. It enables new approaches to resolving many of the stubborn problems associated with the concept of disease. (shrink)

A well known fact is that every Lebesgue measurable set is regular, i.e., it includes an F$_{\sigma}$ set of the same measure. We analyze this fact from a metamathematical or foundational standpoint. We study a family of Muchnik degrees corresponding to measure-theoretic regularity at all levels of the effective Borel hierarchy. We prove some new results concerning Nies's notion of LR-reducibility. We build some $\omega$-models of RCA$_0$which are relevant for the reverse mathematics of measure-theoretic regularity.

In this paper a new property of theories, called effective retractability is introduced and used to obtain a characterization for the degrees of subtheories of arithmetic and set theory. By theory we understand theory in standard formalization as defined by Tarski [10]. The word degree refers to the Kleene-Post notion of degree of recursive unsolvability [2]. By the degree of a theory we mean, of course, the degree associated with its decision problem via Gödel numbering.

The standard natural deduction rules for the identity predicate have seemed to some not to be harmonious. Stephen Read has suggested an alternative introduction rule that restores harmony but presupposes second-order logic. Here it will be shown that the standard rules are in fact harmonious. To this end, natural deduction will be enriched with a theory of definitional identity. This leads to a novel conception of canonical derivation, on the basis of which the identity elimination rule can be justified in (...) a proof-theoretical manner. (shrink)

A logic \ is called self-extensional if it allows to replace occurrences of a formula by occurrences of an \-equivalent one in the context of claims about logical consequence and logical validity. It is known that no three-valued paraconsistent logic which has an implication can be self-extensional. In this paper we show that in contrast, there is exactly one self-extensional three-valued paraconsistent logic in the language of \ for which \ is a disjunction, and \ is a conjunction. We also (...) investigate the main properties of this logic, determine the expressive power of its language, and provide a cut-free Gentzen-type proof system for it. (shrink)

In diesem Aufsatz wird ein neues Paradoxon vorgestellt, der Super-Lügner. Er ist stärker als alle bekannten Lügner-Sätze, nicht mehr eindeutig selbstreferentiell und läßt sich darüber hinaus in eindeutig in die Tarski-Hierarchie einordnen. Eine unendlich große Familie von Super-Lügnern auf Metaebenen ist konstruierbar. Schließlich widersetzt sich der Super-Lügner der Auflösung durch die neue vielversprechende Reflexionslogik LR von U. Blau.

If complexity is a necessary but not sufficient premise for the existence and expression of the living, anticipation is the distinguishing characteristic of what is alive. Anticipation is at work even at levels of existence where we cannot refer to intelligence. The prospect of artificially generating aesthetic artifacts and ethical constructs of relevance to a world in which the natural and the artificial are coexistent cannot be subsumed as yet another product of scientific and technological advancement. Beyond the artificial, the (...) synthetic conjures the understanding of aesthetics and ethics no longer from the perspective of the How? type of question, but rather the Why? Given the current infatuation with synthetic biology (i.e., making life from non-life), there is a practical consequence to such considerations. Synthetic life, as any other form of life, implies the possibility of evolution. Anticipation, which is the underlying factor of evolution, is thus expected. At the level of human existence, anticipation is expressed, for instance (but not exclusively), in aesthetic forms and ethical values. This translates, in turn, into an argument for the role aesthetics and ethics play in the process. Consequently, to qualify as life, the synthesis of the physical and the living will have to efficiently handle ambiguity. Current computational facilities, regardless of their nature or performance, operate exclusively in the semiotic domain of the well defined non-ambiguous. (shrink)

Martin [4, Theorems 1 and 2] proved that a Turing degree a is the degree of a maximal set if, and only if, a′ = 0″. Lachlan has shown that maximal sets have minimal many-one degrees [2, §1] and that every nonrecursive r.e. Turing degree contains a minimal many-one degree [2, Theorem 4]. Our aim here is to show that any r.e. Turing degree a of a maximal set contains an infinite number of maximal sets whose many-one degrees are pairwise (...) incomparable; hence such Turing degrees contain an infinite number of distinct minimal many-one degrees. This theorem has been proved by Yates [6, Theorem 5] in the case when a = 0′. The need for this theorem first came to our attention as a result of work done by the author [3, Theorem 2.3]. There we looked at the structure / obtained from the recursive functions of one variable under the equivalence relation f ~ g if, and only if, f(x) = g(x) a.e., that is, for all but finitely many x ∈, where M is a maximal set, and M is its complement. We showed that / 1 ≡ / 2 if, and only if, 1 = m 2, i.e., 1. and 2 have the same many-one degree. However, it might be possible that some Turing degree of a maximal set contains exactly one many-one degree of a maximal set. Theorem 1 was proved to show that this was not the case, and hence that the theory of / is not an invariant of Turing degree. (shrink)

A myth has arisen concerning Turing's paper of 1936, namely that Turing set forth a fundamental principle concerning the limits of what can be computed by machine - a myth that has passed into cognitive science and the philosophy of mind, to wide and pernicious effect. This supposed principle, sometimes incorrectly termed the 'Church-Turing thesis', is the claim that the class of functions that can be computed by machines is identical to the class of functions that can be computed by (...) Turing machines. In point of fact Turing himself nowhere endorses, nor even states, this claim (nor does Church). I describe a number of notional machines, both analogue and digital, that can compute more than a universal Turing machine. These machines are exemplars of the class of _nonclassical_ computing machines. Nothing known at present rules out the possibility that machines in this class will one day be built, nor that the brain itself is such a machine. These theoretical considerations undercut a number of foundational arguments that are commonly rehearsed in cognitive science, and gesture towards a new class of cognitive models. (shrink)

ABSTRACTA conditional is natural if it fulfils the three following conditions. It coincides with the classical conditional when restricted to the classical values T and F; it satisfies the Modus Ponens; and it is assigned a designated value whenever the value assigned to its antecedent is less than or equal to the value assigned to its consequent. The aim of this paper is to provide a ‘bivalent’ Belnap-Dunn semantics for all natural implicative expansions of Kleene's strong 3-valued matrix with two (...) designated elements. (shrink)