d4-conf-aaai-2018-0838 (d4-conf-aaai-2018-0838)

Fix affine logic \(L\in\{\mathrm{MLL},\mathrm{MALL}\}\). An instance gives a finite type set \(T\), each type's endowment multiset \(E_t\) and goal formula \(g_t\), rational population masses \(\mu_t\) with \(\sum_{t\in T}\mu_t=1\), and rational coalition masses \(x_t\) with \(0\le x_t\le\mu_t\) and \(\sum_t x_t>0\). Decide whether there are finitely many nonzero integer templates \(k^j\in\mathbb{N}^T\), each with an affine-\(L\) proof \(\biguplus_{t\in T} E_t^{\uplus k^j_t}\vdash\bigotimes_{t\in T}g_t^{\otimes k^j_t}\), and weights \(\lambda_j\in\mathbb{R}_{\ge0}\) such that \(x_t=\sum_j\lambda_j k^j_t/\sum_{u\in T}k^j_u\) for every \(t\in T\).

Fix \(\mathcal L\in\{\mathrm{MLL},\mathrm{MALL}\}\), interpreted as classical propositional affine linear logic, with units and weakening but without contraction or exponentials.
A society is given by its support \(T\): the list of its \(\tau=|T|\) types with positive binary rational masses \(\mu_t\), where \(\sum_t\mu_t=1\); \(\tau\) is the support size, not the number of possible types.
Each type has one goal formula \(g_t\) and a finite, possibly empty, endowment multiset \(E_t\), explicitly listing all formula occurrences. The input also gives binary rational coalition masses \(0\le x_t\le\mu_t\) with \(\sum_t x_t>0\).
A winning template is \(k\in\mathbb Z_{\ge0}^{T}\setminus\{0\}\) such that \(\biguplus_{t\in T}E_t^{\uplus k_t}\vdash_{\mathcal L}\bigotimes_{t\in T}g_t^{\otimes k_t}\). Here the powers denote repeated multiset union and tensor product; a zero tensor power is \(1\). Weakening permits unused endowments, and each template member requires its own goal occurrence.
Call the coalition feasible if there exist \(r\ge1\), winning templates \(k^1,\ldots,k^r\), and real weights \(\lambda_j\ge0\) satisfying \(x_t=\sum_{j=1}^{r}\lambda_j k_t^j/(\sum_{u\in T}k_u^j)\) for every \(t\). This requires a finite exact representation, without taking a closure; template sizes are unrestricted.
Let \(m\) be the number of distinct propositional atoms and \(L\) the total input bit length; state running times in \(m,\tau,L\).

For each fixed \(\mathcal L\), is deciding coalition feasibility solvable in polynomial time, or is it \(\mathrm{NP}\)-hard?

