Results 1 to 6 of 6

Math Help - Enderton 3.4 Problem 1

  1. #1
    Junior Member
    Joined
    Nov 2011
    Posts
    59

    Enderton 3.4 Problem 1

    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.
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,530
    Thanks
    774

    Re: Enderton 3.4 Problem 1

    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.
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Junior Member
    Joined
    Nov 2011
    Posts
    59

    Re: Enderton 3.4 Problem 1

    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.
    Last edited by logics; December 23rd 2011 at 05:12 AM.
    Follow Math Help Forum on Facebook and Google+

  4. #4
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,530
    Thanks
    774

    Re: Enderton 3.4 Problem 1

    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.

    Quote Originally Posted by logics View Post
    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.

    Quote Originally Posted by logics View Post
    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.

    Quote Originally Posted by logics View Post
    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.
    Follow Math Help Forum on Facebook and Google+

  5. #5
    Junior Member
    Joined
    Nov 2011
    Posts
    59

    Re: Enderton 3.4 Problem 1

    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.
    Follow Math Help Forum on Facebook and Google+

  6. #6
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,530
    Thanks
    774

    Re: Enderton 3.4 Problem 1

    Yes, this seems fine.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Enderton Problem 3.5
    Posted in the Discrete Math Forum
    Replies: 1
    Last Post: January 5th 2012, 11:49 AM
  2. Enderton 3.3 Problem 5
    Posted in the Discrete Math Forum
    Replies: 7
    Last Post: December 19th 2011, 07:34 AM
  3. Enderton 3.3 Problem 8
    Posted in the Discrete Math Forum
    Replies: 3
    Last Post: December 19th 2011, 05:46 AM
  4. Enderton 3.1 problem 1 (p.193)
    Posted in the Discrete Math Forum
    Replies: 8
    Last Post: December 4th 2011, 10:30 AM
  5. Enderton 3.1 Problem 6 (p. 193)
    Posted in the Discrete Math Forum
    Replies: 6
    Last Post: December 3rd 2011, 12:12 PM

Search Tags


/mathhelpforum @mathhelpforum