On Contextual Programs Under Three-Valued Łukasiewicz Logic Islam Hamada∗ Technische Universität Dresden, 01062 Dresden, Germany Abstract Weak completion semantics is based on a cognitive theory that managed to model human reasoning in a variety of scenarios. It is based on a non-monotonic theory that uses normal logic programs under three-valued Łukasiewicz logic. We discuss contextual programs in this paper, in that it will be shown that the monotonicity of their semantic operators is generally undecidable. It will also be shown that the 昀椀xed point of the semantic operator of acyclic contextual programs is not only a model but a minimal model. Keywords human reasoning, weak completion semantics, Łukasiewicz logic, contextual programs, monotonicity, minimal model 1. Introduction The weak completion semantics (WCS) is a cognitive theory that models human reasoning using normal logic programs [1]. It is a non-monotonic theory that uses three-valued Łukasiewicz logic. It was 昀椀rst used to model the suppression task [1], then it has been further developed to model human choices in the selection task [2], syllogistic reasoning [3], and ethical decision problems [4]. The semantics can model di昀昀erent types of conditionals [5, 6, 7], as well as disjunctions [8]. It has an operational semantics given by the implementations in Prolog, Python and ASP. Finally the (least) model one reasons with respect to can be computed by a connectionist network [9]. Consider the following example If today is Sunday, Jack will rest the whole day. Today is Sunday. What do we conclude? The example will be modeled as a program following Stenning and van Lambalgen in [10]. The 昀椀rst statement is represented by {�㕟 ← �㕠 ∧ ¬�㕎�㕏�㕠 , �㕎�㕏�㕠 ← ⊥}, where �㕟 and �㕠 denote that Jack will rest the whole day and Today is Sunday, respectively, and �㕎�㕏�㕠 is an abnormality predicate which is assumed to be false represented by �㕎�㕏�㕠 ← ⊥. The second statement is represented by �㕠 ← ⊤, which means �㕠 should be mapped to true in the model. Consequently, �㕠 ∧ ¬�㕎�㕏�㕠 is mapped to true, therefore �㕟 is also mapped to true. So one reasons w.r.t. the model ⟨{�㕟, �㕠}, {�㕎�㕏�㕠 }⟩. The model speci昀椀es that �㕟 and �㕠 are mapped to true, whereas �㕎�㕏�㕠 is mapped to false, and there are no atoms 8th Workshop on Formal and Cognitive Reasoning, September 19, 2022, Trier, Germany ∗ Corresponding author. ɛ客 islamhamada222@gmail.com (I. Hamada) �ᘀ 0000-0002-6730-1743 (I. Hamada) © 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) 16 mapped to unknown because there are no other atoms le昀琀. Consequently one concludes that Jack will rest the whole day. Sometime ago an operator known as the context operator (ctxt) was added to WCS in [10]. Programs that use the context operator are called contextual programs. Contextual programs are useful in cases, where default reasoning is involved [11]. The context operator ctxt assumes an atom to be false when it is neither assigned true or false, which mimics negation as failure. For example we will extend the previous example into the following: If today is Sunday, Jack will rest the whole day, unless he knows an exam is coming. If the semester is ending soon, and exam is coming soon. Today is Sunday. What do we conclude? The 昀椀rst sentence is represented by {�㕟 ← �㕠 ∧ ¬�㕎�㕏�㕠 , �㕎�㕏�㕠 ← �㕐�㕡�㕥�㕡 �㕒}, where atom �㕒 denotes that an exam is coming, and the other atoms denote the same as before. The second sentence is represented by {�㕒 ← �㕑 ∧ ¬�㕎�㕏�㕑 , �㕎�㕏�㕑 ← ⊥}, where �㕑 denotes the semester is ending. The last sentence is represented by �㕠 ← ⊤. Note that �㕎�㕏�㕑 is mapped to false, while �㕑 is unknown, so �㕑 ∧ ¬�㕎�㕏�㕑 is unknown, hence �㕒 is unknown too. This means that �㕐�㕡�㕥�㕡 �㕒 is mapped to false, consequently �㕎�㕏�㕠 is mapped to false. This means that �㕠 ∧ ¬�㕎�㕏�㕠 is mapped to true, hence �㕟 is also mapped to false. The model we just built is ⟨{�㕠, �㕟}, {�㕎�㕏�㕑 , �㕎�㕏�㕠 }, from which we conclude that Jack will rest the whole day. Note that if we remove the context operator from the previous program, we will get the model ⟨{�㕠}, {�㕎�㕏�㕑 }⟩ instead, from which we conclude that it is unknown whether Jack will rest the whole day. This means that the operator ctxt preceding the atom �㕒 enables us to assume that There is no coming exam by default, since Jack lacks knowledge about whether an exam is coming, hence the utility of the context operator. Despite their utility, contextual programs gave rise to some questions because they do not share the same properties that non-contextual programs have. For example the models we computed in the two previous examples can be computed using a semantic operator in WCS. This semantic operator is always monotonic for non-contextual programs [12, 10]. Consequently, the semantic operator of a non-contextual program always has a (unique) least 昀椀xed point [12]. This 昀椀xed point was shown to be the least model of the weak completion of the program. Furthermore, reasoning in WCS is done w.r.t. this 昀椀xed point, i.e., w.r.t. the least model of the weak completion of programs. On the other hand, contextual programs o昀琀en do not have monotonic semantic operators, hence they sometimes do not have any 昀椀xed points. This explains our interest in deciding whether a given (contextual) program has a monotonic semantic operator because if a (contextual) program has a monotonic semantic operator, then its semantic operator indeed has a unique 昀椀xed by the Knaster-Tarski Fixed Point Theorem [12]. This will be later shown to be an undecidable problem. Finally, we consider a certain subclass of contextual programs, the class of acyclic contextual programs. This is because the semantic operator of an acyclic contextual program always has a unique 昀椀xed point [11, 13], this 昀椀xed point was shown to be a model of the weak completion of the program, and was conjectured to be a minimal model. In the weak completion semantics minimal models are preferred because a minimal model does not assign true or false to any atoms unnecessarily, i.e., a minimal model is minimal in information (knowledge) ordering. For example in the reasoning scenario above there is nothing about the premises that suggests whether an exam is coming, so one should expect the model that we reason with respect to to map �㕒 to U, which was the case. It will be shown that the 昀椀xed point of the semantic operator of an acyclic contextual contextual is indeed a minimal model. 17 F ¬F ∧ ⊤ U ⊥ ∨ ⊤ U ⊥ ← ⊤ U ⊥ ↔ ⊤ U ⊥ �㕒 �㕐�㕡�㕥�㕡 �㕒 ⊤ ⊥ ⊤ ⊤ U ⊥ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ U ⊥ ⊤ ⊤ ⊥ ⊤ U U U ⊥ U ⊤ U U U U ⊤ ⊤ U U ⊤ U ⊥ ⊥ U U ⊥ ⊥ ⊥ ⊥ ⊥ ⊤ U ⊥ ⊥ ⊥ U ⊤ ⊥ ⊥ U ⊤ U ⊥ Table 1 The truth tables of the connectives ¬, ∧, ∨, ← and ↔ in three-valued Łukasiewicz logic [15], plus the truth table of the operator �㕐�㕡�㕥�㕡. Note that �㔹 denotes a formula, while �㔿 denotes a non-contextual literal. Cells where one of the operands is mapped to U are in gray. 2. The Weak Completion Semantics We assume the reader to be familiar with classical logic [14]. Let ⊤, ⊥ and U be truth constants denoting true, false, unknown, respectively. A non-contextual literal is an atom or its negation. A contextual literal has the form ctxt �㔴 or ¬ctxt �㔴 where �㔴 is a non-contextual literal. A (logic) program is a 昀椀nite set of clauses of the form �㔵 ← Body, where �㔵 is an atom and Body is either ⊤, ⊥, or a 昀椀nite non-empty conjunction of literals. Clauses of the form �㔵 ← ⊤, �㔵 ← ⊥ and �㔵 ← �㔿1 ∧ … ∧ �㔿�㕛 are called facts, assumptions and rules, respectively, where �㔿�㕖 , 1 ≤ �㕖 ≤ �㕛, are literals. In this paper, �㖫 denotes a program. Program �㖫 is contextual if it has at least one occurrence of a contextual literal, otherwise it is a non-contextual program. An atom �㔵 is de昀椀ned if and only if �㖫 contains a clause of the form �㔵 ← Body. The truth tables needed throughout the paper are shown in Table 1. Consider the following transformation: (1) For all de昀椀ned atoms �㔵 occurring in �㖫 , replace all clauses of the form �㔵 ← �㔵�㕜�㕑�㕦1 , �㔵 ← Body1 ∨ Body2 ∨ … (2) Replace all occurrences of ← by ↔. The resulting set of equivalences is called the weak completion of �㖫 : for short, �㕤�㕐�㖫 . It di昀昀ers from the completion de昀椀ned by [16] in that unde昀椀ned atoms are not mapped to false, but to unknown instead. As shown by Hölldobler and Kencana Ramli [12], each weakly completed non- contextual program admits a least model under three-valued Łukasiewicz [12]. This model is denoted by ℳ�㕤�㕐�㖫 . It can be computed as the least 昀椀xed point of a semantic operator introduced by Stenning and van Lambalgen [10]. Let �㖫 be a program and �㔼 a three-valued interpretation represented by the pair ⟨�㔼 ⊤ , �㔼 ⊥ ⟩, where �㔼 ⊤ and �㔼 ⊥ are the sets of atoms mapped to true and false by �㔼, respectively, and atoms which are not listed are mapped to unknown by �㔼. An interpretation �㔼 = ⟨�㔼 ⊤ , �㔼 ⊥ ⟩ is subsumed by interpretation �㔼 ′ = ⟨�㔼 ′⊤ , �㔼 ′⊥ ⟩, i.e., �㔼 ⊆ �㔼 ′ , i昀昀 �㔼 ⊤ ⊆ �㔼 ′⊤ and �㔼 ⊥ ⊆ �㔼 ′⊥ . De昀椀nition 1. For a program �㖫 and an interpretation �㔼, Φ�㖫 �㔼 = ⟨�㔽 ⊤ , �㔽 ⊥ ⟩1 , where �㔽 ⊤ = {�㔴 | there exists �㔴 ← �㔵�㕜�㕑�㕦 ∈ �㕔(�㖫 ) �㕎�㕛�㕑 �㔼 (�㔵�㕜�㕑�㕦) = ⊤}, �㔽 ⊥ = {�㔴 | there exists �㔴 ← �㔵�㕜�㕑�㕦 ∈ �㕔(�㖫 ) and for all �㔴 ← �㔵�㕜�㕑�㕦 ∈ �㕔(�㖫 ), we 昀椀nd �㔼 (�㔵�㕜�㕑�㕦) = ⊥}. where �㕔(�㖫 ) denote the grounding of program �㖫 . Note that �㕔(�㖫 ) was used in the above de昀椀nition instead of �㖫 , in case �㖫 is 昀椀rst-order. Note also that �㕔(�㔹 ) denotes the set of ground instances of formula �㔹, and that for a program �㖫 , 1 Whenever we apply a unary operator like Φ�㖫 to an argument like �㔼, we omit parenthesis and write Φ�㖫 �㔼 instead. 18 �㕔(�㖫 ) denotes the program containing all the ground instances of each clause occurring in �㖫 . the semantic operator of non-contextual programs was shown to be monotonic, i.e., let �㔼 and �㔼 ′ be two interpretations, if �㔼 ⊆ �㔼 ′ , then Φ�㖫 �㔼 ⊆ Φ�㖫 �㔼 ′ , hence the existence of a least 昀椀xed point of the semantic operator for non-contextual programs. However, the semantic operator is o昀琀en not monotonic for contextual programs, and sometimes does not have any 昀椀xed points. Nevertheless, we are still interested in the unique 昀椀xed points of their semantic operators, if they exist. The class of acyclic contextual programs is a subclass of programs where a unique 昀椀xed point of the semantic operator always exists. A program �㖫 is acyclic i昀昀 �㖫 is acyclic w.r.t. some level mapping. A level mapping �㕙�㕣�㕙 is a mapping from the set of ground atoms to the set ℕ of natural numbers. For our purpose we extend the level mapping �㕙�㕣�㕙 by �㕙�㕣�㕙 ¬�㔴 = �㕙�㕣�㕙 �㔴 = �㕙�㕣�㕙 �㕐�㕡�㕥�㕡 �㔴 = �㕙�㕣�㕙 �㕐�㕡�㕥�㕡¬�㔴 = �㕙�㕣�㕙 ¬�㕐�㕡�㕥�㕡 �㔴 = �㕙�㕣�㕙¬�㕐�㕡�㕥�㕡¬�㔴. �㖫 is acyclic w.r.t. lvl if and only if for every rule �㔴 ← �㔿1 ∧ … ∧ �㔿�㕛 occurring in �㕔(�㖫 ), we 昀椀nd �㕙�㕣�㕙 �㔴 ≥ �㕙�㕣�㕙 �㔿�㕖 for all 1 ≤ �㕖 ≤ �㕛. Note that lfp(Φ�㖫 ) denotes the least 昀椀xed point of the semantic operator Φ�㖫 , and it is usually used in the context of acyclic contextual programs. 3. Fixed Points Are Minimal Models The semantic operator of acyclic programs (contextual or non-contextual) is a contraction by the Banach Contraction Mapping Theorem [13]. Consequently, it has a unique 昀椀xed point that can be reached by iterating the semantic operator starting with any interpretation. This 昀椀xed point has been shown to be a model of the weak completion of contextual programs [11]. We will also show that it is a minimal model in this section. 3.1. Alternative Definition of The Semantic Operator De昀椀nition 1 happens to be equivalent to the following: De昀椀nition 2. For any program �㖫 , an interpretation �㔼, and a ground atom �㔴 �㔼 (�㔷) if �㔴 is de昀椀ned in �㖫 and �㔴 ↔ �㔷 ∈ wc(�㕔(�㖫 )), Φ�㖫 �㔼 (�㔴) = { U if �㔴 is unde昀椀ned in �㕔(�㖫 ). Which means that a昀琀er an iteration of the semantic operator the mapping of a de昀椀ned atom �㔴 is the same as the mapping of the right-hand side of the equivalence in �㕤�㕐(�㕔(�㖫 )), which �㔴 happens to be its le昀琀-hand side. If �㔴 is unde昀椀ned, then it is mapped to U. The equivalence of De昀椀nition 1 and De昀椀nition 2 can be veri昀椀ed by a direct comparison of both de昀椀nitions. 3.2. The Least Fixed Point lfp(Φ�㖫 ) Is a Minimal Model The least 昀椀xed point lfp(Φ�㖫 ) of an acyclic contextual program �㖫 can be reached by iterating the semantic operator starting with any interpretation. Consider the following program �㖫 = {�㕎 ← �㕏 ∧ �㕐, �㕏 ← ⊤, �㕐 ← ⊥, �㕑 ← �㕒}. Iterating the semantic operator starting with the empty interpretation �㔼 = ⟨∅, ∅⟩ leads to the 昀椀xed point through the following sequence: �㔼 = ⟨∅, ∅⟩ → Φ�㖫 �㔼 = ⟨{�㕏}, {�㕐}⟩ → Φ2�㖫 �㔼 = ⟨{�㕏}, {�㕐, �㕎}⟩ → Φ3�㖫 �㔼 = Φ2�㖫 �㔼. Note that Φ�㖫 �㔼 maps �㕏 to ⊤ by the second clause and maps �㕐 to ⊥ by the third clause. Consequently in the next iteration Φ2�㖫 maps �㕎 to 19 ⊥ by the 昀椀rst clause because �㕏 ∧ �㕐 is mapped to ⊥. Note that Φ�㖫 �㔼 maps �㕎 to U by the 昀椀rst and due to the fact that �㕏 ∧ �㕐 was still mapped to U by �㔼. Another observation is that through the sequence of interpretations once an atom got mapped to ⊤ or ⊥, this mapping does not change in the following iteration. This happens because when an atom gets mapped to ⊤ or ⊥, this is a necessary consequence of the program itself. To elaborate �㕏 is mapped to ⊥ because of the second clause, �㕐 is mapped to ⊤ because of the third clause, 昀椀nally �㕎 is mapped to ⊥ by the 昀椀rst clause and due to the propagation of the necessary mappings of �㕎 and �㕏 through the iteration process. All the mappings to ⊥ or ⊤ were necessary due to the program itself. This (least) 昀椀xed point is minimal w.r.t. the mappings of atoms to ⊥ or ⊤, i.e., the 昀椀xed point has to be a minimal model of the weak completion of the program as we will see later. Proposition 1. Let �㖫 be a contextual program such that Φ�㖫 has a unique 昀椀xed point �㕀. If �㕀 ′ is a model for �㕤�㕐�㖫 and �㕀 ′ ≠ �㕀, then �㕀 ′ must map an unde昀椀ned atom to true or false. Proof. Let �㖫 be a contextual program, �㕀 the unique 昀椀xed point of Φ�㖫 , and �㕀 ′ be a model for �㕤�㕐�㖫 such that �㕀 ′ ≠ �㕀. Because �㕀 ′ is a model for �㕤�㕐�㖫 , it must map each equivalence �㔴 ↔ �㔹 occurring in �㕤�㕐�㖫 to true. The latter holds if and only if �㕀 ′ (�㔴) = �㕀 ′ (�㔹 ) for each equivalence �㔴 ↔ �㔹 occurring in �㕤�㕐�㖫 . Because �㕀 ′ ≠ �㕀 and �㕀 is the unique 昀椀xed point of Φ�㖫 , we 昀椀nd a ground atom �㔵 such that �㕀 ′ (�㔵) ≠ Φ�㖫 �㕀 ′ (�㔵). Assume that �㔵 is de昀椀ned. In this case we 昀椀nd �㔵 ↔ �㔹 ∈ �㕤�㕐�㖫 . Because �㕀 ′ is a model for �㕤�㕐�㖫 , we 昀椀nd �㕀 ′ (�㔵) = �㕀 ′ (�㔹 ). But �㕀 ′ (�㔹 ) = Φ�㖫 �㕀 ′ (�㔵) by De昀椀nition 2 and, thus, �㕀 ′ (�㔵) = Φ�㖫 �㕀 ′ (�㔵). Consequently, our assumption is wrong and we conclude that �㔵 must be unde昀椀ned. In this case, by de昀椀nition, Φ�㖫 �㕀 ′ (�㔵) = U. Consequently, �㕀 ′ (�㔵) must be either true or false. Consider the following contextual program: �㖫 = {�㕎 ← ¬�㕏 ∧ �㕐�㕡�㕥�㕡 �㕐, �㕎 ← ⊥, �㕏 ← ⊥}. Program �㖫 is acyclic because it acyclic w.r.t. the following level mapping �㕙�㕣�㕙 ∶ �㕙�㕣�㕙 �㕎 = 1, �㕙�㕣�㕙 �㕏 = 0, �㕙�㕣�㕙 �㕐 = 0. Therefore Φ�㖫 has a unique 昀椀xed point, namely lfp(Φ�㖫 ) = ⟨∅, {�㕎, �㕏}⟩, which is a model of the weak completion �㕤�㕐�㖫 . There are two other models, namely �㕀1 = ⟨∅, {�㕎, �㕏, �㕐}⟩ and �㕀2 = ⟨{�㕎, �㕐}, {�㕏}⟩. Model �㕀1 maps the unde昀椀ned atom �㕐 to ⊥, and model �㕀2 maps the unde昀椀ned atom �㕐 to ⊤. Now we can proceed to prove the main theorem. Theorem 1. Let �㖫 be a contextual program. If �㖫 is acyclic, then the unique 昀椀xed point of Φ�㖫 is a minimal model of �㕤�㕐�㖫 . Proof. Let �㖫 be an acyclic contextual program. The semantic operator Φ�㖫 has a unique 昀椀xed point. Let �㕀 be this 昀椀xed point. Assume that �㕀 is not a minimal model for �㕤�㕐�㖫 . Then, we 昀椀nd a model �㕀 ′ for �㕤�㕐�㖫 such that �㕀 ′ ⊆ �㕀. By Proposition 1, we 昀椀nd an atom �㔵 such that �㔵 is unde昀椀ned in �㖫 and �㕀 ′ maps �㔵 to either true or false. Because �㕀 ′ ⊆ �㕀, �㕀 must map �㔵 to either true or false, too. However, because �㔵 is unde昀椀ned in �㖫 , Φ�㖫 �㕀 will map �㔵 to U, in which case Φ�㖫 �㕀 ≠ �㕀. In other words, �㕀 is not a 昀椀xed point anymore and, thus, our assumption is false. Consequently, �㕀 is a minimal model for �㕤�㕐�㖫 . 4. Undecidability of The Monotonicity Problem The monotonicity problem refers to the question whether a given contextual program has a monotonic semantic operator. It is an important property because whenever the semantic 20 operator is monotonic, the Knaster-Tarski Fixed Point Theorem guarantees the existence of a least 昀椀xed point of the semantic operator [12]. This problem will be shown to be undecidable by a reduction from the Post correspondence problem. 4.1. The Monotonicity Problem The monotonicity problem is to decide for a given contextual program whether it has a monotonic semantic operator. Some contextual programs have monotonic semantic operators, while some others have non-monotonic semantic operators. Consider the following contextual program �㖫 1 = {�㕎 ← �㕐, �㕎 ← �㕐�㕡�㕥�㕡 �㕏}. Program �㖫 1 has a non-monotonic semantic operator because we can 昀椀nd the two interpretations �㔼 = ⟨∅, {�㕐}⟩ and �㔼 ′ = ⟨{�㕏}, {�㕐}⟩ such that �㔼 ⊆ �㔼 ′ and Φ�㖫 1 �㔼 = ⟨∅, {�㕎}⟩ ⊈ Φ�㖫 1 �㔼 ′ = ⟨{�㕎}, ∅⟩. On the other hand the following contextual program �㖫 2 = {�㕎 ← ⊤, �㕎 ← �㕐�㕡�㕥�㕡 �㕏} has a monotonic semantic operator because we cannot 昀椀nd any two interpretations �㔼 and �㔼 ′ where �㔼 ⊆ �㔼 ′ and Φ�㖫 2 �㔼 ⊈ Φ�㖫 2 �㔼 ′ . Similarly the following program �㖫 3 = {�㕎 ← ¬�㕐, �㕎 ← �㕐, �㕎 ← �㕐�㕡�㕥�㕡 �㕏} has a monotonic semantic operator too. Is the monotonicity problem decidable? The monotonicity problem is easily decidable for any propositional program because we can verify for a given program �㖫 whether all pairs of interpretations �㔼 and �㔼 ′ satisfy the following statement: if �㔼 ⊆ �㔼 ′ , then Φ�㖫 �㔼 ⊆ Φ�㖫 �㔼 ′ . This constitutes a sound, complete and terminating procedure for the monotonicity problem because there is a 昀椀nite number of interpretations that can be de昀椀ned over the alphabet of a propositional program. However, this is not the case for 昀椀rst-order programs with in昀椀nite Herbrand Base because the previous procedure is not terminating due to the possibly in昀椀nite number of interpretations. It will shown that the monotonicity problem is undecidable by showing that it is undecidable for a subclass of contextual programs, named class �㖱. 4.2. Class �㖱 of Programs A program belonging to class �㖱 has the following form {�㕟 ← �㕏�㕜�㕑�㕦1 , �㕟 ← �㕏�㕜�㕑�㕦2 , … , �㕟 ← �㕏�㕜�㕑�㕦�㕛 , �㕟 ← �㕐�㕡�㕥�㕡 �㕞}, where �㕟 and �㕞 are nullary predicate symbols and �㕏�㕜�㕑�㕦�㕖 is a non-contextual conjunction of literals such that �㕟 and �㕞 do not occur in �㕏�㕜�㕑�㕦�㕖 for all 1 ≤ �㕖 ≤ �㕛, and �㕛 ∈ ℤ+ . Note the three contextual program �㖫 1 , �㖫 2 and �㖫 3 that we used in the previous subsection belong to class �㖱. Note also that every program of class �㖱 has clauses that share the same head. We are interested in class �㖱 because a program �㖫 of class �㖱 is non-monotonic i昀昀 �㖫 is equivalent to �㖫 ′ ∪ �㖫 �㕣 , where �㖫 �㕣 belongs to class �㖱, and �㖫 ′ shares no de昀椀ned atoms with �㖫 �㕣 , in case �㖫 ′ is not empty, and most importantly �㖫 �㕣 has a non-monotonic semantic operator too. For example program �㖫 = {�㕎 ← �㕐, �㕎 ← �㕐�㕡�㕥�㕡 �㕏, �㕏 ← ¬�㕐 ∧ �㕐�㕡�㕥�㕡 �㕎, �㕐 ← ⊤} has a non-monotonic semantic operator Φ�㖫 because �㖫 = �㖫 ′ ∪ �㖫 �㕣 , where �㖫 ′ = {�㕏 ← ¬�㕐 ∧ �㕐�㕡�㕥�㕡 �㕎, �㕐 ← ⊤} and �㖫 �㕣 = {�㕎 ← �㕐, �㕎 ← �㕐�㕡�㕥�㕡 �㕏}, and �㖫 �㕣 belongs to class �㖱, shares no de昀椀ned atoms with �㖫 ′ , and program �㖫 �㕣 can be shown to have a non-monotonic semantic operator using the pair of interpretations �㔼 = ⟨∅, {�㕐}⟩ and �㔼 ′ = ⟨{�㕏}, {�㕐}⟩, because �㔼 ⊆ �㔼 ′ but Φ�㖫 �㕣 �㔼 ⊈ Φ�㖫 �㕣 �㔼 ′ . Note that this same pair of interpretations can be used to show that Φ�㖫 is non-monotonic. 21 4.3. The Post Correspondence Problem (PCP) The Post correspondence problem is a well-known undecidable problem. The PCP problem well be introduced next using the notation in [17]. An instance �㔾 of the PCP can be de昀椀ned as a 昀椀nite sequence �㔾 = (�㗼1 , �㗽1 ), … , (�㗼�㕛 , �㗽�㕛 ) of pairs (�㗼�㕖 , �㗽�㕖 ) were �㗼�㕖′ �㕠 and �㗽�㕖′ �㕠 are nonempty 昀椀nite words over {0, 1}. The question is whether where exists a nonempty sequence �㕖1 , �㕖2 , … , �㕖�㕘 of indices �㕖1 , … , �㕖�㕘 ∈ {1, … , �㕛} such that �㗼�㕖1 ⋅ �㗼�㕖2 ⋅ … ⋅ �㗼�㕖�㕘 = �㗽�㕖1 ⋅ �㗽�㕖2 ⋅ … ⋅ �㗽�㕖�㕘 , where ⋅ is a binary concatenation operator. It has been established that a PCP instance K has a solution i昀昀 the formula �㔺�㔾 is valid in classical two-valued logic as shown in [18]. The formula �㔺�㔾 = (�㔹1 �㔾 ∧ �㔹2 �㔾 ) → �㔻�㔾 , such that �㕛 �㕛 �㔹1 �㔾 = ⋀ �㕝(�㕓�㗼�㕖 (�㕐), �㕓�㗽�㕖 (�㕐)), �㔹2 �㔾 = (∀�㕋 , �㕌 )(�㕝(�㕋 , �㕌 ) → ⋀ �㕝(�㕓�㗼�㕖 (�㕋 ), �㕓�㗽�㕖 (�㕌 ))), �㔻�㔾 = (∃�㕍 )�㕝(�㕍 , �㕍 ). �㕖=1 �㕖=1 The formula �㔺�㔾 will be used later in the form derived below. �㕛 ¬�㔹1�㔾 ≡2 ⋁ ¬�㕝(�㕓�㗼�㕖 (�㕐), �㕓�㗽�㕖 (�㕐)) �㔺�㔾 = (�㔹1�㔾 ∧ �㔹2�㔾 ) → �㔻�㔾 �㕖=1 �㕛 ≡2 ¬�㔹1�㔾 ∨ ¬�㔹2�㔾 ∨ �㔻�㔾 ¬�㔹2�㔾 ≡2 ¬(∀�㕋 , �㕌 )(¬�㕝(�㕋 , �㕌 ) ∨ ⋀ �㕝(�㕓�㗼�㕖 (�㕋 ), �㕓�㗽�㕖 (�㕌 ))) �㕛 �㕖=1 ≡2 ⋁ ¬�㕝(�㕓�㗼�㕖 (�㕐), �㕓�㗽�㕖 (�㕐)) �㕛 �㕖=1 ≡2 (∃�㕋 , �㕌 )(�㕝(�㕋 , �㕌 ) ∧ (⋁ ¬�㕝(�㕓�㗼�㕖 (�㕋 ), �㕓�㗽�㕖 (�㕌 )))) �㕛 �㕖=1 ∨ ⋁(∃�㕋 , �㕌 )(�㕝(�㕋 , �㕌 ) ∧ ¬�㕝(�㕓�㗼�㕖 (�㕋 ), �㕓�㗽�㕖 (�㕌 ))) �㕛 �㕖=1 ≡2 ⋁(∃�㕋 , �㕌 )(�㕝(�㕋 , �㕌 ) ∧ ¬�㕝(�㕓�㗼�㕖 (�㕋 ), �㕓�㗽�㕖 (�㕌 ))) ∨ (∃�㕍 )�㕝(�㕍 , �㕍 ) �㕖=1 We use ≡2 to denote equivalence in classical two-valued logic. Note that �㔺�㔾 uses a constant symbol �㕐, two unary function symbols �㕓0 and �㕓1 , a binary predicate symbol �㕝. For simplicity we use the following abbreviation: �㕓�㔎1 …�㔎�㕚 (�㕋 ) ∶= �㕓�㔎�㕚 (… (�㕓�㔎1 (�㕋 )) …), where �㔎�㕖 ∈ {0, 1} for all 1 ≤ �㕖 ≤ �㕚. Note �㕐 denotes �㔖, the empty word, �㕓0 denotes the function ”concatenate 0 to the right”, and �㕓1 denotes the function ”concatenate 1 to the right”. Thereby �㕓�㗼�㕖 (�㕋 ) concatenates to the right of word �㕋. For example �㕓01 (00) = �㕓0 (�㕓1 (00)) = �㕓0 (001) = 0010. We will show that a PCP instance K has a solution i昀昀 �㔺�㔾 is valid in classical two-valued logic i昀昀 a program �㖫 �㔾 has a monotonic semantic operator. How does the monotonicity of the semantic operator have anything to do with validity in classical two-valued logic? 4.4. Monotonicity and Validity in Classical Two-valued Logic To see the connection between the monotonicity problem and validity in classical two-valued logic, let us have another look at the examples we discussed in this section: �㖫 1 = {�㕎 ← �㕐, �㕎 ← �㕐�㕡�㕥�㕡 �㕏}, �㖫 2 = {�㕎 ← ⊤, �㕎 ← �㕐�㕡�㕥�㕡 �㕏}, and �㖫 3 = {�㕎 ← ¬�㕐, �㕎 ← �㕐, �㕎 ← �㕐�㕡�㕥�㕡 �㕏}. Program �㖫 1 was shown to have a non-monotonic semantic operator, while program �㖫 2 and �㖫 3 were shown to have monotonic semantic operators. All of those programs share common features such as belonging to class �㖱 and containing the clause �㕎 ← �㕐�㕡�㕥�㕡 �㕏. So the di昀昀erence has to arise from the bodies of the rest of the clauses. Note that the disjunction of the bodies of the rest of the clauses are the following: (1) �㕐, (2) ⊤, and (3) ¬�㕐 ∨ �㕐. (1) is not valid in classical two-valued logic, whereas (2), (3) are valid in classical two-valued logic. This is not a coincidence, and it will be formally proved to be the reason why Φ�㖫 1 is non-monotonic, whereas Φ�㖫 2 and Φ�㖫 3 are monotonic. 22 To that end, one needs to show the link between validity in three-valued Łukasiewicz logic and classical two-valued logic. Before we proceed to do so, a few propositions on the relation between interpretations that are subsumed by each other will be presented next. 4.5. Subsumed Interpretations The relations between subsumed interpretations will be shown in this section in four statements, each consisting of two parts. In these statements we assume that �㔼1 and �㔼2 are interpretations and �㔼1 ⊆ �㔼2 . Note that a formula is non-contextual, when no contextual literal occurs in it. Now we proceed to prove the four statements. Observation 1. For a ground atom �㔴(1) If �㔼1 (�㔴) = ⊤, then �㔼2 (�㔴) = ⊤, (2) If �㔼1 (�㔴) = ⊥, then �㔼2 (�㔴) = ⊥. Proof. Let �㔼1 = ⟨�㔼1⊤ , �㔼1⊥ ⟩ and �㔼2 = ⟨�㔼2⊤ , �㔼2⊥ ⟩. Because �㔼1 ⊆ �㔼2 , �㔼1⊤ ⊆ �㔼2⊤ and �㔼1⊥ ⊆ �㔼2⊥ . If �㔼 (�㔴) = ⊤, then �㔴 ∈ �㔼1⊤ , consequently �㔴 ∈ �㔼2⊤ . So �㔼2 (�㔴) = ⊤. The second part can be proved similarly. Proposition 2. For a non-contextual literal �㔿 (1) If �㔼1 (�㔿) = ⊤, then �㔼2 (�㔿) = ⊤, (2) If �㔼1 (�㔿) = ⊥, then �㔼2 (�㔿) = ⊥. Proof. If �㔿 = �㔴, where �㔴 is an atom, then the proposition follows by Observation 1. If �㔿 = ¬�㔴, where �㔴 is an atom, then �㔼1 (�㔿) = �㔼1 (¬�㔴). If �㔼1 (¬�㔴) = ⊤, then �㔼1 (�㔴) = ⊥. By Observation 1, �㔼2 (�㔴) = ⊥. Consequently �㔼2 (¬�㔴) = ⊤. The second part can be proved in a similar fashion. Proposition 3. For a non-contextual conjunction of literals �㔶 (1) If �㔼1 (�㔶) = ⊤, then �㔼2 (�㔶) = ⊤, (2) If �㔼1 (�㔶) = ⊥, then �㔼2 (�㔶) = ⊥. Proof. If �㔶 is the empty conjunction, �㔶 denotes ⊤. Consequently �㔼1 (�㔶) = �㔼2 (�㔶) = ⊤, which satis昀椀es the proposition trivially. Otherwise �㔶 is a non-empty conjunction of literals, �㔶 = �㔿1 ∧ … ∧ �㔿�㕛 , where �㔿�㕖 is a non-contextual literal for all �㕖 where 1 ≤ �㕖 ≤ �㕛. Then we will prove each claim separately. (1) Assume �㔼1 (�㔶) = ⊤. Then �㔼1 (�㔿1 ∧ … ∧ �㔿�㕛 ) = ⊤. So for all �㕖 where 1 ≤ �㕖 ≤ �㕛, �㔼1 (�㔿�㕖 ) = ⊤. By Proposition 2, �㔼2 (�㔿�㕖 ) = ⊤ for all �㕖 where 1 ≤ �㕖 ≤ �㕛. So �㔼2 (�㔿1 ∧ … ∧ �㔿�㕛 ) = ⊤, and �㔼2 (�㔶) = ⊤. (2) Assume �㔼1 (�㔶) = ⊥. Then �㔼2 (�㔿1 ∧ … ∧ �㔿�㕛 ) = ⊥. So for some �㕖 where 1 ≤ �㕖 ≤ �㕛, �㔼2 (�㔿�㕖 ) = ⊥. By Proposition 2, �㔼2 (�㔿�㕖 ) = ⊥. Consequently �㔼2 (�㔿1 ∧ … ∧ �㔿�㕛 ) = ⊥, and �㔼2 (�㔶) = ⊥. Proposition 4. For a non-contextual disjunction of conjunctions of literals �㔷 (1) If �㔼1 (�㔷) = ⊤, then �㔼2 (�㔷) = ⊤, (2) If �㔼1 (�㔷) = ⊥, then �㔼2 (�㔷) = ⊥. Proof. If �㔷 is the empty disjunction, then �㔷 denotes ⊥. Consequently, �㔼1 (�㔷) = �㔼2 (�㔷) = ⊥, which satis昀椀es the proposition trivially. Since �㔷 is a non-contextual disjunction of conjunctions of literals, �㔷 = �㔶1 ∨ … ∨ �㔶�㕛 , where �㔶�㕖 is a non-contextual conjunction of literals. Then we will prove each claim separately. (1) Assume �㔼1 (�㔷) = ⊤. Then �㔼1 (�㔶1 ∨ … ∨ �㔶�㕛 ) = ⊤. So for some �㕖 where 1 ≤ �㕖 ≤ �㕛, �㔼1 (�㔶�㕖 ) = ⊤. By Proposition 3, �㔼2 (�㔶�㕖 ) = ⊤. Consequently �㔼2 (�㔷) = ⊤. (2) Assume �㔼2 (�㔷) = ⊥. Then �㔼1 (�㔶1 ∨ … ∨ �㔶�㕛 ) = ⊥. So for all �㕖 where 1 ≤ �㕖 ≤ �㕛, �㔼1 (�㔶�㕖 ) = ⊥. By Proposition 3, �㔼2 (�㔶�㕖 ) = ⊥ for all �㕖 where 1 ≤ �㕖 ≤ �㕛. Consequently �㔼2 (�㔶1 ∨ … ∨ �㔶�㕛 ) = ⊥ and �㔼 (�㔷) = ⊥. 23 For example assume we have a disjunction of conjunctions of literals �㔷 = (¬�㕏 ∧�㕐)∨�㕑. Assume we have two interpretations �㔼1 = ⟨{�㕑}, {�㕐}⟩ and �㔼2 = ⟨{�㕑}, {�㕏, �㕐}⟩. �㔼1 maps �㔷 to �㔼1 (�㔷) = (¬U∧⊥)∨⊤ = ⊤. Because �㔼1 ⊆ �㔼2 , �㔼2 must map �㔷 to ⊤ too, �㔼2 (�㔷) = (¬⊥ ∧ ⊥) ∨ ⊤ = ⊤. Note that Proposition 2 does not hold for a contextual literal �㕐�㕡�㕥�㕡 �㕎. Consider the two interpretations �㔼1 = ⟨∅, ∅⟩, �㔼2 = ⟨{�㕎}, ∅⟩. Although �㔼1 ⊆ �㔼2 , interpretation �㔼1 maps the contextual literal �㕐�㕡�㕥�㕡 �㕎 to �㔼1 (�㕐�㕡�㕥�㕡 �㕎) = ⊥, and interpretation �㔼2 maps the same contextual literal to �㔼2 (�㕐�㕡�㕥�㕡 �㕎) = ⊤. The same example can be used to show why Proposition 3 and Proposition 4 do not hold for contextual conjunctions of literals and contextual disjunctions of conjunctions of literals. 4.6. Validity in Classical Two-valued Logic and Three-Valued Łukasiewicz Logic Here we establish the link between validity in classical two-valued logic and three-valued Łuasiewicz Logic. Proposition 5. If there are two interpretations �㔼 and �㔽, where �㔼 is two-valued and �㔽 is three-valued, and that for each ground atom �㔴 occurring in a formula �㔹 we 昀椀nd �㔼 (�㔴) = �㔽 (�㔴), then �㔼 (�㔹 ) = �㔽 (�㔹 ). Proof. The truth tables of the operators of classical logic and three-valued Łukasiewicz logic are identical when none of the operands are mapped to U, and �㔽 maps no atom �㔴 to U and �㔼 cannot map �㔴 to U, hence �㔼 (�㔴) = �㔽 (�㔴). See Table 1. Proposition 6. If �㔷 is a non-contextual disjunction of conjunctions of literals, then there is a two-valued interpretation �㔼 where �㔼 (�㔷) = ⊥ i昀昀 there is a three-valued interpretation �㔽 where �㔽 (�㔷) = ⊥ Proof. To prove the if-half, assume there is a three-valued interpretation �㔽 where �㔽 (�㔷) = ⊥. Construct another three-valued interpretation �㔽 ′ where for each ground �㔴: If �㔽 (�㔴) ≠ U, then �㔽 ′ (�㔴) = �㔽 (�㔴), and If �㔽 (�㔴) = U, then �㔽 ′ (�㔴) = ⊥. By the de昀椀nition of �㔽 ′ , �㔽 ⊆ �㔽 ′ . So �㔽 ′ (�㔷) = ⊥ by Proposition 4. Construct a two-valued Herbrand interpretation �㔼 such that for each ground atom �㔴, �㔼 (�㔴) = �㔽 (�㔴). �㔼 is a two-valued interpretation because �㔽 does not map any atom to U by the de昀椀nition of �㔽 ′ . By Proposition 5, �㔼 (�㔷) = �㔽 (�㔷) = ⊥. To prove the only-if-half, assume there is a two-valued interpretation �㔼 where �㔼 (�㔷) = ⊥. Construct a three-valued interpretation �㔽 where for each ground atom �㔴, �㔽 (�㔴) = �㔼 (�㔴). By Proposition 5, �㔼 (�㔷) = �㔽 (�㔷) = ⊥. For example assume we have a disjunction of conjunctions of literals �㔷1 = �㕎 ∨ (�㕏 ∧ ¬�㕐), and a two-valued interpretation �㔼 = {�㕎}, i.e., the interpretation �㔼 maps the atom �㕎 to ⊤ and the rest of the atoms, �㕏 and �㕐, to ⊥. The interpretation �㔼 maps the disjunction �㔷1 to �㔼 (�㔷1 ) = ⊤ ∨ (⊥ ∧ ⊤) = ⊤. By Proposition 6 this entails the existence of a three-valued interpretation �㔽 such that �㔽 (�㔷1 ) = ⊤. For instance the three-valued interpretation �㔽 = ⟨{�㕎}, ∅⟩ maps the disjunction �㔷1 to �㔽 (�㔷1 ) = ⊤∨(U∧U) = ⊤. On the other hand for a disjunction of conjunctions of literals such as �㔷3 = �㕎∨¬�㕎, �㔷3 is clearly valid in classical two-valued logic, so by the previous proposition we should be able to 昀椀nd a three-valued interpretation �㔽 such that �㔽 (�㔷3 ) = ⊥, which is the case because for all three-valued interpretations, �㔷3 can either be mapped to ⊤ or U. Corollary 1. A non-contextual disjunction of conjunctions of literals �㔷 is valid in classical two- valued logic i昀昀 �㔷 cannot be falsi昀椀ed in three-valued Łukasiewicz logic. 24 Proof. This can be shown by negating both sides of the equivalence of Proposition 6. 4.7. Herbrand’s Theorem Here the weak version of Herbrand’s theorem is introduced as it is needed for the undecidability proof. In this subsection we only speak about validity in classical two-valued logic. Theorem 2. [19] Let �㖯 be a 昀椀nitely axiomatized by universal formulas. Let �㔹 = (∃�㕋1 , … , �㕋�㕛 )�㔺(�㕋1 , … , �㕋�㕛 ) be a purely existential formula. Then �㖯 ⊧ �㔹 i昀昀 there are gound terms �㕝 (�㕡�㕖,�㕗 )1≤�㕖≤�㕝, 1≤�㕗≤�㕛 such that �㖯 ⊧ ⋁�㕖=1 �㔺(�㕡�㕖,1 , … , �㕡�㕖,�㕛 ). Corollary 2. Let �㔹 = (∃�㕋1 , … , �㕋�㕛 )�㔺(�㕋1 , … , �㕋�㕛 ) be a purely existential sentence and �㔺 is a quanti昀椀er-free formula. Then �㔹 is valid i昀昀 there are ground terms (�㕡�㕖,�㕗 )1≤�㕖≤�㕝, 1≤�㕗≤�㕛 such that �㕝 ⋁�㕖=1 �㔺(�㕡�㕖,1 , … , �㕡�㕖,�㕛 ) is valid. Proof. A special case of Theorem 2 where �㖯 = ∅ and �㔹 is a sentence. Remember that �㕔(�㔹 ) denote the set of all ground instances of a formula �㔹. Corollary 3. Let �㔹 = (∃�㕋1 , … , �㕋�㕛 )�㔺(�㕋1 , … , �㕋�㕛 ) be a purely existential sentence and �㔺 a quanti昀椀er- free formula. Then �㔹 is valid i昀昀 ⋁�㔻 ∈�㕔(�㔺) �㔻 is valid. Proof. To prove the if-half, assume �㔹 is valid, then there are ground terms (�㕡�㕖,�㕗 )1≤�㕖≤�㕝,1≤�㕗≤�㕛 such �㕝 that ⋁�㕖=1 �㔺(�㕡�㕖,1 , … , �㕡�㕖,�㕛 ) is valid by Corollary 2. For each �㕖 ≤ �㕝, �㔺(�㕡�㕖,1 , … , �㕡�㕖,�㕛 ) is a ground instance �㕝 of �㔺, i.e., �㔺(�㕡�㕖,1 , … , �㕡�㕖,�㕛 ) ∈ �㕔(�㔺). Hence ⋁�㔻 ∈�㕔(�㔺) �㔻 ≡2 �㔻 ′ ∨ ⋁�㕖=1 �㔺(�㕡�㕖,1 , … , �㕡�㕖,�㕛 ), where �㔻 ′ is a �㕝 disjunction of all the ground instances of �㔺 that do not occur in the disjunction ⋁�㕖=1 �㔺(�㕡�㕖,1 , … , �㕡�㕖,�㕛 ). Consequently, ⋁�㔻 ∈�㕔(�㔺) �㔻 is valid too. To prove the only-if-half, assume ⋁�㔻 ∈�㕔(�㔺) �㔻 is valid. For each �㔻 ∈ �㕔(�㔺), �㔻 = �㔺(�㕡1 , … , �㕡�㕛 ) for some sequence of ground terms �㕡1 , … , �㕡�㕛 . We can give each �㔻 ∈ �㕔(�㔺) a unique natural number say �㕖 such that �㔻 = �㔺(�㕡�㕖,1 , … , �㕡�㕖,�㕛 ). Consequently, there are ground terms (�㕡�㕖,�㕗 )1≤�㕖≤�㕝,1≤�㕗≤�㕛 , where �㕝 is the number of ground instances of �㔺 such that �㕝 ⋁�㕖=1 �㔺(�㕡�㕖,1 , … , �㕡�㕖,�㕛 ) is valid. By Corollary 2, �㔹 is valid. For example the following formula (∃�㕋 , �㕌 )�㕝(�㕋 , �㕌 ) is valid i昀昀 ⋁�㔻 ∈�㕔(�㕝(�㕋 ,�㕌 )) �㔻 is valid by the corollary above. Later we will deal with a formula that is a disjunction of purely existential sentences, hence we need the following proposition. Proposition 7. Let �㔹�㕖 = (∃�㕋�㕖,1 , … , �㕋�㕖,�㕚�㕖 )�㔺�㕖 (�㕋�㕖,1 , … , �㕋�㕖,�㕚�㕖 ) be a purely existential sentence and �㔺�㕖 a quanti昀椀er-free formula for any �㕖 ∈ ℕ. Then �㔹1 ∨…∨�㔹�㕛 is valid i昀昀 (⋁�㔻1 ∈�㕔(�㔺1 ) �㔻1 )∨…∨(⋁�㔻�㕛 ∈�㕔(�㔺�㕛 ) �㔻�㕛 ) is valid. Proof. Note that �㔹1 ∨ … ∨ �㔹�㕛 = ((∃�㕋1,1 , … , �㕋1,�㕚1 )�㔺1 ∨ … ∨ (∃�㕋�㕛,1 , … , �㕋�㕛,�㕚�㕛 )�㔺�㕛 ) ≡2 (∃�㕋1,1 , … �㕋1,�㕚1 , … , �㕋�㕛,1 , … , �㕋�㕛,�㕚�㕛 )(�㔺1 ∨ … ∨ �㔺�㕛 ) By Corollary 3, �㔹1 ∨ … ∨ �㔹�㕛 is valid i昀昀 ⋁�㔻 ∈�㕔(�㔺1 ∨…∨�㔺�㕛 ) �㔻 is valid. It is not hard to see that ⋁�㔻 ∈�㕔(�㔺1 ∨…∨�㔺�㕛 ) �㔻 ≡2 (⋁�㔻1 ∈�㕔(�㔺1 ) �㔻1 )∨…∨(⋁�㔻�㕛 ∈�㕔(�㔺�㕛 ) �㔻�㕛 ) because �㔺1 , …, and �㔺�㕛 share no variables pairwise. 25 For example the following formula (∃�㕋 , �㕌 )(�㕝(�㕋 , �㕌 ))) ∨ (∃�㕍 )(�㕞(�㕍 )) is valid i昀昀 ⋁�㔻1 ∈�㕔(�㕝(�㕋 ,�㕌 ))�㔻1 ∨ ⋁�㔻2 ∈�㕔(�㕞(�㕍 )) �㔻2 , by Proposition 7. 4.8. Validity And The Monotonicity in Class �㖱 Here the connection between the previous validity results and the monotonicity of programs in class �㖱 will be shown. Proposition 8. For a program �㖫 of class �㖱, an interpretation �㔼, a ground atom �㔴 �㔼 (�㕐�㕡�㕥�㕡 �㕞 ∨ (⋁1≤�㕖≤�㕛 ⋁�㔶∈�㕔(�㕏�㕜�㕑�㕦�㕖 ) �㔶)) �㔴 = �㕟 Φ�㖫 �㔼 (�㔴) = { U �㕜�㕡ℎ�㕒�㕟�㕤�㕖�㕠�㕒 Proof. Φ�㖫 �㔼 (�㕟) = �㔼 (�㔷), for a disjunction of conjunctions of literals �㔷 where �㕟 ↔ �㔷 ∈ �㕤�㕐(�㕔(�㖫 )). Note that �㕔(�㖫 ) = {�㕟 ← �㕐�㕡�㕥�㕡 �㕞} ∪ ⋃1≤�㕖≤�㕛 {�㕟 ← �㔶 | �㔶 ∈ �㕔(�㕏�㕜�㕑�㕦�㕖 )}. Hence �㔷 = �㕐�㕡�㕥�㕡 �㕞 ∨ (⋃1≤�㕖≤�㕛 ⋃�㔶∈�㕔(�㕏�㕜�㕑�㕦�㕖 ) �㔶). Consequently Φ�㖫 �㔼 (�㕟) = �㔼 (�㕐�㕡�㕥�㕡 �㕞 ∨ (⋁1≤�㕖≤�㕛 ⋁�㔶∈�㕔(�㕏�㕜�㕑�㕦�㕖 ) �㔶)). Proposition 9. For any program �㖫 of class �㖱, the semantic operator Φ�㖫 is non-monotonic i昀昀 ⋁1≤�㕖≤�㕛 (∃�㕏�㕜�㕑�㕦�㕖 ) is not valid in classical two-valued logic. Proof. To prove the if-half, assume the sentence ⋁1≤�㕖≤�㕛 (∃�㕏�㕜�㕑�㕦�㕖 ) is not valid in classical two- valued logic. By Proposition 7, the formula �㔷 = ⋁1≤�㕖≤�㕛 ⋁�㔶∈�㕔(�㕏�㕜�㕑�㕦�㕖 )�㔶 is not valid in classical two-valued logic either. Hence, we can 昀椀nd a two-valued interpretation �㔼 such that �㔼 (�㔷) = ⊥. By Corollary 1, we can 昀椀nd a three-valued Łukasiewicz interpretation �㔼 ′ where �㔼 ′ (�㔷) = ⊥. So one can construct an interpretation �㔼1 where: (1) For any ground atom �㔴, if �㔴 ≠ �㕞, then �㔼1 (�㔴) = �㔼 ′ (�㔴); (2) �㔼1 (�㕞) = U. Note that �㔼1 (�㔷) = ⊥, since �㔼 (�㔷) = ⊥ and �㕞 does not occur in �㔷. Also �㔼1 (�㕐�㕡�㕥�㕡 �㕞) = ⊥ by de昀椀nition of �㔼1 . Therefore �㔼1 (�㕐�㕡�㕥�㕡 �㕞 ∨ �㔷) = ⊥. Construct another interpretation �㔼2 where: (1) For any ground atom �㔴, if �㔴 ≠ �㕞, then �㔼2 (�㔴) = �㔼 ′ (�㔴); (2) �㔼2 (�㕞) = ⊤. Note that �㔼2 (�㔷) = ⊥, since �㔼 ′ (�㔷) = ⊥ and �㕞 does not occur in �㔷. Also �㔼2 (�㕐�㕡�㕥�㕡 �㕞) = ⊤ by de昀椀nition of �㔼2 . Therefore �㔼2 (�㕐�㕡�㕥�㕡 �㕞 ∨ �㔷) = ⊤. Note also that �㔼1 ⊆ �㔼2 because they only di昀昀er on the mapping of �㕞 where �㔼1 (�㕞) = U and �㔼2 (�㕞) = ⊤. By Proposition 7 Φ�㖫 �㔼1 (�㕟) = �㔼1 (�㕐�㕡�㕥�㕡 �㕞 ∨ �㔷) = ⊥ and Φ�㖫 �㔼2 (�㕟) = �㔼2 (�㕐�㕡�㕥�㕡 �㕞 ∨ �㔷) = ⊤. Hence Φ�㖫 �㔼1 ⊈ Φ�㖫 �㔼2 , while �㔼1 ⊆ �㔼2 . So Φ�㖫 is non-monotonic. To prove the only-if-half, assume Φ�㖫 is non-monotonic. Then There are two interpretations �㔼1 and �㔼2 where �㔼1 ⊆ �㔼2 and Φ�㖫 �㔼1 ⊈ Φ�㖫 �㔼2 . Due to Φ�㖫 �㔼1 ⊈ Φ�㖫 �㔼2 , for some ground atom �㔴, Φ�㖫 �㔼1 (�㔴) ≠ Φ�㖫 �㔼2 (�㔴) and Φ�㖫 �㔼1 (�㔴) ≠ U. Φ�㖫 �㔼1 (�㔴) ≠ U implies that �㔴 is a de昀椀ned atom otherwise Φ�㖫 �㔼1 (�㔴) = Φ�㖫 �㔼2 (�㔴) = U by De昀椀nition 2. Since �㕟 is the only de昀椀ned atom, Φ�㖫 �㔼1 (�㕟) ≠ Φ�㖫 �㔼2 (�㕟) and Φ�㖫 �㔼1 (�㕟) ≠ U. By Proposition 3, �㔼1 (�㕐�㕡�㕥�㕡 �㕞 ∨ �㔷) ≠ �㔼2 (�㕐�㕡�㕥�㕡 �㕞 ∨ �㔷) and �㔼1 (�㕐�㕡�㕥�㕡 �㕞 ∨ �㔷) ≠ U where �㔷 = ⋁1≤�㕖≤�㕛 ⋁�㔶∈�㕔(�㕏�㕜�㕑�㕦�㕖 ) �㔶. Since �㔼1 (�㕐�㕡�㕥�㕡 �㕞 ∨ �㔷) ≠ U, �㔼1 (�㕐�㕡�㕥�㕡 �㕞 ∨ �㔷) is either ⊤ or ⊥. Assume �㔼1 (�㕐�㕡�㕥�㕡 �㕞 ∨ �㔷) = ⊤. Assume �㔼1 (�㕐�㕡�㕥�㕡 �㕞) = ⊤. Then �㔼1 (�㕞) = ⊤. Since �㔼1 ⊆ �㔼2 , �㔼2 (�㕞) = ⊤ and �㔼2 (�㕐�㕡�㕥�㕡 �㕞) = ⊤ so �㔼2 (�㕐�㕡�㕥�㕡 �㕞 ∨ �㔷) = ⊤ but �㔼1 (�㕐�㕡�㕥�㕡 �㕞 ∨ �㔷) ≠ �㔼2 (�㕐�㕡�㕥�㕡 �㕞 ∨ �㔷). A contradiction. So �㔼1 (�㕐�㕡�㕥�㕡 �㕞) ≠ ⊤. Consequently �㔼1 (�㔷) = ⊤, which implies �㔼2 (�㔷) = ⊤, by Proposition 4. So �㔼2 (�㕐�㕡�㕥�㕡 �㕞 ∨ �㔷) = ⊤ but �㔼1 (�㕐�㕡�㕥�㕡 �㕞 ∨ �㔷) ≠ �㔼2 (�㕐�㕡�㕥�㕡 �㕞 ∨ �㔷). A contradiction. �㔼1 (�㔷) ≠ ⊤ either. Hence �㔼1 (�㕐�㕡�㕥�㕡 �㕞 ∨ �㔷) ≠ ⊤, subsequently �㔼1 (�㕐�㕡�㕥�㕡 �㕞 ∨ �㔷) = ⊥. Since �㔼1 (�㕐�㕡�㕥�㕡 �㕞 ∨ �㔷) = ⊥, �㔼1 (�㔷) = ⊥. There is a three-valued Łukasiewicz interpretation �㔼1 where �㔼1 (�㔷) = ⊥. By Corollary 1, �㔷 is not valid in classical two-valued logic. By Proposition 7, the sentence ⋁1≤�㕖≤�㕛 (∃�㕏�㕜�㕑�㕦�㕖 ) is not valid in classical two-valued logic either. 26 �㖫�㔾 = {�㕟 ← ¬�㕝(�㕓�㗼1 �㕐, �㕓�㗽1 �㕐), �㕛 ⋮ �㔺�㔾 ≡2 ⋁ ¬�㕝(�㕓�㗼�㕖 (�㕐), �㕓�㗽�㕖 (�㕐)) �㕟 ← ¬�㕝(�㕓�㗼�㕛 �㕐, �㕓�㗽�㕛 �㕐), �㕖=1 �㕛 �㕟 ← �㕝(�㕋 , �㕌 ) ∧ ¬�㕝(�㕓�㗼1 �㕋 , �㕓�㗽1 �㕌 ), ∨ ⋁(∃�㕋 , �㕌 )(�㕝(�㕋 , �㕌 ) ∧ ¬�㕝(�㕓�㗼�㕖 (�㕋 ), �㕓�㗽�㕖 (�㕌 ))) ⋮ �㕖=1 ∨ (∃�㕍 )�㕝(�㕍 , �㕍 ). �㕟 ← �㕝(�㕋 , �㕌 ) ∧ ¬�㕝(�㕓�㗼�㕛 �㕋 , �㕓�㗽�㕛 �㕌 ), �㕟 ← �㕝(�㕍 , �㕍 ), �㕟 ← �㕐�㕡�㕥�㕡 �㕞 }. Figure 1: For a PCP instance �㔾, the formula �㔺�㔾 is shown on the le昀琀, and program �㖫 �㔾 is shown on the right. 4.9. Reduction As mentioned before a PCP instance �㔾 has solution i昀昀 �㔺�㔾 is valid, see Section 4.3. Note that program �㖫 �㔾 shown on the right has a non-monotonic semantic operator i昀昀 �㔺�㔾 is not valid by Proposition 9. So program �㖫 �㔾 has a monotonic semantic operator i昀昀 �㔺�㔾 is valid. Consequently, program �㖫 �㔾 has a monotonic semantic operator i昀昀 PCP instance �㔾 has a solution. Theorem 3. The monotonicity of the semantic operator of a given contextual program �㖫 is undecidable Proof. If the monotonicity of Φ�㖫 is decidable, then the PCP problem is decidable by the previous reduction. Hence, the monotonicity of Φ�㖫 is undecidable. 5. Conclusion Contextual programs use the context operator (ctxt) to model cases where default reasoning is preferred. There is always a least 昀椀xed point of the semantic operator of non-contextual programs. This is possible because the semantic operator of non-contextual programs is monotonic [12, 10]. On the other hand the semantic operator of contextual programs is o昀琀en non-monotonic and their semantic operators o昀琀en do not have any 昀椀xed points. Nonetheless, for the class of acyclic contextual programs, there is always a least 昀椀xed point of the semantic operator by the Banach Contraction Mapping Theorem [11, 13]. This 昀椀xed point was shown to be a model in [13], and has been shown to be a minimal model by Theorem 1. Contextual programs o昀琀en do not have monotonic semantic operators, that is why there is no guarantee a 昀椀xed point exists. The monotonicity of the semantic operator of a contextual given program has been shown to be generally undecidable in Theorem 3 using a reduction from PCP. However, it is decidable for programs with 昀椀nite Herbrand base because the number of interpretations is 昀椀nite in this case. 27 References [1] E.-A. Dietz, S. Hölldobler, C. Wernhard, Modeling the suppression task under weak completion and well-founded semantics, Journal of Applied Non-Classical Logics 24 (2014) 61–85. doi:10.1080/11663081.2014.911520. [2] E.-A. Dietz, S. Hölldobler, M. Ragni, A computational logic approach to the abstract and the social case of the selection task, in: Proceedings Eleventh International Symposium on Logical Formalizations of Commonsense Reasoning, 2013. [3] A. O. da Costa, E.-A. D. Saldanha, S. Hölldobler, M. Ragni, A computational logic approach to human syllogistic reasoning., in: CogSci, 2017. [4] S. Hölldobler, Ethical decision making under the weak completion semantics, in: Bridging@ IJCAI/ECAI, 2018. [5] M. Cramer, S. Hölldobler, M. Ragni, Modeling human reasoning about conditionals, in: 19 th International Workshop on Non-Monotonic Reasoning, 2021, p. 223. [6] E.-A. Dietz, S. Hölldobler, L. M. Pereira, On conditionals., in: GCAI, volume 36, 2015, pp. 79–92. doi:10.29007/7p4b. [7] E.-A. D. Saldanha, S. Hölldobler, I. L. Rocha, Obligation versus factual conditionals under the weak completion semantics., in: YSIP, 2017, pp. 55–64. [8] I. Hamada, S. Hölldobler, On disjunctions and the weak completion semantics, Proceedings of the Virtual MathPsych/ICCM. via mathpsych. org/presentation/571 (2021). [9] E.-A. D. Saldanha, S. Hölldobler, C. D. P. K. Ramli, L. P. Medinacelli, A core method for the weak completion semantics with skeptical abduction, Journal of Arti昀椀cial Intelligence Research 63 (2018) 51–86. doi:10.1613/jair.1.11236. [10] K. Stenning, M. Van Lambalgen, Human reasoning and cognitive science, MIT Press, 2012. [11] E.-A. Dietz Saldanha, S. Hölldobler, L. M. Pereira, Contextual reasoning: Usually birds can abductively 昀氀y, in: International Conference on Logic Programming and Nonmonotonic Reasoning, Springer, 2017, pp. 64–77. doi:10.1007/978-3-319-61660-58. [12] S. Hölldobler, C. D. P. K. Ramli, Logic programs under three-valued łukasiewicz semantics, in: International Conference on Logic Programming, Springer, 2009, pp. 464–478. doi:10. 1007/978-3-642-02846-5_37. [13] S. Hölldobler, C. K. Ramli, Contraction properties of a semantic operator for human reasoning, in: Proceedings of the 昀椀昀琀h international conference on information, volume 228, 2009, p. 231. [14] D. Van Dalen, D. van Dalen, Logic and structure, volume 3, Springer, 1994. [15] J. Łukasiewicz, L. Borkowski, Jan Łukasiewicz, North-Holland Publishing Company, 1970. [16] K. L. Clark, Negation as failure, in: Logic and data bases, Springer, 1978, pp. 293–322. doi:10.1007/978-1-4684-3384-5_11. [17] S. Hölldobler, Logik und Logikprogrammierung, volume 1: Grundlagen, Heidelberg: Syn- chron Publishers GmbH, 2001. [18] U. Schöning, Logic for computer scientists, Birkhäuser Boston, 2008, pp. 64–66. [19] A. Alcolei, P. Clairambault, M. Hyland, G. Winskel, The true concurrency of herbrand’s theorem, in: 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2018. doi:10.4230/LIPIcs.CSL.2018. 5. 28