[FOM] 617: Removing Connectives 1

[Harvey Friedman]

We explore what happens to PA when we restrict the kinds of
connectives and quantifiers allowed. We have five connectives and two
quantifiers. There are 2^7 possibilities here for restrictions. We let
X be a subset of these seven.

We write L(PA,X) for the set of sentences in L(PA), whose connectives
and quantifiers all lie in X.

The main issue we want to address concerning L(PA,X)  is: in what
sense is L(PA) and L(PA,X) really the same? If not, what is the
relationship between them?

There are semantic and proof theoretic aspects of this study.

In this first posting, we focus only on the most obvious formulation
of this question, which is purely semantic.

What is the complexity of the set of true sentences of L(PA,X)?

THEOREM 1. Let X contain the existential quantifier and negation or
implication or equivalence or universal quantifier.. TRUE(PA,X) is
bi-reducible to TRUE(PA).

THEOREM 2. Let X contain the existential quantifier with no negation,
implication, equivalence, or universal quantifier. TRUE(PA,X) is
complete r.e.

THEOREM 3. Let X contain the  universal quantifier and negation or
implication or equivalence or existential quantifier. TRUE(PA,X) is
bi-reduciable to TRUE(PA).

THEOREM 4. Let X contain the universal quantifier with no negation or
implication or equivalence or existential quantifier. TRUE(PA,X) is
recursive.

THEOREM 5. Let X contain no quantifier. Then TRUE(PA,X) is recursive.

The above relies on the well known fact that every r.e. relation on N
is purely existential in 0,S,+,x (Hilbert's 10th Problem) - MRDP = Y.
Matiyasevich, J. Robinson, M. Davis, H. Putnam.

**********************************************************
My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
This is the 617th in a series of self contained numbered
postings to FOM covering a wide range of topics in f.o.m. The list of
previous numbered postings #1-599 can be found at the FOM posting
http://www.cs.nyu.edu/pipermail/fom/2015-August/018887.html

600: Removing Deep Pathology 1  8/15/15  10:37PM
601: Finite Emulation Theory 1/perfect?  8/22/15  1:17AM
602: Removing Deep Pathology 2  8/23/15  6:35PM
603: Removing Deep Pathology 3  8/25/15  10:24AM
604: Finite Emulation Theory 2  8/26/15  2:54PM
605: Integer and Real Functions  8/27/15  1:50PM
606: Simple Theory of Types  8/29/15  6:30PM
607: Hindman's Theorem  8/30/15  3:58PM
608: Integer and Real Functions 2  9/1/15  6:40AM
609. Finite Continuation Theory 17  9/315  1:17PM
610: Function Continuation Theory 1  9/4/15  3:40PM
611: Function Emulation/Continuation Theory 2  9/8/15  12:58AM
612: Binary Operation Emulation and Continuation 1  9/7/15  4:35PM
613: Optimal Function Theory 1  9/13/15  11:30AM
614: Adventures in Formalization 1  Sep 14 13:43:28 EDT 2015
615: Adventures in Formalization 2  Sep 14 13:44:13 EDT 2015
616: Adventures in Formalization 3  Sep 14 13:45:01 EDT 2015

Harvey Friedman