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.
″ 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.
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.
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).
″ 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.
Thank you.
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?
No, it’s perhaps not the best explained post I’ve done. Though it was intended more for technical purposes.
Not any more, I hope!