1

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?

  • 1
    Those 2 definitions are terrible. A decent definition would be, translate the formula into an abstract syntax tree, a subformula is all subtrees (without creating new leaves) whose root is a boolean (a quantifier, logical operator, or predicate). AM isn't even correct (since it implies that $b=c$ is a subformula of $a+b=c$ and SS is unnecessarily complicated, using "smallest set" instead of a normal inductive definition. – DanielV Aug 25 '16 at 05:23
  • @DanielV: I don't think that $\sf{AM}$ implies that $b=c$ is a subformula of $a+b=c$. With suitable parenthesis probably we can show that $b=c$ is not a subforumla in the sense of $\sf{AM}$. –  Aug 25 '16 at 05:32
  • For 3, we have also : $∃x∀y(y∈x)$. – Mauro ALLEGRANZA Aug 25 '16 at 05:42
  • SS is an inductive def; so you have to start from the base cases, i.e. $\lnot B, B \lor C$ and $\exists x B$ (the possible $A$s). – Mauro ALLEGRANZA Aug 25 '16 at 05:45
  • @MauroALLEGRANZA: Yes. I missed that. Thanks. –  Aug 25 '16 at 10:05
  • @DanielV: Furthermore, $+$ here is a binary function symbol and it can only operate on terms. In your example. $b=c$ is not a term, it is a formula. –  Aug 25 '16 at 10:09
  • @MauroALLEGRANZA: What do you mean by starting from "the base cases, i.e. $¬B,B∨C$ and $∃xB$ (the possible $A$ s)"? –  Aug 25 '16 at 10:17
  • See page 6 : Syntax of FOL for the def of formula : the only three rules for generating a "complex" formula from simpler ones are : $\lnot A, \exists v A, \lor AB$. – Mauro ALLEGRANZA Aug 25 '16 at 10:23
  • This means that, applying the syntactical specifications, a formula must start with $\lnot$ or $\exists v$ or $\lor$. In the case of $∃y(x⋅y=e)$, we have the second possibility : $x⋅y=e$. This is an atomic formula [see def page 6] and thus it is not decomposable into subformuale. – Mauro ALLEGRANZA Aug 25 '16 at 11:22
  • When you have that $\exists y(x\cdot y=e)$ is a subformula you can argue that $(x.y=e)$ is a subformula. But how do we show that $\exists y(x\cdot y=e)$ is a subformula according to $\sf{SS}$, @MauroALLEGRANZA? –  Aug 25 '16 at 13:40
  • @MauroALLEGRANZA: Is it due to the following reason that, since $∀x∃y(x⋅y=e)$ and $\neg\exists x\neg(∃y(x⋅y=e))$ are syntactically equivalent so $\exists x\neg(∃y(x⋅y=e))$ is a subformula and this implies $\neg(∃y(x⋅y=e))$ is a subformula which finally implies $∃y(x⋅y=e)$ is a subformula? –  Aug 25 '16 at 13:48
  • @MauroALLEGRANZA: Yes. Exactly. Sorry, I forgot to write that. –  Aug 25 '16 at 13:51
  • @MauroALLEGRANZA: But observe that although we have arrived at the same conclusion that $∃y(x⋅y=e)$ is a subformula of $∀x∃y(x⋅y=e)$ (henceforth $\mathcal{F}$), in the process of reasoning we also deduced that $\neg(∃y(x⋅y=e))$ is also a subformula of $\mathcal{F}$ according to $\sf{SS}$ but according to $\sf{AM}$ it is not a subformula of $\mathcal{F}$. Why this difference? –  Aug 25 '16 at 13:56
  • To be more precise, according to $\sf{SS}$ all the following formulas are subformulas of $\mathcal{F}$: $∀x∃y(x⋅y=e), ∃x¬(∃y(x⋅y=e)), ¬(∃y(x⋅y=e)), ∃y(x⋅y=e)$ and $(x⋅y=e)$. Whereas according to $\sf{AM}$ (if I am correct) only the following formulas are subformulas of $\mathcal{F}$: $∀x∃y(x⋅y=e), ∃y(x⋅y=e)$ and $(x⋅y=e)$. –  Aug 25 '16 at 14:01

1 Answers1

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.

Mauro ALLEGRANZA
  • 94,169
  • @user170039 - This is not correct ! A subformula is a formula, because the gist of the matter is that a subformula is a string of symbols that is a substring of the original formula and that is itself a formula, i.e. it is compliant with the syntacticcal specs. Thus, e.g $x=0$ is a sub of $\forall x (x=0)$, while $\forall x$ is not. – Mauro ALLEGRANZA Aug 25 '16 at 14:23
  • Although the "gist of the matter is that a subformula is a string of symbols that is a substring of the original formula and that is itself a formula", how can one deduce this from $\sf{SS}$? Observe that using $\sf{SS}$ it is possible to conclude that $\neg \mathcal{F}$ is a subformula of $\mathcal{F}$ because $\neg(\neg\mathcal{F})$ is syntactically equivalent to $\mathcal{F}$. –  Aug 25 '16 at 14:27
  • This means that not every substring of the original formula is a subformula, but of course every subformula must be a substring of the original one. – Mauro ALLEGRANZA Aug 25 '16 at 14:29
  • @user170039 - NO : $\lnot ( \lnot A)$ is semantically equivalent to $A$ but not syntactically. Sintax is about the specifications for generatig string of symbols that are "meaningful", but they are defined without any reference to meaning. – Mauro ALLEGRANZA Aug 25 '16 at 14:31
  • Even in that case also the set of subformulas obtained using two different definitions are different as I have said earlier. That's the problem. By the way, I think that from both definitions we can conclude that "not every substring of the original formula is a subformula, but of course every subformula must be a substring of the original one", can't we? –  Aug 25 '16 at 14:34
  • @user170039 - in no system we may have that $¬F$ is a subformula of $F$, simply because $¬F$ is "longer" than $F$ and thus it cannot be "part (proper or improper) of" it. The substring concept is the equivalent of "consecutive part". – Mauro ALLEGRANZA Aug 25 '16 at 14:39
  • Let us continue this discussion in chat. –  Aug 25 '16 at 14:45
  • How to show the defs are equvivalent? I suppose induction has to be used but i am stuck on proving that if $(\alpha \land \beta)$ is a wff then $p\land q$ cant be a string which is a wff [where p is a terminating segment of $\alpha$ and $q$ is a initial sgement of $\beta$] – Vivaan Daga Dec 29 '21 at 03:48
  • Does this work? since $p$ is a termianting segment it has more ) brackets than ( but that is absurd since an initial segemnt of a wff has the opposite !! – Vivaan Daga Dec 29 '21 at 05:55