0

Have propositional calculi with independence-related features been named and studied? Are they trivial as logical systems? Are there any interesting properties that they either gain or lose relative to ordinary propositional calculi?

Independence-friendly logic as described here introduces a new kind of stanza in an expression headed by a quantifier, a set of definitely-unused variables. It's also described in this question and its answer.

The Wikipedia article has a compact notation for the similar-but-distinct slash logic, reproduced and explained below. I think independence-friendly logic can be implemented on top of slash logic by adding implicit slashes to prevent a player from being able to see their own previous moves (in a certain sense).

$$ \exists w / \{ x_1, x_2, \cdots, x_n \} \mathop. \varphi \;\; \text{is well-formed if and only if none of $\{x_1, x_2, \cdots x_n \}$ appear free in $\varphi$} $$

There's a nice duality between quantifiers, which introduce variables into the current scope and $/$, which removes them from the current scope. The syntax can also be extended to allow connectives to remove variables which name individuals (e.g. $\varphi \; (\land / x) \; \psi$).

It seems only natural to try to extend this to propositional calculus by constraining things that can appear in both subexpressions of a connective. Here's a first stab at doing it, with upper and lower bounds represented by $\land_V$ for lower bounds and $\land^V$ for upper bounds. Because propsitional calculus does not normally have quantifiers, I'm changing the syntax and well-formedness conditions a bit so that connectives can bear upper or lower bounds on which variables can exist in their subexpressions.

$$ \varphi \land_{\{x_1, x_2, \cdots x_n \}} \psi \;\; \text{is well-formed if and only if $\{x_1, \cdots, x_n\} \subset \text{FV}(\varphi) \cap \text{FV}(\psi)$} $$

$$ \varphi \land^{\{x_1, x_2, \cdots x_n\}} \psi \;\; \text{is well-formed if and only if $\text{FV}(\varphi) \cap \text{FV}(\psi) \subset \{x_1, \cdots, x_n\} $} $$

In particular, this makes it easy to express things like the side conditions this question directly in the syntax.

$$ F \lor^{\emptyset} G \;\;\text{if and only if}\;\; \text{$F$ or $G$} \;\;\; \text{where $F$ and $G$ are well-formed formulas}$$

Have such systems been studied?

Greg Nisbet
  • 11,657
  • What is the semantics - just usual conjunction/disjunction assuming the relevant variable use condition is satisfied? – Noah Schweber Jan 19 '21 at 23:21
  • @NoahSchweber yes. That's just meant to be an example of one thing one might do to "control variable sharing" or something similar in a propositional system. – Greg Nisbet Jan 19 '21 at 23:23
  • 2
    I don't really see a connection with independence, though. The thing that makes independence-friendly logics work is that when we turn to the game semantics, there are board-determining moves (= moves which determine what the opponent's set of legal plays are) and auxiliary moves (= the others). The auxiliary moves are supplied by the quantifiers, and any time we have auxiliary moves we get notions of limited-information strategies (since the players don't have to see all the auxiliary moves in order to know what they may legally do). – Noah Schweber Jan 19 '21 at 23:42
  • 2
    But in propositional logic games, all moves are board-determining: we just pick subformulas. So I don't see any room for propositional independence. This seems more about syntactic control than independence in the sense of independence-friendly logic. But maybe I'm missing something: what sort of overall semantic picture do you have in mind? – Noah Schweber Jan 19 '21 at 23:42
  • Do things change if we add quantifiers over truth values? I didn't have an overall semantic picture in mind, the motivation for me was fuzzy and sorta syntactic in nature ... namely I have a gut feeling that limiting unrestricted variable reuse might produce an interesting system. – Greg Nisbet Jan 20 '21 at 00:00

0 Answers0