Groups

2013

Reading

Colin Howson, [1997] Logic with trees Chapter 9

Tutorial

Groups can be characterized by three proper symbols {=,+,0} (ie identity, one infix operator, we will use '+', and an identify element '0') and the three proper axioms

∀x∀y∀z((x+y)+z=x+(y+z)),  (*associativity*)
∀x(x+0=x∧0+x=x),                (*identity element, right and left*) 
∀x∃y(x+y=0∧y+x=0)             (*inverse*)

If these three axioms are taken as starting formulas or 'premises' for a tree, we would be doing Group Theory.

In particular, we can prove such theorems as, the uniqueness of the identity element (0 is an identity element, and it actually is the only one, since others are equal to it. ie

∴ ∀z(∀x(x+z=x∧z+x=x)→0=z)

Here are some other theorems 

∴ ∀x∀y∀z((x+y=y+z)→y=z)

∴∃!y∀x(x+y=x) (*the existence of a unique identity element*)

∴∀x∃!y(x+y=0) (*the existence of a unique complement*)

You can prove these below as exercises. Just take the axioms as premises and edit the conclusion to suit.

Exercise

Here are a few hints

• You have to use the right (unicode/html) logical symbols. Check Writing symbols
• The symbols in use here are ¬ ∧ ∨ → ↔ ∀ ∃ ₁ ₂ ₃ ₄ ₅ ₆ ₇ ₈ ₉ (so copy and paste or drag and drop these). The Howson syntax is that the quantifers do not have brackets around them so a quantified formula might look like ∀x(A(x)→B(x,x)). Notice that the 'arguments' to a predicate have brackets around them, and if the arguments are a list they will be separated by commas. You can use proper subscripts (shown above) on variables (or constants or predicates). For example, ∀x₁(A(x₁)→B(x₁,x₁)).
• When entering from a selection, the software will take a single formula (say, A) or a comma separated list of formulas (say, A,B,C) or a possibly empty comma separated list of formulas followed by ∴ and another formula (say, A,B,C ∴ D). In the last case it will load the negation of the conclusion.
• Just type, cut and paste, or drag and drop, whatever you wish, into the lower text box. Then make a selection and hit the Start button.

If you decide to use the web application you can launch it from here Deriver [Howson] — username 'logic' password 'logic'. Then either copy and paste into the Journal or use the Deriver File Menu to Open Web Page with this address https://softoption.us/test/treesStandAlone/howson/CombinedTutorialsHowson.html . Then select the desired formula(s) and Start Tree off the Actions Menu.

Preferences

You will need to set some Preferences for this. Set identity to true (and that will give you the identity rules) set firstOrder to true (to get first order theories); and  you can check that the parser is set to Howson.