On 9/2/2024 8:25 PM, Ross Finlayson wrote:
> On 09/02/2024 02:46 PM, Jim Burns wrote:
>> On 9/1/2024 2:44 PM, Ross Finlayson wrote:
>>> Then the point that induction lets out is
>>> at the Sorites or heap,
>>> for that Burns' "not.first.false", means
>>> "never failing induction first thus
>>> being disqualified arbitrarily forever",
>>
>> Not.first.false is about formulas which
>> are not necessarily about induction.
>>
>> A first.false formula is false _and_
>> all (of these totally ordered formulas)
>> preceding formulas are true.
>>
>> A not.first.false formula is not.that.
>>
>> not.first.false Fₖ ⇔
>> ¬(¬Fₖ ∧ ∀j> Fₖ ∨ ∃j> ∀j>
>> A finite formula.sequence S = {Fᵢ:i∈⟨1…n⟩} has
>> a possibly.empty sub.sequence {Fᵢ:i∈⟨1…n⟩∧¬Fᵢ}
>> of false formulas.
>>
>> If {Fᵢ:i∈⟨1…n⟩∧¬Fᵢ} is not empty,
>> it holds a first false formula,
>> because {Fᵢ:i∈⟨1…n⟩} is finite.
>>
>> If each Fₖ ∈ {Fᵢ:i∈⟨1…n⟩} is not.first.false,
>> {Fᵢ:i∈⟨1…n⟩∧¬Fᵢ} does not hold a first.false, and
>> {Fᵢ:i∈⟨1…n⟩∧¬Fᵢ} is empty, and
>> each formula in {Fᵢ:i∈⟨1…n⟩} is true.
>>
>> And that is why I go on about not.first.false.
> Then about not.first.false
> thanks for writing that up a bit more,
> then that also you can see what I make of it.
What I find poetic about not.first.false and all that
is that our finiteness isn't only _permitted_
It is _incorporated into_ our logic. _Required_
A finite linear order _must be_ well.ordered
(must be, both ways)
∀γ:T(γ) ⇐ ∀β:(T(β) ⇐ ∀α<β:T(α))
∀α:T(α) ⇐ ∀β:(T(β) ⇐ ∀γ>β:T(γ))
We are finite.
The formulas we write are finitely.many.
In a linear order, they must be in a well.order.
In a well.order,
if each formula Φ[β] is not.first.false
∀β:¬(¬T(Φ[β] ∧ ∀α<β:T(Φ[α])
∀β:(T(Φ[β]) ⇐ ∀α<β:T(Φ[α]))
then each formula is not.false.
∀γ:T(Φ[γ])
...because well.order (because finite).
∀γ:T(Φ[γ]) ⇐ ∀β:(T(Φ[β]) ⇐ ∀α<β:T(Φ[α]))
> Not.ultimately.untrue, ..., has that
> F, bears the value for all F_alpha parameterized by ordinals
> (which suffice, large enough, to totally order things),
> of true, and that,
> there are classes of formulas F,
> for example self-referential or differential formulas,
> defined for example according to
> "when F_alpha is not also as for an ordinal less than omega",
> at least making a trivial clear example of
> a definition that is for classes of these sorts formulas
> where "not.ultimately.untrue" is not held by all classes
> for formulas "not.first.false".
"Not.ultimately.untrue" sounds to me vaguely like "ω-consistent".
But I don't really know what you are talking about.
I usually don't know what you are talking about.
It is what it is.
|
|