Propositional calculus deals with truth values, which can be interpreted as bits. Using this, we can define the half adder and the full adder in pure propositional calculus, and show their basic properties.
The half adder adds two 1-bit numbers. Its two outputs are the "sum" S and the "carry" C. The real sum is then given by 2C+S. The sum and carry correspond respectively to the logical exclusive disjunction (df-xor) and the logical conjunction (df-an).
The full adder takes into account an "input carry", so it has three inputs and again two outputs, corresponding to the "sum" (df-had) and "updated carry" (df-cad).
Here is a short description. We code the bit 0 by and 1 by . Even though and are invariant under permutation of their arguments, assume for the sake of concreteness that (resp. ) is the i^th bit of the first (resp. second) number to add (with the convention that the i^th bit is the multiple of 2^i in the base-2 representation), and that is the i^th carry (with the convention that the 0^th carry is 0). Then, gives the i^th bit of the sum, and gives the (i+1)^th carry. Then, addition is performed by iteration from i = 0 to i = 1 + (max of the number of digits of the two summands) by "updating" the carry.