The fair enumeration of a consistency property #
Let C be a consistency property over L and s a countable member of C. This file extends
s along an increasing chain of members of C, the stages C.stage s e q n, whose union
C.limit s e q contains the target of every clause of C whenever it contains the clause's
trigger: one chosen component of each disjunctive sentence, every component of each conjunctive
one, every Henkin-constant instance of a universal sentence, a witness to each negated
universal sentence, the reflexive equations, substitution of equals into atomic sentences, and an
equation naming each closed term by a Henkin constant. The limit contains neither ⊥ nor a
sentence together with its negation, since each of these would already lie in a stage. The limit
itself is not claimed to be a member of C. These are the properties from which the term model
of the model existence theorem is built.
Each stage adds at most one sentence to the previous one. A request
(ConsistencyProperty.Request) names one clause of C together with its parameters; the
sentences that trigger the clause are named by sources ℕ ⊕ ℕ, where Sum.inl j is the j-th
term of a sequence e enumerating s, and Sum.inr m is the m-th sentence added so far. Every
sentence of the limit is therefore named by a source that keeps naming it from some stage on, so
the requests can be enumerated in advance even though the limit is not known in advance. With
countably many function and relation symbols there are countably many requests. The schedule
q : ℕ → Request L is consulted at stage n at the request q n.unpair.1, so a surjective q
fires every request at arbitrarily late stages. For a countable s over a language with
countably many symbols, an enumeration e with s ⊆ Set.range e exists by
Set.countable_iff_exists_subset_range, and a surjective schedule by exists_surjective_nat.
A request fires by adding one target of its clause, chosen so that the stage stays a member of
C; when its triggers are present, the clause of C guarantees that such a target exists.
Main definitions #
FirstOrder.Language.ConsistencyProperty.Request: the requests of the enumeration.FirstOrder.Language.ConsistencyProperty.stage: the stages of the enumeration.FirstOrder.Language.ConsistencyProperty.limit: their union.
Main results #
FirstOrder.Language.ConsistencyProperty.stage_mem: every stage is a member.FirstOrder.Language.ConsistencyProperty.monotone_stage: the stages increase.FirstOrder.Language.ConsistencyProperty.bot_notMem_limitandFirstOrder.Language.ConsistencyProperty.not_notMem_limit: the limit contains neither⊥nor a sentence together with its negation.FirstOrder.Language.ConsistencyProperty.limit_imp, …,FirstOrder.Language.ConsistencyProperty.limit_eq_name: the limit contains the target of each clause whose trigger it contains, one lemma per clause.
References #
- D. Marker, Lectures on Infinitary Model Theory, Cambridge University Press, 2016, §4.1.
- H. J. Keisler, Model Theory for Infinitary Logic, North-Holland, 1971.
cameronfreer/infinitary-logicat commit518a366cba97b1ae8c4dc64a297a396939bc3e0b,InfinitaryLogic/Methods/Henkin/CountableCompletion/FairEnumeration.lean, which formalizes a fair enumeration of requests whose firing makes a classical choice and leaves its trigger in place. Divergences from that source: the requests name their triggers through the history of the enumeration rather than through a precomputed countable universe of sentences closed under the decomposition targets; the requests follow the clauses ofConsistencyProperty, which allows function symbols and has a naming clause for closed terms; and the schedule fires the requestq n.unpair.1at stagenrather than sweeping prefixes.
A request of the enumeration: a clause of ConsistencyProperty together with its
parameters. The sentences triggering the clause are named by sources ℕ ⊕ ℕ: Sum.inl j names
the j-th sentence of the enumeration of the starting set, and Sum.inr m the m-th sentence
added by the enumeration.
- imp
{L : Language}
(i : ℕ ⊕ ℕ)
: Request L
Decompose the implication named by the source.
- notImpLeft
{L : Language}
(i : ℕ ⊕ ℕ)
: Request L
Extract the hypothesis of the negated implication named by the source.
- notImpRight
{L : Language}
(i : ℕ ⊕ ℕ)
: Request L
Extract the negated conclusion of the negated implication named by the source.
- iInf
{L : Language}
(i : ℕ ⊕ ℕ)
(k : ℕ)
: Request L
Extract the
k-th conjunct of the conjunction named by the source. - notIInf
{L : Language}
(i : ℕ ⊕ ℕ)
: Request L
Choose a negated conjunct of the negated conjunction named by the source.
- iSup
{L : Language}
(i : ℕ ⊕ ℕ)
: Request L
Choose a disjunct of the disjunction named by the source.
- notISup
{L : Language}
(i : ℕ ⊕ ℕ)
(k : ℕ)
: Request L
Extract the negated
k-th disjunct of the negated disjunction named by the source. - all
{L : Language}
(i : ℕ ⊕ ℕ)
(c : ℕ)
: Request L
Instantiate the universal sentence named by the source at the Henkin constant
c. - notAll
{L : Language}
(i : ℕ ⊕ ℕ)
: Request L
Choose a witness to the negated universal sentence named by the source.
- eqRefl
{L : Language}
(t : (L.withConstants ℕ).Term (Empty ⊕ Fin 0))
: Request L
Add the equation
t = t. - eqSubst
{L : Language}
(i j : ℕ ⊕ ℕ)
(φ : { φ : (L.withConstants ℕ).BoundedFormulaω Empty 1 // BoundedFormulaInf.IsAtomic φ })
: Request L
Substitute the equation named by
iinto the instance ofφnamed byj. - eqName
{L : Language}
(t : (L.withConstants ℕ).Term (Empty ⊕ Fin 0))
: Request L
Name the closed term
tby a Henkin constant.
Instances For
With countably many function and relation symbols, there are countably many requests, so
that a surjective schedule ℕ → Request L exists.
The n-th stage of the enumeration of C starting from s, where e enumerates s
and q is the schedule of requests: s together with the sentences added by the first n
requests.
Instances For
The limit of the enumeration of C starting from s: the union of its stages.
Instances For
A sentence lies in the limit exactly when it lies in some stage.
Every stage is contained in the limit.
The starting set is the zeroth stage.
Each stage is contained in the next.
The stages of the enumeration increase.
The starting set is contained in every stage.
The starting set is contained in the limit.
Every stage of the enumeration starting from a member is a member.
The limit of the enumeration starting from a member does not contain ⊥.
The limit of the enumeration starting from a member does not contain a sentence together with its negation.
Firing requests #
The clauses in the limit #
The limit contains the negated hypothesis or the conclusion of each of its implications.
The limit contains the hypothesis and the negated conclusion of each of its negated implications.
The limit contains every conjunct of each of its countable conjunctions.
The limit contains the negation of some conjunct of each of its negated countable conjunctions.
The limit contains some disjunct of each of its countable disjunctions.
The limit contains the negation of every disjunct of each of its negated countable disjunctions.
The limit contains the instance at every Henkin constant of each of its universal sentences.
The limit contains a witness at some Henkin constant to each of its negated universal sentences.
The limit contains every reflexive equation between closed terms.
The limit is closed under substitution of equals into atomic sentences.
The limit contains, for every closed term, an equation naming it by a Henkin constant.