Untersuchungen über das logische Schließen I¶
Gentzen, G. (1935). Untersuchungen über das logische Schließen I. Mathematische Zeitschrift, 1934-1935.
Cited by¶
4 citations across 4 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 (marker 224).
- … 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).
- Setup–Resolution Pair
- And the scope discipline is what makes both detectable: the bearer here is the proof's own nesting structure, which holds each assumption open and refuses to let anything derived under it escape until the pairing move is made.
This sourceEstablishes natural deduction with assumption discharge and scope discipline, so that a derivation carrying an undischarged assumption is incomplete as a unit and only the implication-introduction move retires it.
- And the scope discipline is what makes both detectable: the bearer here is the proof's own nesting structure, which holds each assumption open and refuses to let anything derived under it escape until the pairing move is made.
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¶
This reference passed the adversarial substantiation pipeline: it was checked to exist and to support the claim it is attached to. 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