|Intuitionistic Logic Explorer Home Page|| First >
|Mirrors > Home > ILE Home > Th. List|
Intuitionistic Logic (Wikipedia [accessed 19-Jul-2015], Stanford Encyclopedia of Philosophy [accessed 19-Jul-2015]) 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, 12-Feb-2018)
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) 12 intuitionistic axioms whose second part of the name begins with the letter "i" to the classical logical axioms of set.mm.
Among these 12 new axioms, the 6 first (ax-ia1, ax-ia2, ax-ia3, ax-io, ax-in1 and ax-in2), when substituted to ax-3 and added with ax-1, ax-2 and ax-mp, allow for the development of intuitionistic propositional logic. Each of them is a theorem of classical propositional logic, but ax-3 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 (ax-ial, ax-i5r, ax-ie1 and ax-ie2) together with the set.mm axioms ax-4, ax-5, ax-7 and ax-gen do not mention equality or distinct variables.
The last two new axioms (ax-i9 and ax-i12) are variants of the classical axioms ax-9 and ax-12. The substitution of ax-i9 and ax-i12 with ax-9 and ax-12 and the inclusion of ax-8, ax-10, ax-11, ax-13, ax-14 and ax-17 allow for the development of the intuitionistic predicate calculus.
Each of the 12 new axioms is a theorem of classical first order logic with equality. But some axioms of classical first order logic with equality, like ax-3, cannot be derived 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.
As with the classical axioms we have propositional logic and predicate logic.
The axioms of intuitionistic propositional logic consist of some of the axioms from classical propositional logic, plus additional axioms for the operation of the 'and', 'or' and 'not' connectives.
|Axiom Simp||ax-1||⊢ (φ → (ψ → φ))|
|Axiom Frege||ax-2||⊢ ((φ → (ψ → χ)) → ((φ → ψ) → (φ → χ)))|
|Rule of Modus Ponens||ax-mp||⊢ φ & ⊢ φ → ψ => ⊢ψ|
|Left 'and' elimination||ax-ia1||⊢ ((φ ∧ ψ) → φ)|
|Right 'and' elimination||ax-ia2||⊢ ((φ ∧ ψ) → ψ)|
|'And' introduction||ax-ia3||⊢ (φ → (ψ → (φ ∧ ψ)))|
|Definition of 'or'||ax-io||⊢ (((φ ∨ χ) → ψ) ↔ ((φ → ψ) ∧ (χ → ψ)))|
|'Not' introduction||ax-in1||⊢ ((φ → ¬ φ) → ¬ φ)|
|'Not' elimination||ax-in2||⊢ (¬ φ → (φ → ψ))|
Unlike in classical propositional logic, 'and' and 'or' are not readily defined in terms of implication and 'not'. In particular, φ ∨ ψ is not equivalent to ¬ φ → ψ, nor is φ → ψ equivalent to ¬ φ ∨ ψ, nor is φ ∧ ψ equivalent to ¬ (φ → ¬ ψ).
The ax-in1 axiom is a form of proof by contradiction which does hold intuitionistically. That is, if φ implies a contradiction (such as its own negation), then one can conclude ¬ φ. By contrast, assuming ¬ φ and then deriving a contradiction only serves to prove ¬ ¬ φ, which in intuitionistic logic is not the same as φ.
The biconditional can be defined as the conjunction of two implications, as in dfbi2 and df-bi. Other ways of understanding the biconditional, such as dfbi1 or dfbi3, however, are classical rather than intuitionistic results (following the proofs on those pages shows they depend on ax-3).
Predicate logic adds set variables (individual variables) and the ability to quantify them with ∀ (for-all) and ∃ (there-exists). Unlike in classical logic, ∃ cannot be defined in terms of ∀. As in classical logic, we also add = for equality (which is key to how we handle substitution in metamath) and ∈ (which for current purposes can just be thought of as an arbitrary predicate, but which will later come to mean set membership).
Our axioms are based on the classical set.mm predicate logic axioms, but adapted for intuitionistic logic, chiefly by adding additional axioms for ∃ and also changing some aspects of how we handle negations.
|Axiom of Specialization||ax-4||⊢ (∀xφ → φ)|
|Axiom of Quantified Implication||ax-5||⊢ (∀x(φ → ψ) → (∀xφ → ∀xψ))|
|The converse of ax-5o||ax-i5r||⊢ ((∀xφ → ∀xψ) → ∀x(∀xφ → ψ))|
|Axiom of Quantifier Commutation||ax-7||⊢ (∀x∀yφ → ∀y∀xφ)|
|Rule of Generalization||ax-gen||⊢ φ => ⊢ ∀xφ|
|x is bound in ∀xφ||ax-ial||⊢ (∀xφ → ∀x∀xφ)|
|x is bound in ∃xφ||ax-ie1||⊢ (∃xφ → ∀x∃xφ)|
|Define existential quantification||ax-ie2||⊢ (∀x(ψ → ∀xψ) → (∀x(φ → ψ) ↔ (∃xφ → ψ)))|
|Axiom of Equality||ax-8||⊢ (x = y → (x = z → y = z))|
|Axiom of Existence||ax-i9||⊢ ∃x x = y|
|Axiom of Quantifier Substitution||ax-10||⊢ (∀x x = y → ∀y y = x)|
|Axiom of Variable Substitution||ax-11||⊢ (x = y → (∀yφ → ∀x(x = y → φ)))|
|Axiom of Quantifier Introduction||ax-i12||⊢ (∀z z = x ∨ (∀z z = y ∨ ∀z(x = y → ∀z x = y)))|
|Axiom of Bundling||ax-bnd||⊢ (∀z z = x ∨ (∀z z = y ∨ ∀x∀z(x = y → ∀z x = y)))|
|Left Membership Equality||ax-13||⊢ (x = y → (x ∈ z → y ∈ z))|
|Right Membership Equality||ax-14||⊢ (x = y → (z ∈ x → z ∈ y))|
|Distinctness||ax-17||⊢ (φ → ∀xφ), where x does not occur in φ|
(Placeholder for future use)
page was last updated on 22-Jul-2015.
Your comments are welcome: Norman Megill
Copyright terms: Public domain
|W3C HTML validation [external]|