Conjunctivitis

"Jill loves all Y and all that Y eats fish"

All Y loves(jill, Y) /\ eats(Y, fish)


Axiom B of modal Logic S5:   P  ->  <>P

Changes this to:  "Jill loves all Y and all that Y eats fish is only true as far as legitimately non-contradictory bindings of Y exist"
 (*and* They might not even exist)

So you want to hold "All things in the universe" still?

We cannot without a complete knowledge of the unknown decide the impossible bindings of Y (or even the possibilities)
But at least we can accept bindings of Y that are not contradicted for  "loves(jill, Y)"  OR  "eats(Y, fish)"

To keep this from being to complex let's pretend our universe has only zero objects besides jill and fish?
Too arbitrary? ok let's pretend 4
So shall we go ahead and replace all our universal quantifiers with
  exists Y member(Y,The4Ys) ..

Anyhow, let's not game the universal quantifiers.

Let's start over and go about it with a more realistic approach be realistic and properly represent jill and fish:


In what way is this expression:

"All Y loves(jill, Y) /\ eats(Y, fish)"

different than:

Exists J,F, All Y  (named(jill,J) /\ someType(F,fish) ->  loves(J, Y) /\ eats(Y, F))" ?

I believe they are the same awkward sentence.


At solemnizes to ...

(named(jill,skJill()) /\ someType(skFish(Y),fish) /\ equals(J,skJill()) /\ equals(F,skFish(J)) ->
   loves(skJill(), Y) /\ eats(Y, skFish(J))

See the skolem imbalance?

Lets instead use "Fair skolems"  (This means they represent the entire formula"
(Also means each skolem gets universally represented in this light)

(named(jill,skJill(J,F,Y)) /\ someType(skFish(J,F,Y),fish) /\ equals(J,skJill(J,F,Y)) /\ equals(F,skFish(J,F,Y)) ->
   loves(skJill(J,F,Y), Y) /\ eats(Y, skFish(J,F,Y))

So that is what we said?

Which becomes:

named(jill,skJill(J,F,Y)) /\ someType(skFish(J,F,Y),fish) /\ equals(J,skJill(J,F,Y)) /\ equals(F,skFish(J,F,Y))
   -> loves(skJill(J,F,Y), Y).

named(jill,skJill(J,F,Y)) /\ someType(skFish(J,F,Y),fish) /\ equals(J,skJill(J,F,Y)) /\ equals(F,skFish(J,F,Y))
   ->  eats(Y, skFish(J,F,Y)).



I believe this conjunctive elimination looks like in order to not "dangle" (preserves the accessibility of the two relations now .. representing the initial assertion. A/\B