Single Idea 13619

[catalogued under 5. Theory of Logic / H. Proof Systems / 2. Axiomatic Proof]

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]