9/27/19
Introduction
Intuitionistic Propositional Logic (I.P.L) may seem like a strange topic to be discussing at this point. However, there is a strong connection between IPL and type theory (embraced by the Curry-Howard Isomorphism, which we will get to).
Intuitionism in mathematics and logic is an approach having its modern origins in the work of Brouwer, and his student Heyting, in the early twentieth century. It turns on emphasizing the notion of proof or construction, as opposed to truth.
Consider an arbitrary proposition P. The standard view would be that either P is true, or, failing that, P is false (and ~P is true). In contrast, the intuitionists would say: it may be that we have not been able to prove P and also we have not been able to prove ~P. In which case, the statement (either P is provable or ~P is provable) is false.
The statement (P v ~P) is known as Tertium Non Datur or The Law of the Excluded Middle . Intuitionists deny the Law of Excluded Middle.
There are different ways of setting up ILP but in the system we are going to use it requires one change to one rule.
Standard Propositional Logic
There is suitable background for this in Tutorial 5: Valid arguments, searching for a proof through to Tutorial 10: Common Inference Patterns and Rewrite Rules . (The text there uses ⊃ for conditional, we'll be using →. Also, there is mention of Rewrite Rules, but it is good to be aware that these relatively elementary systems can use both Rewrite and Introduction-Elimination style Rules). Here are some examples of derivations in ordinary propositional logic for you to try.
Intuitionistic Propositional Logic
IPL has one rule that is different to Standard Propositional Logic (SPL). It is the Rule for the Elimination of Negation (~E). Roughly speaking, in SPL if you have a formula with a double negation e.g. ~~P you can take both the negations off and have P by the Rule for the Elimination of Negation (~E). In IPL, the the Rule for the Elimination of Negation (~E) starts from a formula that has negation as its main connective, e.g. ~P and you can infer from that a conditional formula, say (P→?) where P is the first formula without its negation and the ? is any formula whatsoever.
To give it in slightly more detail, in the present setting
The Rule of the Elimination of Negation ∼E
If a derivation contains a line of the form
n. <assumptions> ∼<formula1> <any justification>
a line of the form
<next line number> <assumptions + optional further assumptions> <formula1> → <formula2> 'n ∼E'
may be added to the derivation.
Implementation of ∼E
∼E removes single negation from a selected ∼<formula1> to add <formula1> → <formula2> 'n ∼E' . You will be asked to enter a formula that will become formula2.
Some relations between the two logics
In SPL, you can prove ~P ∴ P→X for any formula X (you proved an instance of that above). This means that in SPL you can prove the IPL Rule (~E). All other rules of IPL are rules of SPL. So every theorem of IPL is a theorem of SPL. On the other hand, ∴ P ∨ ~P can be proved in SPL but not in IPL. So, SPL contains all the theorems of IPL and some more besides.