Born in Bethlehem — Micah 5:2

This page is generated from arguments/TestimonyArguments/BornInBethlehem. Every heading and paragraph below is a docstring in those files; every formula is rendered from the encoding they check. If the page and the source disagree, the page is the one that is wrong, and regenerating it is the fix.

Atoms are numbered propositional variables, numbered once for the whole page, so the same variable means the same claim in every position below. Reading the logic is the short version of what the notation means. A result marked ⚗ is one this library constructs rather than reports.

TestimonyArguments.BornInBethlehem — Phase 1 vertical slice

Matthew 2:5–6 quotes Micah 5:2 as grounds that the Messiah is born in Bethlehem. Both the Christian predictive reading and a critical reading are encoded, and the argument is carried through to a SatisfactionWitness — the first end-to-end connection from cited premises to a claim that a person meets a messianic criterion.

jesusBornInBethlehem is cited to scripture alone. That is visible in the generated manifest via scriptureOnlyAtoms, and it should be: the historicity of the Bethlehem birth is disputed in critical scholarship, and an argument that assumes it on the authority of the texts whose reading is in question is assuming part of what it sets out to show.

The argument is short enough to stay in one file. It runs on a single line of reason, which is exactly why it is the weakest of the fulfilment arguments and why critical_not_establishes costs the rival so little: deny the one interpretive premise and nothing is left standing. Compare BornOfAVirgin, which runs on four.

The claims, numbered

※ grounded in scripture alone: the reading is assumed, not argued for.

quotationEdge

Matthew explicitly quotes Micah — uncontroversial verbal citation, attested across traditions.

def quotationEdge : IntertextEdge :=
  { fromPassage := Scripture.matthew2_6, toPassage := Scripture.micah5_2,
    relation := RelationType.quotation,
    source := Scripture.na28Apparatus Scripture.matthew2_6 }

predictiveReading

The Christian predictive reading of Micah 5:2.

def predictiveReading : Interpretation :=
  { passage := Scripture.micah5_2,
    reading := "Micah 5:2 predicts the Messiah's birthplace as Bethlehem",
    asRelation := some RelationType.prediction,
    source :=
      {
        primary :=
          Reference.work Bib.keilDelitzschMinorProphets
            (Bib.Locus.adLoc Scripture.micah5_2),
        tradition := Tradition.christianTypological,
        confidence := Confidence.wellSupported } }

bornInBethlehem

The criterion this argument establishes a candidate must meet.

def bornInBethlehem : FulfillmentCriterion :=
  { name := "born in Bethlehem", basis := predictiveReading }

cite

Citation and classification for every atom. Total, so nothing is uncited.

def cite : Claim → AtomMeta

The line of reason

One strand, and the argument's whole weight is on it.

toCriterion

From the predictive reading and Matthew's intent, the criterion follows.

toFulfilment

From the criterion and the historical claim, the fulfilment follows.

predictiveLine — Predictive reading of Micah 5:2

The predictive line. Micah's oracle read as prophecy, Matthew's quotation read as a fulfilment claim, and the criterion that follows.

criticalLine — Critical reading of Micah 5:2 as a near-term oracle

The critical line: the quotation is granted and the prediction denied, so the same step delivers nothing.

Packages

christian — Christian predictive reading of Micah 5:2

The Christian predictive argument.

Grounded in scripture alone: Jesus of Nazareth was born in Bethlehem.

critical — Critical reading of Micah 5:2 as a near-term oracle

The critical reading: the quotation is granted, the prediction is not.

Grounded in scripture alone: Jesus of Nazareth was born in Bethlehem.

Results

christian_establishes

Given the Christian premises, the conclusion follows.

theorem christian_establishes : Establishes christian
-- axioms: propext, Quot.sound

criticalReading

The critical reading, written down: Micah's oracle concerns a contemporary Judaean ruler, so no messianic birthplace criterion arises and nothing about Jesus follows from it.

def criticalReading : Valuation Claim :=
  fun a =>
    match a with
    | Claim.micahPredictsBethlehem => False
    | Claim.messiahBornInBethlehem => False
    | Claim.jesusSatisfiesCriterion => False
    | x => True

critical_not_establishes

The critical reading does not establish the conclusion.

theorem critical_not_establishes : ¬Establishes critical
-- axioms: propext, Quot.sound

jesus_satisfies_bethlehem

End to end: under the Christian package, Jesus satisfies the Bethlehem criterion. This is the first result in the library that runs from cited premises through a machine-checked entailment to a claim about a person.

theorem jesus_satisfies_bethlehem : Satisfies jesus bornInBethlehem
-- axioms: propext, Quot.sound

Satisfiability

Entails is vacuously true over a premise set with no model, so a package built from contradictory premises would establish its conclusion with every gate passing. Only the package carrying a positive Establishes result needs checking: critical has a countermodel already, and a countermodel is a valuation satisfying every premise.

Not tagged @[headline] — a claim about the health of the encoding rather than about Micah.

everythingHoldsReading

The reading on which every claim in this argument holds at once.

def everythingHoldsReading : Valuation Claim :=
  fun x => True

christian_is_satisfiable

The Christian package has a model, so christian_establishes is not vacuous.

theorem christian_is_satisfiable : Satisfiable christian.premises
-- axioms: propext, Quot.sound