For finite societies with one goal per agent, deciding whether a specified nonempty coalition is winning is \(\mathrm{NP}\)-complete for affine \(\mathrm{MLL}\) and \(\mathrm{PSPACE}\)-complete for affine \(\mathrm{MALL}\). [Source](https://troquard.bitbucket.io/PAPERS/Tr18aaai.pdf)
No result settling this exact finite-template mass formulation was located in the literature search.

Proven result. Coalition feasibility is \(\mathrm{NP}\)-hard for both logics. For affine \(\mathrm{MALL}\), it is moreover \(\mathrm{PSPACE}\)-hard. These statements hold for every prescribed constant support size \(\tau\geq 1\), with nonempty atomic endowments and \(x_t=\mu_t>0\) for every type.

Empty endowments already allow a theoremhood reduction. The proof below establishes hardness with nonempty endowments and verifies soundness for every finite template size.

Encoding the source problem. Fix \(\mathcal L\in\{\mathrm{MLL},\mathrm{MALL}\}\). We use the finite-society hardness stated in the question: winning-coalition recognition with one goal per agent is \(\mathrm{NP}\)-complete for affine \(\mathrm{MLL}\), and \(\mathrm{PSPACE}\)-complete for affine \(\mathrm{MALL}\). In the affine setting, a specified coalition is winning exactly when its combined endowments entail the tensor of its goals. These are Lemma 17 and Proposition 18 of [Troquard’s paper](https://troquard.bitbucket.io/PAPERS/Tr18aaai.pdf).

Given such a source instance with specified nonempty coalition \(C\), let
\[ \Gamma=\biguplus_{i\in C}E_i,\qquad A=\bigotimes_{D\in\Gamma}D,\qquad B=\bigotimes_{i\in C}g_i, \]
where \(A=1\) if \(\Gamma\) is empty. Define \(F=A\multimap B\), with linear implication abbreviating \(A^\perp\parr B\).

Then
\[ C\text{ is winning}\quad\Longleftrightarrow\quad \Gamma\vdash_{\mathcal L}B \quad\Longleftrightarrow\quad \vdash_{\mathcal L}F. \]

Here is the justification of the second equivalence. From \(\Gamma\vdash B\), tensor-left combines the antecedent into \(A\), and implication-right yields \(\vdash A\multimap B\). For an empty antecedent, first use unit-left to obtain \(1\vdash B\). Conversely, implication-left and identity give \(A,A\multimap B\vdash B\). Cutting with \(\vdash F\) gives \(A\vdash B\); cutting this with the tensor of the identity proofs \(\Gamma\vdash A\) gives \(\Gamma\vdash B\). When \(\Gamma\) is empty, use \(\vdash1\).

Identity, these connective rules, and admissible cut are available in both specified classical affine calculi.

The target society and the replication argument. Choose any fixed integer \(s\geq1\), and choose pairwise distinct fresh atoms \(q_1,\ldots,q_s\), none occurring in \(F\). Construct the support \(T=\{1,\ldots,s\}\) by setting
\[ E_t=\{q_t\},\qquad g_t=q_t\otimes F,\qquad \mu_t=x_t=\frac1s. \]

These data satisfy all input requirements. In particular, every endowment is nonempty, every type has one goal, and the coalition has total mass \(1\).

We prove the following statement for every \(k\in\mathbb Z_{\geq0}^{T}\setminus\{0\}\):
\[ k\text{ is winning}\quad\Longleftrightarrow\quad \vdash_{\mathcal L}F. \]

For the forward direction, write
\[ Q(k)=\biguplus_{t\in T}\{q_t\}^{\uplus k_t}, \qquad G(k)=\bigotimes_{t\in T}(q_t\otimes F)^{\otimes k_t}. \]
Winning means \(Q(k)\vdash G(k)\).

Because \(k\neq0\), the formula \(G(k)\) contains at least one displayed occurrence of \(F\). Starting with \(F\vdash F\), left weakening supplies all other atomic and \(F\)-components of \(G(k)\). Tensor-left then combines them, with unit-left handling zero powers, to obtain \(G(k)\vdash F\). Cutting gives
\[ Q(k)\vdash F. \]

Now uniformly substitute \(1\) for every \(q_t\). Uniform formula substitution preserves derivability: connective rules remain instances of the same rules, and substituted identity axioms remain derivable identities. The substitution sends \(q_t^\perp\) to \(1^\perp=\bot\), so it also respects linear negation. Freshness ensures that \(F\) is unchanged. Consequently,
\[ \underbrace{1,\ldots,1}_{\sum_t k_t\text{ occurrences}}\vdash F. \]
Cutting each antecedent unit against \(\vdash1\) yields \(\vdash F\).

For the reverse direction, suppose \(\vdash F\). Tensor-right applied to \(q_t\vdash q_t\) and \(\vdash F\) gives \(q_t\vdash q_t\otimes F\). Combining the required number of these proofs by tensor-right, and using \(\vdash1\) for zero powers, proves \(Q(k)\vdash G(k)\).

Thus unrestricted replication cannot create a winning template when \(F\) is unprovable.

Exact feasibility and complexity. If \(\vdash F\), take the single winning template \(k=(1,\ldots,1)\), with weight \(\lambda=1\). Its normalized coordinates are exactly \(1/s=x_t\), so this is a finite exact representation.

Conversely, feasibility supplies winning templates. By the statement just proved, any such template implies \(\vdash F\). Therefore
\[ C\text{ is winning in the source instance} \quad\Longleftrightarrow\quad x\text{ is feasible in the constructed society}. \]
No closure or limiting argument is involved.

Let \(L_0\) be the source bit length, and let \(m_0\) count the atoms occurring in its relevant endowments and goals. The construction has
\[ m=m_0+s,\qquad \tau=s,\qquad L=O\!\left(s\bigl(L_0+\log(s+1)\bigr)\right). \]
For each prescribed constant \(s\), it can be implemented in \(O(L_0^2)\) bit operations, with \(L=O(L_0)\). Hence it is a polynomial-time many-one reduction.

Applying the source hardness separately proves the claimed \(\mathrm{NP}\)-hardness for affine \(\mathrm{MLL}\) and \(\mathrm{PSPACE}\)-hardness for affine \(\mathrm{MALL}\). In particular, an algorithm polynomial in \(m,\tau,L\) would imply \(\mathrm P=\mathrm{NP}\) in the first case and \(\mathrm P=\mathrm{PSPACE}\) in the second.

⟨structured verdict parsed — rendered above⟩

The argument is correct and resolves the requested hardness alternative for both logics. No major or minor mathematical issues were found.

• Source problem and cited result.

The prover states the source problem precisely: winning-coalition recognition for finite societies with one goal per agent, using the corresponding classical affine logic. Lemma 17 identifies winning with entailment from the combined endowments to the tensor of the coalition’s goals; Proposition 18 gives the stated completeness results. Both citations match [Troquard’s paper](https://troquard.bitbucket.io/PAPERS/Tr18aaai.pdf). The affine setting, formula language, and goal multiplicities agree with the task. The source hardness also applies to nonempty specified coalitions: the paper’s hardness reduction uses a singleton coalition.

• Encoding the source instance as theoremhood.

The definitions of \(\Gamma\), \(A\), and \(B\) retain every relevant formula occurrence. Since the source coalition is nonempty, \(B\) contains at least one goal occurrence. The formula \(F=A\multimap B\), interpreted as \(A^\perp\parr B\), belongs to the same logical fragment.

Both directions of \(\Gamma\vdash B\) if and only if \(\vdash F\) are justified by the stated rules. Tensor-left combines the antecedent without duplicating or discarding required occurrences. The converse uses identity, implication-left, and admissible cut with matching cut formulas. The empty-endowment case is explicitly handled using \(A=1\), unit-left, and \(\vdash1\).

• Validity of the target input.

For each prescribed integer \(s\geq1\), the construction gives exactly \(s\) distinct types. Fresh, pairwise distinct atoms distinguish their endowments and goals. Each endowment is a nonempty singleton, and each type has exactly one goal formula.

The masses \(\mu_t=x_t=1/s\) are positive binary rationals, satisfy the coordinate bounds, and sum to \(1\). The construction therefore satisfies every input restriction, including the case \(s=1\).

• Extracting theoremhood from an arbitrary winning template.

The proof quantifies over every finite nonzero template \(k\), with no bound on its coordinates. Nonzeroness ensures that \(G(k)\) contains an occurrence of \(F\).

The derivation of \(G(k)\vdash F\) is valid: identity provides the selected occurrence, weakening supplies the other antecedent components, and tensor-left reconstructs the prescribed tensor structure. Unit-left handles zero tensor powers. Cutting with \(Q(k)\vdash G(k)\) yields \(Q(k)\vdash F\). This step uses weakening but no contraction.

• Fresh-atom substitution and removal of units.

The substitution argument is correctly specified. Replacing each \(q_t\) by \(1\), and its negation by \(\bot\), respects linear negation. Logical and structural rules remain valid rule instances; substituted identity sequents remain derivable. Freshness guarantees that \(F\) is unchanged.

The resulting antecedent consists of finitely many occurrences of \(1\). Each can be removed by the stated cut against \(\vdash1\), leaving \(\vdash F\). Thus the forward implication remains sound for every finite template size, including templates whose coordinates contain zeros.

• Constructing winning templates from theoremhood.

Given \(\vdash F\), tensor-right combines it with \(q_t\vdash q_t\) to obtain the required individual goal. Repeating this construction for every template member and combining the proofs by tensor-right yields exactly \(Q(k)\vdash G(k)\).

Reusing the closed derivation of \(F\) in separate proof branches does not require contraction on resources. Zero powers are handled by \(\vdash1\). The claimed equivalence between template winning and theoremhood is established in both directions.

• Finite exact feasibility.

When \(\vdash F\), the template \(k=(1,\ldots,1)\) with weight \(1\) has normalized coordinates exactly \(1/s=x_t\). This is an admissible finite exact representation.

Conversely, feasibility requires at least one winning template because the definition specifies \(r\geq1\). Every such template implies \(\vdash F\), independently of its weight. Hence allowing zero weights introduces no loophole. Neither direction uses closure, approximation, or limits.

• Encoding size and complexity conclusion.

The atom count \(m=m_0+s\) and support size \(\tau=s\) are correct. Explicitly copying \(F\) into each goal gives the stated size bound \(L=O(s(L_0+\log(s+1)))\). For fixed \(s\), the construction has linear output length and can be performed within the stated polynomial time bound.

The established equivalence is therefore a polynomial-time many-one reduction. It proves \(\mathrm{NP}\)-hardness for affine \(\mathrm{MLL}\) and \(\mathrm{PSPACE}\)-hardness, hence also \(\mathrm{NP}\)-hardness, for affine \(\mathrm{MALL}\), even at every prescribed constant support size. The conditional consequences for algorithms polynomial in \(m,\tau,L\) follow correctly. No upper complexity bound is established or needed to answer the requested hardness alternative.

No additional clarification or repair is required.

⟨structured verdict parsed — rendered above⟩