WS19/20 - Problem 5.2 (First-Order Tableau)

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

WS19/20 - Problem 5.2 (First-Order Tableau)
I have a question to this type of problem. First of all the brackets in the problem statement and in the solution are different.

In the solution there is the substitution s for Z [s/Z] in the left branch.
Is it ok just to say we use this substitution to close the branch or do we additionally have to replace all occurences of Z with s in all lines above?

If the latter applies, i gets very annoying to keep free spaces for all variables in the progress or confusing when making the corrections afterwards, because we only know in the end which substitution we can use.

Hope this was comprehensive enough to understand what i mean.

In the lecture slides (417, and 431) it is done by ⊥ : (without replacing all Variables)

yes, but in one exercise session it was mentioned that you have to replace them, so i asked.


if I am not wrong, the argumentation is related that way.

The tableau represents an algorithm and in that tenor, everything goes gradually forward.
One step is the substitution and after that, the variable is replaced.
The other way round, every step before this step are just before the substitution.

Shortly, you don’t have to substitute every variable before this.


1 Like

Substitute everywhere
You have to replace it.
The intuition behind it is the following:

When you branch, you want to show (or fail to show) that both branches lead to a contradiction.
But if you choose two different values for the same variable then that’s cheating, you can close branches you shouldn’t be able to close.

Example (from tutor Frederik Schäfer): (∀X.∃F.p(X,F)) ⇒ ∃Y.p(s,Y) ∧ p(t,Y)

p(X, F): F is the mother of X

So the formula means, that if all people have a mother, then it follows that there is a mother who is the mother of s and t.
Obviously this is not valid, but according to Frederik you could prove this formula using FO Tableau if you don’t substitute everywhere.

Best regards, Tobi (tutor)

So we realy have to go through the whole proof and replace it after the substitution? That looks awful. It should be enough if you forbid different substitutions for the same variable in different branches.

1 Like

EDIT: See Frederik’s post

On slide 415:
⊥instantiates the whole tableau by σ.

My guess is: The important thing is that you don’t substitute for a variable in two different ways - even if it’s on different branches.
Instantiating the entire tableau would be prevent that from happening (and is what slide 415 requires).

How to do that nicely on paper is of course a different question.

Thanks for the fast response! :slight_smile:

However you don’t need to cross out and rewrite every single variable name before that, no need to make a mess.
Just write a comment and be careful.
In that sense the official solution is fine.

Don’t worry about minor details like that though. It’s really just a detail. Just make sure we know you are aware of it.

Best regards, Tobi

1 Like