آناليز سازنده بيشاپ و مقايسه­ آن با آناليز كلاسيك

در اين مقاله، منطق شهودي براوِر در رياضيات و آناليز رياضي سازنده بيشاپ مبتني بر اين منطق را معرفي كرده و تفاوت‌هاي آن‌ها با منطق و آناليز رياضي كلاسيك را بيان مي‌كنيم. تفاوت بنيادي آناليز سازنده با آناليز كلاسيك در اين است كه در آناليز سازنده بر خلاف آناليز كلاسيك، همواره راهكار و الگوريتم يافتن عناصر مطلوب در قضاياي وجودي، ارائه مي‌شود و لذا مي‌توان اين نوع از آناليز رياضي را يك نوع زبان برنامه‌نويسي سطح بسيار بالا قلمداد كرد. به منظور آشنايي دقيق با روش‌هاي استدلال سازنده، ابتدا دستگاه اعداد حقيقي را با يك روش سازنده ساخته و تفاوت‌هاي اصولي آناليز سازنده نسبت به آناليز كلاسيك را كه ريشه در خواص شناخته شده اعداد حقيقي دارد، تبيين مي‌نماييم. در ادامه، چند قضيه وجودي در آناليز كلاسيك و معادل سازنده­ آنها را بيان مي‌كنيم. خواهيم ديد كه در اكثر مواقع، قضاياي وجودي دقيق در آناليز كلاسيك، به قضاياي وجودي تقريبي در آناليز سازنده تبديل مي‌شوند.