2.9 Simple Put Sentences


As introduced before, this is a simple replacement of names or functions. Further, a logical proposition is included in functions. A simple put sentence is written in one sentence with a line saying<simple.put. line>. That general form is such:

<label>:put <general.function.form>=<general.formula>;

This<general.function.form>can be<name>.

For example,
AB : Put f(x)=Nat(x) and GT(1, x);
C4 : Put 2= P1(1);
a3 : Put Commutative(S) (p)=(All x)

(All y)(S(x) and S(y) imp[p (x, y)=p(y,x)]);

D4 : Put add3(x, y, z)=Add (Add(x,y), z);

When there is a simple put sentence, the system does mainly two things. One of them is to register the names that are newly defined to a name table. From the example above, name f from formula AB, name 2 from formula C4, name Commutative from formula a3, and name add3 from formula D4 are registered to a name table. Furthermore, new names go to the left side of the equalities which come behind the Put. New names must not appear to the right side of the equalities. Namely, new names that emerge at the right side of the equalities must already be registered to a name table at that point.

The second job that the system performs is to register new names to a formula table (udirect), and make it so that they can be cited by labels later. From the example above, let us indicate what kinds of formulas get registered to a formula table. For each label,

AB : (All x)([f(x)=Nat(x)and GT(1,x)])
C4 : [2=P1(1)]
a3 : (All S)(All p)([Commutative (S)(p)=(All x)(All y)(S(x)and S(y)imp[p(x,y)=p(y,x)])])
D4 : (All x)(All y)(All z)([add3(x,y,z)=Add(Add(x,y),z)])

Therefore, the arguments on the left side of the function form all become bound variables and the whole formula becomes quantitized. Such formulas as C4 which does not have an argument will not have all the symbols attached to it; the equalities formulas will only be enclosed by Japanese quotation marks. Therefore, when citing put sentences, one needs to be careful because formulas that were changed as above will be used, instead of the original formulas that start with Put.