disjunction property

The disjunction property (or DP for short) is the meta-statement in logic, which says

if $\\vdash A\\lor B$ , then $\\vdash A$ or $\\vdash B$ .

DP fails for classical propositional logic, but is true for intuitionisitc propositional logic. In fact, there are infinitely many intermediate logics between classical and intuitionistic logics that satisfy DP. Furthermore, there are no intermediate logics maximal with respect to satisfying DP. With respect to predicate logic, DP is ture in first order intuitionistic logic without function symbols.

There is also a modal version of the disjunction property (or MDP for short), which states:

if $\\vdash\\square A\\lor\\square B$ , then $\\vdash A$ or $\\vdash B$ .

It is not hard to see that MDP holds in normal modal logics K, T, K4, S4, and GL, and fails in D, B, and S5.

Remark. In predicate logic, there is also a sort of infinitary analog of DP called the existence property (EP), or the witness property, which states:

if $\\vdash\\exists xP(x)$ , then there is a closed term $t$ such that $\\vdash P(t)$ .

Like DP, EP fails in classical first-order logic, but true in first-order intuitionistic logic without function symbols and with at least one constant symbol.

单词	DisjunctionProperty
释义	disjunction property The disjunction property (or DP for short) is the meta-statement in logic, which says if $\\vdash A\\lor B$ , then $\\vdash A$ or $\\vdash B$ . DP fails for classical propositional logic, but is true for intuitionisitc propositional logic. In fact, there are infinitely many intermediate logics between classical and intuitionistic logics that satisfy DP. Furthermore, there are no intermediate logics maximal with respect to satisfying DP. With respect to predicate logic, DP is ture in first order intuitionistic logic without function symbols. There is also a modal version of the disjunction property (or MDP for short), which states: if $\\vdash\\square A\\lor\\square B$ , then $\\vdash A$ or $\\vdash B$ . It is not hard to see that MDP holds in normal modal logics K, T, K4, S4, and GL, and fails in D, B, and S5. Remark. In predicate logic, there is also a sort of infinitary analog of DP called the existence property (EP), or the witness property, which states: if $\\vdash\\exists xP(x)$ , then there is a closed term $t$ such that $\\vdash P(t)$ . Like DP, EP fails in classical first-order logic, but true in first-order intuitionistic logic without function symbols and with at least one constant symbol.
随便看	PermutationModel permutation model PermutationNotation permutation notation PermutationOperator permutation operator PermutationPattern permutation pattern PermutationRepresentation permutation representation PerpendicularBisector perpendicular bisector PerpendicularityInEuclideanPlane perpendicularity in Euclidean plane PerrinPseudoprime Perrin pseudoprime PerrinSequence Perrin sequence PerronFamily Perron family PerronFrobeniusTheorem Perron-Frobenius theorem p.ERROR(\tmspace)-.1667emv.⁡(1/x) is a distribution of first order PersistenceOfAnalyticRelations persistence of analytic relations