Generalize to sets as signs

[rzach]

One thing that would be nice to have would be a way to generate systems not just for the signs {v_1}, ..., {v_n} but for any set of signs. How hard would that be to do?

[gsalzer]

Rules where the formula in the conclusion appears with an arbitrary sign are straight-forward: Select all interpretations/distributions where the operator/quantifier yields a truth value not in the sign and start rule construction from there. The premises, however, would look the same as they do now, i.e., they are singleton sets, or, if you collect them for each formula, may be arbitrary sets.

If you want to fix a system of signs beforehand (say, the up-sets in a lattice) and search for rules that use these signs exclusively, the situation seems unclear. In general, there will be operators and systems of signs where no rules exist. For lattice-based operators and quantifiers, there are always rules using the up- and down-sets wrt to the lattice. Are you aware of further results in this direction that might help?

The underlying problem seems to be the question, whether the sets of truth values occurring in the premises of the constructed rules can be represented as the union or intersection of signs present in the given system of signs. A literal S:phi in a clause S:phi v C can be rewritten as S1:phi v S2:phi, where S1 union S2 = S, but also as (S1:phi v C) & (S2:phi v C) where S1 intersection S2 = S. In this sense, S can be reduced to the signs S1 and S2 (and maybe some more) which are chosen from the system of signs.

[rzach]

In the Studia Logica paper we required that a set of labels allows the expression of any single truth value as a finite intersection of signs. So in terms of possibility of producing rules, the following should work to find the CNF for a sign S = {w_1,...,_w_n}:

• Express the condition Op(A_1,..., A_n)^S as a disjunction of conjunctions of A_i^{v}.
• Translate to sign system by writing A^{v} as A^S_1 /\ ... /\ A^S_k for {v} = S_1 \cap ... \cap S_k.
• Turn DNF into optimized CNF.
• Optimize individual clauses/premises (e.g., replace A^S \/ A^T by A^S if T \subseteq S).