2
$\begingroup$

Jech page 162 states :

Let Form denote the set of all formulas of the language {$\in$}. As with any actual (metamathematical) natural number we can associate the corresponding element of N (i.e. the smallest inductive set), we can similarly associate with any given formula of set theory the corresponding element of the set Form. To make the distinction, if $\varphi$ is a formula, let $\ulcorner \varphi \urcorner $ denote the corresponding element of Form.

If M is a set and E is a binary relation on M and if $a_1,..,a_n$ are elements of M, then

(12.16)$\hspace{2cm} \varphi^M{^,}^E(a_1,...,a_n)\leftrightarrow(M,E)\models\ulcorner \varphi \urcorner[a_1,...,a_n]$

as can be easily verified. Thus in the case when M is a set and $\varphi$ a particular (metamathematical) formula, we shall not make a distinction between the two meanings of the symbol $\models$. We note however that the left-hand side of (12.16) (relativization) is not defined for $\varphi$ $\in$ Form, and the right-hand side (satisfaction) is not defined if M is a proper class.

Would it be possible to ask two questions :

1) As Jech works in ZFC metatheory, is Form a set in the metatheory defined by a metamathematical ZFC formula with its variables ranging over the formulae $\varphi$ coded as metamathematical ZFC sets $\ulcorner \varphi \urcorner$.

and

2) Why in (12.16) does $\ulcorner \varphi \urcorner$ appear on the right hand side, and not just $\varphi$, with (12.16) being a metamathematical ZFC formula, or is (12.16) actually a metamathematical ZFC formula thats using coded formula within the coded logic & model theory? (apologies this isnt too clear - hence the question - I tried to use https://mathoverflow.net/questions/23060/set-theory-and-model-theory/23077#23077). If anyone knows of a book that describes in detail how metamathematical ZFC can be used to code logic & model theory that would be good to know.

$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

I'll answer your second question first: I don't really know of a book that discusses exactly what is going on in this case in depth. But the ideas of coding used here are the same as those in Godel's incompleteness theorem. Recall that $ZFC$ is formally a countable language. So that kind of coding makes sense. This can be done with PRA for example, which is much weaker than set theory.

As to the first question; I believe what is going on is the following (hopefully someone will point it out if I'm wrong); We work within a meta theory, such as PRA (Primitive Recursive Arithmetic). The exact meta theory used is of interest to certain people, but is not really necessary for the purposes of this question.

Now we have way of talking about what it means for $ZFC$ to prove something. We develop model theory inside of ZFC the usual way. Now Jech is saying: $ZFC\vdash({\varphi}^{(M,E)}\leftrightarrow{(M,E)\models{\ulcorner\varphi\urcorner}})$. Here inside of $ZFC$ we have developed the formal theory of (a copy of) ZFC. So we assume that $\ulcorner\varphi\urcorner$ is associated in some canonical way to $\varphi$ (The formula $\varphi$ is actually represented by a code (a unique natural number) in the meta theory. Now $ZFC$ also has access to a version of the natural numbers, then we are implicitly assuming that the code in the meta theory is the "same as the" code in the formal copy of $ZFC$ in $ZFC$).

$\endgroup$
4
  • $\begingroup$ Thanks, I'm still thinking about your response, which looks very like $ZFC \vdash (\varphi(a_1,...,a_n)\leftrightarrow Truth(\ulcorner \varphi \urcorner))$, the Tarski truth definition. I have always wondered how to determine the truth of the LHS of the equivalence. $\endgroup$
    – user239186
    Jul 1, 2016 at 19:14
  • 1
    $\begingroup$ @ColinHarling For every single formula $\phi$ we can internally decide whether $(M,E) \models \phi$ - we just can't do it for all formulas at once. This is where the 'meta theory' comes into play: In our meta theory, we can formulate this theorem for every formula $\phi$. $\endgroup$
    – Stefan Mesken
    Jul 2, 2016 at 11:53
  • $\begingroup$ So just to check : the ZFC in the expression $ZFC \vdash \varphi\leftrightarrow(M,E)\models\ulcorner \varphi \urcorner$ is the formal ZFC and the expression is actually a formula $\psi$($\varphi$,$\ulcorner \varphi \urcorner$) in the formal ZFC - which is in turn $\ulcorner \psi \urcorner$ in the ZFC metatheory ? $\endgroup$
    – user239186
    Jul 4, 2016 at 11:23
  • $\begingroup$ @Stefan - neat point. Presumably the metatheory ZFC constructs the formal theory ZFC in its entirety as something that is only part of the metatheory ZFC - so all classes in the formal theory are sets in the metatheory. $\endgroup$
    – user239186
    Jul 4, 2016 at 15:06

You must log in to answer this question.