more from this thinker     |     more from this text

Single Idea 13249

[filed under theme 4. Formal Logic / E. Nonclassical Logics / 2. Intuitionist Logic ]

Full Idea

The inference of 'distribution' (∀x)(A v B) |- (∀x)A v (∃x)B) is valid in classical logic but invalid intuitionistically. It is straightforward to construct a 'stage' at which the LHS is true but the RHS is not.

Gist of Idea

(∀x)(A v B) |- (∀x)A v (∃x)B) is valid in classical logic but invalid intuitionistically

Source

JC Beall / G Restall (Logical Pluralism [2006], 6.1.2)

Book Ref

Beall,J/Restall,G: 'Logical Pluralism' [OUP 2006], p.64

A Reaction

This seems to parallel the iterative notion in set theory, that you must construct your hierarchy. All part of the general 'constructivist' approach to things. Is some kind of mad platonism the only alternative?

The 15 ideas with the same theme [logic which uses 'provable' in place of 'true']:

18832 Mathematical statements and entities that result from an infinite process must lack a truth-value [Dummett]
18073 Dummett says classical logic rests on meaning as truth, while intuitionist logic rests on assertability [Dummett, by Kitcher]
18122 Classical interdefinitions of logical constants and quantifiers is impossible in intuitionism [Bostock]
18074 Intuitionists rely on assertability instead of truth, but assertability relies on truth [Kitcher]
15430 Is classical logic a part of intuitionist logic, or vice versa? [Burgess]
15431 It is still unsettled whether standard intuitionist logic is complete [Burgess]
13715 You can employ intuitionist logic without intuitionism about mathematics [Sider]
18789 Intuitionist logic looks best as natural deduction [Mares]
18790 Intuitionism as natural deduction has no rule for negation [Mares]
13249 (∀x)(A v B) |- (∀x)A v (∃x)B) is valid in classical logic but invalid intuitionistically [Beall/Restall]
8708 Double negation elimination is not valid in intuitionist logic [Friend]
17925 Showing a disproof is impossible is not a proof, so don't eliminate double negation [Colyvan]
17926 Rejecting double negation elimination undermines reductio proofs [Colyvan]
18798 It is the second-order part of intuitionistic logic which actually negates some classical theorems [Rumfitt]
18799 Intuitionists can accept Double Negation Elimination for decidable propositions [Rumfitt]