User:IssaRice/Computability and logic/Intuitiveness and simplicity tradeoff
In various places in computability and logic, there is a tradeoff between the intuitiveness of a formalization and its inherent simplicity.
- The more our deductive system resembles natural deduction, the easier it is intuitively (e.g. easier to prove theorems within the formal system), but the harder it is to prove things about the system metalogically. Peter Smith makes this point in his Gödel book.
- The more connectives we have in our logical system, the more intuitive it gets (i.e. the more it resembles how mathematicians write ordinary proofs), but the more tedious it becomes to prove things about it since we need more cases in our inductive metalogical proofs.
- The more instructions our loop programs can use, the closer it gets to high level programming (e.g. how pseudocode is written), but the harder it becomes to prove other formalizations of computation can fully simulate our loop programs.
- The more types of constants we have in our system (relations, constants, functions), the more cases in our inductive proofs.