Predicate Logics of Constructive Arithmetical Theories

2006 ◽  
Vol 71 (4) ◽  
pp. 1311-1326 ◽  
Author(s):  
Albert Visser
Keyword(s):  
Predicate Logic ◽  
Uniqueness Condition ◽  
Church’S Thesis ◽  
Church's Thesis

AbstractIn this paper, we show that the predicate logics of consistent extensions of Heyting's Arithmetic plus Church's Thesis with uniqueness condition are complete . Similarly, we show that the predicate logic of HA*. i.e. Heyting's Arithmetic plus the Completeness Principle (for HA*) is complete . These results extend the known results due to Valery Plisko. To prove the results we adapt Plisko's method to use Tennenbaum's Theorem to prove ‘categoricity of interpretations’ under certain assumptions.

Lifschitz' realizability

1990 ◽  
Vol 55 (2) ◽  
pp. 805-821 ◽  
Author(s):  
Jaap van Oosten
Keyword(s):  
Axiomatic Characterization ◽  
Uniqueness Condition ◽  
Church’S Thesis ◽  
Second Order Arithmetic ◽  
Elementary Analysis ◽  
Continuous Application ◽  
Church's Thesis ◽  
Order Arithmetic ◽  
Intuitionistic Arithmetic

AbstractV. Lifschitz defined in 1979 a variant of realizability which validates Church's thesis with uniqueness condition, but not the general form of Church's thesis. In this paper we describe an extension of intuitionistic arithmetic in which the soundness of Lifschitz' realizability can be proved, and we give an axiomatic characterization of the Lifschitz-realizable formulas relative to this extension. By a “q-variant” we obtain a new derived rule. We also show how to extend Lifschitz' realizability to second-order arithmetic. Finally we describe an analogous development for elementary analysis, with partial continuous application replacing partial recursive application.

Proving Church's Thesis

2000 ◽  
Vol 8 (3) ◽  
pp. 244-258 ◽  
Author(s):  
ROBERT BLACK
Keyword(s):  
Church’S Thesis ◽  
Church's Thesis

scholarly journals Reflections on Church's thesis.

1987 ◽  
Vol 28 (4) ◽  
pp. 490-498 ◽  
Author(s):  
Stephen C. Kleene
Keyword(s):  
Church’S Thesis ◽  
Church's Thesis

Trial and error predicates and the solution to a problem of Mostowski

1965 ◽  
Vol 30 (1) ◽  
pp. 49-57 ◽  
Author(s):  
Hilary Putnam
Keyword(s):  
Finite Number ◽  
Correct Answer ◽  
Decision Procedure ◽  
Finite Sequence ◽  
Decision Procedures ◽  
Turing Machines ◽  
Trial And Error ◽  
Church’S Thesis ◽  
Church's Thesis ◽  
Empirical Means

The purpose of this paper is to present two groups of results which have turned out to have a surprisingly close interconnection. The first two results (Theorems 1 and 2) were inspired by the following question: we know what sets are “decidable” — namely, the recursive sets (according to Church's Thesis). But what happens if we modify the notion of a decision procedure by (1) allowing the procedure to “change its mind” any finite number of times (in terms of Turing Machines: we visualize the machine as being given an integer (or an n-tuple of integers) as input. The machine then “prints out” a finite sequence of “yesses” and “nos”. The last “yes” or “no” is always to be the correct answer.); and (2) we give up the requirement that it be possible to tell (effectively) if the computation has terminated? I.e., if the machine has most recently printed “yes”, then we know that the integer put in as input must be in the set unless the machine is going to change its mind; but we have no procedure for telling whether the machine will change its mind or not.The sets for which there exist decision procedures in this widened sense are decidable by “empirical” means — for, if we always “posit” that the most recently generated answer is correct, we will make a finite number of mistakes, but we will eventually get the correct answer. (Note, however, that even if we have gotten to the correct answer (the end of the finite sequence) we are never sure that we have the correct answer.)

Epistemic Church’s Thesis and Absolute Undecidability

2016 ◽  
pp. 254-272
Author(s):  
Marianna Antonutti Marfori ◽  
Leon Horsten
Keyword(s):  
Church’S Thesis ◽  
Church's Thesis
Sign in / Sign up

Export Citation Format

Share Document