I came across this site: http://mally.stanford.edu/tutorial/sentential.html It lists four axioms of "sentential" logic. I first would like to know if there are other axioms not listed here. Wouldn't you need some axiom like if P is true, then ~P is false? It seems difficult to prove the law of disjunctive inference with these axioms. Next, I need some help understanding the notation. One axiom is: P -> (Q -> P) Can this be interpreted as given P therefore Q -> P for any statement Q? In other words, if I precede the antecedent with the word "given" and exchange the main operator (which is always the conditional in these cases) with the word "therefore", is the meaning of the statement the same? This issue is important to me as a matter of proving theorems. Also, one source refers to "->", "V", "and", and "<->" as binary operations. I just recently learned about binary operations and abstract systems. Does this mean that we can study argument forms as an abstract system? Can we prove the associativity/commutivity/distributivity properties of the operations using the above axioms? For a binary operation aOb=c How does this relate to P->Q? IOW P->Q=what? Is it merely the joining of the statements by the words "if" and "then"?