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


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).

  • 1
    $\begingroup$ 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)$... $\endgroup$ – Self-teaching worker Mar 1 '15 at 18:03
  • 2
    $\begingroup$ @Self-teachingDavide Is that OK now? $\endgroup$ – Demosthene Mar 1 '15 at 18:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.