« first day (9 days earlier)      last day (21 days later) » 

15:43
@spaceisdarkgreen Ad "write down some long formula in the language of set theory defining what a formula is". Just to expand what that actually means, as seemingly we dealing here with 2 levels of formulas: The "long formulas" are those living in background theory (...about which we know to be a set theory, eg ZF), and these are defining what (syntactically) formulas in object theory are, in sense of that formulas of backgrd theory define syntax/wfness of formulas of object theory, is that
what you mean in this sentence?
@spaceisdarkgreen And when you draw connection to Andres' notes, where essentially is elaborated how to formulas of object theory are consistently associated sets, you mean it in the way that once formulas from object theory are "translated" into sets, the free variables of the formulas from background theory can be naturally evaluated in these "as sets encoded formulas" (from obj theory)? So in short, once we have performed this procedure from Andres' notes mapping
@spaceisdarkgreen consistently formulas from object theory to sets, the variables of background theory formulas can be "naively" evaluated in these, and that's the joke?
16:13
what joke?
To your first, yes.
(Although we need to do a lot more defining than just wf-ness etc to end up with the basic definitions model theory.)
 
2 hours later…
18:18
@spaceisdarkgreen And is also what I wrote in 2nd paragraph of last comment correctly stated? So that this whole business described in the script to translate formulas of object theory to sets serves to make the formulas from background theory to be evaluatable in these through their variables?

« first day (9 days earlier)      last day (21 days later) »