|
|
Re: 10^7-ZFC
Posted:
Apr 24, 2012 7:28 AM
|
|
On Apr 24, 7:56 pm, "Ross A. Finlayson" <ross.finlay...@gmail.com>
wrote:
>
> Heh, no, Noodles and Asparagus, I know what that is.
>
I think I had that last night. I just spent the last 6 nights
rationing 10 packets of 2 minute noodles, though I found an old can of
vegetable soup last night.
Finally convinced someone from Facebook to drive 400km to pick me up
on the side of the highway!
Okay now!
While formula or proof length finite boundaries is one type of model,
let's call it Formula_Width_Limited
A more useful model would be a finite bound on the number of axiom
invocations starting will a null formula, Formula_Depth_Limited.
I call these axiom invocations AXIOPS.
I think this correlates to the levels of the constructable ZFC
Universe U.
Proof checkers use heuristics to select which Axiom to invoke to match
to the current goal to prove.
START
NULL FORMULA
()
Axiom-a() -> S 1 AXIOP
Axiom-b(S) -> SS 2 AXIOPS
Axiom-c(SS) -> SSS 3 AXIOPS
Axiom-d(SSS) -> SSSS 4 AXIOPS
...
Axiom-x(SS..) -> SSS..
Formula_Depth_Limited to X AXIOPS
Herc
|
|
