|
|
George Dance wrote:
> Chris Menzel wrote:
> > On 18 Aug 2006 17:33:32 -0700, George Dance <georgedance04@xxxxxxxx>
> > said:
> > > ...
> > > What's all this about axioms being proveable in a system? I've never
> > > heard of such a system - how does that work?
> >
> > In pretty much every mathematical logic text, a proof in an (axiomatic)
> > system S is defined to be a sequence of formulas (in the language of S),
> > each of which is either an axiom of S or follows from formulas occurring
> > earlier in the sequence by a rule of inference of S. A formula F is
> > said to provable in S if F is the formula occurring last in a proof in
> > S. Thus, trivially, for any axiom A of S, the 1-element sequence <A> is
> > a proof of A in S; so A is provable in S.
>
> Thank you, Chris. I have heard of such one-line proofs - in fact, I
> remember a longish thread about the term 'self-proving procedures' in
> which they came up here on sci.logic. However, that can't be what Nam
> is talking about; as he mentioned using model theory to prove that an
> axiom unproveable, and as there would be such a 'self-proof' of the 5th
> axiom in G, he can't mean a proof procedure like that.
i took it to mean
nam was looking for a model framework for forcing
that could prove the independence of the 5th axiom
in other words
starting with the assumption
of a the standard four "geometric" axioms
(and a logical calculus of application)
is there a "natural" language
where we can form boolean valued models
whose generic objects can prove independence
of course
the result has been known for hundreds of years
and there are the classical spherical and hyperbolic models
that first brought non-euclidean geometry recognition
but i took nam's question
as focused more on the "natural" i have quoted
which is a vague and informal universal property
that has something to do with efficient language
(if i understand correctly - not always likely)
the responses have all seemed to focus
on whether analysis was needed
or choice or ...
certainly you do not need the full machinery of differential geometry
but you need some of the information of a metric
because that is essential to the 5th axiom
in my opinion
this was what rota was after with his matroid work
-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
galathaea: prankster, fablist, magician, liar
|
|