[FOM] Satisfies

[Peter Tenriffe]

I apologize for continuing to post while I am so far behind in reading
FOM.   But I want to get this written down before I forget the proof. -
Sandy

Satisfies is another semantic relation, one of several that allow a
purely extensional FOL to act, to some extent, as its own meta-language,
by referring to the Gödel numbers of its own expressions.   Other
semantic relations and predicates considered already have been:
   Denotes(g, x),  which means that the term G, whose G.n. is g, refers
to x.
   True(f), which means the formula F, whose G.n. is f, is true.

Satisfies(v, p, y) :  where p is the G.n. of a formula P(x) with one
open variable, and v is the G.n. of that variable, then Satisfies(v, p,
y) is equivalent to P(y).   For example suppose p is the G.n. of
"Human(x) => Mortal(x)".   In the numbering I am using, the G.n. of "x"
is 47.   Thus:
     Satisfies(47, p, Socrates)  <=>  ( Human(Socrates) =>
Mortal(Socrates) ).

I introduced an operator Unary(f, g).   If "F" and "G" have G.n.s f and
g, then the G.n. of "F(G)"  is Unary(f,g).

This axiom, called the Axiom of Denoted Item Satisfaction, relates the
three concepts, Denotes, True, and Satisfies.
   (\/ y, w) ( Denotes(y, w) => (\/ x) (
          True(Unary(x, y)) <=> (\/ v) Satisfies(v, Unary(x, v), w) ) )

For a given predicate, for example "Mortal(x)," an axiom using Satisfies
can associate that predicate with its G.n.  The G.n. of "Mortal" is
8550.   So we have the Predicate Axiom for Mortal:
   (\/ x) ( Mortal(x) <=> (\/ v) Satisfies(v, Unary(8550, v), x) )

Digital(x), for any non-negative integer x, is the G.n. of the standard
decimal representation of x.  I'll use N for positive integers.
-------------
For this exposition only, I introduce an operation SetFunc, where, given
terms K and W with G.n.s k and w:
   SetFunc(w, k) = the G.n. of "{ y e N | <K, y> e W }"

Also, a predicate EachUntrue, with G.n. 8701, such that:
   (\/ s) ( EachUnTrue(s) <=> (\/ f e s) ~ True(f) )

This introduced predicate, like any predicate, has a predicate axiom to
associate it with its G.n.
   (\/ x) ( EachUnTrue(x) <=> (\/ v) Satisfies(v, Unary(8701, v), x) )

I'll use "G" as abbreviation for the expression:
"{ p e (N x N) | (E x, y) ( p = <x, y> &
        y = Unary(8701, SetFunc(x, Digital(x)) ) ) }"

And "g" as abbreviation for the standard digital representation of the
G.n. of G.

And I'll use "D" as abbreviation for the expression:  "{y e N | <g, y> e
G}," or rather, if you take this expression and replace "G" and "g" by
what they abbreviate, "D" abbreviates the result.

And d is the G.n. of the expression D abbreviates.

>From the definitions of SetFunc and D, we have:
d = SetFunc( g, Digital(g) )

Define q = Unary( 8701, SetFunc(g, Digital(g)) )

For each x, G contains the ordered pair < x, Unary( 8701, SetFunc(x,
Digital(x)) ) > and no other ordered pair starting with x.  So G is a
function.   Only one ordered pair starting with g is in G, it is < g,
Unary( 8701, SetFunc(g, Digital(g)) ) >, aka <g, q>.   D is {y e N | <g,
y> e G}, so D = { q }.
------------
1.   Denotes(d, D) ; Assumption 1.

2.   D = { q } ; proved above.

3.   Denotes(d, {q}) ; Liebniz, 1, 2

4.   Denotes(d, {q}) => (\/ x) (
    True( Unary(x, d) ) <=> (\/ v) Satisfies(v, Unary(x, v), {q}) )  ;
   Axiom of Denoted Item Satisfaction.

5.   (\/ x) (
    True( Unary(x, d) ) <=> (\/ v) Satisfies(v, Unary(x, v), {q}) ) ;
    Modus Ponens, 3, 4

6.  True( Unary(8701, d) ) <=> (\/ v) Satisfies(v, Unary(8701, v), {q})
; \/elim, 5

7.   d = SetFunc( g, Digital(g) ) ; proved above.

8.   q = Unary(8701, SetFunc(g, Digital(g)) ) ; definition of q

9.   True( Unary(8701, SetFunc( g, Digital(g) )) ) <=>
      (\/ v) Satisfies(v, Unary(8701, v), {q}) ; Liebniz, 6, 7

10. True( q ) <=> (\/ v) Satisfies(v, Unary(8701, v), {q}) ; Liebniz, 9,
8

11.    (\/ x) ( EachUnTrue(x) <=> (\/ v) Satisfies(v, Unary(8701, v), x)
) ;
     Predicate Axiom for EachUnTrue

12.   EachUnTrue({q}) <=> (\/ v) Satisfies(v, Unary(8701, v), {q}) ;
     \/elim, 11

13. True( q ) <=> EachUnTrue({q})  ; Transitivity of <=>, 10, 12

14.  (\/ s) ( EachUnTrue(s) <=> (\/ f e s) ~ True(f) ) ;  Definitional
Axiom for EachUnTrue,

15.   EachUnTrue({q})  <=> (\/ f e {q}) ~ True(f) ; \/elim, 14

16.   (\/ f e {q}) ~ True(f)  <=> ~ True(q) ;  Transitivity of <=>, 13,
15, 16

17.  True(q) <=>  ~ True(q)

Contradiction.

Once again we have a choice as to which assumption to give up.   My own
choice is to give up Denotes(d, D).    This is another instance of the
same Naive Law of Denotation of Defined Sets, which I chose to reject in
the case of "Denotes".

The expression D names a perfectly valid set, equal to { q }.
Nevertheless the G.n. d of D does not Denote anything, I think.

One way to think about this is to consider "The least integer not
Denotable by an expression using less than 1000 symbols."   I'm pretty
sure I can express this, and I will not need 1000 symbols to do it.
This expression will, from the point of view of the meta-language, name
a number, but the G.n. of this expression will not Denote a number, in
the sense of Denote available from within the object language.

I think that when you have an expression  "{ x e S | phi(x) }", and
phi(x) itself contains semantic concepts, it can well happen that the
G.n. of  "{ x e S | phi(x) }" does not Denote { x e S | phi(x) }, and
that this must be true for any concept of Denote that is defined within
the object language.

It might seem that this is a reason to prefer the meta-language.   But
it is not.   Suppose you have an object language that does not contain
any semantic concepts.  When the object language has an expression {x e
S | phi(x)}, it will always be the case in the meta-language, that one
can talk about what "{x e S | phi(x)}" denotes, and that will refer to
what it really does denote.   But you will never be able to talk about
what "{x e S | phi(x)}" denotes for a phi(x) that contains semantic
concepts, because there are no semantic concepts in this object
language.  So moving to the meta-language makes you worse off, rather
than better.  If on the other hand you do want semantic concepts in the
object language, then I think they will always be subject to certain
limitations.

  [ The G.n. of "Human(x) => Mortal(x)" is 8551604770228550604770. ]
------- -- ---- - --- -- --------- -----
Sandy Hodges / Alameda,  California,   USA
mail to SandyHodges at attbi.com will reach me.