Re: A question about FOL theories and models


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

.

Relevant Pages

  • Re: A question about FOL theories and models
    ... You could formalize some meta-theory about G. ... Constructing a counter-model is only one way of proving ... function in the language and a relation for every ... the axiom-set "the axioms of G plus the denial of the axiom you ...
    (sci.logic)
  • [OT] Right Books (was re: Excuses, Excuses)
    ... I only wish I could speak a 2nd language. ... axiomization and the associated theory was not explained. ... >a true axiom of T if P is in A and is true (according to the definition ... >contains a false axiom). ...
    (sci.logic)
  • Re: non-Archimedean models of Euclidean geometry?
    ... The axiom basically says that if every point in A is to the ... isomorphism exactly one model for each infinite cardinal. ... example where the non isomorphic models have then same language. ... has non-isomorphic models of the same cardinality. ...
    (sci.logic)
  • Re: Idiocy of Muckenheim was Re: countability of reals
    ... >> the uncountability of real numbers into the language of logic you ... >> to be true within the same proof, or are an axiom of ZFC. ... can easily be understood as equivalent to a definition of reals between ... and in logic free variables are not even allowed for defining some ...
    (sci.math)
  • Re: Idiocy of Muckenheim was Re: countability of reals
    ... >> the uncountability of real numbers into the language of logic you ... >> to be true within the same proof, or are an axiom of ZFC. ... can easily be understood as equivalent to a definition of reals between ... and in logic free variables are not even allowed for defining some ...
    (sci.logic)