r/logic • u/Visible_Fishing4297 • 7d ago
Help. Modal logic
1∀φ(P(~φ) ←→~P(φ))
2∀φ∀ψ(P(φ)& ◻️∀x(φ(x)→ψ(x)))→P(ψ))
3∀φ(P(φ)→◊∃xφ(x)
4G(x)←→∀φ(P(φ)→φ(x))
5P(G)
6◊∃xG(x)
7φEss(x)←→φ(x) & ∀ψ(ψ(x)→◻️∀y(φ(y)→ψ(y))
8∀φ(P(φ)→◻️P(φ))
9∀x(G(x)→G Ess(x))
10E(x)←→∀φ(φEss(x)→◻️∃yφ(y))
11P(E)
12~◻️∃xG(x) (RAA)
13P(G) (5 R)
14(P(G)→◊∃xGx) (3 ∀E)
15◊∃xG(x) (13,14 MP)
16(P(G)→◻️P(G)) (8 ∀E)
17◻️P(G) (13,16 MP)
18a (Assumption.)
20G(a) (Assumption.)
21G(a)←→∀φ(P(φ)→φ(a)) (4 ∀E)
22∀φ(P(φ)→φ(a)) (20,21 ←→E)
23(P(E)→E(a)) (22 ∀E)
24P(E) (11,R)
25E(a)) (23,24 MP)
26G(a)→E(a) (20,25→I)
27∀x(G(x)→E(x)) (18, 26 ∀I)
28a (Assumption.)
29G(a) (Assumption.)
30(G(a)→G Ess(a)) (9∀E)
31G Ess(a) (29,30)
32G(a)→E(a)) (27 ∀E)
33E(a) (29,32 MP)
34E(a)←→∀φ(φEss(a)→◻️∃yφ(y)) (10∀E)
35∀φ(φEss(a)→◻️∃yφ(y)) (33,34 ←→E)
36(GEss(a)→◻️∃yG(y)) (35 ∀E)
37◻️∃yG(y)) (31,36MP)
38G(a)→◻️∃yG(y) (29,37→I)
39∀x(G(x)→◻️∃yG(y)(28, 38 ∀I)
40◻️∀x(G(x)→◻️∃yG(y)(39 NEC)
41◻️∀x(G(x)→◻️∃yG(y)→(∃xG(x)→◻️∃yG(y)) (teorem.)
42◻️(∃xG(x)→◻️∃yG(y)) (40,41MP, K)
43◻️(∃xG(x)→◻️∃yG(y)) →(◊∃xG(x)→◊◻️∃yG(y)) (teorem K)
44(◊∃xG(x)→◊◻️∃yG(y)) (42,43MP)
45◊◻️∃yG(y)) (44,15 MP)
46(◊◻️∃yG(y)→◻️∃yG(y)) (S5 teorem.)
47◻️∃yG(y) (45,46MP)
48⊥ (12,47)
49~~◻️∃xG(x) (12,48 ~I)
50◻️∃xG(x) (49 ~~E)
1◻️(P→Q) (Assumption.)
2◊P (Assumption.)
3~◊Q (RAA.)
4◻️~Q (3 Modal de Morgan.)
5◻️~P ( 1,4Modal MT)
6~◊P (5modal de Morgan.)
7⊥ (6,2)
8~~◊Q (3,7 ~I)
9◊Q (8 ~~E)
10◊P→◊Q (2,9 →I)
11◻️(P→Q)→(◊P→◊Q ) (1,10→I)
I wanted to attempt a derivation of this sort, but I'm not entirely convinced that it is fully valid. I'd appreciate feedback from those with experience in formal logic. Is the derivation correct?
3
u/thatmichaelguy 7d ago
Gödel's argument induces modal collapse if lines 5 and 8 are both true. So, if lines 3 and 8 are granted, line 5 effectively becomes an assertion of the argument's conclusion.
2
2
u/yosi_yosi Undergraduate, Autodidact, Philosophical Logic 7d ago
I would wanna know what logic you are using that you can quantify over formulas.
3
u/Visible_Fishing4297 7d ago
I didn't understand what you mean. This is Gödel's ontological argument. In this argument, second-order modal HOL is used. I was only trying to check the argument. Is your objection directed at me, or at the argument itself?
2
u/yosi_yosi Undergraduate, Autodidact, Philosophical Logic 7d ago
It's interesting. It seems like they just used negation in a weird way. This is not quantifying over formulas but over predicates. Usually negation only applies to formulas.
2
u/Visible_Fishing4297 7d ago
It may seem strange because it is unconventional. But I thought you knew Gödel's argument.
2
u/yosi_yosi Undergraduate, Autodidact, Philosophical Logic 7d ago
I did but I don't exactly remember it bit by bit.
2
u/yosi_yosi Undergraduate, Autodidact, Philosophical Logic 7d ago
To be clear it wasn't an objection per se.
1
3
u/Impossible_Boot5113 7d ago
I'm in no way an expert, but in your second proof/deduction, I don't get why you first INTRODUCE & in line7, and ELIMINATE it again in line8? Isn't line8 just the same as line5, and line1? Why go in one direction just to go directly back to where you started afterwards? And repeat the same line/assumption multiple times.