A Mathematical Introduction to Logic¶
Enderton, H. B. (2000). A Mathematical Introduction to Logic. Academic Press.
Cited by¶
20 citations across 20 artifacts.
Each citation links to the sentence it supports in the citing article.
Primes¶
- Canonical Form
- In logic and proof theory it is conjunctive and disjunctive normal form, prenex and Skolem normal form, and beta-normal form in lambda calculus.
This sourceStandard reference for conjunctive, disjunctive, prenex, and Skolem normal forms.
- In logic and proof theory it is conjunctive and disjunctive normal form, prenex and Skolem normal form, and beta-normal form in lambda calculus.
- Decidability Computability
- Mathematical logic. Decidable versus undecidable theories — Presburger arithmetic decidable by quantifier elimination, Peano arithmetic undecidable by Church's theorem, the theory of real-closed fields (elementary geometry over the reals) decidable so a fixed algorithm settles geometric statements that defeat human geometers — where the class is the well-formed formulas closed under the theory's rules, the procedure a decision algorithm for theoremhood, and the question "is this a theorem?"
This sourceTreats decidable versus undecidable theories, including Presburger arithmetic's decidability by quantifier elimination and the undecidability of richer theories.
- Mathematical logic. Decidable versus undecidable theories — Presburger arithmetic decidable by quantifier elimination, Peano arithmetic undecidable by Church's theorem, the theory of real-closed fields (elementary geometry over the reals) decidable so a fixed algorithm settles geometric statements that defeat human geometers — where the class is the well-formed formulas closed under the theory's rules, the procedure a decision algorithm for theoremhood, and the question "is this a theorem?"
- Deductive Reasoning
- Mathematics and formal logic Theorem proving from axioms; propositional and predicate calculus; model theory and proof theory; computer-checked formal verification. Philosophy Classical syllogistic logic (Aristotle); symbolic logic (Frege, Russell); analytic philosophy's use of deduction in conceptual analysis. Computer science and formal methods Automated theorem proving
This sourceStandard graduate text on first-order logic covering proof, truth, soundness, completeness, and computability (incl. a dedicated Soundness and Completeness Theorems section). WebSearch confirmed coverage. Cited for computer-science / formal-methods uses of deduction; supports formal-logic foundations though it is not centrally about automated theorem proving.
- Mathematics and formal logic Theorem proving from axioms; propositional and predicate calculus; model theory and proof theory; computer-checked formal verification. Philosophy Classical syllogistic logic (Aristotle); symbolic logic (Frege, Russell); analytic philosophy's use of deduction in conceptual analysis. Computer science and formal methods Automated theorem proving
- Epistemic Mode Of A Proposition
- In logic and mathematics, its origin substrate, the mode vocabulary is sharply typed and the gating is explicit: an Axiom is used freely but cannot be refuted from within its system, a theorem is an asserted result that has been proved, a conjecture is a target held open for proof or disproof, a premise under conditional proof is discharged to convert a conditional into a categorical, and a lemma is a proved waypoint — and the whole architecture of proof is a discipline of mode transitions (conjecture → theorem, premise → discharged conditional).
This sourceStandard mathematical-logic text covering deductive systems, the deduction theorem, and conditional proof — the introduction of a premise/assumption and its discharge to convert a derived conclusion into a categorical conditional, supporting the axiom/theorem/premise typing and the discharge operation.
- In logic and mathematics, its origin substrate, the mode vocabulary is sharply typed and the gating is explicit: an Axiom is used freely but cannot be refuted from within its system, a theorem is an asserted result that has been proved, a conjecture is a target held open for proof or disproof, a premise under conditional proof is discharged to convert a conditional into a categorical, and a lemma is a proved waypoint — and the whole architecture of proof is a discipline of mode transitions (conjecture → theorem, premise → discharged conditional).
- Local-to-Global Aggregation
- Mathematical induction — base case plus induction step aggregate to a statement over all naturals; the well-ordering of the naturals is the discipline.
This sourceMathematical induction (base case plus induction step) lifting to a statement over all naturals, licensed by the well-ordering of the naturals.
- Mathematical induction — base case plus induction step aggregate to a statement over all naturals; the well-ordering of the naturals is the discipline.
- Predicate
- In logic and mathematics first-order logic is built on predicates and quantifiers, set-builder notation defines a set as the extension of a predicate, relations are multi-place predicates, and type systems are predicate-based.
This sourceStandard text developing first-order logic with predicates, quantifiers, and the satisfier-set (extension) of a predicate.
- In logic and mathematics first-order logic is built on predicates and quantifiers, set-builder notation defines a set as the extension of a predicate, relations are multi-place predicates, and type systems are predicate-based.
- Preimage
- In logic the antecedent set of a conclusion — every set of premises that entails it — is the preimage under the entailment mapping.
This sourceDefines the semantic consequence relation (Γ ⊨ α: every model of the premise set Γ satisfies α), so the family of premise-sets entailing a conclusion is the preimage of that conclusion under entailment.
- In logic the antecedent set of a conclusion — every set of premises that entails it — is the preimage under the entailment mapping.
- Surjectivity
- In logic it is the witness clause of the existential quantifier — a model satisfies "for every y there exists an x such that f(x) = y" exactly when the interpretation of f is surjective — so completeness of a construction is a surjectivity claim.
This sourceThe existential-quantifier witness clause and the satisfaction of '∀y ∃x f(x)=y' exactly when the interpretation of f is surjective.
- In logic it is the witness clause of the existential quantifier — a model satisfies "for every y there exists an x such that f(x) = y" exactly when the interpretation of f is surjective — so completeness of a construction is a surjectivity claim.
Domain-specific¶
- Deductive closure
- Formal Theory
- Formation rule
- Functional completeness
- Literal (Mathematical Logic)
- Metatheorem
- NAND Logic
- Every Boolean function of finitely many variables can be expressed by a finite composition of NAND operations
This sourceEnderton's section 1.5, 'Sentential Connectives', is the complete-sets-of-connectives material this result belongs to; the section text was not reachable for direct confirmation in this pass.
- Every Boolean function of finitely many variables can be expressed by a finite composition of NAND operations
- Non-logical symbol
- Principle of distributivity
- Symbol (formal)
Mechanisms¶
- Empty Set Literal
- … trap is vacuous truth: every universally quantified statement about the members of `∅` is true, which is logically correct but routinely surprising — "all items in the empty cart are discounted" evaluates to true, and a rule engine that reads that as a green light can act on nothing as though it were something.
This sourceA universal statement restricted to an empty set has no counterexample and is therefore true under standard quantifier semantics.
- … trap is vacuous truth: every universally quantified statement about the members of `∅` is true, which is logically correct but routinely surprising — "all items in the empty cart are discounted" evaluates to true, and a rule engine that reads that as a green light can act on nothing as though it were something.
- Existential Witness Card
- In logic this is exactly the role of a witness: the object that makes an existential true
This sourceDefines an existential formula as true when some object in the domain satisfies its matrix.
- In logic this is exactly the role of a witness: the object that makes an existential true
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 20 citations of this work carries a recorded support check.
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 5 other ways.
- https://www.sciencedirect.com/book/9780122384523/a-mathematical-introduction-to-logic ×3
- https://www.educate.elsevier.com/book/details/9780080496467 ×2
- https://www.elsevier.com/books/a-mathematical-introduction-to-logic/enderton/978-0-12-238452-3 ×2
- https://www.google.com/books/edition/A_Mathematical_Introduction_to_Logic/dVncCl_EtUkC ×2
- https://shop.elsevier.com/books/a-mathematical-introduction-to-logic/enderton/978-0-12-238452-3 ×1
Registry ID ref:c1f83b889e28 · see in the full table