Enderton 3.4 Problem 1

**logics** · December 21st 2011, 04:26 AM

There is a representable relation Sb1 such that for a formula $\alpha$ , variable $x$ , and term $t$ , $<\sharp \alpha ,\sharp x,\sharp t> \in \text{Sb1}$ iff $t$ is substitutable for $x$ in $\alpha$ .

The necessary definitions can be found in

http://cs.nyu.edu/courses/fall03/G22...c/lec12_h4.pdf (slide 6, 9)

=============
t is substitutable for x in $\alpha$ if $\alpha$ is an atomic formula, and so on (Enderton p 113).

How do I prove this problem using the definition of "t is substitutable for x in $\alpha$ "?

Thanks.

**emakarov** · December 21st 2011, 11:08 AM

The list of representable sets and relations in your lecture notes is intended to produce an intuition that decidable relations are representable. In fact, this is stated in slide 11. I don't have the precise definition of "decidable" in your course, but by that I mean relations that can be precisely described by algorithms. In fact, $A_E$ can be considered as a programming language and formulas as programs that return true or false. In fact, using Gödel numbers as codes and arithmetical formulas is a remnant from the 1930s, when Gödel's incompleteness theorems were proved. It is more convenient to consider logics dealing with more complicated programming datatypes, like lists and trees.

However, not all formulas can be executed because of quantifiers. A quantifier corresponds to a loop in conventional programming languages, and an unbounded quantifier is an infinite loop. A paradigmatic example of an unbounded loop is a formula defining the relation $\{\sharp\alpha\mid A_E\vdash\alpha\}$ . This set is definable (in the sense of slide 10 of lecture 11) by the formula $\exists y\,\mathrm{Deriv}(y,x)$ where $\mathrm{Deriv}(y,x)$ represents the relation "y is the code of a derivation in $A_E$ of the formula with code x." But evaluating $\exists y\,\mathrm{Deriv}(y,S^n0)$ for each concrete n requires trying an unbounded number of y's.

If a formula has only bounded quantifiers, then there are two ways to evaluate it. The first is to find if it is true in $\mathcal{N}$ : we know how to evaluate closed atomic formulas $t_1=t_2$ and $t_1<t_2$ , and bounded quantifiers require considering only a finite number of cases. The second way is to search for a derivation of either the formula itself or its negation in $A_E$ . If a formula has only bounded quantifiers, then it is numeralwise determined, so one of the derivation exists. For such formulas, these two ways of evaluation are equivalent.

The definition of a substitutable term can be described by an algorithm. This description does not appeal to infinite loops. It just says that the a variable in not in the scope of some quantifiers. This can be described in the language of arithmetical formulas, but the result would be very long.

**logics** · December 23rd 2011, 04:05 AM

Thank you for your explanation.
===============
Edit: SB1 is the corresponding function for the Sb1 relation such that

$SB1(\sharp \alpha, \sharp x, \sharp t) =1$ iff $<\sharp \alpha, \sharp x, \sharp t> \in \text{Sb1}$ and $SB1(\sharp \alpha, \sharp x, \sharp t) =0$ iff $<\sharp \alpha, \sharp x, \sharp t> \notin \text{Sb1}$
=============
My attempt is as follows:

(The necessary definitions for Sb and Fr can be found in the slides in the previous link.)

Case 1:
$\alpha$ is an atomic formula:
$<\sharp \alpha, \sharp x, \sharp t> \in \text{Sb1} \leftrightarrow <\sharp \alpha, \sharp x, \sharp t> \in \text{Sb}$ .

Case 2: $t$ is substitutable for $x$ in $(\neg \alpha)$ iff it is substitutable for $x$ in $\alpha$ .
If $(\exists i < a)[i$ is the Gödel number of a wff $\& a = <h((), h(\neg)> *\text{ } i \text{ }* <h())>]$ then
$\text{SB1}(a, b, c) = <h((), h(\neg)> * \text{ SB1}(i, b, c) \text{ }* <h())>$

Case 3: $t$ is substitutable for $x$ in $(\alpha \rightarrow \beta)$ iff it is substitutable for $x$ in both $\alpha$ and $\beta$ .
If $(\exists i,j < a)[i$ and $j$ are the Gödel numbers of a wff $\& a = <h(()> \text{ * } i \text{ * } h(\rightarrow)> \text{ * }j \text{ * } <h())>]$ then

