Can "syntactic forcing" add ordinals? Kunen, in paragraph VII.9 of his book talks about forcing "via syntactical models", where the we do not use set models of ZFC. Still, the functional $x \mapsto \check x$ can be defined as usual and is, in a sense, an embedding of the ground model $\mathbf V$ in any forcing model $\mathbf V ^\mathbb P$ (obtained, say by completeness theorem). Then, there is also a sense in asking if the $\mathbf V ^\mathbb P$ has more ordinals than $\mathbf V$, i.e. if $\mathbf V ^\mathbb P$ contains an ordinal larger than all $\check \alpha$ for $\alpha$ an ordinal in $\mathbf V$.
I cannot find any formulation of this question in $\mathbf V$ or $\mathbf V ^\mathbb P$. I wonder if any exists.
Also, I suspect that as in usual forcing, $\mathbf V ^\mathbb P$ has the same ordinals as $\mathbf V$, but cannot prove it. I wonder how this, or its negation, can be proved.
Thank you
 A: The answer is that there is one sense in which no new ordinals are added, but there is a second sense in which new ordinals are added. 
On the one hand, the sense in which no additional ordinals are added is that for any name $\dot\alpha$, we have an equality in the Boolean values:
$$[\![\dot\alpha\text{ is an ordinal}]\!]=\bigvee_{\beta\in\text{Ord}}[\![\dot\alpha=\check\beta]\!],$$
which says exactly that $\dot\alpha$ is naming an ordinal exactly to the extent that it is equal to one of the ground model ordinals. So every name for an ordinal is a mixture of ground model check-names for ordinals, and any generic filter will select exactly one of those names from the antichain of possibilities. One can prove the equation by induction on the rank of the name $\dot\alpha$, since the value that $\dot\alpha$ is an ordinal is equal to the value that it is a transitive set of ordinals, and this claim reduces to versions of the equation for smaller rank names.
For any forcing notion $\mathbb{P}$, let $\mathbb{B}$ be the Boolean completion of $\mathbb{P}$ and we may form the structure $V^{\mathbb{B}}$ as a Boolean $\mathbb{B}$-valued structure, defining the Boolean values $[\![\varphi]\!]$ by (meta-theoretic) induction on $\varphi$. You can find full details in my paper Well-founded Boolean ultrapowers as large cardinal embeddings, or in the lecture notes from my tutorial on the Boolean ultrapower at the Hausdorff Center in Bonn, 2011, which are available at that link. 
If one continues with your idea of the map $x\mapsto\check x$, you arrive fairly quickly at the Boolean ultrapower. Namely, in a contruction due originally to Vopenka and then studied by Solovay and Scott, let $U\subset\mathbb{B}$ be any ultrafilter (not necessarily generic), and then define the equivalence on names $\sigma=_U\tau\iff[\![\sigma=\tau]\!]\in U$. The quotient structure $V^{\mathbb{B}}/U$ is an actual model of set theory, satisfying $\varphi$ if and only if $[\![\varphi]\!]\in U$, which is a form of the Los theorem. The point is that one may define the ground model $\check V$ of $V^{\mathbb{B}}$, and get a corresponding model $\check V/U$ in the quotient. The Boolean ultrapower map is precisely the map $$x\mapsto [\check x]_U,$$ which is an elementary embedding of $V$ into $\check V/U$. 
On the other hand, there is a second sense in which one can think that ordinals are added. Namely, as we explain in the article, the filter $U$ is $V$-generic if and only if the corresponding Boolean ultrapower is an isomorphism. So if you take the Boolean ultrapower by a generic filter, you don't get new ordinals in the Boolean ultrapower, but otherwise you do, since the filter will not always decide the antichains that gave rise to those names for ordinals. Basically, if $U$ misses a maximal antichain, then you can mix distinct ordinals on that antichain to get a name for an ordinal that will not be equivalent to any check name in the Boolean ultrapower. 
The previous paragraph describes the sense in which "non-generic" is the right generalization of "non-principal" for ultrafilters on a Boolean algebra. Although it might seem that generic filters are very complicated and principal filters are trivial, nevertheless it is the principal filters that are generic on the atomic Boolean algebras that arise from power sets, and it is because of the genericity that the ultrapower by a principal filter is trivial. 
