New answers tagged


The first part of the disjunction is for stating that the next "state/m-configuration" of the machine is the one established in $Inst(q_i, S_j, S_k, L, q_l)$ (in case z takes as value the next cell of y', i.e., y), the second part of the disjunct is used to say that the part of the tape not scanned by the machine preserves its value.


You always remove quantifiers in the order in which they appear in the prefix, from left to right, that is, you first eliminate $\exists y$ and then $\forall x$. But the variables to apply the skolem function to are just the variables occurring free in the expression, no bound ones. Since $x$ is bound by $\forall x$, and $y$ is being skolemized away, the ...


No, it does not satisfy compactness anymore. Least fixed point operators can let us define, for example, the standard part of a model of $\mathsf{PA}$. The standard part of a model $\mathfrak{A}=(A;+^\mathfrak{A},\times^\mathfrak{A},0^\mathfrak{A},1^\mathfrak{A})$ of $\mathsf{PA}$ is just the smallest subset of $A$ containing $0^\mathfrak{A}$ and closed ...

Top 50 recent answers are included