2.10 Compound Put sentences


The following definition rules of functions by each individual case emmerge often in traditional mathematics.

These definitions are done by compound put sentences and by blocks made by multiple lines like <compound.put.block>, they are written in such forms as below.

<label>:Put<general.function.form>=; <label>:<general.formula> if <term>;

<label>:<general.formula>if <term>;
.............
<label>:<general.formula> otherwise;

Specifically, it is written like this:

A0 : Put f(x)=;

A1 : 0 if GE(x,5);

A2 : 1 otherwise;

The formulas after "if" are inference terms and they all have to be logically exclusive with each other. This needs more explanation.

For example, when defining the following formula as function g,

we turn GE(x,5) into a proposition [x<=5] and GT(5,x) into [5<x] and GE(x,10)into [x <=10], and if we write

B0 :Put g(x)=;
B1 : 0 if GE (x,5) ;
B2 : 1 if GT (5,x) and GE (x,10) ;
B3 : 2 otherwise ;

it will be an error. It is because propositions GE(x,5) and {GT(5,x) and GE(x,10)} appear (propositional logically) to not be exclusive to each other. Therefore, in such cases, we have to write

B0 : Put g(x) = ;
B1 : 0 if GE (x,5) ;
B2 : 1 if not GE (x,5) and GE (x,10) ;
B3 : 2 otherwise ;

In this way, even if we do not know the meaning of functions GE or GT, the fact that [GE(x, 5)] and [not GE(x, 5)and GE(x, 10)] are exclusive to each other would be obvious.

Further, when such compound put sentences as above appear, other than new names being registered to a name table (ndirect), the following three formulas are also registered to a formula table (udirect).

B1 : (All x) (GE (x,5) imp [g(x)=0])
B2 : (All x) (not GE (x,5) and GE (x,10) imp [g(x)=1])
B3 : (All x) (not (GE (x,5) or not GE (x,5) and GE (x,10)) imp [g(x)=2])

As the above, formulas are transformed and then registered. Corresponding with "otherwise", formulas after "if" get connected by "or" and on top of that, "not" is attached (shown in B3). To connect formulas after "if" with "or", <term> needs to be inserted where"and" is the final operator following "if". For registered formulas after imp, they would have parentheses whenever needed , so we need to be careful when quoting.

Furthermore, the end of compound put sentences have to be otherwise sentences.