 The notation formula_3 means that there is a deduction that ends with formula_4 using as axioms only logical axioms and elements of formula_1.Thus, informally, formula_3 means that formula_4 is provable assuming all the formulas in formula_1.Hilbert-style deduction systems are characterized by the use of numerous schemes of logical axioms.