user267839

@spaceisdarkgreen Think slowly I got it now, thanks a lot for the explanations ...and patience :)

@spaceisdarkgreen Do the last comments make sense?

@spaceisdarkgreen In other words, eg the formula Form(x) is actually strictly speaking a predicate on sets, eg map SETS \to {0,1} which evaluates to 1 in a set S iff S encodes a formula from object theory under the procedure presented in the script. Did I phrased it now acurately?

are evaluated in sets. Eg if under above map we map an object language fmla \phi(x) to a set S(\phi(x)), then strictly speaking the predicate Form(x) is evaluated in sets(!) and what it does is that it feedbacks if a set S where it is evaluated comes from a fmla from object theory via the above map \phi(x) to S(\phi(x)). Did I understood it correctly?

@spaceisdarkgreen Just to avoid confusions about the machanism presented in the linked script: Strictly speaking there happens several steps. Firstly, there is introduced an inductive process associating to formulas from object theory(!) cerain sets (in a compatible way), so something like $\phi(x) \to S(\phi(x)) \in SETS. Then the formulas from background theory,eg like Form(x) which "detects" if the inputed x is a wf formula of the object theory is strictly speaking

If what I wrote in 2nd part is wrong then - passing a step back - what is meant by "to write formal definition of a formula"? Write as what, and where? As a predicate in background language?

In other words, that this $\psi(x)$ is a predicate formula phrased in background language - which "accepts" as arguments evaluated in x formulas from object theory and which decides if the input x is syntactically well formed as formula ob object theory?

Is this what you mean in quoted sentence?

@spaceisdarkgreen Another point ad: "By "encode formulas as sets" I mean the same thing "write formal definitions of formulas from logic/model theory in the language of set theory" ": So you mean by this that we there produce formulas in language of set theory which accept as arguments formulas from logic/model theory and carry information if the inserted argument (=formula from logic\model theory) is well formed? Eg, \psi(x):=" x is well formed formula in object language".

@spaceisdarkgreen A typo: In prev question in last line I actually meant "...procedure assuring that formulas of this language L' can evaluate in their variables statements about model theory (not meta, as I wrongly wrote abve) of T?"[...]

the language L' would be expressible enough to incluee a statement like $M\models \psi$ where $M$ is a model of T and \psi a wf proposition in language of T?

@spaceisdarkgreen A nitpick: You refered a couple of times to "formalize the model theory (of a theory) in a language". Could you sketch what this procedure means? A guess: Say we have a formal theory T. Then, does it mean to "formalize the model theor of this T in certain (formal) language L' - which, a priori has noting to do with language of T itself - a procedure assuring that formulas of this language L' can evaluate in their variables statements about metatheory of T? Eg,

@spaceisdarkgreen Yes, that was exactly the point I wasn't sure about if that was linguistically the same, thanks!

Ups, a correction: I meant that the sentence "And also, for a specific formula, we can write down a definition in the language of set theory of that formula, which the background theory will be able to prove satisfies the previously mentioned definition of what a formula is[...] is in middle ("to prove satisfies") syntactically (not grammatically) oddly stated

These two parts of the quoted sentence seem to grammatically not to fit together, making it hard to understand what is actually meant there

@spaceisdarkgreen This is essentially rephrasing of the first part of the quoted sentence, ie the part "And also, for a specific formula, we can write down a definition in the language of set theory of that formula, which the background theory will be able to prove[...]". This one I understand. What I not understand is the sequent subordinate clause "...satisfies the previously mentioned definition of what a formula is[...]"

...sorry for annoying meticulousness, but I not understand the grammatical composition of that part of this quoted sentence making it difficult to understand its actual meaning

Even just grammatically, its not clear what "...to prove satisfies..." means

what is said there.

@spaceisdarkgreen Could you reformulate/clarify the sentence "[...]for a specific formula, we can write down a definition in the language of set theory of that formula, which the background theory will be able to prove satisfies the previously mentioned definition of what a formula is..." The part "...about to prove satisfies the prev..." I not understand semantically.

(...this part of the sentence is difficult to parse)

@spaceisdarkgreen then the backgrnd theory will be able to proof what? You wrote "will be able to prove satisfies the previously mentioned definition of what a formula is". Could you explain it, I'm not sure what you mean in this passage?

@spaceisdarkgreen Furthermore, I not fully understand the statement "And also, for a specific formula, we can write down a definition in the language of set theory of that formula, which the background theory will be able to prove satisfies the previously mentioned definition of what a formula is [...]". You mean if we pick a specific formula from object theory(?) whose definition we can write down in backgrnd theory (...latter makes sense since backgrd theory is a set theory),

@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?

@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?

@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

what you mean in this sentence?

@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

Or, maybe I misunderstood what you actually meant in the quoted sentence...

@spaceisdarkgreen But here I'm just refering to definition in en.m.wikipedia.org/wiki/Theory_(mathematical_logic). Just that a formal theory consists by definition of some sentences, that's it. On the other hand, where you wrote "formulas of the object theory that need to be encoded as sets in the background theory" raises a "domain error" problem: If a container consists of formulas you cannot put sets in it .

previously quoted sentence that formulae of object theory are encoded as sets(!) in background theory. Surely, as you said, background theory used to reason about sets, but itself it not contains sets, only some formulae (declared to be its axioms)

