more from this thinker     |     more from this text

Single Idea 13619

[filed under theme 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 Ref

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]

The 7 ideas with the same theme [proofs built up from some initially accepted truths]:

22277 Boole's method was axiomatic, achieving economy, plus multiple interpretations [Boole, by Potter]
13609 Frege produced axioms for logic, though that does not now seem the natural basis for logic [Frege, by Kaplan]
13619 Quantification adds two axiom-schemas and a new rule [Bostock]
13622 Axiom systems from Frege, Russell, Church, Lukasiewicz, Tarski, Nicod, Kleene, Quine... [Bostock]
13687 No assumptions in axiomatic proofs, so no conditional proof or reductio [Sider]
13688 Good axioms should be indisputable logical truths [Sider]
12198 Geometrical axioms in logic are nowadays replaced by inference rules (which imply the logical truths) [Rumfitt]