Access the full text.

Sign up today, get DeepDyve free for 14 days.

Axioms
, Volume 9 (2) – Jun 16, 2020

/lp/multidisciplinary-digital-publishing-institute/minimal-systems-of-temporal-logic-eUI91a3nw5

- Publisher
- Multidisciplinary Digital Publishing Institute
- Copyright
- © 1996-2020 MDPI (Basel, Switzerland) unless otherwise stated Disclaimer The statements, opinions and data contained in the journals are solely those of the individual authors and contributors and not of the publisher and the editor(s). Terms and Conditions Privacy Policy
- ISSN
- 2075-1680
- DOI
- 10.3390/axioms9020067
- Publisher site
- See Article on Publisher Site

axioms Article ID Dariusz Surowik University of Bialystok, Swierkowa 20 B, 15-328 Białystok, Poland; surowik@uwb.edu.pl Received: 6 April 2020; Accepted: 26 May 2020; Published: 16 June 2020 Abstract: The article discusses minimal temporal logic systems built on the basis of classical logic as well as intuitionistic logic. The constructions of these systems are discussed as well as their basic properties. The K system was discussed as the minimal temporal logic system built based on classical logic, while the IK system and its modiﬁcation were discussed as the minimal temporal logic system built based on intuitionistic logic. Keywords: temporal logic; intuitionistic logic; minimal system; knowledge 1. Temporal Logic Temporal logic is the logic in which they appear, as logical constants, expressions whose meaning is determined by a reference to time. In its wide sense, temporal logic includes all logical problems of temporal representation of information. The task of temporal logic is to deﬁne and systematize inference rules for reasoning carried out in a language in which the same expression in terms of shape is used to pronounce sentences whose logical value may not be the same in different temporal contexts of their use. The precursor of temporal logics was A. N. Prior. One of Prior ’s basic concepts was the temporal interpretation of modal operators. The enriched language of temporal logic was to enable formalization of reasoning regarding situations changing in time. Originally, temporal logic was to be a tool for formalizing philosophical, linguistic and semiotic considerations. Currently, apart from these applications, temporal logic is also widely used in computer science. Among temporal logics, tense logic stands out, i.e., logic in a language whose only speciﬁc time operators are grammatical operators. 2. K —Minimal Tense Logic The basic deductive system of logic of time is the K system (K is a temporal analogue of the K system t t (minimal deductive system for modal logic).). K is a tense logic system built over classical propositional calculus by enriching this logic with speciﬁc axioms and rules. This is the minimal system. Therefore, the theses of this system are all and only those sentences that are true regardless of what properties time has (In fact, one assumption is made about the structure of time, namely it is assumed that a semantic time in the K has a point structure.). The K system, as a minimal system, can be expanded by adding additional rules and speciﬁc axioms. In this sense, the minimality of K means that any other temporal logic system built above classical propositional logic is richer than the K . In the tense logics we have the tense operators: F, G, P, H understood as follows: Axioms 2020, 9, 67; doi:10.3390/axioms9020067 www.mdpi.com/journal/axioms Axioms 2020, 9, 67 2 of 28 Fj - it will be that j, Pj - it was that j, Gj - it always will be that j, Hj - it always was that j. However, usually the operators F and G and operators P and H are mutually deﬁnable (The mutual deﬁnability of operators F and G as well as P and H occur in temporal logic systems based on classical logic. In temporal logic systems based on intuitionistic or multi-valued logic, the mutual deﬁnability of these operators usually does not take a place.). Deﬁnition 1 (The alphabet of the language L ). countable set of propositional letters AP , connectives: :,!, temporal operators: G, H (In some tense logic systems, as a primary operators are assumed F and P.), brackets: ), (. A set of sentences is deﬁned as follows: Deﬁnition 2 (A set of sentences ). The set of sentences is the smallest set FOR(L ) such that: AP FOR(L ), if j, y 2 FOR(L ), then :j, j ! y, Gj, Hj 2 FOR(L ). K K t t In the language L , all boolean symbols retain their meaning. However, there are additional speciﬁc operators in this language. Therefore, when we speak about the validity of propositions due to the meaning of classical propositional connectives, then we mean the sentences in which new operators occur. We accept the following abbreviations: (a) j_ y :j ! y, (b) j^ y : (j ! :y) , (c) j $ y : [(j ! y) ! : (y ! j)] , (d) Fj :G:j, (e) Pj : H:j. Axioms The K system is axiomatizable (The axiomatic system is one of many possible forms of a deductive system. This approach to construction of a deductive system has many advantages when it comes to methodological research. However, in case of axiomatic systems, we have some problems when it comes to practical command. This is due to the unstructured axiomatic systems. The structure of the sentence does not indicate the method of proving this sentence. In the case of other approaches to construction of a deductive system, e.g., sequent calculus, natural deduction or semantic tables, it is different.). Various sets of axioms and rules of this system were proposed. These differences are primarily due to the decision on a set of speciﬁc primitive symbols. Usually, the set of these symbols consists of the symbols G and H, while F and P are deﬁned. When building a set of axioms for invariant systems, i.e., systems without the rule of substitution for sentence letters, apart from speciﬁc axiom schemes, either all tautologies of Axioms 2020, 9, 67 3 of 28 classical propositional logic or only selected tautology schemes are taken, but they are selected in such a way that all tautologies of classical propositional logic can be obtained. In this work, we used the second option and for the purposes of our considerations regarding K we will adopt the following set of axioms: Axioms: For any sentences j, y 2 L (K can be axiomatizable in many ways. The completeness of the K K t t with respect of these set of axioms was demonstrated by J. F. A. K. van Benthem [1].). 1. All tautologies of the classicall propositional calculus of the language L , 2. G(j ! y) ! (Gj ! Gy), 3. H(j ! y) ! ( Hj ! Hy), 4. j ! GPj, 5. j ! H Fj. Rules j ! y, j j j MP : . RG : R H: . y Gj Hj The speciﬁc K axioms are the 2–5 axioms. Axioms 2–3 are temporal equivalents of the K axiom for modal logics. These axioms apply only to the properties of G and H, respectively. Axioms 4–5 bind the operators G and P as well as H and F respectively. The proof in K is understood in the usual way. Deﬁnition 3 (Proof in K ). Let S be any set of sentences of the language L . The sentence string j , j , ..., j is t K 0 1 n a proof of the sentence j from the set S, (we write S ` j) if and only if j = j and for any i such that 0 i n at least one of the following conditions holds: 1. j is an element of the set S, 2. j is an axiom, 3. j is obtained from their predecessors by MP, RG or RH, respectively. The sentence j, which is derived from the empty set S, or Æ ` j, is the thesis of the system K . K t Instead of writing Æ ` j, we will write ` j. K K t t In the K system, if a subsentences j of the sentence f is equivalent to the sentence y, entering f in the place of the sentence j as the inscription of the sentence y, f(y/j), gives the sentence equivalent to f. Theorem 1. If S ` j $ y, then S ` f $ f(y/j). (This theorem is not just the K theorem. It is the theorem K K t t t of tense priorist logic.) Proof. We will prove by induction due to the length of the sentence f. Let S ` j $ y. Let f be a propositional letter p. The only subsentence of a sentence f is the propositipnal letter p. Then j is equal p. Result of replacement j in the f by y will be the sentence y. Because by assumption we have S ` j $ y, then: S ` f $ f(j/y). As an induction assumption, we assume that for any sentence f witch length is not greater than k the thesis is true, i.e., S ` f $ f (j/y). K i i t Axioms 2020, 9, 67 4 of 28 We will show that this thesis is also true for sentences of length k + 1. Let the string j , j , ..., j (= f $ f (y/j)) be a proof of the sentence: f $ f (y/j). We add the 1 2 i i i i following sentences to this proof: n+1. :f (j/y) $ :f TRANS, n i i n+2. (:f (j/y) $ :f ) ! (f $ f (j/y)) axiom 1 i i i i n+3. f $ f (j/y) MP,n+1,n+2 i i The sentence :f (j/y) is (:f )(j/y), then: i i S ` :f $ (:f )(j/y). K i i Let it now f will be according to the character f ! f , with sentences f and f meet the induction i j i j assumption, i.e., S ` f $ f (j/y) K i i and S ` f $ f (j/y). K j j Let the string j , j , ..., j (= f $ f (y/j)) be a proof of the sentence f $ f (y/j), while the 1 2 k i i i i string j , j , ..., j (= f $ f (y/j)) be a proof of the sentence: f $ f (y/j). To the sequence of k+1 k+2 n j j j j the sentences j , j , ..., j , j , j , ..., j we add sentences: 1 2 k k+1 k+2 n+1. (f $ f (y/j)) ! f(f $ f (y/j)) ! [(f ! f ) $ (f (y/j) ! f (y/j))]g axiom 1 i i j j i j i j n+2. (f $ f (y/j)) ! [(f ! f ) $ (f (y/j) ! f (y/j))] MP,k,n+1 j j i j i j n+3. [(f ! f ) $ (f (y/j) ! f (y/j))] MP,n,n+2 i j i j (f (y/j) ! f (y/j))] is the sentence (f (y ! f (y/j))], so we received proof that i j i j S ` (f ! f ) $ (f ! f (y/j)). K i j i j Now let us consider the case when the sentence f is the sentence of the form Gf , with the sentence f is a sentence satisfying the induction assumption, i.e., S ` f $ f (j/y). Let the string j , j , ..., j i K i i 1 2 n be a proof of the sentence f $ f (j/y) from the sentence S. To the proof we add: i i n+1. Gf $ Gf (j/y). i i Gf (j/y) is the sentence (Gf )(j/y). So we received proof that i i S ` Gf $ Gf (j/y). K i i The case where the sentence f is according to the form Hf is similar to the case when f is the sentence Gf . The Theorem 1 will be used in the proof of the next Theorem, which says that one of the K inference rules is the REQ replacement rule. This rule is a very useful rule in proving the theses of the K system. Theorem 2 (Rule REQ). If S ` j $ y, then . f(y/j) Proof. Let S ` j $ y and S ` f. According to the Theorem 1 there is a proof of the sentence K K t t f $ f(j/y) from the set S. To this proof we add the proof of the sentence f. We add to the proof sequence the sentence f(j/y), which is a result from applying the Modus Ponens rule to sentences: f and f $ f(j/y). Axioms 2020, 9, 67 5 of 28 In addition to the three inference rules proposed in this version of the axiomatics of the K system can be used to derive in this system the rules corresponding to the regularity rule for modal logics. j ! y Theorem 3. The RRG rule : is a rule of K . Gj ! Gy Proof. To demonstrate that RRG is a secondary rule K , it must be demonstrated that if S ` j ! y, then S ` Gj ! Gy. K K t t Let S ` j ! y. Let the sequence j , ..., j will prove the sentence j ! y from the set S. To this we K 1 n add the following sentences: n+1. G(j ! y) RG,n n+2. G(j ! y) ! (Gj ! Gy) axiom 2 n+3. Gj ! Gy MP,n+1,n+2. The resulting sequence is a proof of the sentence Gj ! Gy from the set S. j ! y Theorem 4. The RR H rule : is a secondary rule of K . Hj ! Hy Proof. Analogical to the proof of the previous theorem (using the axiom 3 and the rule R H). Based on Theorems 3 and 4 two further inference rules can be derived in K . j ! y Theorem 5. The RF rule : is a secondary rule of K . Fj ! Fy Proof. Let S ` j ! y. Let the sequence: j , ..., j will prove the sentence j ! y from the set S. To this K 1 n we add the following sentences: n+1. :y ! :j TRANS,n n+2. G:y ! G:j RRG,n+1 n+3. :G:j ! :G:y TRANS,n+2 n+4. Fj ! Fy REQ(:G:j/Fj), REQ(:G:y/Fy). The resulting sequence is proof of the sentence Fj ! Fy from the set S. j ! y Theorem 6. The RP rule : is a secondary rule of K . Pj ! Py Proof. Analogical to the proof of the Theorem 5. Operators H,P and G,F have the Mirror Image Property. Deﬁnition 4 (Mirror Image Property). The mirror image of the j formula is created by simultaneously replacing each instance of the H operator with the G operator and the G operator with the H operator in the j formula, and simultaneously replacing each instance of the P operator with the F operator and the F operator with the P operator. The Mirror Image of the j we will mean by M I(j). E.g: M I(j ! GPj) = j ! H Fj. The mirror image of the set of S is the mirror image set of the S elements. We mean the mirror image of S by M I(S) and deﬁne as follows: Axioms 2020, 9, 67 6 of 28 Deﬁnition 5 (A mirror image of a set of formulas). M(S) = f M I(j) : j 2 Sg. If j is derivable from S, then mirror image of j is derivable from mirror image of the S. Theorem 7. For any S( FOR(L )): if S ` j, then M I(S) ` M I(j). K K K t t t Proof. Let S ` j. Let the sequence j , j , ..., j will be a proof of j from the S. We will show that 2 n K 1 the sequence M I(j ), M I(j ), ..., M I(j ) is a prooof of the sentence M I(j) from the M I(S), M I(S) ` 1 2 n K M I(j). We will carry out the proof by induction due to the length of the proof of the sentence j. If j is an axiom, then M I(j ) is also an axiom. If j is an element of S, then M I(j ) is also 1 1 1 1 an element of M I(S). Then if S ` j , then M I(S) ` M I(j ). K 1 K 1 t t Let us assume that for i, i k : if S ` j , then M I(S) ` M I(j ). K i K i t t We will show that if S ` j , then M I(S) ` M I(j ). Let S ` j . The sentence j can K k+1 K k+1 K k+1 k+1 t t t be an axiom or an element of a set S. There are cases discussed for the sentence j . Now let us consider the cases where the sentence j was obtained using one of the inference rules. Let them j will be a k+1 k+1 sentence derived from sentences j and j ! j by applying the rule MP. By induction, we have that m m k+1 M I(S) ` M I(j ) K m and M I(S) ` M I(j ! j ). K m k+1 Because M I(j ! j ) has the form M I(j ) ! M I(j ), so applying the rule MP to the m m k+1 k+1 sentences M I(j ) ! M I(j ) and M I(j ), we obtain M I(j ). Let it now j will be the sentence m k+1 m k+1 k+1 derived from the sentence j by applying the rule RG. By induction, we have that M I(S) ` M I(j ). m m After applying the rule R H to the sentence M I(j ) we obtain H M I(j ). However, this sentence is equal m m to the sentence M I(Gj ). Then M I(S) ` M I(Gj ). The case when the sentence j was obtained by m m K k+1 applying the R H rule to the sentence j is similar to the previous case. Corollary 1. Let M I(S) S. If S ` j, then S ` M I(j) K K t t or M I(j) is a secondary rule. Corollary 2. Let M I(S) fj : S ` jg. If S ` j, then S ` M I(j) K K t t or M I(j) is a secondary rule. Axioms 2020, 9, 67 7 of 28 3. IK —Minimal Intuitionistic Temporal Logic Now we will discuss a system of temporal logic over intuitionistic propositional logic. It is a system of minimal intuitionistic temporal logic IK (IK is the intuitionistic analogue of the system K - minimal t t t temporal logic built over classical propositional logic.). This system can be used to formally describe knowledge that changes over time, although there are no explicit epistemic operators in the language of this system. Knowledge representation is not implemented at the syntactic level, but because of the properties of intuitionistic logic, knowledge is represented at the semantic level. This is the result of semantics proposed for intuitionistic logic, using terms such as proof (It was proposed by Kolmogorov.), information, or knowledge (Kripke-style semantics.). Kripke-style semantics are proposed for intuitionistic temporal logic. Thus, in Kripke models we have a set of worlds W and the relationship R. In the case of intuitionistic logic, we do not speak about elements of the W set as possible worlds, but rather as information states, states of knowledge, etc. The reachability relationship between the elements w and v (i.e., wRv) is interpreted as w has access to v, which means that the v information state is available from the w information state. The key difference between Kripke models for intuitionistic logic and Kripke models for modal logic built over classical logic lies in the fact that in the case of modal logic built over classical logic, the R relation is only used to interpret modal operators, and in the case of intuitionistic logic, this relation is used to interpret the intuitionistic negation and implication. The formula:j is true (In intuitionistic logic the term forced is also used.) in some information state w if and only if there is no information state available from w in which j is true. In other words, the formula :j is true in the state w if there is no possibility that j is true in any information state accessible from the state w. The same is true with the intuitionistic implication. The formula j ! y is true in the information state w, if and only if, in any information state available from the state w , the truth of j implies the truth of y. In addition, Kripke models assume monotonicity for intuitionistic logic. The formula fulﬁlled in a given information state remains fulﬁlled in any extension of this state. Modality in intuitionistic logic can be seen on the example of the syntactic deﬁnition of intuitionistic negation. The :j formula is equivalent to the j ! ? formula. Intuitionistic negation can therefore be seen as a kind of impossibility operator. Kripke’s intuitionistic model is a triangle M = hW, R, Vi, where V : AP ! 2 . The formula j is satysﬁed in the model M, in the state w, when: M, w j= j w 2 V(j), when j 2 AP , 0 0 M, w j= :j for any wRw : M, w 2 j, M, w j= j^ y M, w j= j and M, w j= y, M, w j= j_ y M, w j= j or M, w j= y, 0 0 0 0 M, w j= j ! y for any w such that wRw , if M, w j= j, then M, w j= y. In intuititionistic logic from the truth of the :j formula in the current information state, we do not only know that j is not true in the current information state (such information is obtained in the case of classical logic), but we also know that the formula j will never be true, and our never applies to all available extensions of the current information state. In addition to the information provided explicitly, we therefore have an additional information in intuitionistic logic. This feature of intuitionistic logic van Benthem calls knowledge implicite [2]. No additional speciﬁc operators are needed to express it in intuitionistic logic. Despite similar semantics, this feature deﬁnitely distinguishes intuitionistic logic from epistemic logic built on classical logic. The language of epistemic logic is used to represent knowledge explicitly, and to Axioms 2020, 9, 67 8 of 28 represent it, in addition to classical sentence connectives, the epistemic operator K is used. The language of intuitionistic logic allows expressing certain concepts without explicitly referring to epistemic operators. For example, based on the truth of the formula ::j, we say that for each information state there is such an extension in which j is true. Apart from details, it is very close to that we know that j must be true. In Kripke semantics for epistemic logic built over classical propositional calculus, the formula Kj in the M model, in the w information state, was deﬁned as follows: 0 0 M, w j= Kj for any wRw : M, w j= j. Let us consider the truth of the formula K:j in the model M, in the state w. In accordance with the condition of satisfy with the operator K we have: 0 0 M, w j= K:j for any wRw : M, w j= :j. Taking into account the condition of fulﬁlling of the negation in epistemic logic built over classical logic, we have: 0 0 M, w j= K:j for any wRw : M, w 2 j. The condition of fulﬁlling of the intuitionistic negation, i.e., 0 0 M, w j= :j for any wRw : M, w 2 j Indicates that intuitionistic negation (:) can be seen as a combination of the K operator and classical negation (K:). Similarly, it can be shown that the intuitionistic formula j ) y can be seen, aside from the details, as modalized implication K(j ! y), i.e., a combination of the K epistemic operator and the classic implication. IK (The construction of the IK system and proof of the system’s completeness with respect to the t t proposed semantics was provided by W.B. Ewald [3].) is a system of temporal logic built over intuitionistic propositional calculus. The language L is the language of intuitionistic propositional logic enriched IK with temporal operators: G, H, F, P. Deﬁnition 6. The set of sentences FOR(L ) is the smallest set of ﬁnite sequences of elements of the language IK alphabet L such that: IK 1. if j 2 AP , then j 2 FOR(L ), IK 2. if j, y 2 FOR(L ), then :j, Gj, Fj, Hj, Pj, (j^ y), (j_ y), (j ! y), (j $ y) 2 FOR(L ). IK IK t t In the IK system, the operators G and F as well as H and P, unlike systems built over classical logic, are not mutually deﬁnable. 4. Semantics for IK Proposed by Ewald The construction of semantics for IK is based on a partially ordered set of states of knowledge, which is considered by the cognitive subject. Each state of knowledge is assigned a set of time moments and temporal order. When the cognitive subject reaches a greater state of knowledge (According to Ewald [3], the cognitive subject moves to a greater states of knowledge.), retains all the information that he had in lower states of knowledge. To deﬁne semantics for this system, Ewald constructs an intuitionistic temporal structure. Axioms 2020, 9, 67 9 of 28 Deﬁnition 7 (intuitionistic temporal structure [3]). An intuitionistic temporal structure M is an ordered quintuple hS,,fT g ,fm g ,fR g i s s2S s s2S s2S,t2T t s where: (S,) is a partially ordered set, T is a non-empty set, m is a binary relation to T , s s R is a formula relation that satisﬁes the conditions: s s 0 1. R (j) R (j), when j 2 AP and s s , t t s s s 2. R (j^ y) R (j) and R (y), t t t s s s 3. R (j_ y) R (j) or R (y), t t t s 0 s 4. R (:j) for any s s it is not true that R (j), t t 0 0 s 0 s s 5. R (j ! y) for any s s (if R (j), then R (y)), t t t s 0 0 s 6. R (Fj) there is t , tm t : R (j), s 0 s 0 0 s 7. R (Pj) there is t , t m t : R (j), s 0 t t s 0 0 0 0 0 s 8. R (Gj) for any s , t such that: s s , t 2 T 0 , tm 0 t : R (j), s s t t s 0 0 0 0 0 s 0 0 9. R ( Hj) for any s , t such that: s s , t 2 T , t m t : R (j), s s 0 We will now give intuitions related to individual elements of the above structure. The (S,) pair is a partially ordered set of states of knowledge. T is a set of time moments in the state s. m is a binary s s relation on the set T . In addition, to fulﬁll the postulate that the cognitive entity, achieving a greater state of knowledge, retains all information from smaller states, it is required that for s s the following conditions holds: T T 0 and m m 0 . In other words, a cognitive subject achieving a higher state of s s s s knowledge maintains a set of time moments and temporal order from smaller states of knowledge. The truth of a formula in an intuitionistic temporal structure and the truth of the formula are deﬁned as follows: Deﬁnition 8 (the truth in an intuitionistic temporal structure). M j= j, the formula j is true in the intuitionistic temporal structure M, if and only if for any s 2 S and any t 2 T : R (j). Deﬁnition 9 (the truth of the formula). j= j, formula j is true if and only if, for any M : M j= j. 5. Axioms IK (1) j, if j is a tautology of the intuitionistic logic of the language L . IK t Axioms 2020, 9, 67 10 of 28 (2) G (j ! y) ! (Gj ! Gy) (2’) H (j ! y) ! ( Hj ! Hy) (3) G j^ y $ Gj^ Gy (3’) H j^ y $ Hj^ Hy ( ) ( ) ( ) ( ) (4) F (j_ y) $ (Fj_ Fy) (4’) P (j_ y) $ (Pj_ Py) (5) G (j ! y) ! (Fj ! Fy) (5’) H (j ! y) ! (Pj ! Py) (6) Gj^ Fy ! F j^ y (6’) Hj^ Py ! P j^ y ( ) ( ) ( ) ( ) (7) G:j ! :Fj (7’) H:j ! :Pj (8) F Hj ! j (8’) PGj ! j (9) j ! GPj (9’) j ! H Fj (10) (Fj ! Gy) ! G (j ! y) (10’) (Pj ! Hy) ! H (j ! y) (11) F (j ! y) ! (Gj ! Fy) (11’) P (j ! y) ! ( Hj ! Py) Rules: MP, RH, RG. Ewald [3] proves the adequacy of the IK system with respect to the class of intuitionistic temporal structures. For the purposes of proof of adequacy, the concept of consistent pair of sets is introduced. Deﬁnition 10 (consistent pair of sets). The (X, Y) pair of set of sentences is consistent if and only if such ﬁnite subsets do not exist X (= fj , j , ..., j g) X and Y (= fy , y , ..., y g) Y such that ` (j ^ j ^ ...^ m n 0 1 2 0 1 2 1 2 j ) ! (y _ y _ ..._ y ) m 1 2 n In the IK we can to prove the intuitionistic equivalent of the Lindenbaum lemma, namely: 0 0 Theorem 8. If the pair (X, Y) is consistent, then there is the consistent pair of (X , Y ) such that: 0 0 1. X X and Y Y , 0 0 2. X \ Y = Æ, 0 0 3. for any formula j : j 2 X or j 2 Y . The pair that fulﬁlls these conditions is maximum consistent pair. Each (X, Y) maximum consistent pair can be represented by a valuation v : v : FOR( I K ) ! f0, 1g, such that v(j) = 1 iff j 2 X. Ewald proves for the IK system the strong completeness Theorem in the following version: Theorem 9 (Adequacy IK [3]). For any IK valuation v there is an intuititionistic structure t t M = hS,,fT g ,fu g ,fR g i, state on knowledge s 2 S and moment t 2 T such that for any s s s s2S s2S s2S,t2T t s formula j 2 FOR(L ) holds R (j) iff v(j) = 1. IK t t In the semantic of the IK system, we did not impose any conditions on the temporal order in intuitionistic temporal structures. The IK system is therefore an analogue of the K system, i.e., it is t t a minimal system of intuitionistic temporal logic. 6. Modiﬁed Semantics for IK We will consider the modiﬁed semantics for IK and examine its basic properties. IK is used to t t describe states of knowledge that change as knowledge gains. Acquiring knowledge in IK is understood as moving to states of knowledge; however, as in the IK system, it is assumed that all knowledge from a given state of knowledge is available in any state of knowledge not lesser than contemplated. Therefore, Axioms 2020, 9, 67 11 of 28 the monotonicity of the knowledge acquisition process is assumed. We achieve knowledge by enriching our knowledge with new facts. This can occur in several cases. We can enrich our knowledge when by research we describe events from the past that took place at times that were not known in a given state of knowledge. We did not have any information about these events in this state of knowledge. In this case, the temporal structure in not lesser state of knowledge expands into the past and is a superset of the temporal structure of a given state of knowledge. For the same reasons, the time structure of the state of knowledge may expand into the future. The expansion of the temporal structure (regardless of whether it takes place in the past or in the future) causes a change in the domain of the relationship. Therefore, in the new state of knowledge, the changed relation between moments of time should be considered. Another possible option to achieve knowledge is the situation when the set of moments of time does not change, but the powers of sets of formulas increase, which we can determine if they are fulﬁlled in given time moments. Therefore, in this case there is no expansion of the time structure, neither into the past nor into the future, but by getting to know the present, past or future better within the known temporal structure, we attribute to moments more numerous sets of formulas fulﬁlled in these moments. In the proposed semantics, the state of knowledge consists of a set of facts, which are semantic correlates of formulas, a set of moments of time, and the relationship at the set of moments of time. A subset of the set of facts assigned to a speciﬁc moment is understood as the set of facts known at that moment. Achievable states of knowledge are different in their level of knowledge. The level of knowledge is determined by its constituent elements, namely: a set of moments of time , the temporal order relation and sets of formulas fulﬁlled at individual time moments. We will say that the state of knowledge of m has not lesser level of knowledge than the state of knowledge of m , if and only if the following conditions are satisﬁed: 0 00 1. The set of moments of time in the state m is included in the set of moments of time in the state m . (Changing the number of moments of time causes a change in the level of knowledge.) 2. In the m , there are - occurring between moments of time - earlier-later relationships that existed in 0 00 the m state of knowledge. Also, in the m , such relationships can occur that did not take place in the state m . 0 00 3. All events that are known in the state of knowledge m are also known in the state of knowledge m . (What is known does not cease to be known also when new known events occur.) In addition at the moments of time of the state of knowledge m , may be known some events that are not known in the equivalents of these moments in the state of knowledge m . There are speciﬁc relationships between conditions 1, 2 and 3. Fulﬁllment of condition 1 implies fulﬁllment of condition 2, because we skip situations in which new moments of time are not in any relationship earlier-later with other moments. A change in the set of moments of time therefore entails a change in the relationship between the moments of time. It is not the other way round. Changing the relationship between the moments of time does not have to involve changing the set of time moments. In the state of knowledge with no less level of knowledge, new relationships earlier-later can occur between time moments in the state of knowledge with a lower level of knowledge. Therefore, fulﬁllment of condition 2 does not entail fulﬁllment of condition 1. Similarly, fulﬁllment of condition 3 does not entail fulﬁllment of condition 1 or 2, because new facts may be known without new time moments or new relationships earlier-later. Each moment is assigned a non-empty set of known events. If there are new moments, there are also new facts known. The fulﬁllment of condition 1 implies the fulﬁllment of condition 3. Axioms 2020, 9, 67 12 of 28 The existence of new relationships earlier-later, on the other hand, entails the existence of new facts known at the times in which new relationships earlier-later take place. Thus, as in the case of condition 1, the fulﬁllment of condition 2 implies the fulﬁllment of condition 3. We have two types of time. The ﬁrst is the time that is assigned to the state of knowledge. It is a structure consisting of a set of moments of time and relationship earlier-later of a given state of knowledge. The other is time that is not relativized to any state of knowledge. This time is the sum of the times assigned to all possible states of knowledge. We write theese intuitions in a formal way. I is a non-empty set (indexes of state of knowledge). T (i 2 I) is a non-empty set (of moments in the state of knowledge indexed by i). R ( T T ) is a binary relation deﬁned on a set of moments of time in the state of knowledge i i i indexed by i. Relation R is understood as the relation earlier-later on the set of moments of time of state of knowledge indexed by i. T = hT , R i. It is a time in the state of knowledge indexed by i. i i i T = T is a set of all time moments existing in any state of knowledge. i2 I R = R is a binary relation on the set T. This relation is understood as the earlier-later relation for a i2 I time not relativized to any state of knowledge. We note that R T T. T = hT, Ri it is a time not relativized to any state of knowledge. AP V T 2 , where i 2 I. V is a function that assigns t 2 T subsets V (t) to a set of sentence letters. i i i i i F = fV : i 2 Ig is a set of valuations. m = hT , R , Vi where i 2 I. (m is the state of knowledge indexed by i.) i i i i i M = fhT , R , Vi : V 2 F , i 2 Ig, or M = fm : i 2 Ig. M is a model based on the T and class i i i i i F function. We deﬁne the relationship ( M M) Deﬁnition 11. For any i, j 2 I : m m iff T T and R R and for any t 2 T : V (t) V (t) . i j i j i j i i j That for the states of knowledge m , m the relation (m m ) is understood as follows: state of i j i j knowledge m has no lower level of knowledge than the state of knowledge m . j i The relationship is determined by the inclusions of a set of moments of time, the relationship between the moments of time and sets of events known at particular moments of time. The relation is therefore reﬂexive and transitive. Theorem 10 ([4]). For any m (2 M) : m m . i i i Theorem 11 ([4]). For any m , m , m (2 M) : i j k if (m m and m m ), then m m . i j j i k k The relationship partially organizes the set of states of knowledge. In the states of knowledge, various relationships may occur between sets of time moments, earlier-later relations and valuations. Let us consider some of them. The ﬁrst possible situation is: Axioms 2020, 9, 67 13 of 28 T = T and R = R and 8 V (t) V (t) . i j i j i j t2T This situation occurs when sets of time moments of states of knowledge m and m are the same i j T = T . The relations R = R are the same in both states of knowledge. The state of knowledge m , i j i j j as a state of knowledge with no lower level of knowledge than the state of knowledge m , is created by changing the value of the function V that assigns moments to subsets of the set AP . In other words, in this case, the state of knowledge about a not lower level of knowledge is created by increasing the amount of facts known at particular times. The second possible situation may be as follows: T T , R R and 8 V (t) = V (t) . i j i j i j t2T In this case, the m , as a state of knowledge with not lesser level of knowledge than the m , is created j i by adding to the structure of the state of knowledge m new moments of time. For any time t (2 T ) i i does not change the set V t . The change in the level of knowledge is that in the state of knowledge m ( ) i j new time moments appear (in the future or in the past). Due to the new time moments, in the state of knowledge m all the components change. The set of time moments changes. The relation earlier-later is changing, because certain time moments of the state of knowledge m will be in relation earlier-later with new time moments. The evaluating function is also changing, assigning subsets of the sentence letter set to moments of time because its domain is changing (subsets of the set of sentence letters will be assigned new time moments). Yet another option is: T = T , R R and 8 V (t) V (t) . i j i j i j t2T It may also be that the change in the level of knowledge of the state of knowledge does not consist of changing the set of time moments known in the state of knowledge m but on the change of the property of time in the state of knowledge m . In other words, the change of ownership of the relationship in this state of knowledge. Such a change, however, entails a change in the number of facts known at these times. Further states of knowledge - with an increasingly higher level of knowledge—can arise by increasing the level of knowledge regarding the various components of the state of knowledge. To shorten the entries we will introduce the designation: Mark m (= hT , R , V i) (where i 2 I ) is any m (2 M) such that m m . j i j i i i i Deﬁnition 12 (the truth of a formula in the state of knowledge at some moment of time). The truth of the formula j(2 FOR(L )) in the model M, state of knowledge m (= hT , R , Vi), at the moment t(2 T ) we deﬁne IK i i i i i as follows: Axioms 2020, 9, 67 14 of 28 1. M, m , t j= j j 2 V (t), if j 2 AP , i i 2. M, m , t j= :j for any m 2 M : M, m , t 2 j i i 3. M, m , t j= j_ y M, m , t j= j or M, m , t j= y, i i i 4. M, m , t j= j^ y M, m , t j= j and M, m , t j= y, i i i 5. M, m , t j= j ! y for any m 2 M : (M, m , t 2 j or M, m , t j= y), i i i 0 0 0 6. M, m , t j= Fj there exists t 2 T , tR t : M, m , t j= j, i i i i 0 0 0 7. M, m , t j= Gj for any m (2 M), for any t (2 T ) such that tR t : M j= m , t j, i i i i 0 0 0 8. M, m , t j= Pj there exists t 2 T , t R t : M, m , t j= j, i i i i 0 0 0 9. M, m , t j= Hj for any m (2 M), for any t (2 T ) such that t R t: M j= m , t j, i i i i The necessary condition for the sentence Fj to be true in the state of knowledge m , at the time of t (2 T ) is the existence in the time structute of the state of knowledge m the moment t (2 T ) , later than t i i i (tR t ), in which the sentence j is true. If such a moment exists in the structure of time of m , then from the i i deﬁnition of the relationship and the theory of multiplicative properties of inclusions it follows that such a moment also exists in the structure of time of each state of knowledge with a level of knowledge not less than the level of state of knowledge m . Hence veriﬁcation of the truth of the sentence Fj in the state of knowledge m can be limited to the state of knowledge m . Please note that if the sentence Fj is i i not true at the time t it does not mean that in t the sentence F:j is true. For the G operator the situation is different. According to understanding the G operator, the sentence Gj reads: it will always be in the future that j. For the sentence Gj to be true in the state of knowledge m at t (2 T ), it is necessary that the sentence j is true in any state of knowledge m at any time t 2 T i i later than t (tR t ). The truth of the sentence Gj cannot be considered only within the temporal limits of a given state of knowledge. Just because the sentence j is always true in the future means that j is true at any point in the future. Since the state of knowledge m is assigned only a certain fragment of the time structure, when deﬁning the concept of the truth for a sentence built using the operator G, all states of knowledge with a level of knowledge not lower than the level of knowledge of state m . If the deﬁnition of the truth of the sentence Gj were in the form that was adopted in the system, e.g., in the system T [5] (intuitionistic temporal logic of unchanging time (By unchanging time (in accepted terminology) is understood a time such that for any i, j 2 I: (T = T and R = R ).)), i.e., i j i j 0 0 0 M, m , t j= Gj iff for any t 2 T , such that tR t : M, m , t j= j i i i i this would lead to contradictions. It would be possible that in some state of knowledge m would occur at the moment t M, m , t j= Gj. (1) and at some level of knowledge m , with a level of knowledge not lesser than the level of knowledge of the state of knowledge m , i.e., m m , there would be a moment t 2 T such that: t 2 / T , tR t and i i j 1 j 1 i j 1 M, m , t 2 j. Therefore, we have: j 1 M, m , t 2 Gj. (2) What is known does not cease to be known when the level of knowledge increases. Since the state of knowledge of m is a state of knowledge with a level of knowledge of not less than the level of knowledge of the state of m , so that M, m , t j= Gj we conclude that M, m , t j= Gj. This is contrary to (2). i i j Axioms 2020, 9, 67 15 of 28 The understanding of the truth of the formula Gj, in the state of knowledge m , at the moment t excludes the situation described above. We will now give some basic deﬁnitions. Deﬁnition 13. M j= j, j is true in the model M, iff for any state of knowledge m (2 M) and for any t(2 T ) : M, m , t j= j. i i Deﬁnition 14. T j= j, j is true in time T, iff j is true in the model M for any non-empty classF(= fV : i 2 Ig) of function. Deﬁnition 15. j= j, j is true iff for any T : T j= j. In some sciences (e.g., empirical sciences) it happens that sentences considered to be true at some time, with the development of scientiﬁc theories, turn out to be false. It happens that certain laws of empirical sciences in force in a given period are subject to veriﬁcation and are changed, and sometimes even rejected, as laws that inaccurately or even misrepresent the state of the world. Such veriﬁcation is possible due to the increase in the level of knowledge. In our terminology, we would write this fact as follows: the sentence true in some state of knowledge m , in some state of knowledge which level of knowledge is not lesser than the level of knowledge of m may not be true. In the IK system, this is not possible. What is i t true in the state of knowledge m is also true in any state of knowledge, with a level of knowledge not lesser than the level of knowledge of m . There are many differences between temporal logic systems based on classical logic and temporal logic systems based on intuitionistic logic. One of them is that failing to the truth of j does not entail the truth of :j. Let us consider the following situation. The sentence j is not known in the state of knowledge m at the moment t(2 T ), while is known at this moment in a state of knowledge m , whose level knowledge is i j not lesser than the level of knowledge in the state m . If the sentence j is not known at the time t in the state m , it would be considered that at the time t the sentence :j is known, then—according to the accepted condition of fulﬁlling :j - the sentence j could not be known at the time of t in any state of knowledge with a level of knowledge not lesser than the level of knowledge of m . In particular, the sentence j could not be known at the time t, in the state of knowledge m . This leads to a contradiction, since we get that j is known at the time of t, in the state m , and we conclude that it is known and unknown at the same time. When the sentence j is known at some moment of time, in some state of knowledge m , then in any state of knowledge with the level of knowledge not lesser than the level of knowledge of state m at this moment the sentence j is known. However, when :j is not known at some moment of time, it does not mean that at this moment, in any state of knowledge with a level of knowledge no lesser than the level of knowledge of m , is known j. It only means that it is not true that in every state of knowledge in which the level of knowledge is not lesser than the level of knowledge of m , j is currently unknown. We will prove a lemma that expresses the monotonicity of knowledge in the I K system. What is known in the state of knowledge m is also known in every state of knowledge whose level of knowledge is not lesser than the level of knowledge of the state m . Lemma 1. For any formula j(2 FOR(L )), for any m , m (2 M) : IK i j if (m m and M, m , t j= j), then M, m , t j= j. i j i j Proof. We will prove by induction, due to the length of the formula j. Suppose that m m . i j Axioms 2020, 9, 67 16 of 28 (j 2 AP) Let us ﬁrst consider the case when j is a sentence letter. By Deﬁnition 11 if m m , then for any t 2 T holds i j i V (t) V (t). (3) i j If M, m , t j= j, then from the Deﬁnition 12 j 2 V (t). (4) From (3) and (4) we receive j 2 V (t). (5) Because j is a sentence letter, so from (5) and the deﬁnition of 12 we have M, m , t j= j. Induction assumption: Let j, y be such that : (a) if M, m , t j= j, then M, m , t j= j, i j and (b) if M, m , t j= y, then M, m , t j= y. i j We will consider complex formulas built from the formulas j, y using sentence connectives and temporal operators. (:j) Let us assume that M, m , t j= :j. From the deﬁnition of the condition for negation (Deﬁnition 12) we have: for any m , such that m m : M, m , t 2 j. (6) k i k k Let us consider any state of knowledge m with a level of knowledge not lesser than the level of m , i.e., m m . (7) j l From (7), the assumption that m m and the transitivity of the, we have that m m . Therefore, i j i l from (6) we have: M, m , t 2 j. Because m is any state of knowledge whose level of knowledge is l l not lesser than the level of knowledge of m , we get: for any m such that m m we have: M, m , t 2 j. (8) l j l l From (8) and the condition for negation (Deﬁnition 12) we have: M, m , t j= :j. (j^ y) Let us assume that M, m , t j= j^ y. So from the condition for the conjunction (Deﬁnition 12) we have: M, m , t j= j, (9) and M, m , t j= y. (10) From (9) and point a) of the induction assumption we get: M, m , t j= j. (11) j Axioms 2020, 9, 67 17 of 28 Similarly, from (10) and point b) of the induction assumption we get: M, m , t j= y. (12) From (11), (12) and the condition for the conjunction (Deﬁnition 12) we get M, m , t j= j^ y. (j_ y) Reasoning analogous to conjunction. (j ! y) Let us assume that M, m , t j= j ! y. From the condition for the implication (Deﬁnition 12) we have: for any m (2 M) : (M, m , t 2 j or M, m , t j= y), (13) i i i Let us consider the state of knowledge m with a level of knowledge not lesser than the level of knowledge of m , i.e., m m . (14) j l From (14), the assumption that m m and the transitivity of the relationship we get that m m . i j i l From (13) we have: M, m , t 2 j or M, m , t j= y. Because m is any state of knowledge in which the l l l level of knowledge is not lesser than the level of knowledge in the state m , we get: for any m such that m m : M, m , t 2 j or M, m , t j= y. (15) l j l l l From (15) and the condition for the implications (Deﬁnition 12) we get M, m , t j= j ! y. (Gj) Suppose M, m , t j= Gj. From the condition for the G operator (Deﬁnition 12) we have: for any m (2 M), for any t (2 T ) such that tR t : M, m , t j= j, (16) 1 1 1 i i i i Let us consider any state of knowledge m witch a level of knowledge is not lesser than the level of knowledge of the state m , i.e., m m . (17) j l From (17), the assumption that m m and the transitivity of the relationship, we get that m m . i j i l Som from (16) we get : for any t (2 T ) such that tR t holds: M, m , t j= j. (18) 1 l l 1 l Because the state of knowledge m is a state of knowledge with a level of knowledge not lower than the level of knowledge in the state m we have: for any m , for any t (2 T ) if (m m and tR t ), then M, m , t j= j. (19) l 1 l j l l 1 l 1 From (19) and the condition for the G operator (Deﬁnition 12) we obtain: M, m , t j= Gj ( Hj) Reasoning similar to the G operator. (Fj) Let us assume that M, m , t j= Fj. From the condition for the operator F (Deﬁnition 12) there is the moment t (2 T ), tR t , such that: 1 i i 1 M, m , t j= j. (20) i 1 From (2) and point a) of the induction assumption we have: M, m , t j= j. (21) j 1 Axioms 2020, 9, 67 18 of 28 Assuming that m m and the deﬁnition of 11 we get that: i j t 2 T , t 2 T , tR t . (22) j 1 j j 1 From (21), (22) and the condition for the F operator (Deﬁnition 12) we obtain M, m , t j= Fj. (Pj) Reasoning similar to the F operator. We have therefore shown that what is true in a given state of knowledge m it is also true in any state of knowledge in which the level of knowledge is not lesser than the level of knowledge in the state m . 7. Simpliﬁed Axiomatics IK The axioms proposed by Ewald IK are dependent axioms. Some axioms can be derived from other axioms. Proofs of dependencies of selected axioms were provided by Surowik [6]. We offer a simpliﬁed set of axioms for IK : A1) j, if j is a tautology of the intuitionistic logic of the language L . IK (A2) G (j ! y) ! (Gj ! Gy) (A2’) H (j ! y) ! ( Hj ! Hy) (A3) F (j_ y) ! (Fj_ Fy) (A3’) P (j_ y) ! (Pj_ Py) (A4) G (j ! y) ! (Fj ! Fy) (A4’) H (j ! y) ! (Pj ! Py) (A5) Fj ! :G:j (A5’) Pj ! : H:j (A6) F Hj ! j (A6’) PGj ! j 9A7) j ! GPj (A7’) j ! H Fj (A8) (Fj ! Gy) ! G (j ! y) (A8’) (Pj ! Hy) ! H (j ! y) Rules: MP, RH, RG. We will prove that this axiomatics is equivalent to the axiomatics proposed by Ewald. To demonstrate the derivability of some IK axioms with the other axioms of this system, the following Theorems will be useful. Theorem 12. j ! y (a) The RRG rule : is a rule of IK . Gj ! Gy j ! y (b) The RR H rule : is a rule of IK . Hj ! Hy Proof. We will prove only (a). Proof (b) is analogous. (a) 1. ` j ! y assumption IK 2. ` G(j ! y) 1,RG IK 3. ` G(j ! y) ! (Gj ! Gy) A2 IK 4. ` Gj ! Gy 2,3,MP IK t Axioms 2020, 9, 67 19 of 28 Theorem 13. j ! y (a) The RF rule : is a rule of IK . Fj ! Fy j ! y (b) The RP rule : is a rule of IK . Pj ! Py The proof of this theorem is obtained in a manner analogous to the proof of the theorem of the previous one, with the difference that instead of the axiom A2 (A2 ’) we use the A4 (A4’) axiom. 0 0 0 0 We will show that in IK ’ “old” axioms 3, 3 , 6, 6 , 7, 7 , 11, 11 are inferable. The implications of the “old” 4 and 4 axioms are also inferable. Lemma 2. ` G (j^ y) $ (Gj^ Gy) IK Proof. (A) ` G (j^ y) ! (Gj^ Gy) IK 1. ` (j^ y) ! j A1 IK 2. ` (j^ y) ! y A1 IK 3. ` G(j^ y) ! Gj 1, RRG IK 4. ` G(j^ y) ! Gy 2,RRG IK 5. ` G (j^ y) ! Gj ! G (j^ y) ! Gy ! G (j^ y) ! (Gj^ Gy) A1 IK 6. ` G (j^ y) ! Gy ! G (j^ y) ! (Gj^ Gy) 3,5,MP IK 7. ` G(j^ y) ! (Gj^ Gy) 4,6,MP IK (B) ` (Gj^ Gy) ! G (j^ y) IK 1. ` j ! y ! (j^ y) A1 IK 2. ` Gj ! G y ! (j^ y) 1,RRG IK 3. ` G y ! (j^ y) ! Gy ! G(j^ y) A2 IK 4. ` Gj ! Gy ! G(j^ y) 2,3,SYLL IK 5. ` Gj ! Gy ! G(j^ y) ! (Gj^ Gy) ! G(j^ y) A1 IK 6. ` (Gj^ Gy) ! G(j^ y) 4,5,MP IK With (A) and (B) we get a thesis. The next lemma is proved similarly. Lemma 3. ` H (j^ y) $ ( Hj^ Hy) IK Lemma 4. ` (Fj_ Fy) ! F (j_ y) IK Proof. 1. ` j ! (j_ y) A1 IK 2. ` y ! (j_ y) A1 IK 3. ` Fj ! F (j_ y) 1,RF IK t Axioms 2020, 9, 67 20 of 28 4. ` Fy ! F (j_ y) 2,RF IK 5. ` Fj ! F (j_ y) ! Fy ! F (j_ y) ! (Fj_ Fy) ! F (j_ y) A1 IK 6. ` Fy ! F (j_ y) ! (Fj_ Fy) ! F (j_ y) 3,5,MP IK 7. ` (Fj_ Fy) ! F (j_ y) 4,6,MP IK Lemma 5. ` (Pj_ Py) ! P (j_ y) IK Proof analogous to the proof of the previous lemma. Lemma 6. ` (Gj^ Fy) ! F(j^ y) IK Proof. 1. ` j ! y ! (j^ y) A1 IK 2. ` Gj ! G y ! (j^ y) 1, RRG IK 3. ` G y ! (j^ y) ! Fy ! F (j^ y) A4 IK 4. ` Gj ! Fy ! F (j^ y) 2,3, SYLL IK 5. ` Gj ! Fy ! F (j^ y) ! (Gj^ Fy) ! F(j^ y) A1 IK 6. ` (Gj^ Fy) ! F(j^ y) 4,5, MP IK Lemma 7. ` ( Hj^ Py) ! P (j^ y) IK Proof analogous to the proof of the previous lemma. Lemma 8. ` G:j ! F:j IK Proof. 1. ` Fj ! :G:j A5 IK 2. ` (Fj ! :G:j) ! (G:j ! :Fj) A1 IK 3. ` (G:j ! :Fj) 1,2,MP IK Lemma 9. ` H:j ! :Pj IK Proof analogous to the proof of the previous lemma. Lemma 10. ` F (j ! y) ! (Gj ! Fy) IK Proof. 1. ` j ! (j ! y) ! y A1 IK 2. ` Gj ! G (j ! y) ! y 1,RRG IK 3. ` G (j ! y) ! y ! F (j ! y) ! Fy A4 IK 4. ` Gj ! F (j ! y) ! Fy 2,3, SYLL IK t Axioms 2020, 9, 67 21 of 28 5. ` Gj ! F (j ! y) ! Fy ! F (j ! y) ! Gj ! Fy A1 IK 6. ` F (j ! y) ! Gj ! Fy 4,5, MP IK Lemma 11. ` P (j ! y) ! ( Hj ! Py) IK Proof analogous to the proof of the previous lemma. 0 0 We will show that the ” new ” A5 and A5 axioms are we can derive from the’ ’old’ ’8 and 8 axioms. Lemma 12. G:j ! :Fj ` Fj ! :G:j I K Proof. 1. ` G:j ! :Fj assumption IK 2. ` (G:j ! :Fj) ! (Fj ! :G:j) axiom 1 IK 3. ` (Fj ! :G:j) 1,2,MP IK It is likewise proved that: Lemma 13. H:j ! :Pj ` Pj ! : H:j IK Thus, we have shown that the given axioms are equivalent. In further considerations we will use “new” axiomatics of IK . 8. The Adequacy of IK Relative to Modiﬁed Semantics The natural question is the question about the relationship between modiﬁed semantics and the assumed set of axioms for IK . Theorem 14. The IK axioms are true in any model, and the IK inference rules are infallible. t t 0 0 Proof. We will prove only A2 , A4 axioms and R H rule. Proofs for the other rules and axioms is carried out in analogous manner. A2’ For any M, m (2 M), and t(2 T ): M, m , t j= H (j ! y) ! ( Hj ! Hy) . i i i Suppose for some M, m (2 M) and t (2 T ) : M, m , t 2 H (j ! y) ! ( Hj ! Hy) . i i i Therefore, from the condition of the truth for the implications, there is a state of knowledge m , m m , such that: i j M, m , t j= H (j ! y) , (23) M, m , t 2 Hj ! Hy. (24) From (24) and the condition of the truth for the implications, in a certain state of knowledge m , with a level of knowledge not lesser than the level of knowledge of the state m , i.e., such that m m : j k M, m , t j= Hj, (25) M, m , t 2 Hy. (26) k Axioms 2020, 9, 67 22 of 28 From (25) and the condition of the truth for the H operator we get: for any state of knowledge m such that m m and l k l for any t 2 T such that t R t holds: M, m , t j= j. (27) 1 1 1 l l l From (26) and the condition of the truth for the H operator, there is a state m sucht that m m ) p p and there is a moment t 2 T such that t R t, in which: 2 p 2 p M, m , t 2 y. (28) Because m m and t R t therefore from (27) we have that at the moment t holds M, m , t j= j. p 2 p 2 p 2 Hence, from (28) and the condition of the truth of the implications we get: M, m , t 2 j ! y. (29) From (23) and the condition of the truth of the operator H we have: for any m such that m m and r j r for any t 2 T such that t R t holds : M, m , t j= j ! y. (30) r r r 3 3 3 Because: m m , m m , so from the transitivity of the relationship we get m m . j k k p j p The moment t is such that t R t. Therefore, from (30) we have: 2 2 p M, m , t j= j ! y. This is contrary to 29. A4’ For any M, m (2 M) and t (2 T ): M, m , t j= H (j ! y) ! (Pj ! Py) . i i i Suppose for some M, m (2 M) and t (2 T ) M, m , t 2 H (j ! y) ! (Pj ! Py) . i i i Thus, from the condition of the truth of the implications, in a certain state of knowledge m , such that m m we have: i j M, m , t j= H (j ! y) , (31) M, m , t 2 Pj ! Py. (32) From (32) and the condition of the truth of the implications, in some state of knowledge m , such that m m : j k M, m , t j= Pj, (33) and M, m , t 2 Py. (34) From (33) and the condition of the truth of the P operator we have: there exists t (2 T ) , t R t such that M, m , t j= j. (35) 1 k 1 k k 1 From (34) and the condition of the truth of the P operator we obtain: does not exist moment of time t (2 T ) , t R t, such that M, m , t j= y. (36) 2 k 2 k k 2 Axioms 2020, 9, 67 23 of 28 Let us consider the moment t satisfying (35). Because t R t, so from (36) we have: 1 1 k M, m , t 2 y. (37) k 1 If M, m , t j= y, it would be against (36). k 1 From (35), (37) and the condition of the truth of the implications, we get that M, m , t 2 j ! y. k 1 From (31) and condition the truth of the operator H we have: for any m such that m m and for any t (2 T ) such that t R t : M, m , t j= j ! y. (38) 3 3 3 l j l l l l Because m m , t R t and M, m , t 2 (j ! y) , so we get a contradiction with (38). j k 1 k k 1 RH If M j= j, then M j= Hj. Let us assume that M j= j. So for any m and for any t(2 T ) holds M, m , t j= j. So especially for i i i any t (2 T ) such that t R t : M, m , t j= j. So for any t(2 T ) holds M, m , t j= Hj. Because we 1 i 1 i i 1 i i were considering any m , therefore M j= Hj. Adequacy IK with respect to modiﬁed semantics was demonstrated by Surowik [4]. Theorem 15. S ` j iff S j= j. IK IK t t The proof of this theorem is similar to the proof of the adequacy theorem demonstrated by Ewald in [3]. 9. Mutual Undeﬁnability in IK Operators H, P and G, F We will now prove theorems that show some special properties of the IK system, essentially distinguishing this system from systems built on the basis of classical logic. For the formula to be the tautology of the IK system, it needs to be true at any time, in any state of knowledge. To show that a formula is not true, it is enough to indicate the state of knowledge and the moment in which this formula is not true. We will show that some relationships between the operators H and P and G and F holds in the system K but do not occur between the equivalents of these operators in the system IK . t t Theorem 16. (a) 2 :P: p ! H p, IK (b) 2 : H: p ! P p IK (c) 2 : H p ! P: p IK (d) 2 :F: p ! G p IK (e) 2 :G: p ! F p IK Proof. (a) Let T = ft , t g , R = f(t , t )g . Let I be a set of indexes. For any i: T = T, R = R. Let k, k > 1, 1 2 1 2 i i be a certain index of state of knowledge. Let F = fVg be a class of functions satisﬁed the i2 I following conditions: for any i such that i k holds p 2 / V (t ), (39) i 1 Axioms 2020, 9, 67 24 of 28 and for any i such that k < i holds p 2 V (t ). (40) i 1 The V valuations are therefore selected so that the sentence p is true at the time of t in the states of i 1 knowledge with index not greater than k and at the same time it was not true at the time of t in the states of knowledge with index greater than k. Let T = hT, Ri. Let M = fm : i 2 Ig . From the construction of the M model, we get that there are states of knowledge in the M which level of knowledge is not lesser than the level of knowledge of m in which at the moment t p is true and there are states of knowledge with a level of knowledge not lesser than the level of knowledge of m , in which at the moment t is not true that p. Therefore, it is not 1 1 true that in any state of knowledge m (2 M) holds M, m , t 2 p. Therefore, by Deﬁnition 12 we get 1 1 M, m , t 2 : p. From the construction of the M model we get that in any state of knowledge m (2 M) 1 1 holds M, m , t 2 : p. Because t R t , therefore, by the Deﬁnition 12 we have M, m , t 2 P: p. By the 2 2 1 1 1 1 1 Deﬁnition 12 we get M, m , t :P: p. (41) Because the moment t is such that t R t and M, m , t 2 p so by the Deﬁnition 12 1 1 1 2 1 1 M, m , t 2 H p. (42) From (41), (42) and the Deﬁnition 12: we have M, m , t 2 :P: p ! H p. Therefore 2 :P: p ! H p. 1 2 IK (b) The M model proposed in the proof of a) will be used to prove that : H: p ! P p is not a tautology of IK . Please note that from the construction of the model and by Deﬁnition 12 we have M, m , t 2 : p. Because in any state of knowledge m 2 M the only time before t is the time t , so by the ( ) 2 1 Deﬁnition 12 for any m holds M, m , t 2 H: p. Hence, by the Deﬁnition 12 1 1 M, m , t : H: p. (43) From the construction of the model M we have M, m , t 2 p. Because t R t , therefore by the 1 1 1 1 2 Deﬁnition 12 M, m , t 2 P p. (44) 1 2 From (43), (44) and the Deﬁnition of 12 we obtain: M, m , t 2 : H: p ! P p. Therefore 1 2 2 IK : H: p ! P p. (c) We will now show that : H p ! P: p is not a tautology of IK . Let T = ft , t g , R = f(t , t )g . t 1 1 2 1 2 1 Let the function V be such that p 62 V (t ) . States of knowledge in which the level of knowledge is 1 1 2 not lower than the level of m we construct as follows: T = T [ft g , (45) i+1 i i+2 R = R [f(t , t )g . (46) i+1 i i+2 1 V is such that for t 6= t : p 2 V (t) , and for t = t : p 2 / V (t) . (47) i+1 i+2 i+1 i+2 i+1 Axioms 2020, 9, 67 25 of 28 State of knowledge m is an ordered triple hT , R , V i. Let F = fVg will be a class of i+1 i+1 i+1 i+1 i i2 I S S functions satisfying the condition (47), T = h T , R i, M = fm : i 2 Ig , the states of knowledge i i i i2 I i2 I m are constructed in accordance with conditions (45), (46) and (47). From the construction of the M model we get that in every state of knowledge m (2 M), there is a moment t, earlier than t such that tR t in which such that M, m , t 2 p. So by the Deﬁnition 12 for any state of knowledge m we 1 1 1 have M, m , t 2 H p. From the deﬁnition of 12 we have that: M, m , t : H p. (48) From the construction of the model we have that if at some moment of time t, in any state of knowledge m (2 M) is that M, m , t 2 p, then in every state of knowledge m (2 M) holds M, m , t i i i i p. In the state of knowledge m 2 M the only time before t is the moment t . The moment t is ( ) 1 1 2 2 such that p 2 / V (t ) . In the classical model, this would sufﬁce to say that M, m , t : p. This is not 1 2 1 2 the case in the temporal logic model built upon intuitionistic logic. From the way of constructing states of knowledge with no lower level of knowledge than the level of knowledge in the state m we have p 2 V (t ) . Therefore, by the Deﬁnition 12 2 2 M, m , t 2 : p. (49) 1 2 By the Deﬁnition 12 we have M, m , t 2 : H p ! P: p. 1 1 We construct counter-examples for d), e) and f) in an analogous way. In the IK system, between the G and F and H and P operators there are no relationships usually found in temporal logic systems that are based on classical logic. However, the above conclusion is not sufﬁcient to state that the operators G and F as well as H and P are not mutually deﬁnable in IK . The conclusion is only that they do not occur between these operators deﬁnition relationships the same as those in classical tense logics. We will show that in intuitionistic temporal logic, temporal operators are not deﬁnable as they are in temporal logics based on classical propositional logic. We will show that intuitionistic temporal operators are not deﬁnable in any other way using sentence connectives and other intuitionistic temporal operators. To show that a temporal operator is not deﬁnable in the IK , two structures should be indicated such that the sentence with the considered operator at a moment t in one structure is true, and it is false in the other. On the other hand, all sentences in which the operator does not appear have the same logical value in both structures at the moment t. Theorem 17 ([4]). The intuitionistic temporal operators F and G as well as P and H are not each other deﬁnable in the IK . Proof. We will show ﬁrst that the operator F is not deﬁnable if we use of intuitionistic sentence connectives and other temporal operators. We will show that F p is not equivalent to any temporal formula in which the F operator does not occur. F: Let T = ft , t g, T = ft , t , t g, R = f(t , t )g, R = f(t , t ) , (t , t )g, T = T [ T . Let V : T ! 1 1 2 2 1 2 3 1 1 2 2 1 2 1 3 1 2 1 1 AP AP 2 be such that p 62 V (t ) while V : T ! 2 will be such a function that: V (t ) = V (t ), 1 2 2 2 2 1 1 1 V (t ) = V (t )[f pg, V (t ) = V (t ) . Let F =fV , V g , m = hT , R , V i, m = hT , R , V i, 2 2 1 2 2 3 1 2 1 2 1 1 1 1 2 2 2 2 M = fm , m g . 1 2 By means of structural induction, it can be shown that for any j without the F operator we have Axioms 2020, 9, 67 26 of 28 M, m , t j iff M, m , t j. (50) 1 1 2 1 At the same time, M, m , t F p and M, m , t 2 F p. Therefore, the F operator is not deﬁnable in IK . 2 1 1 1 t G: We will now show that the operator G is not deﬁnable if we use of intuitionistic sentence connectives and other temporal operators. We will show that G p is not equivalent to any temporal formula in which the G operator is not present. Let T = ft , t , t g, T = ft , t , t g , R = f(t , t )g, R = f(t , t ) , (t , t )g , T = T [ T . Let V : 1 1 2 3 2 1 2 3 1 1 2 2 1 2 1 3 1 2 1 AP AP T ! 2 will be such a function that p 62 V (t ) . Let V : T ! 2 will be such a function 2 2 2 1 1 that: V (t ) = V (t ) , V (t ) = V (t ) [ f pg , V (t ) = V (t ) , p 2 V (t ) . Let F =fV , V g . 2 1 1 1 2 2 1 2 2 3 1 3 1 3 1 2 Let m = hT , R , V i, m = hT , R , V i. Let M = fm , m g . By means of structural induction, it can 2 2 2 2 2 1 1 1 1 1 be shown that for any j sentence without the G operator we have: M, m , t j iff M, m , t j. (51) 1 1 2 1 At the same time, M, m , t G p and M, m , t 2 G p. So the G operator is not deﬁnable in IK . 2 1 1 1 t Similarly, we can to show that P and H are not each other deﬁnable in IK . It is not, however, that the operators G, F, H, P are completely independent of each other. Certain relationships between the operators H and P and G and F occur in IK . We will prove some of them: Theorem 18. (a) ` H:j ! :Pj, IK (b) ` Hj ! :P:j, IK (c) ` P:j ! : Hj, IK (d) ` G:j ! :Fj, IK (e) ` Gj ! :F:j, IK (f) ` F:j ! :Gj. IK Proof. (a) ` ( H:j ! :Pj) IK 1. ` (Pj ! : H:j) ! ( H:j ! :Pj) axiom 1, IK 2. ` H:j ! :Pj A5’,1,MP. IK (b) ` Hj ! :P:j IK 1. ` j ! ::j axiom 1, IK 2. ` H(j ! ::j) 1,RH, IK 3. ` H(j ! ::j) ! ( Hj ! H::j) A2’, IK 4. ` Hj ! H::j 2,3,MP, IK 5. ` H::j ! :P:j case (a), IK 6. ` Hj ! :P:j 4,5, SYLL. IK (c) ` (P:j ! : Hj) IK t Axioms 2020, 9, 67 27 of 28 1. ` ( Hj ! :P:j) ! (P:j ! : Hj) axiom 1, IK 2. ` P:j ! : Hj 1, case (b),MP. IK The proofs of the cases (d), (e) and (f) are similar, so we skip them. 10. Summary Temporal logic systems can be built in a variety of ways. They can be based on classical logic, but also, as we presented in this article, based on intuitionistic logic. The discussed systems are minimal systems, which means that no properties have been imposed on the time structure. One can, however, enrich these systems with additional speciﬁc axioms, build a temporal logic systems adequate to various time structures, e.g., reﬂexive, symmetrical, transitive, linear or branched. However, while in tense logic systems based on classical logic, the thesis of logical determinism can be rejected by modifying the structure of time and assuming, as a semantic time, a branching time into the future, in tense logics based on intuitionistic logic, modiﬁcation of the time structure is not necessary. Formulas expressing the thesis of logical determinism are not theses of the minimal system because of its basic properties, no matter what time structure is adopted as a semantic time. There is a relationship between the systems being discussed. Each thesis of the IK system is also the thesis of K , so: IK K . t t In addition, as we have shown in this article, intuitionistic temporal logic can be used to represent knowledge that changes over time. Intuitionistic logic and knowledge are closely related. This epistemic approach is the epicenter of Brouwer ’s intuitionistic explanation of truth as provability by an ideal mathematician, or more generally by an ideal cognitive subject. Kripke’s intuitionistic models are good tools for modelling the evolutionary learning process of the cognitive subject. The intuitionistic temporal logic IK has many advantages when we understand it as a formal tool for the logical representation of knowledge changing over time. Knowledge is implemented in this system on a semantic level in a natural way. In a natural way, by means of a set of partially ordered states of knowledge, the way of acquiring knowledge is also modeled. However, this system has some imperfections and limitations. The ﬁrst is the limited applicability of this system. Due to the adopted monotonicity of knowledge, i.e., a fact recognized in a given state of knowledge is known in all states of knowledge with a not lower level of knowledge, this system is a good tool for a modelling of mathematical or logical knowledge that changes over time. Conﬂicts of Interest: The authors declare no conﬂict of interest. References 1. Van Benthem, J.F.A.K. The Logic of Time: A Model-Theoretic Investigation into the Varietes of Temporal Ontology and Temporal Discourse, 2nd ed.; LII 874. Synthese library; Kluwer Academic Publishers: Dordrecht, The Netherlands; Boston, MA, USA; London, UK, 1991; Volume 156. 2. Van Benthem, J.F.A.K. Reﬂections on epistemic logic. Logique et Analyse 1991, 34, 5–14. 3. Ewald, W.B. Intuitionistic tense and modal logic. J. Symb. Log. 1986, 51, 166–179. [CrossRef] 4. Surowik, D. Intuitionistic Tense Logic and Indeterminism. Ph.D. Thesis, Lodz University, Łódz, ´ Poland, 2001. (In Polish) Axioms 2020, 9, 67 28 of 28 5. Trzesicki, ˛ K. Logic of Grammar Time Operators and the Problem of Determinism. Habilitation Thesis, University of Warsaw, Warsaw, Poland, 1986. (In Polish) 6. Surowik, D. Some thechnical results in a certain intuitionistic tense logic. In Topics in Logic Informatics and Philosophy of Science; University of Białystok: Białystok, Poland, 1999. 2020 by the authors. Licensee MDPI, Basel, Switzerland. This article is an open access article distributed under the terms and conditions of the Creative Commons Attribution (CC BY) license (http://creativecommons.org/licenses/by/4.0/).

Axioms – Multidisciplinary Digital Publishing Institute

**Published: ** Jun 16, 2020

Loading...

You can share this free article with as many people as you like with the url below! We hope you enjoy this feature!

Read and print from thousands of top scholarly journals.

System error. Please try again!

Already have an account? Log in

Bookmark this article. You can see your Bookmarks on your DeepDyve Library.

To save an article, **log in** first, or **sign up** for a DeepDyve account if you don’t already have one.

Copy and paste the desired citation format or use the link below to download a file formatted for EndNote

Access the full text.

Sign up today, get DeepDyve free for 14 days.

All DeepDyve websites use cookies to improve your online experience. They were placed on your computer when you launched this website. You can change your cookie settings through your browser.