@spaceisdarkgreen More precisely, as you write "The formal background theory is (semantically) about sets". Yes, but itself as "datum" the formal background theory consists of a bunch of formulas, not more not less, do you agree? So even if backgrd theory is about sets, it consist as every formal of theory just of certain formulas, not eg sets. Thus I not understand what you mean in

But if background theory is a formal theory - independently of if it is additionally also a set theory - it consists by definition of a bunch of formulas phrased in its formal language, or not? (As previously you wrote that from formalist's view object- and background theories are seen as formal theories)

@spaceisdarkgreen When you say a formal theory (...as formalists we assume background theory is a formal theory) is a "set theory" you mean by this a formal theory (... in sense of the wiki link from prev comnt) subjected to restrictive condition that it's underlying formal language has to be given by only one symbol $\{ \in \}$, right? If yes, then I still not understand the sentence "formulas of the object theory that need to be encoded as sets in the background theory":

A guess:So, say $\varphi(x)$ is a formula in object language, then we as first step we "encode it as certain set" - say $S:=S(\varphi(x))$- which at this stage only lives in metatheory, but then - in next step - associate a constant symbol $c_S$ with this set S and extend now the background theory by this constant $c_S$. Is this the trick you are refering above to when you say "formulae of obj thoery encoded as sets in the background theory"?

Therefore I not understand what you actually mean by "formulas of the object theory that need to be encoded as sets in the background theory" as a formal theory "not knows" sets. Or, do you mean by this an additional step that these "formulas encoded as sets" are implemented into extension of background theory as added NEW constant terms?

@spaceisdarkgreen ...Maybe to avoid talking past another: When one says "formal theory" I'm thinking of this datum: en.m.wikipedia.org/wiki/Theory_(mathematical_logic) And so far I understand your point formalists treat object theory and backgrnd theories as formal theories, right? (...to contrast them from informal metatheory) But a formal theory "knows" only formulae phrased in underlying forml language.

@spaceisdarkgreen Maybe another point ad "It's the formulas of the object theory that need to be encoded as sets in the background theory": What you mean by "sets in background theory"? From formalist's perspective backgrd theory is treated strictly as a formal theory, that consists as any formal theory of a bunch of wf formulas (=axioms) written in certain fixed undrlying formal language ( ie inclding a alphabet, syntax rules apparatus). What does it mean to say that a "formal theory contains sets"?

@spaceisdarkgreen this "encoding as sets" precedure correctly - it picks this formula $\varphi(x)$ - a prori regarded as object from object theory - and produces a "copy"/ reproduction of $\varphi(x)$ as term in background theory, making the formula "M\models \exists x\varphi(x)" linguistically understandable for background theory's language? Is this the idea & raison d'être for this "encoding as sets" machinery here?

@spaceisdarkgreen More concretely, eg we want that our background theory T' "formalizes" model theory of the object theory T. This would imply that background theory have to be able to include formulas like eg "M\models \exists x\varphi(x)". But a priori it "not understands" what the part "... \exists x\varphi(x)" as a priori $\varphi(x)$ is phrased in language of object theory and not of background theory. Now - so far I understand the "magic" of

@spaceisdarkgreen Essentially, what I was asking for - pinning down the formalist's picture - was about the role & 'raison d'être' of this "mysterious" procedure "encoding formulas as sets". So far I understand your last explanations correctly, here this is applied only to formulas of object theory and the reason to do it, is precisely that this "encoding formulas as sets" serves here as "gadget" to pick formulas of object theory and translate these into terms in background theory, right?

@spaceisdarkgreen As, if we as formalists assume that the background theory 2) is already a formal theory, what is the sense to "formalize" the formulae contained there?

@spaceisdarkgreen Presumably I not understand what is going on in that part, but it appears strange to me how we proceed there: We take a formula in already formal background theory and encode it as a set. What is the meaning behind this procedure?

@spaceisdarkgreen Isn't this step redundant from viewpoint of formalist as we already assume to have our background theory to be already giva formal theory? So why do we need this "encoding in sets" construction? This part I not understand.

@spaceisdarkgreen ...So far we are in object theory. Now, background theory is formalized theory - as we are formalists -about object theory. So in backgrd theory we are dealing with formulae like eg $T \vdash \exists ! x\varphi(x)$ and $M\models \exists ! x\varphi(x)$ (M model of T), right? (as about(!) T). Now my question is why is it neccessary as you suggested to encode the formulae from this background theory in sets as you claimed above?

@spaceisdarkgreen Think previous issues have been more or less been resolved. But what I still not understand is the reason to encode as intermediate step the formulae as sets. Lets stick on formalist's picture only. So we have 3 levels: 1) metatheory 2) background theory T' 3) object theory T. The formula $\varphi(x)$ is a priori written in language of object theory T, and by assumption $\exists^! x\, \varphi(x)$ is provable in T.

@spaceisdarkgreen Update #3: Or, think I see. You mean "coding concepts into definitions involving sets" precisely in sense described in the link caicedoteaching.wordpress.com/…, right?

@spaceisdarkgreen ...if that's correct so far, think my confusion reduces to pin down what it should mean to say "to coding concepts ( or sentences of a theory) into definitions involving sets." What does it mean?

Update #2: Maybe I see what "formalize model theory" (...what I mentioned in prev comment) should be: Is it equivalent to existence of a formal background theory (...so "stage 2 structure" in formalist's hierarchy you adressed above) which is "able to express" statements about models of the object theory, eg like $M \models \phi$ as wf formula. Is this what it means "formalize model theory"?

@spaceisdarkgreen Could you maybe recomend sources discussing this? Is it standard?