Intuitionistic Logic Explorer Home Page  First > Last > 

Mirrors > Home > ILE Home > Th. List 
Intuitionistic Logic (Wikipedia [accessed 19Jul2015], Stanford Encyclopedia of Philosophy [accessed 19Jul2015]) can be thought of as a constructive logic in which we must build and exhibit concrete examples of objects before we can accept their existence. Unproved statements in intuitionistic logic are not given an intermediate truth value, instead, they remain of unknown truth value until they are either proved or disproved. Intuitionist logic can also be thought of as a weakening of classical logic such that the law of excluded middle (LEM), (φ ∨ ¬ φ), doesn't always hold. Specifically, it holds if we have a proof for φ or we have a proof for ¬ φ, but it doesn't necessarily hold if we don't have a proof of either one. There is also no rule for double negation elimination. Brouwer observed in 1908 that LEM was abstracted from finite situations, then extended without justification to statements about infinite collections.
Contents of this page  Related pages External links 
(Placeholder for future use)
(By Gérard Lang, 19Jul2015)
Mario Carneiro's work (Metamath database) "iset.mm" provides in Metamath a development of "set.mm" whose eventual aim is to show how many of the theorems of set theory and mathematics that can be derived from classical first order logic can also be derived from a weaker system called "intuitionistic logic." To achieve this task, iset.mm adds (or substitutes) 13 intuitionistic axioms whose second part of the name begins with the letter "i" to the classical logical axioms of set.mm.
Among these 13 new axioms, the 6 first (axia1, axia2, axia3, axio, axin1 and axin2), when substituted to ax3 and added with ax1, ax2 and axmp, allow for the development of intuitionistic propositional logic. Each of them is a theorem of classical propositional logic, but ax3 cannot be derived from them. Similarly, other basic classical theorems, like the third middle excluded or the equvalence of a proposition with its double negation, cannot be derived in intuitionistic propositional calculus. Glivenko showed that a proposition φ is a theorem of classical propositional calculus if and only if ¬¬φ is a theorem of intuitionistic propositional calculus.
The next 4 new axioms (axial, axi5r, axia1 and axia2) being added to ax4, ax5, ax6, ax7 and axgen allow for the development of intuitionistic pure predicate calculus.
The last 3 new axioms (axi9, axi11e and axi12) are variants of the classical axioms ax9, ax11 and ax12. The substitution of axi9 and axi12 with ax9 and ax12 and the addition of axi11e with ax8, ax10, ax11, ax13, ax14 and ax17 allow for the development of the intuitionistic predicate calculus.
Each of the 13 new axioms is a theorem of classical first order logic with equality. But some axioms of classical first order logic with equality, like ax3, cannot be derivefd in the intuitionistic predicate calculus.
One of the major interests of the intuitionistic predicate calculus is that its use can be considered as a realization of the program of the constructivist philosophical view of mathematics.
(Placeholder for future use)
(Placeholder for future use)
This
page was last updated on 22Jul2015. Your comments are welcome: Norman Megill Copyright terms: Public domain 
W3C HTML validation [external] 