$\text{SB1}(a, b, c) = <h(()> * \text{ SB1}(i, b, c)$ $\text{ * } <h(\neg)>\text{ * }\text{SB1}(j, b, c)\text{ * }<h())>$

Case 4: $t$ is substitutable for $x$ in $\forall y \alpha$ iff $x$ does not occur free in $\forall y \alpha$ .
If $(\exists i,j < a)[i$ is the Gödel number of a variable $\& i \neq b \& j$ is the Gödel number of a wff $\& a = <h(\forall)> \text{ * } i \text{ * }j]$ then
$\text{SB1}(a, b, c) = <h(\forall)>\text{ * } i \text{ * }\text{SB1}(j, b, c)$ and $<\sharp \forall y, \sharp x> \in \text{Fr}$ (item 7 in the slide 9).

The remaining part is to apply the characteristic function for Sb1.

Is this approach O.K ?

Thanks.

**emakarov** · December 23rd 2011, 09:57 AM

The name of the relation $\{\langle\sharp a,\sharp x,\sharp t\rangle\mid t\mbox{ is substitutable for }x\mbox{ in }a\}$ in the PDF file (slide 9, item 9) is Sbl, not Sb1.

Originally Posted by logics

Case 1:
$\alpha$ is an atomic formula:
$<\sharp \alpha, \sharp x, \sharp t> \in \text{Sb1} \leftrightarrow <\sharp \alpha, \sharp x, \sharp t> \in \text{Sb}$ .

$Sb$ is a function, not a relation. If you want the corresponding relation, you need four arguments. However, you need to define whether the term is substitutable, not the result of substitution. In fact, a term is always substitutable in an atomic formula.

Originally Posted by logics

Case 2: $t$ is substitutable for $x$ in $(\neg \alpha)$ iff it is substitutable for $x$ in $\alpha$ .
If $(\exists i < a)[i$ is the Gödel number of a wff $\& a = <h((), h(\neg)> *\text{ } i \text{ }* <h())>]$ then
$\text{SB1}(a, b, c) = <h((), h(\neg)> * \text{ SB1}(i, b, c) \text{ }* <h())>$

SB1 is a characteristic function; it should return 0 or 1.

Originally Posted by logics

Case 4: $t$ is substitutable for $x$ in $\forall y \alpha$ iff $x$ does not occur free in $\forall y \alpha$ .

No. What's the use of substituting a term for a variable if the variable does not occur free? The result would be an identical formula. A term t is substitutable for a variable x if no variable in t is captured when x is replaced by t.

Note that you define SB1 by strong (or complete, or course-of-values) recursion, when the value at a may depend on the value at any number less than a. Strong recursion is expressible through regular primitive recursion and sequences, so it's not more powerful.

**logics** · December 24th 2011, 05:34 AM

I have changed my previous post into the updated one using the characteristic function. Let f be the corresponding characteristic function for the relation Sbl.

Case 1:
f(a)=1 if a is the Gödel number of an atomic formula.

Case 2:
f(a)=1 if $(\exists i < a)[a = <h((), h(\neg)> *\text{ } i \text{ }* <h())>$ and f(i)=1].

Case 3:
f(a)=1 if $(\exists i,j < a)[a = <h(()> \text{ * } i \text{ * } <h(\rightarrow)> \text{ * }j \text{ * } <h())>$ and $f(i)=f(j)=1]$ .

According to my textbook (Enderton page 113),

t is substitutable for x in $\forall y \alpha$ iff either
(a) x does not occur free in $\forall y \alpha$ (although it is of no use as you mentioned), or
(b) y does not occur in t and t is substitutable for x in $\alpha$ .

I think I need to make Case 4 based on the above definition.

Is this approach O.K?

Thanks.

**emakarov** · December 24th 2011, 06:17 AM

Yes, this seems fine.

Thread: Enderton 3.4 Problem 1

LinkBack

Thread Tools

Display

Enderton 3.4 Problem 1

Re: Enderton 3.4 Problem 1

Re: Enderton 3.4 Problem 1

Re: Enderton 3.4 Problem 1

Re: Enderton 3.4 Problem 1

Re: Enderton 3.4 Problem 1

Similar Math Help Forum Discussions

Enderton Problem 3.5

Enderton 3.3 Problem 5

Enderton 3.3 Problem 8

Enderton 3.1 problem 1 (p.193)

Enderton 3.1 Problem 6 (p. 193)

Search Tags