Propositional calculus

I met many different definitions of propositional calculus, which are mostly incomplete, but of course not conflicting with each other. In Wikipedia article there is a general definition, which covers all other definitions. So let's define it.

Definition

Propositions
A proposition is a statement, which can be true or false. For example "3 is prime" and "4 is odd" are propositions and the first one is true and the second is false. In general we write those propositions with letters and do not care about theirs truths. So let A be the finite set of propositions.
Connectives
Connectives are Boolean operators. In general connectives can have any arity, but often discussed operators with arity 0,1 and 2. Some of connectives are "", "⋀" ,"⋁" and etc. And let Ω be the finite set of connectives.

With propositions and connectives we can define the syntax. The formulas of Propositional calculus construct with the following rules:

1. Any element of A is a formula.
2. If p1,p2,...,pn are formulas and ω is operator of arity n from Ω then ω(p1,p2,...,pn) is a formula also.
3. Nothing else is a formula.

In particular case when discussed only operators with arity less or equal 2, the 2nd step formulated differently.For example when Ω={,⋀,⋁,→,↔} then the formulation is

• If p and q are formulas then p, (p⋀q),(p⋁q),(p→q) and (p↔q) are formulas also.

The next two steps will define the semantic of propositional logic.
Axioms

Axioms syntactically are formulas, but in place of propositions we can put any formula. Let I be the set of formulas.
Inference rules
In general inference rule is a set of formulas,the last one of which called conclusion and others are premises. Like the case of axioms, in place of the propositions in formulas of inference rules we can put any formula. Let Z be the set of formulas.
For example on of the familiar inference rules is the Modus Ponens.

premises - p→q and p
conclusion - q

L=L(A,Ω,Z,I) system we call propositional calculus. Let P be the formula of L. We say that P is provable in L and write ├P if there exist a sequence of formulas such that

• The last formula of the sequence is P.
• Each next formula is a axiom instance or the conclusion of inference rules which premises are the formulas from previous elements of sequence.