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

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!!!

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).
• Thank you for your answer! Forgive me: I don't understand the first line, among other things, but I would say that that $\lnot(A\land FB\rightarrow F(PA\land B))\iff (A\land FB)\land\lnot F(PA\land B)$... – Self-teaching worker Mar 1 '15 at 18:03