# BCSK

[Humberstone,
2000]

[Wos and Spinks,
2005]

## Notes

## Based on

- Rules
- Uniform substitution (US)
(*** Original is really in terms of axiom schemata, not axioms and
uniform substitution *** -JH)
- Modus Ponens for > (MP>:
if |- p and |- p>q infer |- q)

- Axioms
- A1: A => (B=>A)
- A2: A => (B=>C)) => ((A=>B)=>(A=>C))
- A3: ((A=>B)=>A) => A
- A4: A => (B>A)
- A5: (A>(B>C)) => ((A>B)>(A>C))
- A6: (A>(B>C)) => (B>(A>C))
- A7: ((A>B)>A) => A
- A8: (A=>B) > (A>B)
- A9: ((A=>B)>B) => ((B=>A)>A)

[Humberstone,
2000, p8]

(Different sources give different numberings of the axioms,
all tracing back to Dr. Spinks' circulating but unpublished papers,
some of which flip 8 and 9. Dr. Spinks, when contacted, stated that
the Humberstone numbering is the prefered one. -JH)

## Basis for

## Compare with

# Go to ...

This page is http://www.cc.utah.edu/~nahaj/logic/structures/systems/index.html
This page was last modified on August 16th, 2006.