|
|
Re: 10^7-ZFC
Posted:
May 13, 2012 2:20 PM
|
|
On May 13, 2:02 pm, "LudovicoVan" <ju...@diegidio.name> wrote:
> "Alan Smaill" <sma...@SPAMinf.ed.ac.uk> wrote in message
>
> news:fwe7gx42i73.fsf@eriboll.inf.ed.ac.uk...
>
>
>
>
>
>
>
>
>
> > "LudovicoVan" <ju...@diegidio.name> writes:
> >> "Aatu Koskensilta" <aatu.koskensi...@uta.fi> wrote in message
> >>news:87r4vdwlo6.fsf@uta.fi...
> >>> Zuhair <zaljo...@gmail.com> writes:
>
> >>>> Consistency can be viewed as a piddling correctness condition
> >>>> informally yes, but of course it can depart from that, correctness or
> >>>> Truth match is stronger than consistency, ZFC + ~Con(ZFC) is
> >>>> consistent but not true (if ZFC is consistent of course).
>
> >>> Right, which is why consistency is a piddling correctness condition:
>
> >> Down there in the engineering room, we care much more for correctness:
> >> then we know that the system in question is at least as reliable as
> >> its premises are.
>
> > You're not worried about whether your premises/specifications
> > are consistent?
>
> Is it just sci-fi that we could build up a system step by step, adding an
> axiom/definition at a time, along with its closure, and checking the
> correctness of the resulting system at each step? If that is possible,
> wouldn't the resulting system always stay correct and, a fortiori,
> consistent?
>
> Thanks for any enlightenment,
>
> -LV
Actually that's an idea that occurred into my mind, but I really don't
know what strength theories built in this way would have.
My guess is that theories built in this way (which are consistent by
definition!) are weak theories, anyhow I'm not sure of the effect of
this method.
A nice example that I gave once to do that is to number all symbols
used in a language, and each formula would receive a number that is
obtained by concatenation of the numbers
of individual symbols in it in sequence, so we obtain a unique number
for each formula, and not two different formulas share the same
number, something like Godel's numbers.
Then we start with substituting formulas in the axiom schema of Naive
comprehension such that we begin with the smallest sized formula
having the smallest number, lets' say that was y=y. Now we check if
Exist x for all y. y e x <-> y=y is not refuted in Extensionality +
FOL(e,=)+Identity theory, lets say the proof of such non decidability
is to be carried in less than 100 steps, now after having this proof
we add that sentence (call it Exist V) to the list of axioms of the
theory we wont to define. Now we take the next formula which has three
characters and having the next Godel number, lets say it was y e y,
and we repeat the above check (with the proof in 100 steps from Ext.
+FOL(e,=)+Identity theory+ Exist V) Now if a proof of non decidability
of the resulting substitution was not found then we add the sentence
Exist x. For all y. y e x <-> y e y, and so on......
The merit is that those theories recursively defined in that way are
CONSISTENT BY DEFINITION. so unlike ordinary theories which are
defined and then after completing their definition one tries to prove
them consistent, here the above theory is consistent by definition.
Anyhow I'm not sure what kind of theories can be obtained in such a
manner, I mean how strong they could be??? are they useful for
mathematics? I'm not sure.
Zuhair
|
|
