# Creative Commons Attribution-Share Alike 3.0 Unported (http://creativecommons.org/licenses/by-sa/3.0/)
# {{header
# | title = Axioms of intuitionistic propositional logic
# | subtitle =
# | left =
# | right =
# | shortcut =
# | notes = [[w:Intuitionistic logic|Intuitionistic logic]] is a subset of [[Interface:Classical propositional calculus]] (subset in the sense that every theorem of intuitionistic logic is also a theorem of classical logic). It differs in omitting the [[Interface:Law of the excluded middle|law of the excluded middle]]. This interface contains one axiomization of intuitionistic logic.
# }}
# {{modules
# | parameters = ''None''
# | importedby = [[Intuitionistic propositional logic]]
# | exportedby = none
# }}
#
# The axioms here are essentially identical to those in the ''Stanford Encyclopedia of Philosophy''.[[http://plato.stanford.edu/entries/logic-intuitionistic/ Intuitionistic Logic],
# First published Wed Sep 1, 1999; substantive revision Wed Apr 28, 2010, ''Stanford Encyclopedia of Philosophy'']
#
# == Well-formed formulas ==
#
# We first introduce the kind of [[w:well-formed formulas|well-formed formulas]] and a few variables for this kind.
kind (formula)
tvar (formula p q r s)
#
# == Connectives ==
# Although it is possible to define intuitionistic logic with a single (complicated) connective, or with as few as three of the usual connectives, here we take implication, disjunction, conjunction, and negation as primitive:
#
term (formula (¬ p)) # Negation
term (formula (→ p q)) # Implication
term (formula (∨ p q)) # Disjunction
term (formula (∧ p q)) # Conjunction
#
# == Inference rule ==
#
# The one rule is [[w:modus ponens|modus ponens]]:
stmt (applyModusPonens () (p (→ p q)) q)
#
# == Implication ==
#
# The first two of the [[Interface:Standard axioms of propositional logic]] serve as our axioms governing implication:
#
stmt (Simp () () (→ p (→ q p)))
stmt (Frege () () (→ (→ p (→ q r)) (→ (→ p q) (→ p r))))
#
# == Disjunction ==
#
# For disjunction, we assume the ability to introduce a left hand or right hand side to any proposition:
stmt (DisjunctionLeftIntroduction () () (→ p (∨ q p)))
stmt (DisjunctionRightIntroduction () () (→ p (∨ p q)))
#
# and the following form of disjunction composition:
stmt (DisjunctionCompositionAxiom () () (→ (→ p r) (→ (→ q r) (→ (∨ p q) r))))
#
# == Conjunction ==
#
# A conjunction implies either of its propositions:
stmt (ConjunctionLeftElimination () () (→ (∧ p q) q))
stmt (ConjunctionRightElimination () () (→ (∧ p q) p))
#
# and can be derived from its propositions:
stmt (ConjunctionRightIntroduction () () (→ p (→ q (∧ p q))))
#
# == Negation ==
#
# If an antecedent implies both a consequent and its negation, we can infer the negation of the original statement.
stmt (ProofByContradiction () () (→ (→ p q) (→ (→ p (¬ q)) (¬ p)))) # *2.65 in Principia
#
# From a contradiction, anything follows. This is also known as the [[w:Principle of explosion|principle of explosion]]. The presence of this axiom distinguishes intuitionistic logic from [[w:Minimal logic|minimal logic]].
stmt (Explosion () () (→ p (→ (¬ p) q))) # *2.24 in Principia
#
# == Truth ==
#
# Although ghilbert can, basically, define truth and falsity in terms of the above concepts, it doesn't appear to have the ability to give a notation for truth (⊤) or falsity (⊥) without an additional axiom. We adopt an axiom that asserts that ⊤ holds, which is enough (⊥ can be defined in terms of ⊤).
term (formula (⊤))
stmt (True () () (⊤))
#
# == Biconditional ==
# Note that biconditional can be defined in terms of conjunction and implication, so an axiom
# is not necessary to introduce it; Ghilbert's defthm mechanism is powerful enough. See
# [BiconditionalJust] for the theorem justifying the definition.
#
# == References ==
#
#
# [[Category:Subsystems of classical logic|{{PAGENAME}}]]