# Semantic expressiveness of modal logic

I am wondering how much of the semantic of basic philosophical questions can be expressed by formal arguments in modal logic. Here is one argument I formalised myself:

P1 ◇ ∀a, ∃x // GNB(x, a) ∧ C(a) ≡ S(x)

P2 ◻ ∀b, ∃y // GNB(y, b) ∧ A(b) ≡ F(S(y))

C ◇ ∀c // A(c) ≡ F(C(c))

The original argument, in ordinary language, proved very difficult to understand for most people I have tested with it.

Is it possible to prove the validity of such an argument in a formal way, given its apparent complexity for most people? How complex proven arguments can be? Could you give a representative example of a complex argument?

• Is `GNB` a single predicate symbol? – Gregory Nisbet Jan 16 at 21:55
• I am unsure of the symbolism; it would be a great help if you explain them. – Bertrand Wittgenstein's Ghost Jan 17 at 7:29
• @GregoryNisbet Yes, GNB(x, a) could be rewritten as G(x, a) for example. – Speakpigeon Jan 17 at 10:42
• @BertrandWittgenstein'sGhost ◇ ∀a, ∃x // GNB(x, a) ∧ C(a) ≡ S(x) just mean: For all we know, it is possible that whatever a, there is at least one x such that the predicate GNB is true of the ordered pair (x, a) and that the predicate C being true of a is identical to the predicate S being true of x. Is that enough? – Speakpigeon Jan 17 at 10:47
• @MauroALLEGRANZA OK, that's for you to tell me. I think the argument is valid on the face of it, intuitively, so I would myself interpret the fact that it is not formally valid as an indication that something is missing in the formal method you use. – Speakpigeon Jan 17 at 10:53