[FOM] FOL as its own meta-language : Satisfies

[Sandy Hodges]

I continue to investigate the properties of a first-order language, with
Leibniz' law, that acts to some extent as its own meta-language using
relations between the Gödel numbers of its own expressions, and the
objects of its domain.

My previous posting on this subject touched off a long discussion about
Leibniz' law and intensional and extensional contexts.    In
investigating first-order languages with Leibniz' law, I do not wish to
claim that these languages could be used to express any philosophical
claim that anyone might wish to make, concerning the state of our
knowledge about the identity of the author of Hamlet, for example.
First-order logics with Leibniz' law are notorious for their weakness in
just this respect.   My point is that when the languages have the
ability to refer to their own expressions by means of the numbering,
they acquire abilities which I consider it quite surprising that a
first-order, purely extensional logic should have.

My latest results concerns a relation Satisfies, which holds between the
G.n. of an expression with an open variable, such as "Greek(x) &
Male(x)", and each individual for which the expression holds.

1.  One observation is that this relation makes possible some things
that you couldn't do if you were trying to relate a set (the extension
of the predicate) to the G.n. of the predicate formula.     Thus if g is
the G.n. of  "~(x e x)", then Satisfies(g, z) holds for each z such that
~(z e z).   There is of course no such set as { z | ~ (z e z ) }.

2.   The obvious axiom schema for Satisfies, given the meaning, is what
I call the Naive Law of Satisfaction.   It says that for "P(x)" any
formula with one open variable, with p the digital form of the G.n. of
"P(x)," then this is an axiom:
    (\/ x) ( Satisfies(p, x) <=> P(x) )
This axiom schema leads to a contradiction.  The proof, which I'll post
if anyone wants to see it, is based on the proof of Tarski's theorem.

3.  The alternative to the Naive law of satisfaction, are these weak
laws of satisfaction and dissatisfaction (which must be introduced).
These laws are, under the same conditions,
   (\/ x) ( Satisfies(p, x) => P(x) )
   (\/ x) ( Dissatisfies(p, x) => ~P(x) )
These laws do not need to be introduced as axiom schemas, as any
individual instance of them can be proved using axioms from a finite
list.  Some of these axioms are given below.

4.   I define a few operators to make manipulating G.n.s easier.
Where a and b are the G.n.s of expressions A and B, and where r is the
G.n. of relation R,   Infix(a, r, b), is the G.n of "A R B" or of "(A) R
B", or of "A R (B)" or of "(A) R (B)", depending on the associative
priority of the operators.  a %e b is defined as Infix(a, 28, b), where
28 is the G.n. of the element-of relation e.   A few other operators,
such as %=, %&, %V, %=>, and %<=>, are defined similarly.   %x is a
constant, equal to 47, which is the G.n. of variable "x".   %/0 is a
constant equal to 10, which is the G.n. of "/0", the null set symbol.
a // b is the G.n of A(B).

4A.  Given these definitions, ((%x %e %/0 ) %V f) is thus the G.n. of
"(x e /0) V F".   And (x e /0) is of course not the case for any x.

5.   "True" can be defined in terms of Satisfied, and "False" in terms
of Dissatisfied, as
    (\/ f) ( True(f) <=> Satisfies( ((x %e %/0 ) %v f), /0
   (\/ f) ( False(f) <=> Dissatisfies( ((x %e %/0 ) %v f). /0)
I am using /0 as ascii code for the null set symbol.

5B.   The weak laws of satisfaction and dissatisfaction, together with
the definitions of True and False, yield this theorem schema:
     for "P" any formula with no open variables, with p the digital form
of the G.n. of "P" these are theorems:
       True(p) => P
       False(p) => ~P

6.  Satisfies is a relation between items and the G.n.s of formulas with
one open variable.   If we have a formula phi(x, y, z) with two or more
variables, we can look at the expression
    (E x, y, z) ( p = {<1, x>, <2, y>, <3, z>} & phi(x, y, z) )
This is an expression with only one open variable, p, and asking whether
it is Satisfied by some item, is comparable to asking whether phi(x, y,
z) is satisfied by some three items.

7.   The relation I talked about earlier, Denotes, can be defined in
terms of Satisfies.
   (\/ p, y) ( Denotes(p, y) <=> Satisfies( (%x %= p), y )
There is also a Disdenotes
   (\/ p, x) ( Disdenotes(p, x) <=> Dissatisfies((%y %= p), x )

7A.   Thus Satisfies and Dissatisfies are the only semantic relations
needed, since True, False, Denotes, Disdenotes can be defined, and
Satisfies can be used for formulas with more than one open variable as
well as just one.

8.   Many (all, as far as I know) constants get an axiom like this one,
which relates the constant with its G.n.   Here is the example for "/0".

    (\/ y) ( Satisfies( (%x %= 10), y ) <=> y = /0 )

9.   Many predicates, but not "True" and "False" get an axiom like this
one:   Here is the axiom for "Mortal" which has G.n. 8550.
      (\/ y) ( Satisfies( (8550 // %x), y ) <=> Mortal(y) )
9A.  For "True" and "False" the axiom is in one direction only
      (\/ y) ( Satisfies( (8223 // %x), y ) => True(y) )

10.   Some Axioms:
    (\/ a, b) (   True(a // b) <=> a e Predicates & (E y) ( Satisfies(
(a // %x), y) & Satisfies( (%x %= b), y ) )  )
    (\/ a, b) (   False(a // b) <=> a e Predicates & (E y) (
Dissatisfies( (a // %x), y) & Satisfies( (%x %= b), y ) )  )

   (\/ a) (     True(%~ a) <=> False(a) )
   (\/ a) (     False(%~ a) <=> True(a) )

     (\/ a, b) (    True(a %V b) =>  True(a) V True(b)   )
     (\/ a, b) (    True(a %V b) <=>  True(b %V a)   )
     (\/ a, b) (    True(a) & ( True(b) V False(b) ) => True(a %V b)   )

    (\/ a, b) (    True(a %& b) <=>  True(a) & True(b)   )

    (\/ a, b) (    False(a %& b) =>  False(a) & False(b)   )
     (\/ a, b) (    False(a %& b) =>  False(b %& a)   )
     (\/ a, b) (    False(a) & ( True(b) V False(b) ) => False(a %& b)
)
    (\/ a, b) (    False(a %V b) <=>  False(a) V False(b)   )

    (\/ a, b) (    True(a %=> b) <=>  True( (%~ a) %V b)   )
    (\/ a, b) (    True(a %<=> b) <=>  True( (a %=> b) %& (b %=> a)   )

   (\/ a, b) (    False(a %=> b) <=>  False( (%~ a) %V b)   )
    (\/ a, b) (    False(a %<=> b) <=>  False( (a %=> b) %& (b %=> a)
)

     (\/ v, p, x, y) (  Satisfies( (v %= p), x ) & Satisfies( (v %= p),
y ) => x = y )

     (\/g, h, a, b) (  Denotes(g, a) & Denotes(h, b) => Denotes(Pair(g,
h), <a, b>)  )

11.  An axiom schema:
Where g is the digital form of the G.n. of any expression of the form
"{x e S | phi(x) }," and s is the digital form of the G.n. of the
sub-expression S,  then this is an axiom:
               (E y) Denotes(s, y) & (E z) Denotes(g, z) => Denotes(g, {
x e S | phi(x) } )

------- -- ---- - --- -- --------- -----
Sandy Hodges / Alameda,  California,   USA
Remove THESE WORDS from SandyTHESEhodges at AlamedaWORDSnet.net
Note: This is a new address as of 20 June 2003