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.
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!