0
$\begingroup$

I've begun studying mathematical logic with Hodel's 'An Introduction to Mathematical Logic', and have just learnt about formal systems and their components. In the textbook, Hodel gives as an example of a formal system the system 'ADD', whose theorems correspond to true statements about addition; it is defined as follows:

  • Symbols: $| \,,+,=$
  • Formulae: statements of the form $x+y=z$ where $x,y$, and $z$ are expressions in $|$
  • Axiom: $|+|=||$
  • Rules of Inference: $\frac{x+y=z}{x|+y=z|}$ (R1) and $\frac{x+y=z}{y+x=z}$ (R2)

As an exercise (exercise 3 of section 1.3 for those with the book), Hodel then asks the reader to create a formal system 'MULT', which has theorems corresponding to our standard notions of multiplication; he also asks the reader to prove within this system that $|| \times ||| = ||||||$.

I believe I have a solution to this, but I would be grateful if someone wouldn't mind checking it for me - I'm new to this area of maths so want to make sure my fundamentals are strong. My system is defined as follows:

  • Symbols: $|\, , \times, + , =$
  • Formulae: statements of the form $x\times y = z$ or $x+y=z$ where $x, y,$ and $z$ are expressions in $|$
  • Axioms: $|+|=||$ (A1) and $| \times x = x$ (A2)
  • Rules of inference: $\frac{x+y=z}{x|+y=z|}$ (R1), $\frac{x+y=z}{y+x=z}$ (R2), $\frac{x\times y=z}{x|\times y=z+y}$ (R3), and $\frac{x\times y=z}{y\times x=z}$ (R4)

and my proof that $\vdash_{\text{MULT}}|| \times ||| = ||||||$:

  1. $|\times||=||$ (A2)
  2. $||\times || = ||+||$ (R3)
  3. $|+|=||$ (A1)
  4. $||+| = |||$ (R1)
  5. $|+|| = |||$ (R2)
  6. $||+|| = |||| = || \times || $(R1 and step 2)
  7. $||| \times || = ||||+||$ (R3)
  8. $|| + || = ||||$ (step 6 and previous)
  9. $||||+|| = |||||| = ||| \times ||$ (R1 twice and step 7)
  10. $ || \times ||| = ||||||$ (R4) $\square$

What makes me doubt whether this is the simplest solution is that I have included all of ADD within my new system, however I suppose this does reflect how multiplication is defined in terms of iterated addition.

Improvements, corrections, and other solutions welcomed and greatly appreciated :)

$\endgroup$
  • $\begingroup$ Comment : if the rule for formulas is : $x+y=z$ where $x,y$, and $z$ are expressions in |, then the conclusion of (R3) : $x| \times y= z+y$ is not well-formed, because $z+y$ is not "an expression in |". $\endgroup$ – Mauro ALLEGRANZA Jun 27 '18 at 19:58
  • $\begingroup$ @MauroALLEGRANZA thanks for that. I can’t see an obvious way to resolve this — is it reasonable just to adjust the definition of formulae in my system to include the form of R3? $\endgroup$ – aidangallagher4 Jun 27 '18 at 21:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.