[FOM] Formal treatment of expressions that refer to each other

[Sandy Hodges]

VI.  DEFINITIONAL AXIOM FOR "ValRef"

For the sake of the presentation, I will alter the example slightly, so
that instead of saying "The sum of the numbers designated by Abelard's
utterances," Heloise says "The sum of the integers designated by
Abelard's first utterance, plus, the sum of the integers designated by
Abelard's second utterance."   Abelard's second utterance is modified
similarly.

This definitional axiom for a binary relation, "ValRef," will allow the
lovers to be more concise:

(\/ s) (\/ u e UtOccasions) ( ValRef(s,u) = Sum( { x e s | (E g e NN)(E
v e UtOccasions) ( v = u & Uttered(v, g) & Designates(v, g, x) ) } ) )

The meaning of "ValRef(s,u)" is thus: that member of s which was
designated on utterance occasion u, or if no member of s was designated,
then zero.

The exact formulas Abelard utters are:

"17"
"ValRef(ZZ, DayOccasion(Heloise,Easter1117,1) ) + ValRef(ZZ,
DayOccasion(Heloise,Easter1117,2) )"

the formulas Heloise utters are:

"62"
"ValRef(ZZ, DayOccasion(Abelard,Easter1117,1) ) + ValRef(ZZ,
DayOccasion(Abelard,Easter1117,2) )"

the formula Alberic utters is:

"ValRef(ZZ, DayOccasion(Abelard,Easter1117,1) ) + ValRef(ZZ,
DayOccasion(Abelard,Easter1117,2) )"

VII.   QUOTATION BY GODEL NUMBER

I want to express the Heloise-Abelard example in the language that the
characters in the example use.   That is, I want to say that Abelard did
indeed utter "17" on Easter Sunday Anno Domi. 1117, and so on.    The
language has no mechanism of quotation (and no intensional contexts of
any kind).   The way to refer to an expression of the language, from
within the language, will be by Gödel number.    So I could say:

(E g e NN) ( Uttered(DayOccasion(Abelard,Easter1117,2),g) &
 g =
82096082106982076084216985316951707030820960821069820760842169853169527070
)

to convey what it was that Abelard said, but no one would be the wiser
for this.   So some operators and relations concerning Gödel numbers
will be useful.    The concatenation operator "\." joins numbers in
Hindu-Arabic notation, so "20 \. 58 = 2058".   The operator has this
definitional axiom:

(\/ a,b e ZZ)(E d,x e NN) (  a \. b = a*d+b  &  d > b  &  d < 10*b  &  d
= 10^x)

In the Gödel numbering I am using, the logical constant "Abelard" is
assigned the Gn. 8420.   In order to prove, within the language, that a
Gn. containing "8420" has any connection with Abelard, we need the
axiom:

Denotes(8420,Abelard)

And similarly the axioms:

Denotes(8421,Heloise)
Denotes(8423,Alberic)
Denotes(8531,Easter1117)

Here are three axioms for the Gödel numbering of positive integers:

(\/ z e ZZ)( ( 0 <= z  &  z <= 9 )   <=>   Digit(50+z,z)

(\/ c,x e NN)(\/ z e ZZ)( ( 0 <= z  &  z <= 9  )   =>  (
Digit(c*100+50+z,x*10+z) <=> Digit(c,x) ) )

(\/ z e ZZ)(\/ g e NN) ( Digit(g,z) => Denotes(g,z) )


The right and left parentheses are 60 and 70 in the numbering, and the
comma is 69.    These axioms introduce relations useful for building the
Gns. of compound expressions:

(\/ r,a,b e NN) ( BinR(r,a,b) = ( r \. 60 ) \. (( a \. 69 ) \. ( b \. 70
))   )

(\/ r,a,b,c e NN) ( TertR(r,a,b,c) = (( r \. 60 ) \. ( a \. 69 )) \. ((
b \. 69 ) \. ( c \. 70 ))   )


The Gn. of "DayOccasion" is 8207.   So the Gn. of
"DayOccasion(Abelard,Easter1117,2)" is TertR(8207,8420,8531,52).

The Gns. of "ValRef" and "ZZ" are 8209  and 8210, so

BinR(8209,TertR(8207,8420,8531,52)) is the Gn. of
"ValRef(ZZ, DayOccasion(Abelard,Easter1117,2))".

VIII.    UNIQUE DESIGNATION AXIOM

(\/ u,v e UtOccasions) (\/ g e NN) (\/ x,y) ( Designates(u,g,x) &
Designates(v,g,y) => x = y )

IX.    DENOTES DEFINITIONAL AXIOM, and DENOTATION AXIOM

(\/g e NN) (\/ x) (  Denotes(g,x) <=> (\/ u e UtOccasions)
Designates(u,g,x) )

And we can derive the Unique Denotation theorem:

(\/ g e NN) (\/ x,y) ( Denotes(g,x) & Denotes(g,y) => x = y )

And this motivates the unary operation "Denotation" with the axiom

(\/ g e NN) Denotes(g,Denotation(g))

X.  GODEL NUMBER OF DayOccasion OPERATION

Here's an axiom that establishes the relation between "DayOccasion" and
its Gn. 8207.

(\/ p,d,n e NN) (\/ u) ( ( u =
DayOccasion(Denotation(p),Denotation(d),n)
                               &  u e UtOccasions ) =>
        Denotes(  TertR(8207,p,d,Digit(n)),  u ) )

This allows some useful propositions to be proved, such as:

Denotes( TertR(8207,8420,8531,52), DayOccasion(Abelard,Easter1117,2) )




------- -- ---- - --- -- --------- -----
Sandy Hodges / Alameda,  California,   USA
mail to SandyHodges at attbi.com will reach me.