are they still smaller than omega1CK?what are the notations of them?
The prooftheoretic ordinal of any theory is less than $\omega_1^{CK}$. No notations are known for secondorder arithmetic, let alone ZFC.

1$\begingroup$ Henry, could you elaborate with further explanation of your first sentence? For example, what exactly would it mean to have the prooftheoretic ordinal of ZFC? (And by the way, thanks again for your talk at CUNY last week.) $\endgroup$ – Joel David Hamkins Mar 24 '14 at 23:30

1$\begingroup$ Is the notion of $\omega_1^{CK}$ absolute? I mean, it's a fairly small ordinal (as countable ordinals go), so certainly it is less than the least height of a transitive model of $\sf ZFC$. But given two transitive models of $\sf ZFC$ (regardless to their size), do they have to agree [with $V$] on $\omega_1^{CK}$? (@Joel, you might know the answer to that as well, so I'm pinging you too.) $\endgroup$ – Asaf Karagila♦ Mar 25 '14 at 0:32

1$\begingroup$ For transitive models, yes, it is absolute, since transitive models have all the same TM programs and they agree on whether a given relation on the natural numbers is wellfounded or not. Meanwhile, there are models of ZFC with the same $\mathbb{N}$ that disagree on $\omega_1^{CK}$; this is proved in my recent paper jdh.hamkins.org/satisfactionisnotabsolute. $\endgroup$ – Joel David Hamkins Mar 25 '14 at 0:35

1$\begingroup$ @JoelDavidHamkins: The prooftheoretic ordinal of a theory T is usually defined to be the smallest ordinal $\alpha$ such that there is no computable (equivalently: primitive recursive) representation of $\alpha$ as an ordering of $\mathbb{N}$ such that T proves the wellfoundedness of this ordering. Such an ordinal exists and is less than $\omega_1^{CK}$ because $\omega_1^{CK}$ is, by definition, larger than any ordinal with a computable representation. $\endgroup$ – Henry Towsner Mar 25 '14 at 3:36

$\begingroup$ Roughly what I was saying at the start of that talk was that usually when we talk about a prooftheoretic ordinal, we expect it to have various other properties as well, and sometimes people take one of those to be the definition. But for ZFC (as a "reasonable" theory), they're probably equivalent anyway. $\endgroup$ – Henry Towsner Mar 25 '14 at 4:15