Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Independence questions in a finite axiom-schematization of first-order logic

Benoit Jubin

TL;DR

Some independence results in a finite axiom-schematization of classical first-order logic and it is proved that a certain axiom scheme of this system is independent although all of its instances are provable from the other axiom schemes.

Abstract

We review some independence results in a finite axiom-schematization of classical first-order logic introduced by Norman Megill. We also prove that a certain axiom scheme of this system is independent although all of its instances are provable from the other axiom schemes.

Independence questions in a finite axiom-schematization of first-order logic

TL;DR

Some independence results in a finite axiom-schematization of classical first-order logic and it is proved that a certain axiom scheme of this system is independent although all of its instances are provable from the other axiom schemes.

Abstract

We review some independence results in a finite axiom-schematization of classical first-order logic introduced by Norman Megill. We also prove that a certain axiom scheme of this system is independent although all of its instances are provable from the other axiom schemes.
Paper Structure (35 sections, 14 theorems, 27 equations)

This paper contains 35 sections, 14 theorems, 27 equations.

Table of Contents

  1. Plan of the article
  2. Acknowledgments
  3. Norman Megill
  4. The formal system
  5. Schemes
  6. Proofs
  7. From the scheme level to the object level (and back?)
  8. Independence
  9. Emulating the object level at the scheme level
  10. Soundness and Completeness
  11. Independence
  12. Object-independence
  13. Propositional calculus
  14. Object-independence of modus ponens
  15. Object-independence of the axioms of propositional calculus
  16. ...and 20 more sections

Key Result

Proposition 1.1

A scheme proves all its instances. If $P$ is a proof of the scheme $\Phi$ from the set of schemes $S$ and $\sigma$ is a substitution, then $P^\sigma$ is a proof of $\Phi^\sigma$ from $S^\sigma$ and from $S$. If a scheme is provable from a given set of schemes, then so are all its instances. If the s

Theorems & Definitions (37)

  • Remark 1
  • Remark 2
  • Proposition 1.1
  • proof
  • Proposition 1.2
  • proof
  • Remark 1.3
  • Proposition 1.4
  • Remark 1.5
  • Theorem 2.1: Soundness
  • ...and 27 more