la xorxes has already replied while I am preparing my response, but this may make the problem clearer.
I may agree the point of your idea, but have some objections.
Le mercredi 8 avril 2015 06:52:23 UTC+9, Jacob Errington a écrit :
I'm making a separate thread out of this because I'm going on a tangent here.
On 7 April 2015 at 15:04,
<co...@ccil.org> wrote:
Terms can have FA or tags equally well, but we don't want to merge
FA with BAI generally, to avoid things like "se fa" and ".i fa bo",
which are nonsense.
I agree that {se fa} has no clear interpretation upon first examination. However, {.i fa bo} can be interpreted like any other {.i TAG bo} construct.
.i broda .i TAG bo brode -> .i broda TAG lo su'u brode
Hence,
.i broda .i fa bo brode -> .i broda fa lo su'u brode
This provides us with another way to do essentially what {la'e di'e} does. For instance,
.i mi pu pensi la'e di'e .i lo mi bruna cu cmalu mutce -> .i mi pu pensi .ifebo lo mi bruna cu cmalu mutce
I was thinking about this: my brother is very short.
Taking this idea to the extreme, we can conceive of a somewhat silly higher-order predicate -- call it {brodrfV} for now -- whose x1 is an arbitrary sumti and whose x2 is a nullary predicate supplied with than fV having the value of the x1. We can define {brodrfV} with the following statement.
.i ko'a brodrfV lo du'u broda <=> broda fV ko'a
Your idea seems not a kind of higher-order logic, but simply extraction of an argument from a bridi. Higher-order logic deals with both predicates and arguments in its universe of discourse, while your idea does not seem requiring a universe of discourse in the clause composing x2 of {brodrfV}.
Therefore, {du'u} should be replaced with {ka}, because a bridi in {du'u}-clause has a truth value based on its own universe of discourse, which is generally distinguished from the universe of discourse of the outer bridi. On the other hand, a bridi in {ka}-clause is an open sentence with a free variable {ce'u}. A bridi in {si'o}-clause is also an open sentence with all variables are free, but not suitable for the current topic in which only one argument is extracted by {brodrfV}.
The definition should be then :
.i ko'a brodrfV lo ka fV ce'u broda <=> broda fV ko'a
We can derive some obvious results from this statement.
.i lo brodrfV be lo du'u fV ko'a broda === ko'a
.i fV ko'a broda === .i fi'o brodrfV ko'a broda
Based on the same idea, the first line should be :
.i lo brodrfV be lo ka fV ce'u broda = ko'a
which denotes a substitution of a constant satisfying x1 of {brodrfV} by {ko'a}, not a result derived from the definition of {brodrfV}.
mu'o