|
|
Aatu Koskensilta wrote:
> Here's one version, faithful to the original idea.
Peter Smith contributed another version.
I'm having a lot of trouble matching these up.
> All formulas are boolean combinations of equations of the form
>
> t_1 = t_2
>
> where t_1 and t_2 are terms. The set of terms is defined inductively as
> follows.
Here it matters that terms are being defined AS STRINGS,
as OPPOSED to "symbolic expressions", which it was later falsely
alleged to be their type. Symbolic expressions are ubiquitously
conventionally tree-structured (we have LISP to thank for that).
> - A variable x is a term.
Or, rather, a variable-name is.
> - 0 is a term.
Or, rather, "0" is.
> - t + 1 is a term whenever t is
Or, rather t concatenated with "+ 1" is.
> - F(t_1, ..., t_n) is a term whenever t_i are and F is an n-ary
> function symbol
Yet DESPITE the presence of this rule, AK later insisted on
DENYING that + was a binary F here. While the "t" in "t + 1"
would've made a perfect t_1 here, he was adamant that the "1"
could NOT be a t_2.
That was just stupid, but that doesn't make it unworkable.
Nevertheless, the fact that this rule is, indeed, present,
does make it seem fundamentally silly that he's later going to
claim that 0 + 1 is a symbolic expression that is NOT an instance
of F(t_1,t_2) with F=+,t_1=0,and t_2=1. If you've bothered to BUY
the machinery then you might as well use it.
|
|