[FOM] On definitions of terms, and free logic---a quick follow-up

[Tennant, Neil]

Harvey proposes indefinite-ary (but presumably finitary?) braces as functions or operators: {blah blah blah}.
Looking forward to the details. Presumably he will lay down first principles that will enable one to prove the following sequent:

Ft1 , ... , Ftn, (x)(Fx -> (x=t1 v ... v x=tn)) : {x|Fx}={t1,...,tn} ?

---and to prove such things as

{x|x=t} = {t} = {t,t} = {t,t,t,} ... ;
{x|x=t v x=u} = {t,u} = {u,t} = {t,t,u} = {t,u,t} = {u,t,t} = ... = {t,u,t, t,u,t, t,u,t} = ... ?

What advantages will the complication of adding indefinite-ary braces have, for the formalization of mathematical reasoning, over the definitional abbreviation strategy of simply reading {t1,...,tn} as short for {x|x=t1 v ... v x=tn}?


Neil Tennant
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20151028/8774de48/attachment-0001.html>