search

jkorb / KI1V13001-Inleiding-Logica

This is the source material for the course "Inleiding Logica" (KI1V13001) as taught at Utrecht University for the BSc "Kunstmatige Intelligentie"
Creative Commons Attribution 4.0 International
3 stars 16 forks source link

Clarity on up preservation #108

Open skshvl opened 2 years ago

skshvl commented 2 years ago

I wrote this email to the class email and am copying it here at Prof. Korbmacher's request. This may help clear up some clarity issues in chapter 6 of the notes.

My email:

I had the following question about up preservation, which is defined as "If a formula at a newly generated child node is true under a valuation, then the formula at the parent node is true."

I was thinking of the example p^q. It creates child nodes like this:

p^q p

q

Now let's say p is true and q is false under a valuation.

p is a newly generated child node which is true. By up preservation, that would imply p^q is true.

But we know q is false, so p^q must be false.

Doesn't this contradict up preservation? Of course it is possible that we are on a closed branch, but wouldn't up preservation (as an if-then) hold in any branch of the tableau?

So I assume I am misreading exactly how up preservation works.

Response:

The wording wasn't very good here. What was meant was this: if a rule generates a bunch of nodes possibly on different branches, then if you take all the new nodes on one of those branches together, if they are all true, the upper formula is true. So in this case, p and q have to both be true. Thanks for your email, it's great that you're thinking it through like this: it's exactly what you should be doing! May I ask you one favor? It'd be great if you could file this as an issue on Github, you can just use your email as the issue content. This allows me to keep track of the improvements that need to be done 🙂

jkorb commented 2 years ago

Thanks for this @skshvl ! It's on the radar now :)