Quote by andrewr
Yes, and Yes, although your second question can't be written down inside a text terminal of this size. Representation of an integer is not the same as existence of that same integer.
There are many counting numbers which we know exist, but can't be written down inside a text terminal of this size.
You would agree, no doubt, that "0.999999999....." is a representation of a real number; and by the ellipsis I am suggesting a pattern for something which is much larger than I would like to write down, although I DO KNOW HOW to write it down  eg: and that the representation improves in accuracy and may have a selectable accuracy for a given discussion or purpose.
The algorithm itself can be adapted for various constraints; eg: there are many such algorithms based on a similar methodology.
DO you care if I count only the positive reals, or do I need to include the negative as well?
etc.

if you give a recursive enumeration of every real between 0 and 1, that should sufice. such an algorithm, if you indeed possess it and it does what you claim, it would be of great interest to many people.
but...it is highly likely that there is an undiscovered flaw in your algorithm, which might not easily be detectable (especially if the algorithm is of sufficient complexity).
Quote by micromass
A commutative diagram is not a proof. And many mistakes in category theory actually amount to misleading diagrams. A commutative diagram is a suggestion of a proof. It is merely an illustration.
If you look at Bourbaki, then they show that they treat commutative diagrams very rigorously. They try to prove everything with algebraic means.
To me, a proof is correct if it formilizable in some kind of logical system. You don't actually NEED to formalize it, but just giving a suggestion that it can be done is good enough.

commutative diagrams COULD be proofs. for example p→q is just a small diagram. yes, you have a "different kind of formalizing", but logical need not be lingual. the common usage of diagrams now IS informal, this is true, but formal systems can be created which aren't string manipulation. an example can be found in:
http://www.amazon.com/LawsFormGSp.../dp/0963989901
until relatively recently, geometric proofs ("pictures" a la Euclid), were the gold standard of "formal proofs". it's likely that as we accumulate more knowledge, better formal systems using more sophisticated building blocks will emerge.
(by the way, metamath is an awesome site).
Quote by Hurkyl
Ah joy, "completed infinity".
Just for your information, I have never encountered somebody who uses that terms that could give an even quasirigorous account of what the term means.
From observing people who use it, I quite honestly believe that it literally means "I am unwilling or unable to engage in one more layer of abstraction, and thus have failed to recognize that we're talking about the same idea." (I don't mean insult by this, except possibly in the 'unwilling' case)

why, the uniquely defined impossibly inaccessible cardinal, of course :P