= 27d567bc2d48d9f40e9ccc20ea370b15)
" So the following derivation principles seem reasonable, where the latin indexes (a,b,c...) are meant to represent numbers that can be arbitrarily close to zero"
so universally quantified, but in the meta language.
In response to
Probabilistic Löb theorem
Why would you leave out quantifiers? Requiring the reader to stick their own existential or universal quantification in the necessary places isn't very nice.
Is this the correct interpretation of your assumptions? If not, what is it? I am not interested in figuring out which axioms are required to make your proof (which is also missing quantifiers) work.
- If ⊢ A, then ⊢ ∀(a < 1)(□a A).
- ⊢ □aA → ∀(c < 1)(∃(b > 0)(□c□a+b A)).
- ⊢ □a(A → B) → ∃(b > 0)(□bA → □a+bB).
In response to
You only need faith in two things
This phrase confuses me:
and that some single large ordinal is well-ordered.
Every definition I've seen of ordinal either includes well-ordered or has that as a theorem. I'm having trouble imagining a situation where it's necessary to use the well-orderedness of a larger ordinal to prove it for a smaller one.
*edit- Did you mean well-founded instead of well-ordered?
Every ordinal (in the sense I use the word[1]) is both well-founded and well-ordered.
If I assume what you wrote makes sense, then you're talking about a different sort of ordinal. I've found a paper[2] that talks about proof theoretic ordinals, but it doesn't talk about this in the same language you're using. Their definition of ordinal matches mine, and there is no mention of an ordinal that might not be well-ordered.
Also, I'm not sure I should care about the consistency of some model of set theory. The parts of math that interact with reality and the parts of math that interact with irreplaceable set theoretic plumbing seem very far apart.
[1] An ordinal is a transitive set well-ordered by "is an element of".
[2] www.icm2006.org/proceedings/VolII/contents/ICMVol203.pdf
In response to
You only need faith in two things
This phrase confuses me:
and that some single large ordinal is well-ordered.
Every definition I've seen of ordinal either includes well-ordered or has that as a theorem. I'm having trouble imagining a situation where it's necessary to use the well-orderedness of a larger ordinal to prove it for a smaller one.
*edit- Did you mean well-founded instead of well-ordered?
= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
= f037147d6e6c911a85753b9abdedda8d){kind=logo}
As Larks said, we can quantify (the meta language looking in), but the system itself can't quantify. Because then the system could reason that "∀x>0, P(A)<x" means "P(A)=0", which is the kind of thing that causes bad stuff to happen. Here, the system can show "P(A)<x" separately for any given x>0, but can't prove the same statement with the universal quantifier.
Is it unreasonable of me to be annoyed at that kind of writing?
If I understand what's going on correctly, you have a real-indexed schema of axioms and each of them is in your system.
When I read the axiom list the first time I saw that the letters were free variables (in the language you and I are writing in) and assumed that you did not intend for them to be free variables in the formula. My suggestion of how to bind the variables (in the language we are writing in) was (very) wrong, but I still think that it's unclear as written.
Am I confused?