Intusionisme
Intusionisme
Intusionisme
Intuitionism
Christian Wthrich
http://philosophy.ucsd.edu/faculty/wuthrich/ 124 Philosophy of Mathematics Winter 2012
Christian Wthrich
Topic 7
Characterization (Intuitionism) Intuitionism in or about mathematics is a revisionary form of mathematical constructivism which considers the essence of mathematics to be exhausted by our constructive mental activity, i.e., mental constructions governed by self-evident laws, rather than be constituted by the analytical reasoning involving the formal manipulation of linguistic characters, perhaps revealing the existence and the constitution of independently existing mathematical objects and enabling and governing their application.
Christian Wthrich
Topic 7
Similarly, all laws of classical logic which rely on LEM are rejected in IL. Example: law of double negation elimination in CL, which states that for any proposition , IL: , but To see this, suppose that one can construct a contradiction from , in which case a reductio inference (admissible both in CL and IL) yields . CL: by double negation elimination, one can also infer IL: this is unwarranted, unless you have independent reason for, i.e., a mental construction of, (e.g., to derive a contradiction from nPn does not amount to a construction of a number n such that Pn)
Christian Wthrich
Topic 7
Brouwers intuitionism
Carl Posy, Intuitionism and philosophy, in Shapiro (ed.), The Oxford Handbook of Philosophy of Mathematics and Logic, Oxford University Press (2005), 318-355.
of interest to philosophers because his mathematics rests upon a unique epistemology, a special ontology, and an underlying picture of intuitive mathematical consciousness. (Posey, 319) Shapiro: strong Kantian background in Brouwer, recognizes Kant as precursor Brouwer developed intuitionism in response to Hilberts dominating formalism (practice of) nitary arithmetic: not much difference between intuitionism and formalism but they differ regarding the source of the exact validity of maths; for the intuitionist, its the human intellect, while for formalism, only on paper
Christian Wthrich Topic 7
mathematical truths not analytic (i.e., true by virtue of meaning), but synthetic (like Kant) and a priori (against Mill) antirealism in ontology and truth value (he considered realism incorrect and outdated) maths is mind-dependent, its essence is idealized mental construction maths concerns active role of mind in structuring human experience but Brouwer rejected Kantian view of geometry, particularly his view of space instead: proposal to found all of mathematics on a Kantian view of time (Shapiro, 176) (instead of geometry on the forms of our spatial perception)
Christian Wthrich
Topic 7
i.e., base natural numbers on forms of temporal perception when we apprehend world as linearly ordered sequence of distinct moments discrete moments give rise to natural numbers; but since our intuition also unites the continuous and discrete and gives rise immediately to the intuition of the linear continuum (177), we also obtain the rational and the real numbers then do analytic geometry based on R even geometry is ultimately grounded in our temporal perceptions
Christian Wthrich
Topic 7
practice of mathematics ows from introspection of ones mind (180): The... point of view that there are no non-experienced truths... has found acceptance with regard to mathematics much later than with regard to practical life and to science. Mathematics rigorously treated from this point of view, including deducing theorems exclusively by means of introspective construction, is called intuitionistic mathematics. (Brouwer 1948, 90; cited after Shapiro, 180) in maths, to be is to be constructed incorrect to believe in existence of unknowable truths
Christian Wthrich
Topic 7
right before Brouwer enters the stage, innity came of age in mathematics (Weierstrass, Dedekind, Cantor) Brouwer: there is a problem at the heart of these accounts of innity... Problem of the continuum [T]he new set-theoretic penchant toward arbitrary sets and sequences; sets that cannot be described and sequences whose elements cannot be calculated. (Posey 322) So what was required was a novel account of the mathematical continuum on an epistemically sound basis.
Christian Wthrich
Topic 7
On the mathematical side [Brouwer] provided a constructive theory of nite mathematics together with a new set theory encompassing both discrete and continuous innities. And philosophically he anchored this with special epistemological and ontological doctrines, doctrines that themselves derived from an overall phenomenological outlook. (Posey, 322)
Christian Wthrich
Topic 7
LEM amounts to an inacceptable sort of omniscience (every proposition can be proved or be reduced to absurdity) Brouwer also rejected the use of impredicative denitions as we cannot construct an object from a pre-existing collection containing that entity to be constructed Shapiro: Brouwers conception of the nature of mathematics and its objects leads to theorems that are (demonstrably) false in classical mathematics. (181), and vice versa Example: it implied that functions from R to R are, by necessity, uniformly continuous (i.e., there are no discontinuous functions on R as they would entail instances of LEM!) The resulting mathematics is quite radically different from its classical counterpart (which have some limited use in the sciences). divorce between maths and empirical science
Christian Wthrich Topic 7
Separable mathematics
separable = discrete maths produced by predicative sequential process, parallel to Cantors theory up to 0 conict with Cantors theory of higher cardinals (because he accepts reductio proofs) Brouwer has no bones with Cantors proof that the species (roughly, set) of all (constructible) innite sets of naturals is not countable but we havent thereby constructed a cardinal greater than 0 , so this species denumerably unnished
Christian Wthrich
Topic 7
while at the countable level, Brouwer stays very close to Cantor, he departs from classical mathematics, however, in his theory of the continuum continuum built up from choice sequences which may or may not be fully determinate set theory: species (roughly, sets), spreads (constructive sets of sequences), fans (= a spread with only nitely many successors to each admissible nite sequence, 325) emerging intuitionistic mathematics (a) sometimes weaker than, (b) sometimes renement of, (c) sometimes inconsistent with, classical mathematics
Christian Wthrich
Topic 7
weak form: a function cannot be both total (i.e., have a value at every point in its domain) and discontinuous at some point in its domain (ibid.) strong form: every function that is total on R[0,1] is continuous. (ibid.)
Christian Wthrich Topic 7
Brouwers philosophy:
The phenomenology of intuition and constructivity
General phenomenology: individual elements of primordial consciousness we discern an order among them (temporal) attenuated mental sequences, which form building blocks of the subjects awareness of ordinary empirical objects so mind produces sequences and correlates them, willfully imposing structure on roil of consciousness
Christian Wthrich
Topic 7
Phenomenology of mathematics: rst act of intuitionism: breaking up of one primordial element into two and abstracting away from all particular two-ities to get empty form of common substratum of two-ities; forms phenomenological basis of arithmetical identities in particular, gives discrete innity and the continuum second act of intuitionism: generates innite entities, either through choice sequences, or more abstractly by means of equivalence relations, enables more abstract constructions
Christian Wthrich
Topic 7
Christian Wthrich
Topic 7
Negative doctrines
Intolerance of classical mathematics: mathematical truths are necessary, so since classical mathematics contradicts some of these, it cant be accepted on pain of inconsistency So classical maths in fully meaningful, but necessarily false. Logic: LEM only valid at nitary stage; given the incompleteness of innite mathematics, however, LEM cannot be valid there Importantly: logic follows ontology, but cannot lead! Language: see next slide
Christian Wthrich
Topic 7
logicism and formalism exhibit a focus on logic and language of maths Alberto Coffa (1991): semantic tradition; Michael Dummett (much earlier): linguistic turn Brouwer resisted that tendency, as he considered language as only the imperfect medium for communicating our mental constructions and logic as being subsidiary to mathematics, encoding the basic self-evident rules of our mental constructions
Christian Wthrich
Topic 7
in... construction... neither the ordinary language nor any symbolic language can have any other rle that that of serving as a non-mathematical auxiliary, to assist the mathematical memory or to enable different individuals to build up the same [construction]. For this reason the intuitionist can never feel assured of the exactness of a mathematical theory by such guarantees as the proof of its being non-contradictory, the possibility of dening its concepts by a nite number of words... or the practical certainty that it will never lead to a misunderstanding in human relations. (1912, 81; cited after Shapiro, 185)
Christian Wthrich
Topic 7
Christian Wthrich
Topic 7
Heyting sometimes went as far as claiming that mathematics is empirical (although not along Millean lines): The afrmation of a proposition is not itself a proposition; it is the determination of an empirical fact, viz., the fulllment of the intention expressed by the proposition. (1931, 59; Shapiro, ibid.) Intuitionistic mathematics consists... in mental constructions; a mathematical theorem expresses a purely empirical fact, namely the success of a certain construction. (1956, 8; ibid.) But: Brouwers own Kantianism is not metaphysically neutral!
Christian Wthrich
Topic 7
Heytingean intuitionism
developed a rigorous axiomatization of intuitionistic logic, Heyting predicate calculus Heyting: language of CL (and maths based on it) best understood in terms of objective truth conditions, language of IL (and maths based on it) in terms of proof conditions knowing a proposition means to produce a constructive proof of it Heyting (1930) gives a semantics from which it is clear that many instances of LEM are inadmissible Heyting semantics (Shapiro), or often Brouwer-Heyting-Kolmogorov interpretation, or BHK interpretation, which is supposed to capture the meaning of the logical symbols in the language in which IL is cast
Christian Wthrich Topic 7
Intuitionistic logic
for details, cf. Posey 336f
IL: full language of rst-order logic, includes ten axiom schemata IL contains three inference rules: modus ponens, -introduction, -elimination larger number necessary because logical particles cannot be interdened through the DeMorgan equivalences, so each symbol comes separately with an axiom but rst nine axiom schemata are equivalent to CL-minus-LEM, the axiom schemata in CL is replaced in IL by ( ). syntactically intuitionistic logic is proper subsystem of CL
Christian Wthrich Topic 7
add (standard) axioms for identity and arithmetic formal system HA for intuitionistic arithmetic (Heyting arithmetic), which is a proper subsystem of the standard PA among semantic properties of IL, philosophically most intriguing is model-theoretic approach to semantics precise semantic notion of truth and logical validity (Posey, 338) Evert Beth (1947), Saul Kripke (1965): not single model, but collection of nodes, partially ordered by accessibility relation (demonstrably faithful to IL)
Christian Wthrich
Topic 7
A model-theoretic counterexample to CL
model structure contains three nodes, w1 , w2 , w3 such that w2 and w3 are accessible to w1 though not to one another In Kripke models, e.g.:
1
is true at node w only if is true at any node w accessible to w is true at node w only if is not true at any node w accessible to w ( ) is true at w only if either is true at w or is
Suppose is true at w2 but not at w3 . is not true at w1 (from (1) and Aw3 w1 ) is not true at w1 (from (2) and Aw2 w1 ) is not true at w1 (from (3) and previous lines) counterexample to LEM
Christian Wthrich Topic 7
Heytings interpretation
Heyting: not that IL is formal statement of intuitionistic ontology instead: special intuitionistic meaning of logical particles intuitionism: maths has no unknowable truths in maths: to be true is to be provable; IL result of applying this idea to semantics of connectives and quantiers truth is repalced by assertability (or provability) set out conditions of provability of propositions, as follows...
Christian Wthrich
Topic 7
BHK interpretation
Brouwer-Heyting-Kolmogorov interpretation
(Cited from Shapiro, 186)
[ is not provable.] A proof of a sentence of the form and consists of a proof of and a proof of . A proof of a sentence of the form either or consists of either a proof of or a proof of . A proof of a sentence of the form if then consists of a method for transforming a proof of into a proof of . A proof of a sentence of the form not- consists of a procedure for transforming any proof of into a proof of absurdity. In other words, a proof of not- is a proof [that] there can be no proof of . A proof of a sentence of the form for all x , (x ) consists of a procedure that, given any n, produces a proof of the corresponding sentence (n). A proof of the sentence of the form there is an x such that (x ) consists of the construction of an item n and a proof of the corresponding (n).
Christian Wthrich Topic 7
Some remarks
not- is equivalent to if then one cant prove an existentially quantied sentence without showing how to construct such an x BHK interpretation is informal since construction is not dened and thus open to different interpretations It follows immediately (already at informal level) that LEM is not generally true: to prove or not- one must either deliver a proof of or give a procedure for transforming any proof of into a proof of absurdity. In case we havent done either, the statement does not hold. Once we have done either, the particular instance of tertium non datur is established.
Christian Wthrich Topic 7
Christian Wthrich
Topic 7
Dummetts vantage point is language, since considerations regarding which logic is correct turn on meaning, which is determined by use, by its role in logical inference: The meaning of a mathematical statement determines and is exhaustively determined by its use... if two individuals agree completely about the use to be made of [a] statement, then they agree agree about its meaning... An individual cannot communicate what he cannot be observed to communicate. (Dummett 1973, 98f; cited after Shapiro, 190)
Christian Wthrich
Topic 7
Christian Wthrich
Topic 7
replace truth with veriability or assertability as main constituent of semantics instead of truth conditions for formulae, we seek proof conditions for them against meaning holism: at least some parts of language can be understood independently of others particularly applies to logical terminology including connectives and quantiers offers basis on which practice can be criticized: ways logical operators are usually introduced into proofs inconsistent with classical logic In particular: rules for introducing negation and disjunction separately do not warrant LEM when combined
Christian Wthrich
Topic 7
radically generalizes assertabilist semantics to apply to all human language, not just mathematics IL, and not CL, will be appropriate logic not just for mathematics, but for any discourse in which there are undecidable propositions
Christian Wthrich
Topic 7
Christian Wthrich
Topic 7
Taking stock
Credits: rich technical studies, mature constructivism reecting human aspect of mathematics Debits:
1
intuitionism is a deviation against modern norm, regarded either as messy distraction or technically quixotic curiosity (Posey, 344) internal dissonance: Brouwers (or any) metaphysical grounding of logic is poor bedfellow of Heyting-Dummett assertabilism intuitionism depends on existence of undecidable propositions that it cannot in fact construct, and whose possible existence [it...] may not assert (345) because if it specied an undecidable proposition, the assertability clause for negation would entail that the proposition is false, thus deciding it!
Christian Wthrich Topic 7
Carl Posy
So that is where we are in intuitionism: a house internally divided, bent upon an eccentric technical mission, and based on a fundamental assumption which goes against its own internal standards. [...I believe that a] Kantian perspective can to serve to reconcile the opposing intuitionistic streams. (345)
Christian Wthrich
Topic 7