How to prove that a set containing G$\phi$ and G$\neg \phi$is inconsistent without completeness but with soundness.

Question

I'm stuck with this problem... The logic is a adaptation to temporal logic from $K_4$ of modal logic. The interpretation of G$\phi$ is always true in the future (now is not included). The axioms for the logic are:

$G\phi \rightarrow GG\phi$

$G(\phi \rightarrow \psi) \rightarrow (G \phi \rightarrow G \psi)$

And the derivation rules are Modus Ponens and Necessitation: from $\phi$ infer G$\phi$.

Thank you!

Answer 1

Long comment

Regarding inconsistency, we will use the "standard" definition :

$\Gamma$ is inconsistent iff for some $\phi : \ \Gamma \vdash \phi$ and $\Gamma \vdash \lnot \phi$.

I assume that we can use also the definition of $\lnot \phi$ as : $\phi \to \bot$.

Thus, the above definition is equivalent to :

$\Gamma$ is inconsistent iff $\Gamma \vdash \bot$.

Having said that, from $G \lnot \phi$, i.e. $G(\phi \to \bot)$, by axiom 2 and modus ponens, we get : $G\phi \to G\bot$.

Using $G\phi$ we can conclude, again by mp, with :

$G\bot$

and this formula is unsound, because it asserts that in the future $\bot$ will be true, which is not.

Thus, any set $\Gamma$ containing both $G \phi$ and $G \lnot \phi$ is unsound.

We have that soundness implies consistency, but not vice versa; thus, from the unsoundness of the set $\Gamma$ above, we are not entitled to deduce inconsistency.

It seems to me that some neeeded details about the temporal logic based on $K_4$ is missing ... For example : the logic proves $\lnot G \bot$ ?