해독되지 않은 미적분학으로서 알파벳과 공리(axiom)라는 단어의 집합 및 추론의 법칙에 관계되는 유한 집합으로 구성된 것. 집합론, 불 대수, 포스트(post) 시스템, 배커스(Backus) 정규 형식 등이 있다. 형식 체계는 프로그램 작성 언어의 구문과 어의를 명시하기 위해 사용되며, 구문적 번역과 컴파일러의 검증, 언어의 복잡성 연구에도 사용된다.