Kenneth Rosen Edition 6th Exercise 1.3 Question 40c (Page No. 49)

Question

Express each of these system specifications using predicates,
quantifiers, and logical connectives.

c) The file system cannot be backed up if there is a user
currently logged on.

I got this expression : ∃x(U(x)) -> not F(x)

The answer is given in the manual is:- 
Which one is correct? If the manual is correct then why two variables x,y are required?

Comments

Both are correct, if your answer is ∃x(U(x)) -> not F )

where x is member, U(x) is logged in the system, F is Backup of System

it's depend upon your prepositions....

 

why he use two variables?

he want to change the domain of File system too

---

Thanks :)

---

Only yours is partially correct. The answer from the manual that you are referring, is Wrong for the given specification.

Answer 1

Only your Answer is somewhat Correct for the given specification. Though, the fully correct answer would be :

$\exists x U(x,y) \rightarrow  \,\, \sim F(y) $

Where $U(x,y)$ : User $x$ is currently logged on file system $y$.

and $F(y)$ : File system $y$ can be backed up.

 

The answer is given in the manual is:- 

From which manual you got that answer ?? Because it is wrong for the given specification. 

Comments

∃x ∀y U(x,y) → ∼F(y) then what this is represent

---

∃x ∀y U(x,y) → ∼F(y) then what this is represent

Incomplete information.  Can't give it any meaning.

---

Take Two Users a,b and Three systems 1,2,3

Now, Let U(a,1)=F, U(a,2)=F , U(a,3)=F

and let U(b,3)=T and Let F(3)=T

Now, For the above scenario, Your expression becomes True (Because of user a). But the Given specification becomes False (Because of User b).

 Now, you can apply the above scenario on my expression in the answer, It will become False(because of user b).

Here you mean that:-
[ [U(a,1) -> ~F(1)] ∧ [U(a,2) -> ~F(2)] ∧ [U(a,3) -> ~F(3)] ] v [ U(b,3) -> ~F(3) ]
(T ∧  T∧ T) v F becomes True.  Which should be False.

So,
If it was [U(a,1) -> ~F(1)]  ∧ [U(a,2) -> ~F(2)] ∧  [ [U(a,3) v U(b,3) ] -> ~F(3) ]

Then it will return false. And satisfy:-
(Or with all the user of the specific file) And (with all the user of other specific files) .............................

by ∀y ∃x (U(x,y) → ∼F(y) ) (maybe)