# System IPC

[Hackstaff, 1966]

## Notes

There are structural similarities between IPC and the modal logic
system S4.
[Hughes and Cresswell 1996, p225]
[Zeman, 1973, p231]
(Both apparently quoting
[McKinsey and Tarski, 1948, p13]
which showed that there was a validity preserving mapping between Heyting
Propositional Calculus H and S4.)
But note that Ian Hacking [Hacking, 1963]
proved that the Heyting Propositional Calculus H could also be mapped onto
S3

## Based on

IPC is
Positive Propositional Logic
plus the Axioms IP1 [(p>~p)>~p]
and IP2 [~p>(p>q)]
[Claimed to be from H.Scholz and K.Schröter, as attributed by Church.]
[Hackstaff, 1966, p223]

### OR

Intuitionist PC [as given by Heyting] is

- Rules
- Axioms
- HA1: p=>(p&p)
- HA2: (p&q)=>(q&p)
- HA3:
(p=>q)=>((p&r)=>(q&r))
- HA4:
((p=>q)&(q=>r))=>(p=>r)
- HA5: q=>(p=>q)
- HA6: (p&(p=>q))=>q
- HA7: p=>(p+q)
- HA8: (p+q)=>(q+p)
- HA9:
((p=>r)&(q=>r))=>((p+q)=>r)
- HA10: ~p=>(p=>q)
- HA11:
((p=>q)&(p=>~q))=>~p

[Hackstaff,
1966, p223]

## Contrast

IPC is an alternative to Standard PC,
in contrast to other popular alternatives:

# Go to ...

© Copyright 2006, by John Halleck, All Rights Reserved.

This page is http://www.cc.utah.edu/~nahaj/logic/structures/systems/ipc.html

This page was last modified on November 5th, 2006