I was wondering if we can derive ◻((∃x)Fx ⊃ ◻(∃x)Fx) from ◻(∀x)(Fx ⊃ ◻(E!x & (E!x ⊃ Fx)))? (By the way 'E!' is the existence predicate.)

I am using the Quantified Free Modal Logic constructed/mentioned by Sobel, p.110f from his book Logic and Theism.

  • Isn’t that an obsolete symbol for implication, I’ve only seen it very old and out of date books. Existence, by the way, is not a predicate, even if it formally looks like one. Commented Jan 25, 2019 at 7:50
  • Before trying to answer, I would like to know what does the '!' denote here?
    – SmootQ
    Commented Jan 25, 2019 at 9:23
  • 1
    @SmootQ It's said it denotes existence predicate, but what's that? I know uniqueness quantifier, but quantifiers are not predicates themselves.
    – rus9384
    Commented Jan 25, 2019 at 9:25
  • Ah, you mean this ∃!x , this is the first time I see E!x with E. Thank you
    – SmootQ
    Commented Jan 25, 2019 at 9:42
  • 4
    @SmootQ No, he does not mean ∃!x (that wouldn't be syntactically correct), E!x is the existence predicate from free logic. James McGraw, can you specify, which of the thousand semantics you are using? It is impossible to answer otherwise. Also, are we in S5? More input please. Commented Jan 25, 2019 at 10:23

2 Answers 2


@SmootQ Hello Smoot. I was trying to work on this problem on my own and I think I managed to come up with something. I'd appreciate it if you can let me know if I managed to do this correctly. (Thanks in advance.)

So the problem was to go from ☐(x)(Fx ⊃ ☐(E!x & (E!x ⊃ Fx))) to ☐((∃x)Fx ⊃ ☐(∃x)Fx). The thought was to use a variable domain (free) quantified modal logic S5 system. Here's what I have tried doing:

We start with our premise ☐(x)(Fx ⊃ ☐(E!x & (E!x ⊃ Fx))). From this we can straightforwardly deduce that ☐((∃x)Fx ⊃ (∃x)☐(E!x & (E!x ⊃ Fx))). Call this N. I will come back to this later. Now we assume the consequent of this, i.e. (∃x)☐(E!x & (E!x ⊃ Fx)), for conditional proof.

Conditional proof: So we start with (∃x)☐(E!x & (E!x ⊃ Fx)). From this we can straightforwardly deduce that (∃x)☐(E!x & Fx). At this point using the free logic rule for existential generalization (since we have E!x) we can deduce that (∃x)☐(∃x)Fx. Since the first (∃x) now becomes redundant we can move to ☐(∃x)Fx. That completes our conditional proof. From (∃x)☐(E!x & (E!x ⊃ Fx)) we have deduced that ☐(∃x)Fx. Hence we conclude that (∃x)☐(E!x & (E!x ⊃ Fx)) ⊃ ☐(∃x)Fx.

Since we used nothing more than the rules of our logic to establish this conditional above then by necessitation rule we can move to ☐((∃x)☐(E!x & (E!x ⊃ Fx)) ⊃ ☐(∃x)Fx). Call this N'. Now from N (from above) and N' we can by transitivity of strict implication move to our conclusion ☐((∃x)Fx ⊃ ☐(∃x)Fx).

So, then, we have successfully deduced ☐((∃x)Fx ⊃ ☐(∃x)Fx) from our premise ☐(x)(Fx ⊃ ☐(E!x & (E!x ⊃ Fx))).

  • That's a clever one, assuming the consequent and deducing a conditional logical entailment from it, thank you for sharing! - I was struggling with this proof then I stopped trying for a while just to find time for some other stuff.. , the difficulty I found is in the 1st step in your proof : (x)(Px ⊃ Qx) ∴ ((∃x)Px ⊃ (∃x)Qx), this inference rule did not occur to me. Thank you again. +1
    – SmootQ
    Commented Feb 9, 2019 at 8:59
  • Don't forget to check it as a best answer. ;)
    – SmootQ
    Commented Feb 9, 2019 at 9:01
  • 1
    Thank you for looking it over. Just one question I had, it seems S5 (or even S4 or B or T for that matter) wasn’t used in the proof. So then this would be a valid argument even in a variable domain (free) quantified modal logic K system? Commented Feb 9, 2019 at 16:39
  • yes I think so, since you only used basic inference rules in propositional and first order quantificational logic, of course you are allowed to use axioms in modal systems, but you don't have to.
    – SmootQ
    Commented Feb 11, 2019 at 22:49

The answer is No! and here is the refutation :

  1. ◻(∀x)(Fx ⊃ ◻(E!x & (E!x ⊃ Fx))) [the premise]
    1. ∴◻((∃x)Fx ⊃ ◻(∃x)Fx) [the conclusion]
    2. Assume: ~◻((∃x)Fx ⊃ ◻(∃x)Fx) [we assume the opposite of 2]
    3. ∴ ◇~((∃x)Fx ⊃ ◻(∃x)Fx) [from 3, reverse squiggle]
    4. W ∴ ~((∃x)Fx ⊃ ◻(∃x)Fx) [from 4, we introduce a possible world W]
    5. W ∴ (∃x)Fx [from 5, break not-if, antecedent true]
    6. W ∴ ~◻(∃x)Fx [from 5, break not-if, consequent false]
    7. W ∴ ◇~(∃x)Fx [from 7, reverse squiggle]
    8. W ∴ Fa [from 6, drop existential]
    9. W ∴ (∀x)(Fx ⊃ ◻(E!x & (E!x ⊃ Fx))) [from 1, drop box]
    10. W ∴ (Fa ⊃ ◻(E!a & (E!a ⊃ Fa))) [from 10, drop Universal]
    11. W ∴ (E!a & (E!a ⊃ Fa)) [from 11 and 9, Modus ponens and drop box]
    12. W ∴ E!a [from 12, conjunction elimination]
    13. W ∴ (E!a ⊃ Fa) [from 12, conjunction elimination]
    14. W ∴ (∃y)(y=a) [from 13, according to E!x definition in reference below]
    15. W ∴ b=a [from 15, drop existential]
    16. W ∴ Fa [from 14 and 13, modus ponens]
    17. W ∴ Fb [from 17 and 16, identity]

As you can see, although we have assumed the opposite of the conclusion and have all the propositions broken down, we could not obtain a contradiction.

So, it is possible for the premise ◻(∀x)(Fx ⊃ ◻(E!x & (E!x ⊃ Fx))) to be true, while the conclusion ◻((∃x)Fx ⊃ ◻(∃x)Fx) is false, in a possible world where a=b and where it is possible that no x is F (◇~(∃x)Fx)

Since we could not obtain a contradiction, it means that the premise does not entail the conclusion.

Note: I went from step 13 to 15 using the definition :

E!a := (∃x)(x=a)

Reference : https://plato.stanford.edu/entries/logic-free/#1.1

  • 1
    Thanks for the explanation. Just a question-- so after digging around a bit I found something where someone shows that ◻(∀x)(Fx ⊃ ◻(E!x & Fx)) entails ◻((∃x)Fx ⊃ ◻(∃x)Fx). In our case we're using ◻(∀x)(Fx ⊃ ◻(E!x & (E!x ⊃ Fx))), which entails ◻(∀x)(Fx ⊃ ◻(E!x & Fx)), so shouldn't ◻(∀x)(Fx ⊃ ◻(E!x & (E!x ⊃ Fx))) entail ◻((∃x)Fx ⊃ ◻(∃x)Fx) then? The link below includes a picture of the proof where said person shows ◻(∀x)(Fx ⊃ ◻(E!x & Fx)) to entail ◻((∃x)Fx ⊃ ◻(∃x)Fx) (they use 'P' instead of 'F'). imgur.com/a/q1PhGwo Commented Jan 25, 2019 at 19:20
  • 1
    Oh right, just checking the book you're looking at. It is from this book. On page 87 there is a similar principle that says ◻(∀x)◻(Px ⊃ ◻(E!x & Px)), which he also says entails AP (where AP is ◻((∃x)Px ⊃ ◻(∃x)Px)). Then on page 88 he considers the principle we're talking about ◻(∀x)(Px ⊃ ◻(E!x & Px)) and says that it entails AP as well. Page 113 is where the picture is from. Commented Jan 25, 2019 at 20:14
  • 1
    I don't really know, I will have to read some chapters from that book in order to follow, Using Modal Logic inference rule I would say that the premise does not entail the conclusion, but now I am curious to know exactly what is it all about.
    – SmootQ
    Commented Jan 25, 2019 at 20:18
  • 1
    Just to help you out a little bit so you don't waste time reading irrelevant philosophy of religion stuff: From pages 105 to 107 he explains a logical system that he calls "Sentential modal logic" (SMC for short). Then from pages 110 to 112 he explains a logical system (that is an extension of SMC) that he calls "Free Monadic Quantifier Modal Calculus" (FrMQMdlC for short). And finally on page 113 he shows ◻(∀x)(Px ⊃ ◻(E!x & Px)) to entail ◻((∃x)Px ⊃ ◻(∃x)Px) in FrMQMdlC. Commented Jan 25, 2019 at 20:27
  • 1
    Basically but you don't have to read pages 108 and 109. In those pages he shows some derivations in the SMC system which are irrelevant. Commented Jan 25, 2019 at 20:43

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .