Re: FOL, ZFC, NGB and Prolog

galathaea wrote:

galathaea
thank you very much indeed for writing
it is a great pity i understood only 5% of your kind post
it is a miracle i agree with 100% of it
as usual

> tom
>
> it is very difficult to discuss truth using godel as the source
>
> when he was younger
> he felt that all true things could be proven through mathematics
>
> he was confident
> like hilbert
> that the process of proof could comprehend all truth
>
> but in his attempts to prove this assertion
> he found flaws in this perception
> eventually
> after some careful study of the issues he had discovered
> he developed his famous incompleteness theorems
> in a completely finitary language
> excluding all direct reliance
> on the philosophically vague notion of truth
>
> tarski had a research programme
> where he was studying algebraic formalisations of truth
> by studying the algebraic nature of logic
> (it was really one of the big movements
> of the entire polish school
> which paralleled the algebraicisation
> of topology by classical constructivist henri poincare)
>
> one of the great accomplishes of tarski's programme
> was detailing the importance of satisfaction
> as one particularly relevant notion of truth
> to this whole discussion on computation
>
> computation theory required another algebraic process
> called lambda abstraction
> before it became a full enough description
> to comprehend functional application
>
> however tarski showed
> through what is essentially
> a term representation diagonalisation argument
> that there is no formula in a n-order term calculus
> that represents truth in that calculus
> (though perhaps some may represent (n-1)-order truth)
>
> this theorem is very general
> and applies to many nonboolean term calculi
> as well as classical models
>
> tarski learned of godel's work and commented
> godel learned of tarski's comments
>
> and godel began to believe that truth had been shown to be "unknowable"
> that this proved transcendental truth
> which later godel developed into mystical beliefs about his work
>
> during this time in his life
> godel felt that "truth as proof" was "already disproved"
>
> however that is not what tarski's programme had proved
> and later algebraic clarifications have been made
> on which notions of truth were addressed
> and how the guys over in recursive function theory
> (many, like markov, in the russian school also constructivists)
> were showing that they could explain what proofs were "really doing"
>
> they were showing how notions of truth in proof
> behaved like a certain computational structure
> which also had the same algebraic structure
> as that developed for a different constructivist school
> (heyting algebras)
> which were completely "knowable"
> (which is where curry-howard enters)
>
> all tarski had really done
> was detail a feature
> of the chain of meta and metameta...
>
> the reason i made my clarification
> (and i tried to make my wording clear)
> was that i thought earlier discussion
> could have given the impression that godel
> had only one opinion on truth
>
> he changed his mind throughout his life
> like all honorable people who seek to learn
>
> but i don't think it is really a "good idea"
> to follow godel's opinion on this topic
>
> instead
> i think it is best to stick with the algebra
> there is less controversy with algebra
>
> so i suggested starting with curry-howard
> which really is a good introduction to the connection
> of the algebraicisations
> of logic and computation
>
> it illustrates a nice relationship
> that brings another description of why
> constructive truth has temporal variation
>
> constructive computationalists are a small
> (but still sizable)
> community to this day
> (more popular perhaps in europe and asia than the americas)
>
> in the 60s and 70s
> particularly due to early work by f w lawvere
> metamathematics in the computational constructivist community
> was expressed in the language of category theory
> where translations of ZFC, NGB, and other foundations were begun
>
> categorial notions translate fairly directly
> to declarative computational languages
>
> i know it is not a simple web resource
> but you seem like you are genuinely interested
> in understanding a bit better the structure here
>
> and i don't really know to explain it briefly
>
> if you want to glean some information
> off of a computer language axiomatisation of mathematics
> i think you may have to have some background in the algebraics
>
> particularly since pattern matching is expressed in the same language
> for very much the same reasons
> which seemed to be one of the points of your questions
>
> now
> i wasn't disagreeing with anything that others have told you
> except that i don't place as much emphasis
> on godel's later opinions on truth
>
> i think some of his earlier work more correctly handled
> certain notions of truth
>
> but the others have
> as always
> given you valuable information
>
> but you had said at one point:
> P.S. All I need is a real mathie telling me that ZFCs, as all math,
> pattern matching. Oh, please. Nobody has EVER created a site, NOT even
> written a book that would make me answer the question in the
> affirmative : http://www.macrovu.com/CCTGeneralInfo.html And yet I DID!
> The assumption now in question is one I will NEVER be able to make by /
> after reading any book whatsoever or studying any site whatsoever.
>
> you won't find many willing to say that
> platonic truths exist
> in that there are propositions we can correctly axiomatise as true
> which we cannot axiomatise negated
> yet we cannot tell these from those statements
> that are truly independent (like the continuum hypothesis)
> inside formal proofs
>
> again this is
> (in my opinion)
> best formalised in category theory
> where cohen forcing and diagonalisation arguments
> are stated very naturally
>
> but since platonically true statements exist
> (one of which is the classical godel statement)
> mathematicians have less incentive to use
> only constructively valid statements
>
> even though most of the physically usable parts of mathematics
> are constructively valid
> mathematicians enjoy the freedom of discussing more ephemeral truths
>
> however, if you study categorial foundations of math
> in terms of computation theory
> you will find that there have indeed been many good books
> written about the topic
>
> pattern matching obeys much the same type of models
> when one is talking visual and topological pattern matching
> or computational argument pattern matching like in haskell
> or other functional programming languages
>
> its all related
>
>
> -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
> galathaea: prankster, fablist, magician, liar

my lord
so much information
so little me

always with utmost respect

thank you
tom

.

Relevant Pages

  • Re: Galileos Paradox
    ... the measure of truth of a statement, 0, 1, or somewhere in between? ... I would claim that the mathematical question is "Find a ... a proof is precisely this calculation of truth value for a given statement. ... "Another two universal algebra questions" ...
    (sci.math)
  • Re: JSH: What if no one believes you?
    ... There are 4 equations with 4 unknowns, so it's trivial algebra. ... film demonstrated how to make Mock Banana from parsnips. ... If it were enough to change the entire planet can die. ... And the truth will win, ...
    (sci.math)
  • Re: Galileos Paradox
    ... the measure of truth of a statement, 0, 1, or somewhere in between? ... "Find all pairs of distinct naturals such that x^y = y^x". ... I would claim that the mathematical question is "Find a ... "Another two universal algebra questions" ...
    (sci.math)
  • Re: Who could reason logical results from A |- B and C |- D?
    ... value A and a truth value B to the new truth value AvB, ... as the brute force reference implementation ... on concept algebra have the property similar as v. ...
    (sci.logic)
  • Re: A quote (and question) about intuitionism
    ... how would they know that it really is a property of truth? ... So perhaps some constructivists would say "P or " ... This philosophy does tend to sound subjectivistic to people ... constructive mathematics. ...
    (sci.math)