|
|
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.
|
|