$A\land FB\rightarrow F(PA\land B)$ in temporal logic

Question

Temporal minimal logic $\mathbf{K_T}$ calculus is characterised by the following axioms, where $F=_{\text{def}} \lnot G\lnot$ and $P=_{\text{def}} \lnot H\lnot$:

1. $G(A\rightarrow B)\rightarrow (GA\rightarrow GB)$
2. $H(A\rightarrow B)\rightarrow (HA\rightarrow HB)$
3. $A\rightarrow GPA$
4. $A\rightarrow HFA$

and the rules deriving $GA$ and $HA$ from $\vdash A$. The intensional operators can be read as follows: $F$ 'at some instant in the future', $P$ 'at some instant in the past', $G$ 'always in the future' and $H$ 'always in the past'.

I read -D. Palladino, C. Palladino, Logiche non classiche- that the following theorems follows from such a system:$$A\land FB\rightarrow F(PA\land B)$$$$A\land PB\rightarrow P(FA\land B)$$but I cannot prove it, although I think that the symmetry of the operators allows to use an analogous inference pattern for both cases. If we use Kripke semantics to define instants as worlds with a partial order relation $<$, it is easy for me to see how to derive the desired theorems, but I cannot derive them from the $\mathbf{K_T}$ axioms. Could anybody explain how to do so? I thank you very much!!!

Answer 1

Working by contradiction (i.e. starting with the negation of the statement and trying to show that it is a logical falsehood): \begin{align} &\neg\big(A\land FB\to F(PA\land B)\big)\\ \Longleftrightarrow&(A\land FB)\land \neg F(PA\land B)\\ \Longleftrightarrow&(A\land\neg G\neg B)\land G\neg(\neg H\neg A\land B)\qquad\text{(definition F,P)}\\ \Longleftrightarrow&\neg(\neg A\lor G\neg B)\land G(H\neg A\lor\neg B)\\ \Longleftrightarrow&\neg(\neg A\lor G\neg B)\land G(\neg H\neg A\to\neg B)\\ \Longleftrightarrow&\neg(\neg A\lor G\neg B)\land (G\neg H\neg A\to G\neg B)\qquad\text{(1)}\\ \Longleftrightarrow&\neg(\neg A\lor G\neg B)\land (GPA\to G\neg B)\qquad\text{(definition P)}\\ \Longleftrightarrow&\neg(\neg A\lor G\neg B)\land (\neg GPA\lor G\neg B)\\ \Longleftrightarrow&\neg(\neg A\lor G\neg B)\land (\neg A\lor G\neg B)\qquad\text{(contrapositive of 4)} \end{align}

Clearly the last line is a contradiction, of the form $\psi\land\neg\psi$. Therefore, since the negation of the theorem is false, the theorem itself must be true (tautology).