S5 problem

  1. Philosophy Forum
  2. » Logic
  3. » S5 problem

Get Email Updates Email this Topic Print this Page

Reply Tue 19 May, 2009 05:45 pm
I'm having trouble proving this in S5.

◊(∃x) Fx -> (∃x) ◊Fx
| ◊(∃x) Fx (assume)
| | ~ ◊(∃x) Fx (assume)
| | | ◊ ~ (∃x) ◊Fx (possibility)
| | | □ | ◊ ~ (∃x) ◊Fx (S5 necessity intro)
| | | □◊ ~ (∃x) ◊Fx (necessity)
| | | ~◊~◊~ (∃x) ◊Fx (def of □)
| | | ~◊□ (∃x) ◊Fx (def of □)
| | | □ | (∃x) ◊Fx (assume necessity)
| | | □ | | Fx (Existential instantiation)
| | | □ | | ◊Fx (possibility)
| | | □ | | □ | ◊Fx (S5 necessity intro)
| | | □ | | □ | (∃x) ◊Fx (Existential generalization)
| | | □ | | □(∃x) ◊Fx (necessity)
| | | □(∃x) ◊Fx (necessity)
| | | ◊□(∃x) ◊Fx (possibility)

???
Therefore
◊(∃x) Fx -> (∃x) ◊Fx

I'm not sure how to eliminiate ◊□ from the last step in order to get (∃x) ◊Fx
 
 

 
  1. Philosophy Forum
  2. » Logic
  3. » S5 problem
Copyright © 2020 MadLab, LLC :: Terms of Service :: Privacy Policy :: Page generated in 0.02 seconds on 08/12/2020 at 06:24:20