Untersuchungen über das logische Schließen I¶
Gentzen, G. (1935). Untersuchungen über das logische Schließen I. Mathematische Zeitschrift, 1934-1935.
Cited by¶
3 citations across 3 artifacts.
Each citation links to the sentence it supports in the citing article.
Primes¶
- Deductive Reasoning
- Deductive reasoning can be understood proof-theoretically (as syntactic derivation from axioms via inference rules — Hilbert-style or natural-deduction systems
This sourceFoundational paper introducing natural deduction and the sequent calculus (systems NK/NJ, LK/LJ) and the cut-elimination Hauptsatz. WebSearch confirmed venue, pages, and the natural-deduction / sequent-calculus / cut-elimination content.
- Deductive reasoning can be understood proof-theoretically (as syntactic derivation from axioms via inference rules — Hilbert-style or natural-deduction systems
- Dependency
- … the failure mode is specifiable — if Lemma 2 is shown to have a counterexample, the main theorem's proof is invalidated in a documented way (Tarski's model-theoretic account of entailment makes the failure mode precise: any model that falsifies the lemma also falsifies any derivation that uses the lemma as a premise).
This sourceFounds natural deduction and the sequent calculus; represents proofs as trees whose nodes depend on parent nodes for derivability — cited inline alongside tarski-1936 on the proof/lemma dependency in the Examples section.
- … the failure mode is specifiable — if Lemma 2 is shown to have a counterexample, the main theorem's proof is invalidated in a documented way (Tarski's model-theoretic account of entailment makes the failure mode precise: any model that falsifies the lemma also falsifies any derivation that uses the lemma as a premise).
Domain-specific¶
- Sequent
- Gentzen's sequent calculi made these two contexts the objects transformed by logical and structural inference rules; a derivation is a tree whose nodes are sequents, not a single sequent enlarged into a proof.
This sourceIntroduces natural deduction and the `LK`/`LJ` sequent calculi, structural rules, and cut elimination.
- Gentzen's sequent calculi made these two contexts the objects transformed by logical and structural inference rules; a derivation is a tree whose nodes are sequents, not a single sequent enlarged into a proof.
Verification¶
Does it exist? Confirmed. This work's DOI resolves to a registered record, which fixes its identity. That is all it fixes.
Does it back the claim? Not recorded. Neither this nor any other of the 3 citations of this work carries a recorded support check.
Was it audited? Yes. A second, independent pass read the citation against the article text and recorded a verdict.
Support is checked per citation rather than per work — the same source can be cited soundly in one article and wrongly in another. Per-citation recording began recently, so a citation with no recorded check is a gap in the record rather than evidence it went unchecked.
See how references were verified.
Links previously used in the corpus¶
Before the registry existed this work was also linked 1 other way.
Registry ID ref:5649ce3b7ede · see in the full table