I do not quite understand yet how the proof of a formula works in first order logic. I am currently having the following problem that I assume it is due to lack of comprehension.

The problem is as follows, if I want to proof that a predicate is symmetric. Let us suppose we are talking about s(x,y) defined as "x has a sibling y". I may define this in terms of p(x,y) "x is the parent of y" (let's assume for simplicity that the parent is unique) by the formulae:

$$\forall x \forall y \forall z\, (\neg x = y \wedge p(z,x) \wedge p(z,y) \rightarrow s(x,y)),$$ $$\forall x \forall y\, (s(x,y)\rightarrow \neg x = y \wedge \exists z (p(z,x) \wedge p(z,y))).$$

Here's the thing. If I aim to proof s(x,y) is symmetric, this is,

$$\forall x\forall y\, (s(x,y)\leftrightarrow s(y,x)),$$ and I use the tableau to do so, I should consider $$\neg(\forall x\forall y\, (s(x,y)\leftrightarrow s(y,x))).$$ Then, I introduce the new constant $c$ and obtain

$$s(c,c)\leftrightarrow s(c,c),$$

(additional question, there are two $\forall$ and in both cases I am replacing its values for the new constant $c$. Is this correct whenever I consider the $\forall$ constant introduction? Even when I know the predicate should be false when considering s(x,x))

which gives rise to a closed branch. But this would mean all predicates of two "variables" are symmetric and, for instance, $p(x,y)$ is not.

I'm afraid my main problem is to understand what I am doing. So, I would like to understand the what is going on here. May I assume I know s(x,y) is symmetric because we know the relation having a sibling is? Does it change (conceptually) if I define this predicate using the p(x,y) predicate? I would love to read some lines on this topic to clarify these questions/misconceptions.

Thank you in advance.


Ordinarily, the rule for introducing new constants deals with just a single quantifier, so to replace both $x$ and $y$ you'd need to apply the rule twice. Furthermore, the rule says that the constant you introduce has to be new, i.e., not already involved in your proof. So when you replace the second variable by a constant, it can't be the same constant that you used for the first variable. So your error occurs at the point where $s(c,c)$ appeared.

  • $\begingroup$ Depending on the proof system, either you'll have to convert your negated $\forall$'s to (not negated) $\exists$'s before substituting constants, or there will be a separate rule for negated $\forall$'s. In any case, the proof system won't allow you to use the same $c$ for both variables. $\endgroup$ Apr 30 '20 at 1:46
  • $\begingroup$ Thank you for the answer. I agree that you must add a new variable anytime you use the existence quantifier, however, for the universal quantifier I think you can use as many times as you want the constants that have already appeared. If you could give me a clear reference for the rules that you are refearring to, it would be very helpful. Also, with respect to the s(c,c) question, I was thinking that what I proved there is that the symmetry property is satisfiable, in particular it is true for any interpretation whose domain is a singleton, right? $\endgroup$ Apr 30 '20 at 11:47
  • $\begingroup$ To show that your axioms entail the symmetry property you negate the conclusion and show that all branches close. When you negate your conclusion the quantifiers become existential, so you have to introduce a new variable for each instantiation. For example, Sab <> Sba. If you want to show that your 3 premises are satiafiable then you leave the premises in their original form and show that at least one branch remains open. $\endgroup$
    – Casey
    Apr 30 '20 at 21:31
  • $\begingroup$ Also I don't think those axioms entail your conclusion. I can't get the tree to close nor can I find a proof. $\endgroup$
    – Casey
    Apr 30 '20 at 22:49
  • $\begingroup$ If you use the three equation I gave above: 1. ∀x∀y∀z(¬x=y∧p(z,x)∧p(z,y)→s(x,y)), 2. ∀x∀y(s(x,y)→¬x=y∧∃z(p(z,x)∧p(z,y))), and 3. ¬(∀x∀y(s(x,y)↔s(y,x))), plus the equation 4. $\forall x \neg p(x,x)$, you should be able to close all branches of the tree. So what I think is that if you define the s(x,y) predicate from p(x,y) or you have to define s(x,y) assuming the necessary axioms for that matter. I am not sure if what I'm saying makes sense, but I think it is true you can prove the symmetry in the first way. $\endgroup$ Apr 30 '20 at 23:19

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.