A non-uniformly C-productive sequence & non-constructive disjunctions

John Case, Michael Ralston, Yohji Akama

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Let φ be an acceptable programming system/numbering of the partial computable functions: ℕ = {0; 1; 2; …} →ℕ, where, for p ∈ ℕ N, φp is the partial computable function computed by program p of the φ-system and Wp = domain(φp). Wp is, then, the computably enumerable (c.e.) set accepted by p. The first author taught in a class a recursion theorem proof employing a pair of cases that, for each q, {x | φx = φq} is not computably enumerable. The particular pair of cases employed was: domain(φq) is infinite vs. finite - incidentally, by Rice's Theorem, a non-constructive disjunction. Some student asked why the proof involved an analysis by cases. The answer given straightaway to the student was that his teacher didn't know how else to do it. The present paper provides, among other things, a better answer: any proof that, for each q, {x | φx = φq} is not c.e. provably must involve some such non-constructiveness. Furthermore, completely characterized are all the possible such pairs of (index set based) cases that will work. Along the way, relevantly explored are uniform lifts of the concept completely productive (abbr: c-productive) sets to sequences of sets. The c-productive sets are the effectively non-c.e. sets. A set sequence Sq, q ∈ ℕ, is said to be uniformly c-productive iff there is a computable f so that, for all q, x, f(q, x) is a counterexample to Sq = Wx. Relevance: a completely constructive proof that each Sq is not c.e. would entail the Sqs forming a uniformly c-productive sequence. Relevantly shown, then, is that the sequence {x | φx = φq}, q ∈ ℕ, is not uniformly c-productive | and this even though, of course, the set {‹q, x›| φx = φq} is c-productive. For some results we provide upper and/or lower bounds for them as to position in the Arithmetical Hierarchy of the Law of Excluded Middle needed in addition to Heyting Arithmetic. Results are also obtained for similar problems, including for run-time bounded programming systems and other subrecursive systems. Proof methods include recursion theorems.

Original languageEnglish
Title of host publicationProceedings of the 13th Asian Logic Conference, ALC 2013
EditorsXishun Zhao, Qi Feng, Byunghan Kim, Liang Yu
PublisherWorld Scientific Publishing Co. Pte Ltd
Pages29-52
Number of pages24
ISBN (Print)9789814675994
DOIs
Publication statusPublished - 2013
Event13th Asian Logic Conference, ALC 2013 - Guangzhou, China
Duration: 2013 Sep 162013 Sep 20

Publication series

NameProceedings of the 13th Asian Logic Conference, ALC 2013

Other

Other13th Asian Logic Conference, ALC 2013
CountryChina
CityGuangzhou
Period13/9/1613/9/20

Keywords

  • Arithmetically limited law of excluded middle
  • Clocked programming systems
  • Complete productivity
  • Constructivity
  • Index sets
  • Recursion theorems
  • Uniformly computable

ASJC Scopus subject areas

  • Hardware and Architecture
  • Computer Vision and Pattern Recognition
  • Computational Theory and Mathematics

Fingerprint Dive into the research topics of 'A non-uniformly C-productive sequence & non-constructive disjunctions'. Together they form a unique fingerprint.

Cite this