SE212 - Theories, Equality, Arithmetic, Induction

• Hidden Premise - For a single argument unwritten information is known as hidden premise
• Enthymeme - Argument that contains a hidden premise, arguments that contain unstated premises that are obviously true
• Symmetry - $⊢\forall x,y,\bullet (x=y)\Rightarrow (y=x)$
• Transitivity - $⊢\forall x,y,z,\bullet (x=y)\wedge (y=z)\Rightarrow (x=z)$
• Leibniz's Law - If $t_1=t_2$ is a theorem, then so is $P[t_1/x]\iff P[t_2/x]$
  • Generally referred to as the ability to substitute “equals for equals”
• Theory of Arithmetic
  • Constants: 0
  • Functions:
    • suc (plus 1)
    • • (addition)
    • x (multiplication)
  • Predicates:
    • < (less than)