Full Idea
New axiom-schemas for quantifiers: (A4) |-∀ξφ → φ(α/ξ), (A5) |-∀ξ(ψ→φ) → (ψ→∀ξφ), plus the rule GEN: If |-φ the |-∀ξφ(ξ/α).
Clarification
GEN stands for 'generalisation'
Gist of Idea
Quantification adds two axiom-schemas and a new rule
Source
David Bostock (Intermediate Logic [1997], 5.6)
Book Reference
Bostock,David: 'Intermediate Logic' [OUP 1997], p.221
A Reaction
This follows on from Idea 13610, where he laid out his three axioms and one rule for propositional (truth-functional) logic. This Idea plus 13610 make Bostock's proposed axiomatisation of first-order logic.
Related Idea
Idea 13610 A logic with ¬ and → needs three axiom-schemas and one rule as foundation [Bostock]