1 Introduction
2 Choice Logics
2.1 Syntax and Semantics
2.2 Prominent Choice Logics
\(\mathcal {I}\) | \(a \wedge b\) | \(a \vee b\) | \(a \vec {\times }b\) | \(a \vec {\odot }b\) | \(a \vec {\diamond }b\) |
---|---|---|---|---|---|
\(\emptyset \) | \(\infty \) | \(\infty \) | \(\infty \) | \(\infty \) | \(\infty \) |
\(\{b\}\) | \(\infty \) | 1 | 2 | \(\infty \) | 3 |
\(\{a\}\) | \(\infty \) | 1 | 1 | 2 | 2 |
\(\{a,b\}\) | 1 | 1 | 1 | 1 | 1 |
2.3 Preferred Model Entailment
-
\(\mathcal {I}\) is a lexicographically preferred model of T, written as \(\mathcal {I}\in { Prf}_{\mathcal {L}}^{{ lex}}(T)\), iff \(\mathcal {I}\in { Mod}_{\mathcal {L}}({T})\) and if there is no \(\mathcal {J}\in { Mod}_{\mathcal {L}}({T})\) such that, for some \(k \in \mathbb {N}\) and all \(l < k\), \(\vert \mathcal {I}_\mathcal {L}^k(T)\vert < \vert \mathcal {J}_\mathcal {L}^k(T)\vert \) and \(\vert \mathcal {I}_\mathcal {L}^l(T)\vert = \vert \mathcal {J}_\mathcal {L}^l(T)\vert \) holds.
-
\(\mathcal {I}\) is an inclusion-based preferred model of T, written as \(\mathcal {I}\in { Prf}_{\mathcal {L}}^{{ inc}}(T)\), iff \(\mathcal {I}\in { Mod}_{\mathcal {L}}({T})\) and if there is no \(\mathcal {J}\in { Mod}_{\mathcal {L}}({T})\) such that, for some \(k \in \mathbb {N}\) and all \(l < k\), \(\mathcal {I}_\mathcal {L}^k(T) \subset \mathcal {J}_\mathcal {L}^k(T)\) and \(\mathcal {I}_\mathcal {L}^l(T) = \mathcal {J}_\mathcal {L}^l(T)\) holds.
-
\(\mathcal {I}\) is a minmax preferred model of T, written as \(\mathcal {I}\in { Prf}_{\mathcal {L}}^{{ mm}}(T)\), iff \(\mathcal {I}\in { Mod}_{\mathcal {L}}({T})\) and if there is no \(\mathcal {J}\in { Mod}_{\mathcal {L}}({T})\) such that \({ max}\{{ deg}_{\mathcal {L}}(\mathcal {I},F) \mid F \in T\} > { max}\{{ deg}_{\mathcal {L}}(\mathcal {J},F) \mid F \in T\}\).
3 The Sequent Calculus L[QCL]
-
every model of \((A)_k\) is a model of \(\Delta \) or of some \((B)_l\) with \(l < k\),
-
every model of \((B)_k\) is a model of \(\Delta \) or of some \((A)_l\) with \(l < k\).
-
For the axioms this is clearly the case.
-
\((\lnot r)\) and \((\lnot l)\): follows from the fact that \({ deg}_{\text {QCL}}(\mathcal {I},F) < \infty \iff \mathcal {I}\models { cp}(F)\) for all \(\text {QCL}\)-formulas F.
-
\((\vee l)\): Assume that the conclusion of the rule is not valid, i.e., there is a model M of \(\Gamma \) and \((A \vee B)_k\) that is not a model of \(\Delta \). Then, M satisfies either A or B to degree k and neither to a degree smaller than k. Assume M satisfies A to a degree of k, the other case is symmetric. Then M is a model of \(\Gamma \) and \((A)_k\) but, by assumption, neither of \(\Delta \) nor of \((B)_j\) for any \(j < k\). Hence, at least one of the premises is not valid.
-
\((\wedge l)\): Analogous to the proof for \((\vee l)\): assume that the conclusion of the rule is not valid, i.e., that there is a model M of \(\Gamma \) and \((A \wedge B)_k\) that is not a model of \(\Delta \). Then, M satisfies either A or B to degree k and neither to a degree higher than k. Assume M satisfies A to a degree of k, the other case is symmetric. Then M is a model of \(\Gamma \) and \((A)_k\) but, by assumption, neither of \(\Delta \) nor of \((\lnot B)_1\) or \((B)_j\) for any \(j > k\). Hence, at least one of the premises is not valid.
-
\((\vee r)\): Assume there is a model M of \(\Gamma \) that is not a model of \(\Delta \) or of \((A \vee B)_k\). There are two possible cases why M is not a model of \((A \vee B)_k\):1.M satisfies neither A nor B to degree k. But in this case the premise \(\Gamma \vdash (A)_k,(B)_k, \Delta \) is not valid as M is also not a model of \(\Delta \) by assumption.2.M satisfies either A or B to a degree smaller than k. Assume that M satisfies A to degree \(j <k\) (the other case is symmetric). Then the premise \(\Gamma , (A)_j \vdash \Delta \) is not valid. Indeed, M is a model of \(\Gamma \) and \((A)_j\) but not of \(\Delta \).
-
\((\wedge r)\): Analogous to the proof for \((\vee r)\): assume that the conclusion of the rule is not valid, i.e. there is a model M of \(\Gamma \) that is not a model of \(\Delta \) or of \((A \wedge B)_k\). There are two possible cases why M is not a model of \((A \wedge B)_k\):1.M satisfies neither A nor B to degree k. However, then the premise \(\Gamma \vdash (A)_k,(B)_k, \Delta \) is not valid as M is also not a model of \(\Delta \) by assumption.2.M satisfies either A or B to a degree j higher than k. By symmetry, it suffices to consider the case that M satisfies A to a degree j higher than k. Then either \(k < j \le { opt}_{\text {QCL}}(A)\) or \(j = \infty \). If \(k < j \le { opt}_{\text {QCL}}(A)\) the premise \(\Gamma , (A)_j \vdash \Delta \) is not valid. If \(k = \infty \) the premise \(\Gamma , (\lnot A)_1 \vdash \Delta \) is not valid.
-
\((\vec {\times }l_1)\) and \((\vec {\times }r_1)\): follows from the fact that \((A)_k\) has the same models as \((A \vec {\times }B)_k\) for \(k \le { opt}_{\mathcal {L}}(A)\).
-
\((\vec {\times }l_2)\): Assume the conclusion of the rule is not valid and let M be the model witnessing this. Then M is a model of \((A \vec {\times }B)_{{ opt}_{QCL}(A) +l}\). By definition, M satisfies B to degree l and is not a model of A. However, then it is also a model of \(\Gamma \), \((B)_l\) and \((\lnot A)_1\), which means that the premise is not valid.
-
\((\vec {\times }r_2)\). Assume that both premises are valid, i.e., every model of \(\Gamma \) is either a model of \(\Delta \) or of \((\lnot A)_1\) and \((B)_l\) with \(l \le { opt}_{\mathcal {L}}(B)\). Now, by definition, any model that is not a model of A (and hence a model of \((\lnot A)_1\)) and of \((B)_l\) satisfies \(A \vec {\times }B\) to degree \({ opt}_{QCL}(A) +l\). Therefore, every model of \(\Gamma \) is either a model of \(\Delta \) or of \((A \vec {\times }B)_{{ opt}_{QCL}(A) +l}\), which means that the conclusion of the rule is valid.
-
\(({ do} l)\): \(\Gamma , \bot \) has no models, i.e., the premise \(\Gamma , \bot \vdash \Delta \) is valid. Indeed, the sequent \(\Gamma , \bot \vdash \Delta \) is an axiom in our system. Crucially, the sequent \(\Gamma , (A)_{{ opt}_{\text {QCL}}(A)+k}\) has no models as well since A cannot be satisfied to a degree m with \({ opt}_{\mathcal {L}}(A)< m < \infty \).
-
\(({ do} r)\) is clearly sound.
-
\(({ do} l)\): Assume that a sequent of the form \(\Gamma , (A)_{{ opt}_{\text {QCL}}(A)+k} \vdash \Delta \) with \(k \in \mathbb {N}\) is valid. Since \(\Gamma , \bot \) has no models, \(\Gamma , \bot \vdash \Delta \) is valid.
-
\(({ do} r)\): Assume that a sequent \(\Gamma \vdash (A)_{{ opt}_{\text {QCL}}(A)+k},\Delta \) is valid. \((A)_{{ opt}_{\text {QCL}}(A)+k}\) cannot be satisfied, i.e., \(\Gamma \vdash \Delta \) is valid.
-
\((\lnot r)\) and \((\lnot l)\): Assume that a sequent of the form \(\Gamma \vdash (\lnot A)_1, \Delta \) is valid. Then every model of \(\Gamma \) is either a model of \((\lnot A)_1\) or of \(\Delta \). In other words, every model of \(\Gamma \) that is not a model of \((\lnot A)_1\) (i.e., is model of \({ cp}(A)\)) is a model of \(\Delta \). Therefore, every interpretation that is a model of both \(\Gamma \) and \({ cp}(A)\) must be a model of \(\Delta \). It follows that \(\Gamma , { cp}(A) \vdash \Delta \) is valid. Similarly for \(\Gamma , (\lnot A)_1 \vdash \Delta \).
-
\((\vee l)\) and \((\wedge l)\): Assume that a sequent of the form \(\Gamma , (A\vee B)_k \vdash \Delta \) is valid, with \(k \le { opt}_{\mathcal {L}}(A \vee B)\). We claim that then both \(\Gamma , (A)_k \vdash (B)_{<k}, \Delta \) and \(\Gamma , (B)_k \vdash (A)_{<k}, \Delta \) are valid. Assume to the contrary that \(\Gamma , (A)_k \vdash (B)_{<k}, \Delta \) is not valid (the other case is symmetric). Then, there is a model M of \(\Gamma \) and \((A)_k\) that is neither a model of \((B)_{<k}\) nor of \(\Delta \). But then M is also a model of \(\Gamma \) and \((A\vee B)_k\), but not of \(\Delta \), which contradicts the assumption that \(\Gamma , (A\vee B)_k \vdash \Delta \) is valid. Therefore, both \(\Gamma , (A)_k \vdash (B)_{<k}, \Delta \) and \(\Gamma , (B)_k \vdash (A)_{<k}, \Delta \) are valid. Similarly for a sequent of the form \(\Gamma , (A\wedge B)_k \vdash \Delta \).
-
\((\vee r)\) and \((\wedge r)\): Assume that a sequent of the form \(\Gamma \vdash (A\vee B)_k, \Delta \) is valid, with \(k \le { opt}_{\mathcal {L}}(A \vee B)\). We claim that then for all \(i < k\) the sequents \(\Gamma , (A)_i \vdash \Delta \) and \(\Gamma , (B)_i \vdash \Delta \) and \(\Gamma \vdash (A)_k, (B)_k, \Delta \) are valid. Assume by contradiction that there is an \(i < k\) s.t. \(\Gamma , (A)_i \vdash \Delta \) is not valid. Then, there is a model M of \(\Gamma \) and \((A)_i\) that is not a model of \(\Delta \). However, then M is a model of \(\Gamma \) but neither of \(\Delta \) nor of \((A \vee B)_k\) (as M satisfies \(A \vee B\) to degree \(i \ne k\)), which contradicts our assumption that \(\Gamma \vdash (A\vee B)_k, \Delta \) is valid. The case that there is an \(i < k\) s.t. \(\Gamma , (B)_i \vdash \Delta \) is not valid is symmetric. Finally, we assume that \(\Gamma \vdash (A)_k, (B)_k, \Delta \) is not valid. Then, there is a model M of \(\Gamma \) that is not a model of \((A)_k\), \((B)_k\) or \(\Delta \). Then, M is model of \(\Gamma \) but neither of \(\Delta \) nor of \((A \vee B)_k\), contradicting our assumption. Therefore, all sequents listed above must be valid. Similarly for a sequent of the form \(\Gamma \vdash (A\wedge B)_k, \Delta \).
-
\((\vec {\times }l_1)\) and \((\vec {\times }r_1)\): Assume that a sequent of the form \(\Gamma , (A \vec {\times }B)_k \vdash \Delta \) with \(k \le { opt}_{\text {QCL}}(A)\) is valid. Then \(\Gamma , (A)_k \vdash \Delta \) is also valid since \((A \vec {\times }B)_k\) and \((A)_k\) have the same models if \(k \le { opt}_{\text {QCL}}(A)\). Analogously for sequents of the form \(\Gamma \vdash (A \vec {\times }B)_k, \Delta \).
-
\((\vec {\times }l_2)\): Assume a sequent of the form \(\Gamma , (A \vec {\times }B)_{{ opt}_{\text {QCL}}(A) +l} \vdash \Delta \) is valid, with \(l \le { opt}_{\mathcal {L}}(B)\). We claim that the sequent \(\Gamma , (B)_l, \lnot A \vdash \Delta \) is then also valid. Indeed, if M is a model of \(\Gamma \), \((B)_l\) and \(\lnot A\), then it is also a model of \(\Gamma \) and \((A \vec {\times }B)_{{ opt}_{\text {QCL}}(A) +l}\). Hence, by assumption, M must be a model of \(\Delta \).
-
\((\vec {\times }r_2)\): Assume that a sequent of the form \(\Gamma \vdash (A \vec {\times }B)_{{ opt}_{QCL}(A) +l}, \Delta \) is valid, with \(l \le { opt}_{\mathcal {L}}(B)\). We claim that then also the sequents \(\Gamma \vdash \lnot A, \Delta \) and \(\Gamma \vdash (B)_l, \Delta \) are valid. Assume by contradiction that the first sequent is not valid. This means that there is a model M of \(\Gamma \) that is not a model of neither \(\lnot A\) nor of \(\Delta \). However, then M is a model of A and therefore satisfies \(A \vec {\times }B\) to a degree smaller than \({ opt}_{\text {QCL}}(A)\). This contradicts our assumption that \(\Gamma \vdash (A \vec {\times }B)_{{ opt}_{\text {QCL}}(A) +l}, \Delta \) is valid. Assume now that the second sequent is not valid, i.e., that there is a model M of \(\Gamma \) that is neither a model of \((B)_l\) nor of \(\Delta \). Then, M cannot be a model of \((A \vec {\times }B)_{{ opt}_{\text {QCL}}(A) +l}\) and we again have a contradiction to the assumption.
4 A Calculus for Preferred Model Entailment
-
\(\textbf{v} <_l \textbf{w}\) if there is some \(n \in \mathbb {N}\) such that \(\textbf{v}\) has more entries of value n and for all \(1 \le m < n\) both vectors have the same number of entries of value m.
-
\(\textbf{v} =_l \textbf{w}\) if, for all \(n \in \mathbb {N}\), \(\textbf{v}\) and \(\textbf{w}\) have the same number of entries of value n.
-
\(\textbf{v} <_i \textbf{w}\) if there is some \(n \in \mathbb {N}\) such that every entry in \(\textbf{w}\) with value n also has value n in \(\textbf{v}\), there is an entry in \(\textbf{v}\) with value n that has a value higher than n in \(\textbf{w}\), and for all \(1 \le m < n\) both vectors have exactly the same entries with value m.
-
\(\textbf{v} =_i \textbf{w}\) if \(\textbf{v} \not <_i \textbf{w}\) and \(\textbf{w} \not <_i \textbf{v}\).
5 Beyond QCL
5.1 Calculi for CCL
-
For \(\vec {\odot }l_1\), \(\vec {\odot }l_2\), and \(\vec {\odot }l_3\) this follows directly from the definition of \(\text {CCL}\).
-
\((\vec {\odot }r_1)\). Assume both premises are valid, i.e., every model of \(\Gamma \) is a model of \(\Delta \) or of \((A)_1\) and \((B)_k\) with \(k \le { opt}_{\text {CCL}}(B)\). By definition, any model that satisfies \((A)_1\) and \((B)_k\) satisfies \(A \vec {\odot }B\) to degree k. Thus, every model of \(\Gamma \) is a model of \(\Delta \) or of \((A \vec {\odot }B)_{k}\), which means the conclusion of the rule is valid.
-
\((\vec {\odot }r_2)\). Assume both premises are valid, i.e., every model of \(\Gamma \) is either a model of \(\Delta \) or of \((A)_1\) and \((\lnot B)_1\). By definition, any model that satisfies \((A)_1\) and does not satisfy B (and hence satisfies \((\lnot B)_1\)) satisfies \(A \vec {\odot }B\) to degree \({ opt}_{\text {CCL}}(B)+1\).
-
\((\vec {\odot }r_3)\). Assume that the premise is valid, i.e., every model of \(\Gamma \) is either a model of \(\Delta \) or of \((A)_l\) with \(1 < l \le { opt}_{\text {CCL}}(A)\). By definition, any model that satisfies \((A)_l\), regardless of what degree this model ascribes to B, satisfies \(A \vec {\odot }B\) to degree \({ opt}_{\text {CCL}}(B)+l\).
-
Assume that a sequent of the form \(\Gamma , (A \vec {\odot }B)_{k} \vdash \Delta \) is valid, with \(k \le { opt}_{\text {CCL}}(B)\). All models that satisfy \((A \vec {\odot }B)_{k}\) must satisfy A to a degree of 1 and B to a degree of k. Thus, \(\Gamma , (A)_1, (B)_k \vdash \Delta \) is valid. Similarly for the cases \(\Gamma , (A \vec {\odot }B)_{{ opt}_{\text {CCL}}(B)+1} \vdash \Delta \) and \(\Gamma , (A \vec {\odot }B)_{{ opt}_{\text {CCL}}(B)+l} \vdash \Delta \) with \(1 < l \le { opt}_{\text {CCL}}(A)\).
-
Assume that a sequent of the form \(\Gamma \vdash (A \vec {\odot }B)_k, \Delta \) is valid, with \(k \le { opt}_{\text {CCL}}(B)\). We claim that then \(\Gamma \vdash (A)_1, \Delta \) and \(\Gamma \vdash (B)_k, \Delta \) are valid. Assume, for the sake of a contradiction, that the first sequent is not valid. This means that there is a model M of \(\Gamma \) that is neither a model of \((A)_1\) nor of \(\Delta \). However, then M satisfies \(A \vec {\odot }B\) to a degree higher than \({ opt}_{\text {CCL}}(B)\). This contradicts the assumption that \(\Gamma \vdash (A \vec {\odot }B)_k, \Delta \) is valid. Assume now that the second sequent is not valid, i.e., that there is a model M of \(\Gamma \) that is neither a model of \((B)_k\) nor of \(\Delta \). Then M cannot be a model of \((A \vec {\odot }B)_{k}\), contradicting the assumption. Similarly for the cases \(\Gamma \vdash (A \vec {\odot }B)_{{ opt}_{\text {CCL}}(B)+1}, \Delta \) and \(\Gamma \vdash (A \vec {\odot }B)_{{ opt}_{\text {CCL}}(B)+l}, \Delta \) with \(1 < l \le { opt}_{\text {CCL}}(A)\).
5.2 Calculi for LCL
-
For \(\vec {\diamond }l_1\), \(\vec {\diamond }l_2\), and \(\vec {\diamond }l_3\) this follows directly from the definition of \(\text {LCL}\).
-
\((\vec {\diamond }r_1)\). Assume both premises are valid, i.e., every model of \(\Gamma \) is a model of \(\Delta \) or of \((A)_k\) and \((B)_l\) with \(k \le { opt}_{\text {LCL}}(A)\) and \(l \le { opt}_{\text {LCL}}(B)\). By definition, any model that satisfies \((A)_k\) and \((B)_l\) satisfies \(A \vec {\diamond }B\) to degree \((k-1) \cdot { opt}_{\text {LCL}}(B) + l\). Thus, every model of \(\Gamma \) is a model of \(\Delta \) or of \((A \vec {\diamond }B)_{(k-1) \cdot { opt}_{\text {LCL}}(B) + l}\), which means the conclusion of the rule is valid.
-
\((\vec {\diamond }r_2)\). Assume both premises are valid, i.e., every model of \(\Gamma \) is either a model of \(\Delta \) or of \((A)_k\) and \((\lnot B)_1\) with \(k \le { opt}_{\text {LCL}}(A)\). By definition, any model that satisfies \((A)_k\) and does not satisfy B (and hence satisfies \((\lnot B)_1\)) satisfies \(A \vec {\diamond }B\) to degree \({ opt}_{\text {LCL}}(A) \cdot { opt}_{\text {LCL}}(B) + k\).
-
\((\vec {\diamond }r_3)\). Analogous to \((\vec {\diamond }r_2)\).
-
Assume that a sequent of the form \(\Gamma , (A \vec {\diamond }B)_{m} \vdash \Delta \) is valid, with \(m = (k-1) \cdot { opt}_{\text {LCL}}(B) + l\) such that \(k \le { opt}_{\text {LCL}}(A)\) and \(l \le { opt}_{\text {LCL}}(B)\). Now assume some model satisfies \(\Gamma \), \((A)_k\), and \((B)_l\). Then M satisfies \(\Gamma \) and \((A \vec {\diamond }B)_{m}\), and, since \(\Gamma , (A \vec {\diamond }B)_{m} \vdash \Delta \) is valid, M also satisfies \(\Delta \). Thus, \(\Gamma , (A)_k, (B)_l \vdash \Delta \) is valid.The proofs for sequents of the form \(\Gamma , (A \vec {\diamond }B)_{{ opt}_{\text {LCL}}(A) \cdot { opt}_{\text {LCL}}(B) + k} \vdash \Delta \) and \(\Gamma , (A \vec {\diamond }B)_{{ opt}_{\text {LCL}}(A) \cdot { opt}_{\text {LCL}}(B) + { opt}_{\text {LCL}}(A) + l} \vdash \Delta \) are analogous.
-
Assume that a sequent of the form \(\Gamma \vdash (A \vec {\diamond }B)_{m}, \Delta \) is valid, with \(m = (k-1) \cdot { opt}_{\text {LCL}}(B) + l\) such that \(k \le { opt}_{\text {LCL}}(A)\) and \(l \le { opt}_{\text {LCL}}(B)\). We claim that then \(\Gamma \vdash (A)_k, \Delta \) and \(\Gamma \vdash (B)_l, \Delta \) are valid. Assume, for the sake of a contradiction, that the first sequent is not valid. This means that there is a model M of \(\Gamma \) that is neither a model of \((A)_k\) nor of \(\Delta \). Following Definition 8, M must satisfy \(A \vec {\diamond }B\) to some degree other than m. This contradicts the assumption that \(\Gamma \vdash (A \vec {\diamond }B)_{m}, \Delta \) is valid. Assume now that the second sequent is not valid, i.e., that there is a model M of \(\Gamma \) that is neither a model of \((B)_l\) nor of \(\Delta \). Again, this means that M satisfies \(A \vec {\diamond }B\) to some degree other than m, and this would contradict our assumption that \(\Gamma \vdash (A \vec {\diamond }B)_{m}, \Delta \) is valid. Thus, both \(\Gamma \vdash (A)_k, \Delta \) and \(\Gamma \vdash (B)_k, \Delta \) are valid and \(\Gamma \vdash (A \vec {\diamond }B)_{m}, \Delta \) is provable.The proofs for sequents of the form \(\Gamma \vdash (A \vec {\diamond }B)_{{ opt}_{\text {LCL}}(A) \cdot { opt}_{\text {LCL}}(B) + k}, \Delta \) and \(\Gamma \vdash (A \vec {\diamond }B)_{{ opt}_{\text {LCL}}(A) \cdot { opt}_{\text {LCL}}(B) + { opt}_{\text {LCL}}(A) + l}, \Delta \) are analogous.