Failure of completeness properties of intuitionistic predicate logic for constructive models : (preliminary report)
Daniel M. Leivant · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1975
We consider a principle of constructivity RED which states that every decidable predicate over the natural numbers is (weakly) recursively enumerable (r.e.).RED is easily seen to be derived from Church's thesis CT 0 ("every construction is given by a recursive function").Results:(I) RED implies that the species of valid first order predicate schemata is not r.e., and hence -that intuitionistic first order predicate logic LI is incomplete.(2) We construct a specific schema of LI which is valid if RED, but unprovable in LI .(3) The two results above hold even when validity is generalized to validity with KREISEL-TROELSTRA [70]'s choice sequences as parameters.(4) The method is used also to construct a schema of LI, unprovable in LI, but of whose all metasubstitutions with L~ number theoretic predicates are provable in Heyting's arithmetic A. This is a simple bound on possible improvements of the absoluteness result of LEIVANT [75].