普段我々がやってる、1階の述語論理をいい加減に自然言語に変換したような言語で、ZFCみたいなこっちはわりとちゃんと正確に自然言語に変換できてそうな公理を使った数学を普通の数学って呼んでる