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.
The weak completion semantics (WCS) is a cognitive theory that models human reasoning using
normal logic programs [
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 [
Sometime ago an operator known as the context operator (ctxt) was added to WCS in [
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 [
We assume the reader to be familiar with classical logic [
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 [
= ⟨ ⊤, ⊥⟩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 1Whenever we apply a unary operator like Φ to an argument like , we omit parenthesis and write Φ instead. ( ) 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.
The semantic operator of acyclic programs (contextual or non-contextual) is a contraction by
the Banach Contraction Mapping Theorem [
De昀椀nition 2. For any program
, an interpretation , and a ground atom Φ 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 ⊥ 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 gr↔ound∈ atom . Bseuccahustehat ′ is′(a m)≠odΦel for ′( ) ., wAes s昀椀nudme th′(at) =is d′e(昀椀ne) d..BIunt th′is( c)a=seΦwe 昀椀nd′( ) 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, 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.
is acyclic, then the unique 昀椀xed point of Φ is 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 .
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
operator is monotonic, the Knaster-Tarski Fixed Point Theorem guarantees the existence of a
least 昀椀xed point of the semantic operator [
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 winhcelraess bbeelcoanugssetoa cplraossgram,and of′cslhasasres nisondoen昀椀n-emdoatnoomtosnwicitih昀 is,ienqcuaisvealen′ tistonot ′em∪pty,, and most importantly has a non-monotonic semantic operator too. For example program = { ← , ← , ← ¬ ∧ , ← ⊤} has a non-monotonic semantic operator Φ abnecdausebel=ongs t′o∪clas,sw h,esrheares′ n=o {de昀椀n←ed¬ato∧ms wit,h ← ′⊤,}aannddprogr=am{ ← ca, n b←e 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.
The Post correspondence problem is a well-known undecidable problem. The PCP problem well
be introduced next using the notation in [
=1 ¬ 1 ≡2 ⋁ ¬ ( ( ), ( ))
=1 ¬ 2 ≡2 ¬(∀ , )(¬ ( , ) ∨ ≡2 (∃ , )( ( , ) ∧ ( ⋁ ¬ ( ( ),
=1 ≡2 ⋁(∃ , )( ( , ) ∧ ¬ ( ( ),
( ))) ⋀ ( ( ), =1 ( ))) ( )))) ⋀ ( =1
We use ≡2=1to 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?
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. 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.
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 2( ) = ⊥ .
(1) If 1( ) = ⊤ , then 2( ) = ⊤ , (2) If 1( ) = ⊥ , then 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 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 ( ) = ⊥ . (1) If 1( ) = ⊤ , 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.
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 twovalued logic i昀 cannot be falsi昀椀ed in three-valued Łukasiewicz logic. Proof. This can be shown by negating both sides of the equivalence of Proposition 6.
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. [
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. =
= ∅ 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昀椀erfree 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 quanti昀椀er-free formula for any ∈ ℕ. Then 1 ∨…∨ is valid i昀 (⋁ 1∈ ( 1) 1)∨…∨(⋁ ∈ ( ) is valid. a ) Proof. Note that 1 ∨ … ∨ = ((∃ 1,1, … , 1, 1) 1 ∨ … ∨ (∃ ,1, … , , ) ) ≡2 (∃ 1,1, … 1, 1, … , ,1, … , , )( 1 ∨ … ∨ ) ⋁ ∈ ( 1∨…∨ ) pairwise.
By Corollary 3, 1 ∨ … ∨ is valid i昀 ⋁ ∈ ( 1∨…∨ ) is valid. It is not hard to see that ≡ 2 (⋁ 1∈ ( 1) 1)∨…∨(⋁ ∈ ( ) ) because 1, …, and share no variables For example the following formula (∃ , )( ( , ))) ∨ (∃ )( ( )) ⋁ 1∈ ( ( , )) 1 ∨ ⋁ 2∈ ( ( )) 2, by Proposition 7. is valid i昀
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 Φ Proof. Φ ( ) = ( ), for a disjunction of conjunctions of literals Note that ( ) = { ← } ∪ ⋃1≤ ≤ { ← | ∈ ( (⋃1≤ ≤ ⋃ ∈ ( ) ) . Consequently Φ ( ) = ( where ↔ ∈ )}. Hence = ∨ ⋁(1≤ ≤ ⋁ ∈ ( ) )) .
( ( )) .
∨ Proposition 9. For any program of class , the semantic operator Φ ⋁1≤ ≤ (∃ ) is not valid in classical two-valued logic. is non-monotonic i昀 Proof. To prove the if-half, assume the sentence ⋁1≤ ≤ (∃ ) is not valid in classical twovalued 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. 4.9. Reduction , , , 1 ), ),
}. is shown on the le昀琀, and program is shown on the 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 undecidable is Proof. If the monotonicity of Φ is decidable, then the PCP problem is decidable by the previous reduction. Hence, the monotonicity of Φ is undecidable.
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 [