Meredith's axiom system이라고, 힐베르트 증명 시스템의 일종인데, 

다른 힐베르트 증명 시스템들처럼 countable한 atomic sentence와, connective로 {~, ->}만 사용된 명제를 다룸.   (대충 (p->~q) 같은 거.)

근데, 채택하는 공리꼴이

(( ((A->B) -> (~C->~D)) -> C )  -> E)   ->  ( (E->A) -> (D->A) )  이거 1개임.   (A, B, C, D, E는 아무 명제나 가능.)

그리고 논리 법칙도 전건 긍정 (Modus Ponens) 한 개.   (대충, A이고 (A->B) 이면, B라는 것을 유도할 수 있는 거.)

저 공리꼴 1개와 전건 긍정만으로 (A->A) 나 대우 법칙이나 이중 부정, 귀류법 같은 걸 다 유도할 수 있나 봄.

(일단, A, B, C, D, E의 TF 값에 상관 없이 저 공리는 참이 되긴 함. 근데 저게 언제나 참이 된다는 것도 직관적이진 않은 것 같음.)