Subformula determining using two definitions

Question

In Angelo Margaris's First Order Mathematical Logic a subformula is defined as follows,

A subformula of the forumla $P$ is a consecutive part of $P$ that is itself a formula.

Whereas in S. M. Srivatava's Course on Mathematical Logic it is defined as follows,

A subformula of a formula $A$ is inductively defined as follows: $A$ is a subformula of itself; if $¬B$ or $∃vB$ is a subformula of $A$, then so is $B$; if $B∨C$ is a subformula of $A$, then $B$ and $C$ are subformulas of $A$; nothing else is a subformula of $A$. Thus, the set of subformulas of $A$ is the smallest set $\mathcal{S}(A)$ of formulas of $L$ that contains $A$ and satisfies the following conditions: whenever $¬B$ or $∃vB$ is in $\mathcal{S}(A)$, so is $B$, and whenever $B ∨C$ is in $\mathcal{S}(A)$, so are $B$ and $C$.

Now, let me denote that definition of Margaris's as $\sf{AM}$ and that of Srivastava's as $\sf{SS}$.

Now, I am to determine the subformula's of the following formulas using these definitions.

1. $∀x∃y(x · y = e)$.
2. $∀x∀y∃z(x ∈ z ∧ y ∈ z)$.
3. $¬∃x∀y(y ∈ x)$.

My Solutions (Using $\sf{AM}$)

1. $∀x∃y(x · y = e)$ (if we assume that part in $\sf{AM}$ doesn't exclude whole), $∃y(x · y = e), (x.y=e)$.

2. $∀x∀y∃z(x ∈ z ∧ y ∈ z), ∀y∃z(x ∈ z ∧ y ∈ z), ∃z(x ∈ z ∧ y ∈ z), (x ∈ z ∧ y ∈ z), x\in z, y\in z$.

3. $¬∃x∀y(y ∈ x), ∃x∀y(y ∈ x), ∀y(y ∈ x), (y\in x)$.

Questions

• Are my solutions using $\sf{AM}$ correct?

• Suppose we take (1.) and try to show that $∃y(x · y = e)$ is a subformula of $\forall x ∃y(x · y = e)$. Now accrodig to $\sf{SS}$ for this we need to check whether $\neg(\exists y(x · y = e))$ or $\exists v(\exists y(x · y = e))$ are both subformulas of $A$. But how do we check that?

• How can we use $\sf{SS}$ to find the subformulas of the given formulas?

Answer 1

Regarding these "formal" aspects, you have to take care of the details of the "syntactical specifications".

According to Margaris [page 30] the primitive symbols are:

$\lnot, \to$ and $\forall$.

Thus, $\exists v P$ is an abbreviation for $\lnot \forall v \lnot P$.

In Srivastava's book [page 6]:

$\lnot, \lor$ and $\exists$ are primitive,

and thus $\forall v A$ is an abbreviation for $\lnot \exists v \lnot A$.

Regarding the Srivastava's Exercise [page 7]:

$∀x∃y(x⋅y=e)$,

you have to consider the note: "The preceding formulas mus be considered in their unabbreviated forms."

According to Margaris, it is an abbreviation for:

$∀x¬∀y¬(x⋅y=e)$;

according to Srivastava, it is an abbreviation for:

$¬∃x¬∃y(x⋅y=e)$.

Of course, the three formuale have the same "meaning" but - as strings of symbols - they are different "syntactical" objects.