ここでは、MGTP による証明(超入門編)で、あいまいに記述していた MGTP の文法をやや形式的に説明することにする。
まず、通常論理学で表現されるどんな一階述語論理式も、 常に節形式(連言標準形ともいう)と呼ばれる 一つの標準的表現に変換可能である。 特に、ここでは、MGTP のためにアレンジした節形式表現を用いることにし、 この形式で書かれた節の集合を MG節集合(紛れがない場合は単に節集合)と呼ぶことにする。
MG節集合は、
のように、要素として節(MG節)と呼ばれる Ci が有限個含まれるような 集合である。
MG節集合に含まれる1本(節は１本、２本のように数える)の節(MG節) は、次のような形をしている。
ここで、Ai (1≦i≦n), Bj (1≦j≦m) はアトム(原子論理式ともいう)と呼ばれ、 あらゆる論理式の中で最小の構成単位(要素)である。 ``,''は論理積結合子(``かつ'')、 ``;''は論理和結合子(``または'')、 ``→''は含意結合子(``ならば'')である。
このMG節のくだいた読み方は、 A1 から An までがすべて成り立てば、 B1 から Bm までのいずれかが成り立つ。'' ということである。
→ の左辺を前件(前件部)、右辺を後件(後件部)という。 前件が実質的に空の場合、→ の左辺にtrueと書くことにし、 その節を正節と呼ぶ。正節は、初期ルールとも呼ばれる。 後件が実質的に空の場合、→の右辺にfalseと書くことにし、 負節と呼ぶ。負節は、棄却ルールとも呼ばれる。