3
$\begingroup$

The following formulas are said to be defined in WS1S logic.

$Closed(Z, R) := ∀x ∀y(x ∈ Z ∧ R(x, y) → y ∈ Z)$ $(z_1, z_2) ∈ R^∗ := ∀Z.(z_1 ∈ Z ∧ Closed(Z, R) → z_2 ∈ Z)$

However since WS1S formula requires bounded second order variables to be finite, I am not sure if the second formula is valid. $Z$ which is bounded here, can be an infinite subset of natural numbers. For example, when $R$ is a $succ$ relation.

There are no restrictions on $R$ stated in the reference.

In the paper Implementing WS1S via Finite Automata by James Glenn and William Gasarch : $∀X∃Y ∀z(¬(z ∈ X) ∨ (z + 1 ∈ Y ))$ is stated to be a valid WS1S formula.
$∀x∃y(y < x)$ is stated as an invalid WS1S formula.

However if $X$ is finite in the first formula, $Y$ is infinite and hence I think this should not be a valid formula. In the second formula there are no second order variables and therefore it should be a valid formula. Please let me know what am I missing here.

$\endgroup$
  • $\begingroup$ I'm unfamiliar with WS1S, but $Y$ looks finite to me, if $X$ is finite. Take $Y = \{z+1 | z\in X\}$ which has the same cardinality as $X$. $\endgroup$ – chi Dec 28 '17 at 10:47
1
$\begingroup$

The confusion comes mainly from different meanings of validity.

In the context of syntax, we are used to understand 'valid' as syntactically correct. As in '42["Hello world"] is a valid C expression'. I believe this is also how you understood Glenn&Gasarch. Their statement does make sense with semantic instead of syntactic validity.

Let me shortly recap semantics of WS1S. Generally, in second-order logic (weak or non-weak), the semantic of a formula is defined relative to an interpretation. The interpretation defines the meaning of all symbols. It consists of a structure and an assignment. The structure defines the universe and the meaning of the symbols from the base vocabulary. The assignment defines the meaning of the free variables. For a formula $\varphi$ and an interpretation $\mathcal I$, the semantics define whether $\mathcal I\models\varphi$ shall hold.

In WS1S, the structure is fixed: The universe is the natural numbers and the only other symbol is interpreted by the successor relation. Hence, for formulae $\varphi$ without free variables (sentences), the semantics can do without mentioning the interpretation. That could be written just $\models\varphi$, or $\models_{\text{WS1S}}\varphi$. And that is what Glenn&Gasarch mean with validity.

Let me stress that the finite-subset restriction of WS1S is not a syntactic one. The syntax of WS1S is the same as that of S1S (which has quantification over arbitrary subsets). Hence syntactic validity (well-formedness) is not jeopardized by concerns of what can or cannot be achieved with a finite subset. Indeed the only difference between WS1S and S1S is of semantic nature. By definition, $\mathcal I\models \exists X\varphi$ holds

  1. (in case of S1S) if there is a subset $S$ of the universe such that $\mathcal I[\frac SX]\models\varphi$, or
  2. (in case of WS1S) if there is a finite subset $S$ of the universe such that $\mathcal I[\frac SX]\models\varphi$.

Now to the other two formulae you asked about. Both are syntactically valid, if you allow binary second-order variables ($R$ in this case) as arguments (which is fine for defining subformulae as building blocks; in the end these variables will have to be substituted by other formulae). As they have free variables, we cannot say anything about semantic validity without having an assignment.

However, the names of the formulae suggest intended semantics. And we can compare the actual semantics to the intended ones.

  1. The first formula holds (in the sense of $\models$) iff the set which is assigned to $Z$ is closed to the right under the relation assigned to $R$. That does seem to match the intention.
  2. The second formula holds iff the element assigned to $z_2$ is reachable from the element assigned to $z_1$ by a path all of whose steps belong to the relation assigned to $R$, or if infinitely many elements are reachable in that way. That does not seem to match the intention.

But again, I would not use the notion of validity to discuss whether a formula fulfills its purpose.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.