Dependence logic with generalized quantifiers is strictly more expressive than first-order logic with the same quantifiers, so completeness is typically obtained only for first-order consequences. For the special generalized quantifier “there exist uncountably many” \((Q^1)\), earlier axiomatizations achieved \(FO(Q^1)\)-completeness by adding a Skolem rule that introduces new function symbols. In this paper we show that the Skolem step can be avoided. We present a natural deduction system for dependence logic with \(Q^1\) and its dual that stays in the original signature and prove that it is sound and complete for \(FO(Q^1)\)-consequences. The key idea is to replace Skolemization by a team-based uncountable choice rule that directly reflects the team-semantics clause for \(Q^1\).
Dependence logic with generalized quantifiers is strictly more expressive than first-order logic with the same quantifiers, so completeness is typically obtained only for first-order consequences. For the special generalized quantifier “there exist uncountably many” \((Q^1)\), earlier axiomatizations achieved \(FO(Q^1)\)-completeness by adding a Skolem rule that introduces new function symbols. In this paper we show that the Skolem step can be avoided. We present a natural deduction system for dependence logic with \(Q^1\) and its dual that stays in the original signature and prove that it is sound and complete for \(FO(Q^1)\)-consequences. The key idea is to replace Skolemization by a team-based uncountable choice rule that directly reflects the team-semantics clause for \(Q^1\).
