In sequent calculus, the completeness of atomic initial sequents states that initial sequents A ⊢ A (where A is an arbitrary formula) can be derived from only atomic initial sequents p ⊢ p (where p is an atomic formula). This theorem plays a role analogous to eta expansion in lambda calculus, and dual to cut elimination and beta reduction. Typically it can be established by induction on the structure of A, much more easily than cut elimination.

References

edit
  • Gaisi Takeuti. Proof theory. Volume 81 of Studies in Logic and the Foundation of Mathematics. North-Holland, Amsterdam, 1975.
  • Anne Sjerp Troelstra and Helmut Schwichtenberg. Basic Proof Theory. Edition: 2, illustrated, revised. Published by Cambridge University Press, 2000.
Stub icon

This mathematical logic–related article is a stub. You can help Wikipedia by adding missing information.

📚 Artikel Terkait di Wikipedia

Sequent calculus

redundant: the completeness of atomic initial sequents states that the rule can be restricted to atomic formulas without any loss of provability. Observe

Linear logic

obtain the property that arbitrary initial sequents can be derived from atomic initial sequents, and that whenever a sequent is provable it can be given a

Natural deduction

then Γ ⊢ A. Completeness of ⇒ wrt. ⊢ If Γ ⊢ A, then Γ ⇒ A. It is clear by these theorems that the sequent calculus does not change the notion of truth, because

Theory (mathematical logic)

For first-order logic, the most important case, it follows from the completeness theorem that the two meanings coincide. In other logics, such as second-order

Set theory

377–387, doi:10.1145/362384.362685 Codd, E. F. (1972), "Relational Completeness of Data Base Sublanguages", in Rustin, Randall (ed.), Data Base Systems:

First-order logic

sequent calculus was developed to study the properties of natural deduction systems. Instead of working with one formula at a time, it uses sequents,

Soundness

of the soundness property is the completeness property. A deductive system with a semantic theory is strongly complete if every sentence C {\displaystyle

Gödel's incompleteness theorems

with semantic completeness, which means that the set of axioms proves all the semantic tautologies of the given language. In his completeness theorem (not