Martin-Löf type theory has four basic forms of judgments and is a considerably more complicated system than first-order logic. One reason is that more information is carried around in the derivations due to the identification of propositions and types. Another reason is that the syntax is more involved. For instance, the well-formed formulas (types) have to be generated simultaneously with the provably true formulas (inhabited types).